46 약한 메모리의 증명 — 기본값이면 순서대로 생각해도 된다

먼저 알아야 할 것

27장 병렬 되풀이와 원자 연산 · 기억 차례 order 다섯과 기본값 seq_cst

39장 수학 도구상자 · 부분 순서 — 비교할 수 없는 쌍을 허락하는 순서

45장 경합과 병렬의 증명 · level 1·2 는 경합을 규율로 없앤다

돌아보기

45장의 가둠 그림에서 메모리 모델이 필요한 곳은 어디였는가?

답. level 3 — 원자 연산과 락 — 이었다. 그곳에서는 두 흐름이 같은 자리를 실제로 두드리므로 규율이 경합을 없애 주지 못한다. 이 장은 그 자리에서 “무엇을 언제 볼 수 있는가” 를 정하는 약한 메모리 모델을 정면으로 본다.

이 장의 필요성과 맥락

CPU 와 컴파일러는 명령의 차례를 바꾼다. 흐름이 하나면 티가 나지 않지만, 여러 흐름이 같은 메모리를 보면 티가 난다 — 내가 쓴 차례대로 남이 보지 않는다. Lowent 는 원자 연산에 다섯 가지 세기를 드러내고(relaxed < acquire·release < acq_rel < seq_cst), 기본을 가장 센 seq_cst 로 둔다. 약한 것은 적어야 얻고, 그 코드는 감사 대상이다. 이 결정은 두 명제에 기댄다. 기본값이면 순서대로 생각해도 된다는 것, 그리고 약한 것은 정말로 그것을 깬다는 것. 하나만 증명하면 결정이 정당하지 않다. 첫째가 없으면 “기본 seq_cst” 는 위안일 뿐이고, 둘째가 없으면 “적고 감사한다” 가 과장이 된다.

이 장이 끝나면

순차 일관성이 무엇인지와 그것을 깨는 표준 반례(저장 버퍼링), 실행을 간선 여러 종류의 그래프로 보고 순환이 있으면 그 실행이 존재하지 않는다고 판정하는 RC11 모델을 알게 된다. 기본값이면 반례가 나올 수 없고 relaxed 면 나올 수 있다는 정리 짝, 막는 것이 정확히 어느 공리인지, release·acquire 가 메시지 전달을 실제로 동기화한다는 정리를 익힌다. 모든 실행에 대한 일반 정리, 약하게 적으면 거동이 늘어난다는 단조성, 그 증명이 찾아낸 모델의 결함도 보게 된다.

이 장에서 답할 질문

order 를 적지 않은 원자 연산은 어떻게 되는가?

46.1 순차 일관성과 그 반례#

순차 일관성(sequential consistency, SC)은 “모든 흐름의 모든 접근을 한 줄로 세울 수 있고, 각 흐름 안의 차례가 그 줄에서 지켜진다” 는 뜻이다. 사람이 자연스럽게 상상하는 그림이 이것이다. 실제 하드웨어는 이렇게 동작하지 않는다.

처음: x = 0, y = 0

흐름 1:  x ← 1        흐름 2:  y ← 1
         r1 ← y                r2 ← x

나쁜 결과:  r1 = 0  이고  r2 = 0

저장 버퍼링(store buffering)이라 부르는 표준 반례다. 왜 나쁜가? 한 줄로 세울 수 없다. r1 = 0 이면 흐름 1 의 읽기가 흐름 2 의 쓰기보다 먼저이고, r2 = 0 이면 흐름 2 의 읽기가 흐름 1 의 쓰기보다 먼저다. 그런데 각 흐름 안에서는 쓰기가 읽기보다 먼저다. 모순이다. 그런데 실제 x86 에서 이 결과가 나온다.

46.2 실행은 그래프다#

기준 모델은 RC11(Lahav 외, PLDI 2017)이다. 실행을 그래프로 본다. 사건이 꼭짓점이고 간선이 여러 종류다.

간선	뜻
`hb`(happens-before)	차례가 보장된다
`rf`(reads-from)	이 읽기는 저 쓰기의 값을 읽었다
`mo`(modification order)	한 자리에 대한 쓰기들의 전역 차례
`fr`(from-read)	이 읽기는 저 쓰기보다 먼저다 — 더 낡은 값을 읽었으므로

표 46.1 — RC11 의 간선

판정은 한 문장이다. 어떤 축에서 순환이 생기면 그 실행은 존재하지 않는다. 이것이 이 장에 필요한 수학의 전부다 — 방향 그래프에 순환이 있는가. 위상 정렬을 배웠다면 아는 개념이다. RC11 이 어려운 것은 개념이 아니라 간선 종류가 많아서다.

46.3 기본값이면 나올 수 없고, `relaxed` 면 나올 수 있다#

수학. E1 — sb_sc_impossible

consistent (SB SC) rf_00 mo_SB = false. 모든 접근이 seq_cst 면 “둘 다 0 을 읽는” 결과는 일관성 공리를 어긴다 — 그런 실행은 없다. 순환을 직접 보자. Wx1 —hb→ Ry0 —fr→ Wy1 —hb→ Rx0 —fr→ Wx1. fr 을 읽는 법은 이렇다 — Ry0 은 y 의 처음 값을 읽었는데 Wy1 이 그것을 덮어썼으므로 Ry0 이 Wy1 보다 먼저다. 네 간선이 닫힌 고리를 이루므로 이 실행은 존재할 수 없다.

수학. E2 — sb_relaxed_is_consistent

consistent (SB Rlx) rf_00 mo_SB = true. relaxed 면 그 나쁜 결과가 모든 공리를 만족한다 — 실제로 일어날 수 있다. 순차 일관성 공리는 seq_cst 사건에 대해서만 말하므로, relaxed 뿐이면 그 공리는 공허하게 참이다. 그것이 relaxed 의 값이자 위험이다. 제약을 걷어 내니 빠르지만, 걷어 낸 것이 바로 안전이다.

E1 이 “기본 seq_cst” 라는 문장을 위안이 아니라 정리로 만든다. seq_cst 만 쓰는 코드는 한 줄로 세워 상상해도 된다.

46.4 막는 것은 정확히 그 공리다#

수학. E3 — 어느 축이 일하는가

coherence_alone_does_not_forbid_sb — seq_cst 여도 coherence 축만으로는 저장 버퍼링이 막히지 않는다. it_is_the_sc_axiom_that_forbids_it — 막는 것은 순차 일관성 축이다.

실제 사례. 모델이 틀렸음을 기계가 가르쳐 주었다

처음 쓴 모델은 저장 버퍼링을 seq_cst 에서도 통과시켰다. 공리가 모자랐던 것이다. 그것을 증명기가 드러냈고, 공리를 보태 고쳤다. E3 의 두 정리는 그 교훈을 고정한다. 어느 축이 일하는지 적어 두면, 나중에 누가 공리를 지웠을 때 이 정리가 깨진다. 증명 도구의 진짜 값은 정리를 얻는 것보다 여기에 있다.

46.5 메시지 전달 — 약한 것은 이 모양을 위해 있다#

E1 E3 은 “약한 것이 위험하다” 였다. 그러면 약한 것은 왜 있는가? 정확히 이 모양을 위해서다.

examples/ch46/handoff.low

module handoff_order .

proc publish input k cap atomic . input cells mut slice u64 . output void . effects atomic .
  requires ge (len cells) 2 .
do
  atomic_store cells 0 42 order relaxed .
  atomic_store cells 1 1 order release .
end

proc observe input k cap atomic . input cells mut slice u64 . output u64 . effects atomic .
  requires ge (len cells) 2 .
do
  let flag u64 be atomic_load cells 1 order acquire .
  guard eq flag 1 . else return 0 .
  return atomic_load cells 0 order relaxed .
end

실행 결과

$ lowentc --check handoff.low
== check: ok ==

데이터를 먼저 쓰고(relaxed), 깃발을 release 로 쓴다. 다른 흐름은 깃발을 acquire 로 읽고, 1 이면 데이터를 읽는다. 나쁜 결과는 “깃발 1 을 읽고도 데이터 0 을 읽는” 낡은 값이다.

수학. E4 — 메시지 전달

mp_relacq_forbids_stale — release·acquire 면 낡은 값을 보는 것이 불가능하다. mp_relaxed_allows_stale — 둘 다 relaxed 면 가능하다. mp_sync_is_what_forbids_it — 차이를 만드는 것은 release 쓰기와 acquire 읽기 사이에 서는 동기화 간선 sw 다. 논증은 이렇다. sw 가 데이터 쓰기에서 데이터 읽기로 가는 hb 를 만든다. 그런데 데이터 읽기가 처음 값을 읽었고 데이터 쓰기가 그보다 mo 로 나중이므로 반대 방향 fr 이 선다. 같은 자리에서 순환이 생기므로 coherence 축이 막는다.

E4 는 E1 과 짝이다. E1 은 “기본값이 안전하다”, E4 는 “적으면 동기화된다”. 설계 결정의 양쪽이 모두 기계 위에 있다.

수학. E5 — sb_relaxed_has_a_race

저장 버퍼링의 (0, 0) 결과가 나오는 실행은 경합을 담고 있다. 그런데 45장에서 보았듯 level 1·2 는 그런 실행을 만들 수 없다. 그러므로 level 1·2 코드는 이 장을 읽지 않아도 된다 — 약한 메모리는 level 3 만의 문제이고, 가둠이 성립한다.

46.6 모든 실행에 대해#

위의 정리들은 대부분 vm_compute. reflexivity. 로 끝난다. consistent 를 참·거짓을 내는 판정 함수로 정의했으므로, 특정 실행에 대해 그 함수를 계산해 버리면 증명이 끝난다. 짧고, 모델을 고치면 저절로 다시 확인된다. 대가는 특정 실행에 대한 결과라는 것이다. 설계 결정이 걸린 것이 바로 그 표준 반례들이므로 결정을 정당화하기에는 충분하지만, 거기서 멈추지 않았다.

수학. 모든 접근이 seq_cst 면 순차 일관적이다(LowentRC11SC.v 의 all_sc_is_sc)

all_sc E = true -> consistent E rf mo = true -> sc_com_acyclic E rf mo = true. 모든 접근이 seq_cst 이고 그 실행이 RC11 일관적이면 po ∪ rf ∪ mo ∪ fr 에 순환이 없다 — 모든 실행 · 모든 rf · 모든 mo 에 대해. 공리적 메모리 모델에서 “이 실행은 순차 일관적이다” 를 그렇게 정의하는 것이 표준이다. 증명의 엔진은 한 줄이다 — 부분 관계는 비순환성을 물려받는다.

그리고 순환이 없다는 것에서 한 걸음 더 갔다. “비순환이면 전순서가 있다” 를 추상적으로 논증하는 대신 위상 정렬을 함수로 짓고 그 결과가 진짜 선형 확장임을 증명했다(topo_linearises·sc_witness_orders_everything). 모든 접근을 한 줄로 늘어놓았고, 그 줄이 프로그램 차례와 통신 차례를 전부 지킨다. 좋은 저장 버퍼링 실행에서 실제로 [0; 1; 2; 4; 3; 5] 라는 줄이 나온다.

46.7 약하게 적으면 거동이 늘어난다#

수학. 단조성(LowentRC11Mono.v 의 consistent_monotone)

같은 실행에서 기억 차례만 약하게 한 것도 일관적이다 — 모든 실행 · 모든 rf · 모든 mo · 모든 배정에 대해. 곧 약하게 적으면 가능한 거동이 늘어난다 (줄지 않는다). 간선 수준에서도 약하게 하면 동기화 간선이 줄고 없던 것이 생기지 않는다(sw_weaken). sc_is_the_strongest·rlx_is_the_weakest 로 세기 순서 자체가 정리다.

뒤집으면 실무의 문장이 된다 — 기억 차례를 세게 적는 것은 언제나 안전한 방향이다. 기본값을 seq_cst 로 둔 근거가 이 문장이고, 그것은 믿음이 아니라 정리다.

실제 사례. 단조성 증명이 찾아낸 순서의 결함

옛 세기 순서는 acq_rel 을 seq_cst 위에 두었다. 동기화 간선만 세고 순차 일관성 공리를 보지 않았기 때문이다. 그런데 저장 버퍼링은 acq_rel 에서 일관적이고 seq_cst 에서 일관적이지 않다. 그 순서로는 단조성이 거짓이었다(old_order_is_not_a_strength_order 가 그것을 계산한다). 유계 전수 계산이 이것을 못 본 까닭도 분명했다 — 그 골격들이 순차 일관성 축을 건드리지 않았다. 순서를 고쳐 seq_cst 를 유일한 꼭대기로 만들었다.

46.8 문헌의 시험 일곱#

손으로 고른 실행만 쓰면 모델의 공리가 모자란 것을 못 잡는다(E3 의 실패담). 그래서 문헌의 이름 있는 시험을 먹였다(LowentRC11Sweep.v).

시험	`seq_cst`	`relaxed`
SB · LB · MP · 2+2W · IRIW	금지	허용
CoRR · CoWR	금지	금지

표 46.2 — litmus 시험 일곱의 판정

마지막 줄이 배운 것이다. “relaxed = 아무 보장 없음” 이 아니다. 저장 버퍼링을 막는 것은 순차 일관성 축이고 CoRR·CoWR 을 막는 것은 coherence 축인데, 후자는 기억 차례와 무관하게 늘 있다.

문. order 를 적지 않은 원자 연산은 어떻게 되는가?

답. seq_cst 다. 아무 표시 없는 코드가 가장 안전하다. 기본값을 relaxed 로 두면 아무것도 적지 않은 코드가 위험해지고, 위험을 요청하지 않았는데 얻게 된다. 위험은 적어서 얻는 것이어야 한다. 그리고 한 연산에 뜻이 없는 조합 — 읽기에 release, 쓰기에 acquire — 은 번역에서 거절된다 (27장).

흔한 오해. 성능이 필요하면 원자 연산을 모두 relaxed 로 적으면 된다

E2 가 말하듯 relaxed 는 “둘 다 0 을 읽는” 결과를 실제로 허락한다. 제약을 걷어 낸 만큼 빠를 수 있지만 걷어 낸 것이 바로 순서대로 사고해도 된다는 보장이다. 이 판에서 약한 차례를 명시한 코드 가운데 증명이 있는 것은 spsc 하나뿐이고(47장), 나머지는 감사 대상이다. 기본값 seq_cst 로 쓰고 측정한 뒤, 약하게 해야 할 한 자리를 골라 그 자리의 논증을 적는다.

46.9 증명하지 않은 것#

특정 lock-free 알고리즘을 relaxed 로 검증하는 프로그램 논리는 이 장에 없다. 모델 안의 메타정리(순차 일관성 · 단조성 · 순서 확장)는 증명했고, 프로그램 논리로 검증한 것은 SPSC 링 버퍼 하나이며 그것도 빌린 증명이다(47장).
“비순환이면 위상 정렬이 반드시 성공한다” 는 아직 없다. 지금은 순서를 실제로 얻고 그것이 옳음을 알며, 실패하면 None 으로 알 수 있다 — 조용히 틀린 순서를 내는 일은 없다.
모델은 손으로 옮긴 RC11 이다. 논문의 정의와 맞는지는 사람이 읽어서 확인했고, 한 번 틀렸다(E3).
시험은 표본이다. fence 를 쓰는 시험이 없고(이 모델에 fence 사건이 없다), 골격마다 rf·mo 는 나쁜 결과 하나씩이다.
컴파일러가 이 모델을 지키는지는 별개다. 기억 차례는 C11 atomic 으로 1 대 1 방출되므로 나머지는 C 컴파일러의 몫이다(신뢰 기반). 그 대응과 “원자 연산의 차례를 바꾸지 않는다” 는 시험으로 확인한다.

복습 정리

순차 일관성은 모든 접근을 한 줄로 세울 수 있다는 뜻이고, 저장 버퍼링이 그 표준 반례다. RC11 은 실행을 간선 네 종류의 그래프로 보고 순환이 있으면 그 실행이 없다고 판정한다. 모든 접근이 seq_cst 면 반례가 불가능하고 relaxed 면 가능하며, 막는 것은 순차 일관성 공리다. release·acquire 는 메시지 전달을 실제로 동기화하고, 그런 나쁜 실행에는 경합이 있어 level 1·2 와 무관하다. 모든 실행에 대해 seq_cst 는 순차 일관적이고, 약하게 적으면 거동이 늘어나므로 세게 적는 것이 언제나 안전한 방향이다.

← 이전목차로다음 →