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 usize . effects none .
  parallel s split .
do
  var i usize 0 .
  while lt i. len s. . . do
    set idx s. 0 . cast u64 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 에만 필요하다. 경합이 없는 것과 결정적인 것은 다르며, 겹치지 않게 나누기 · 의존 간선 지키기 · 결합적 모으기의 세 조건이 병렬 결과를 순차와 비트까지 같게 한다. 각 조건에는 빠지면 무엇이 깨지는지 보이는 반례가 붙어 있다.

← 이전목차로다음 →