45 경합과 병렬의 증명 — 규율이 메모리 모델을 대신한다

먼저 알아야 할 것

25장 액터 · 상태는 액터 안에 잠기고 소유는 메시지로 옮겨 간다

27장 병렬 되풀이와 원자 연산 · 나눌 수 있는 되풀이의 세 조건과 reduce

42장 소유와 차용의 증명 · 한 흐름에서 쓰는 이름은 하나다

돌아보기

27장에서 W-PAR-OK 알림은 VM 이 순차로 도는 것이 왜 올바른 구현이라고 했는가?

답. 나눌 수 있는 조건을 만족하면 병렬 결과가 순차 결과와 비트까지 같다는 정리가 증명되어 있기 때문이라고 했다. 이 장은 그 정리와, 그보다 먼저 서야 하는 “데이터 경합이 없다” 는 정리를 다룬다. 둘은 같은 전제에서 나오는 다른 결론이다.

이 장의 필요성과 맥락

두 흐름이 같은 자리를 동시에 만지고 그중 하나가 쓰기면 데이터 경합이다. C·C++ 에서는 정의되지 않은 동작이다. 경합을 다루는 보통의 길은 기억 차례 같은 메모리 모델을 배우는 것인데, 어렵다. 이 언어의 주장은 다르다 — 나누어 도는 되풀이(level 1)와 액터(level 2)의 코드는 메모리 모델을 볼 일이 없다. 경합이 규율로 원천 차단되기 때문이다. 그리고 경합이 없어도 답이 매번 같다는 보장은 따로 필요하다. 이 장은 두 주장을 모두 무거운 동시성 논리 없이 순수 Coq 으로 세운 이야기다. 명제를 정확히 읽으면 필요한 도구가 준다.

이 장이 끝나면

Bernstein 독립이라는 세 줄의 집합 조건과 경합의 정의를 알게 된다. level 1 에서 독립이면 경합이 없고 그 조건이 필요하다는 정리 짝, level 2 에서 서로 다른 액터의 접근 사이에 메시지가 반드시 있다는 정리를 익힌다. 경합이 없는 것과 결정적인 것이 왜 다른지, 병렬 결과가 순차와 비트까지 같다는 DET-1, 스케줄러의 자유를 주는 DET-2, 결합법칙이 축약 나무의 모양을 자유롭게 하는 DET-3 과 각각의 반례도 보게 된다.

이 장에서 답할 질문

“대체로 같은 답” 이면 되지 않는가?

45.1 Bernstein 조건 — 1966 년의 답#

두 태스크의 읽는 자리 집합과 쓰는 자리 집합을 각각 R·W 라 하자. 두 태스크가 독립이라는 것은 세 줄이다.

W₁ ∩ W₂ = ∅      둘이 같은 자리에 쓰지 않는다
W₁ ∩ R₂ = ∅      하나가 쓰는 자리를 다른 하나가 읽지 않는다
R₁ ∩ W₂ = ∅      그 반대도 아니다

교집합이 비었다는 세 줄이 전부다. R₁ ∩ R₂ 는 조건에 없다 — 같은 자리를 함께 읽는 것은 괜찮다. 경합은 “두 태스크가 같은 자리를 건드리고 적어도 하나는 쓰기” 로 정의한다. 보통의 정의에는 “두 접근이 앞뒤로 정해지지 않았다” 가 붙는데, level 1 에서는 그 조건이 저절로 만족된다. 흐름이 갈라진 뒤 모이기 전까지 태스크들 사이에는 앞뒤 간선이 아예 없기 때문이다.

처리기의 진단이 이 조건을 그대로 인용한다.

examples/ch45/par_overlap.low

module par_overlap .
rem expect: E-PAR-WRITE

rem 모든 조각이 첫 칸에 쓴다 --- 남는 값이 누가 마지막이었는지에 달린다
proc stamp input s mut slice u64 . output u64 . effects none .
  parallel s split .
do
  var i u64 be 0 .
  while lt i (len s) . do
    set (index s 0) i .
    set i (add i 1) .
  end
  return len s .
end

실행 결과

$ lowentc --check par_overlap.low
par_overlap.low:10:0 E-PAR-WRITE: a splittable loop may only write its OWN element `index <s> <i>` — this write can collide with another iteration (Bernstein: wr ∩ wr = ∅)
par_overlap.low:10:0 E-PAR-READ: a splittable loop may only read its OWN element of the split slice — reading another index creates a cross-iteration dependence (Bernstein: rd ∩ wr = ∅)

모든 조각이 첫 칸에 쓰므로 wr ∩ wr = ∅ 이 깨졌고, 다른 조각의 칸을 읽으므로 rd ∩ wr = ∅ 도 깨졌다. 27장의 세 조건 — 자기 몫만 읽기, 자기 몫만 쓰기, 되풀이를 넘어 사는 자리에 쓰지 않기 — 이 곧 Bernstein 조건이다.

45.2 독립이면 경합이 없다, 그리고 그 조건이 필요하다#

수학. level 1 — 나누어 도는 되풀이(LowentDRF.v)

l1_no_race : forall t1 t2 l, indep t1 t2 -> ~ races t1 t2 l. 두 태스크가 Bernstein 독립이면 어떤 자리에서도 경합하지 않는다. 증명은 다섯 줄이다. 경합이 있다고 가정하면 “하나가 쓴다” 는데, 독립 조건이 그 자리에 대한 상대의 접근을 세 경우 모두 부정한다. 모순이다.

l1_condition_is_necessary : ~ indep writer reader /\ races writer reader 0. 조건을 어기는 짝 — 하나는 자리 0 에 쓰고 하나는 자리 0 을 읽는다 — 을 실제로 만들면 경합이 있다.

둘째 정리가 정직한 증명의 표식이다. “조건을 만족하면 안전하다” 만 증명하면, 조건이 과하게 엄격해도 정리는 참이다 — 아무것도 통과시키지 않는 조건도 안전하다. 그래서 반례를 함께 증명한다. 조건을 느슨하게 하면 정말로 깨진다는 것. 정리 하나에 반례 하나 — 이 부가 여러 곳에서 쓰는 방식이다.

경합이 없으면 널리 알려진 DRF-SC 정리(Adve–Hill)가 발동해 프로그램이 순차 일관성처럼 행동한다. 곧 순서를 뒤죽박죽으로 상상할 필요가 없다.

45.3 액터 사이에는 반드시 메시지가 있다#

수학. level 2 — 액터(l2_accesses_are_separated_by_a_message)

실행 흔적에서 서로 다른 액터가 같은 자리 l 을 접근한다면, 그 두 접근 사이에 그 자리의 소유권을 넘기는 메시지가 반드시 있다.

논증의 사슬은 이렇다. 한 자리는 정확히 한 액터가 소유한다. 소유자만 접근한다. 소유권은 메시지로만 옮겨진다. 그런데 두 접근의 액터가 다르다. 따라서 그 사이에 소유권 이전이 있었다. 메시지는 앞뒤를 정하는 간선이고, 앞뒤가 정해진 두 접근은 정의상 경합이 아니다. 액터 모형에서 가장 흔한 실수 — 참조를 메시지로 보내고 보낸 쪽도 계속 쓰는 것 — 는 소유권 이전이라 보낸 쪽이 그 자리를 잃으므로 막힌다(25장의 handoff).

42장과의 연결이 요점이다. 한 흐름에서 “쓰는 이름은 하나” 를 강제해 두면 그 규칙이 그대로 “두 태스크가 겹치지 않음” 이 된다. 안전 규칙 하나가 두 곳에서 값을 낸다.

45.4 가둠 — 무거운 도구가 필요한 곳#

level 1 (나누어 도는 되풀이)  ─┐
level 2 (액터 격리)            ─┤→ 경합이 규율로 없다 → DRF-SC → 순서대로 생각한다
level 3 (원자 연산 · 락)        ─┘→ 경합이 실제로 있다 → 메모리 모델이 필요하다

흔한 오해. 동시성을 증명하려면 반드시 분리논리 같은 무거운 도구가 필요하다

처음 계획은 “안전 코드에 경합이 없다” 를 스케치로 두고 기계 증명은 무거운 동시성 논리로 하는 것이었다. 다시 보니 그 명제는 메모리 모델에 대한 주장이 아니었다. “규율이 경합을 막는다” 는 집합론의 주장이다. 무거운 도구가 정말 필요한 곳은 level 3 뿐이고, 증명 파일 가운데 Iris 를 쓴 것은 락 하나다(47장). “동시성이니까 분리논리” 는 반사적 판단이었다.

45.5 경합이 없는 것과 결정적인 것은 다르다#

같은 입력으로 두 번 돌렸는데 답이 다를 수 있다. 경합이 없어도 그렇다. 부동소수 덧셈을 여러 코어가 나눠 더한 뒤 합치면, 합치는 순서가 달라질 때 마지막 비트가 달라진다. 각자 자기 몫만 만졌으니 경합은 없다. 그런데 답이 다르다.

이 언어의 주장은 강하다. level 1 병렬의 결과는 순차 실행 결과와 비트까지 같다. 근사도, 오차 허용도 없다. 그 주장을 세우는 조건이 정확히 셋임을 증명했다(LowentPar.v). 결정성은 경합의 문제가 아니라 Bernstein 조건의 문제다. 같은 조건이 다른 결론을 준다.

조건	있으면	없으면
DET-1 겹치지 않게 나누기	병렬 = 순차(`det1_par_eq_seq`)	차례가 결과를 바꾼다(`overlap_is_nondeterministic`)
DET-2 의존 간선 지키기	나머지 차례는 자유(`det2_schedule_free`)	— 자유를 안 쓰면 손해만 본다
DET-3 모으는 연산의 결합법칙	나무 모양이 결과를 바꾸지 않는다(`assoc_shape_free`)	같은 잎에서 다른 결과(`nonassoc_shape_matters`)

표 45.1 — 결정적 병렬의 세 조건 — 있으면 무엇이, 없으면 무엇이

수학. DET-1 — 병렬은 순차와 같다

태스크들이 쌍쌍이 독립이고 각자 국소적(자기 읽기 집합만 보고 값을 정한다)이면, 병렬 실행의 모든 자리 i 의 값이 순차 실행과 같다. 따름정리의 이름이 주장 그대로다 — det1_bit_identical. 증명의 갈림길이 교육적이다. 자리 i 를 첫 태스크가 쓰면, 나머지 누구도 i 를 쓰지 않으므로 답은 첫 태스크의 것이다. 첫 태스크가 i 를 쓰지 않으면, 나머지 가운데 유일한 기록자가 답을 내는데, 그 태스크의 읽기가 첫 태스크의 쓰기와 겹치지 않으므로 원래 상태를 읽든 첫 태스크가 손댄 상태를 읽든 같은 값이다. 둘째 경우가 “국소적” 이 왜 필요한지 말한다.

반례는 두 태스크가 같은 자리에 각각 1 과 2 를 쓰는 것이다. 차례에 따라 답이 2 아니면 1 이다.

DET-2 는 충돌하지 않는 두 태스크의 차례를 바꿔도 결과가 같다는 정리다. 증명은 인접 교환에 대한 귀납이다. 인접한 둘을 바꿀 수 있으면, 그것을 되풀이해 “충돌 순서를 지키는 임의의 재배열” 에 닿는다 — 정렬 알고리즘과 같은 발상이다. 스케줄러에게 최대한의 자유를 주면서 결정성을 잃지 않으니, 자유가 곧 성능이다.

DET-3 의 반례는 뺄셈이다. (5 − 3) − 1 = 1 이고 5 − (3 − 1) = 3 이다. 연산이 결합적이 아니면 언어가 나무 모양을 고정해야 하고, 스케줄러가 코어 수에 따라 나무를 바꾸면 결과가 스케줄에 달린다. 증명은 IEEE 부동소수를 공리로 들여오지 않고, 뺄셈이라는 비결합 연산의 대표로 “비결합이면 모양이 문제다” 를 일반적으로 보였다. 그래서 reduce acc sub 는 E-PAR-ASSOC 로, 부동소수 덧셈은 E-PAR-FLOAT 로 거절된다(27장).

문. “대체로 같은 답” 이면 되지 않는가?

답. 값이 거의 같으니 괜찮다고 넘기면 회귀 시험을 비트 비교로 쓸 수 없게 된다. 재현성을 잃으면 디버깅 도구 하나를 잃는다. 병렬 합산이 코어 수마다 다른 답을 내는 것은 과학 계산에서 재현이 안 되는 가장 흔한 원인이다. 이 언어에서 “대체로” 는 없다 — 세 조건을 확인할 수 없으면 번역이 거절한다.

45.6 증명하지 않은 것#

DRF-SC 정리 자체는 인용이다. “경합이 없으면 순차 일관성처럼 행동한다” 는 널리 알려진 정리이고, 여기서 증명한 것은 그 정리의 전제(경합 없음)를 우리 규율이 만족한다는 것이다.
정리는 구현을 검증하지 않는다. level 1 병렬은 구현되었지만, 정리가 못 박은 것은 구현이 지켜야 할 조건이다. 구현이 그 조건을 지키는지는 두 백엔드 대조가 경험적으로 받친다.
모델은 정적인 읽기·쓰기 집합을 가정한다. 포인터가 섞이면 그 집합을 미리 알기 어렵고, 실제로는 타입 체계가 그것을 보장해야 한다. “국소적” 도 가정이지 검사가 아니다.
상태 모델은 “자리 → 값” 함수다. 정렬·별칭·부분 쓰기 같은 실제 메모리를 모델링하지 않았다. 부동소수 자체(반올림·NaN·−0)도 다루지 않았다.

복습 정리

Bernstein 독립은 세 줄의 빈 교집합이고, level 1 에서 독립이면 경합이 없으며 그 조건이 필요하다는 것이 반례와 함께 증명되었다. level 2 에서는 서로 다른 액터의 접근 사이에 소유권 메시지가 반드시 있어 경합이 정의상 없다. 무거운 도구는 level 3 에만 필요하다. 경합이 없는 것과 결정적인 것은 다르며, 겹치지 않게 나누기 · 의존 간선 지키기 · 결합적 모으기의 세 조건이 병렬 결과를 순차와 비트까지 같게 한다. 각 조건에는 빠지면 무엇이 깨지는지 보이는 반례가 붙어 있다.

← 이전목차로다음 →