47 락의 증명 — 무거운 도구가 실제로 필요한 자리

먼저 알아야 할 것

26장 태스크와 채널 · 나누어 가지는 자물쇠 상태는 이 판에 아직 없다(E-LOCK-NOTYET)

34장 그릇과 정렬 · spsc 는 락 없는 단일 생산자·단일 소비자 링 버퍼다

46장 약한 메모리의 증명 · release·acquire 는 메시지 전달을 동기화한다

돌아보기

45장은 무거운 동시성 논리가 필요한 곳을 어디라고 했고, 왜 거기만이라고 했는가?

답. level 3, 그중에서도 락이라고 했다. level 1·2 의 규율은 같은 자리를 두 흐름이 만지는 일을 아예 없애서 집합론이면 충분했다. 그러나 스핀락은 두 흐름이 같은 워드를 실제로 동시에 두드리는 장치다. 여기서는 규율이 안전을 줄 수 없고, 불변식이 지켜야 한다. 이 장이 그 추론 — 동시성 분리논리 — 을 다룬다.

이 장의 필요성과 맥락

설계는 “lock·rwlock 은 원자 CAS 위의 라이브러리다” 라고 정했다. 그 문장이 참이려면 CAS 하나로 세운 스핀락이 정말로 상호배제를 주어야 한다. 그리고 이 저장소의 증명 파일 대부분이 순수 Coq 인데 락만 Iris 를 쓰는 까닭을 이해해야 도구를 필요한 만큼만 쓴 판단을 믿을 수 있다. 이 장은 분리논리의 어휘를 처음부터 소개하고, 락·rwlock·교착·굶주림의 정리를 읽고, 약한 메모리에서 빌린 증명이 표준 라이브러리의 spsc 를 어떻게 받치는지 본다. 락은 이 부에서 경계가 가장 많은 주제이기도 하다.

이 장이 끝나면

“서로 다른 조각” 을 뜻하는 접속사 ∗, 명세를 적는 호어 삼중항, 여러 흐름이 나누어 가지는 불변식, 실행에는 없고 증명에만 있는 유령 토큰을 알게 된다. 토큰이 둘일 수 없다는 정리에서 시작해 락 만들기·잡기·놓기의 명세가 무엇을 막는지 익힌다. rwlock 의 두 증명, 오름차순 잠금의 교착 자유와 라운드로빈의 굶주림 없음, 그리고 약한 메모리의 프로그램 논리를 빌려 spsc 를 확인한 일과 그 대가도 보게 된다.

이 장에서 답할 질문

증명된 락이 있는데 이 판에서 lock 은 왜 없는가?

47.1 분리논리의 어휘#

보통의 논리에서 A ∧ B 는 “둘 다 참” 이다. 분리논리는 접속사를 하나 더 둔다. A ∗ B 는 “A 와 B 가 참이고, 서로 다른 메모리 조각에 대한 것이다” 로 읽는다. 메모리에 대한 주장이 소유를 함의해야 하기 때문이다. x ↦ 3 은 “x 가 3 을 담고 있다” 가 아니라 “나는 x 를 소유하고 그 값이 3 이다” 다. 그래서 x ↦ 3 ∗ y ↦ 4 는 x 와 y 가 다른 자리임을 말하고, x 에 쓰는 것이 y 에 대한 주장을 망가뜨리지 않는다. 이것이 국소 추론이다.

12장의 배타 규칙과 같은 발상이다. 실은 순서가 반대다 — Rust 의 차용 검사기가 분리논리의 발상을 타입 체계로 옮겼고, 이 언어의 배타 규칙도 그 계보에 있다. 42장은 이 장의 생각을 번역 시각으로 내린 것이다.

어휘	뜻
호어 삼중항 `{{{ P }}} e {{{ Q }}}`	`P` 를 만족하는 상태에서 `e` 를 돌리면, 끝났을 때 `Q` 가 성립한다
불변식 `lock_inv γ lk R`	`(lk ↦ false ∗ R) ∨ (lk ↦ true)` — 열려 있으면 자원 `R` 이 불변식 안에, 잠겨 있으면 잠근 흐름의 손에
유령 토큰 `locked γ`	`own γ (Excl ())` — 실행에는 없고 증명에서만 도는 회계 장치

표 47.1 — 락 증명의 어휘

불변식 한 줄이 락의 전부다. R 은 두 곳에 동시에 있을 수 없으므로, R 을 가진 흐름은 하나뿐이다.

          acquire — CAS 가 false 를 true 로 바꾼다
   ┌────────────────────────────────────────────┐
   │                                            ▼
 열림  lk ↦ false ∗ R                    잠김  lk ↦ true
       R 은 불변식 안에 있다                   R 과 토큰 locked γ 는 잡은 흐름의 손에
   ▲                                            │
   └────────────────────────────────────────────┘
          release — 토큰과 R 을 둘 다 반납한다

47.2 토큰은 둘일 수 없다#

수학. LowentLock.v 의 정리들

locked_exclusive : locked γ -∗ locked γ -∗ False. 토큰을 둘 가졌다고 가정하면 모순이다. 이것이 상호배제의 기계적 심장이다.

newlock_spec : {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}. 보호할 자원을 넘겨주면 락을 얻는다. 락을 만드는 대가로 자원을 포기한다 — 이제 그 자원에 닿는 유일한 길은 락을 잡는 것이다.

acquire_spec : {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}. 잡으면 토큰과 자원을 둘 다 받는다. ∗ 가 일한다 — 받은 자원은 내 것이고 누구의 것과도 겹치지 않으므로, 그 뒤로는 흐름이 하나인 것처럼 추론한다.

release_spec : {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}. 놓으려면 토큰과 자원을 둘 다 반납해야 하고, 놓은 뒤에는 아무것도 남지 않는다.

두 흐름이 동시에 잡았다면 토큰이 둘이고, 그것은 거짓이다. 놓기의 명세 하나가 두 결함을 막는다. 잡지 않고 놓으면 locked γ 가 없어 사전조건을 못 맞추고, 놓은 뒤에도 자원을 쓰면 R 을 이미 반납했으므로 손에 없다.

증명들의 공통 모양은 셋이다. 불변식을 연다, CAS 를 실행한다(성공과 실패로 갈린다), 불변식을 닫는다. 원자적인 순간에만 불변식을 열 수 있다는 것이 Iris 의 규칙이고, 그 덕에 “불변식이 잠깐 깨진 상태를 다른 흐름이 볼 수 없다” 가 보장된다.

수학. 실전 예 — 두 흐름의 증가(incr_spec·two_threads_spec)

두 흐름이 동시에 acquire ; c ← !c + 1 ; release 를 돈다. 두 흐름이 동시에 증가시켜도 경합 없이 끝나고 프로그램은 값을 하나 낸다. 락 없는 c ← !c + 1 — 고전적인 lost update — 은 c ↦ n 을 락에서 받아야만 쓸 수 있으므로 증명되지 않는다. 정직하게: 이 정리는 결과가 정확히 2 라고 말하지 않는다. 정확한 합계를 말하려면 유령 카운팅이 더 필요하다. 이 파일의 목표는 락이 자원을 지킨다는 것이었다.

47.3 도구를 필요한 만큼만#

파일	도구	왜
차용 · 되풀이 · 경합 · 병렬 · RC11 · 블록 · 칸 · 세탁 · 수	순수 Coq	규율 · 집합론 · 격자 · 그래프 판정이면 된다
락 · rwlock 읽기 쪽	Iris	두 흐름이 같은 자리를 실제로 두드린다
약한 메모리 프로그램 · SPSC	iRC11 · gpfsl(빌림)	약한 메모리 위에서 프로그램을 검증해야 한다

표 47.2 — 증명 파일과 도구

Coq 을 고른 이유도 여기에 있다. Iris 는 Coq 전용이고 Lean 에는 성숙한 대응물이 없다. 언젠가 필요할 도구가 어디 있는지가 증명 언어 선택을 정했다.

47.4 rwlock — 같은 문장의 두 증명#

한 워드에 세 뜻을 담는 고전적 rwlock — 0 은 빔, n > 0 은 독자 n, −1 은 쓰기 잠금 — 에서 쓰기 잠금의 배타성을 직접 증명했다(LowentRWLock.v 의 wlocked_exclusive·wlock_spec·wunlock_spec). CAS 가 0 에서만 성공하므로 “독자가 있는데 쓰기가 들어간다” 가 막힌다. 실제 rwlock 결함의 대부분이 그것이다.

읽기 쪽의 분수 소유권은 Iris 가 이미 갖고 있었다. 라이브러리의 rwlock 인터페이스가 분수 술어 Φ : Qp → iProp 로 적혀 있고 rw_spin_lock 이 검증된 인스턴스다. 독자는 분수 Φ q 를 받고(여럿이 동시에), 쓰기와 읽기는 동시에 있을 수 없으며, 쓰기는 전부 Φ 1 을 받는다. 값진 것은 “쓰기와 읽기는 배타적이다” 가 같은 문장의 다른 증명이라는 점이다. 우리 것은 “CAS 가 0 에서만 성공한다” 로(구현에 가깝게), 빌린 것은 유령 상태로(일반적으로, 분수까지) 보였다. 두 방법으로 만들고 맞대는 원리(31장)가 증명 층에서도 한 번 더 선다.

47.5 교착 자유와 굶주림 없음#

수학. 교착 자유(LowentDeadlock.v 의 no_deadlock)

모든 흐름이 잠금을 오름차순으로만 잡으면, 어떤 상태에서도 진행할 수 있는 흐름이 반드시 있다 — 전원이 동시에 막히지 않는다. 씨앗은 한 문장이다. 가장 큰 잠금을 원하는 흐름을 보라. 그것이 막혔다면 그 잠금을 쥔 다른 흐름이 있고, 규율에 따라 그 흐름이 원하는 것은 더 크다 — 최대성에 모순이다. 규율을 어기면 실제로 교착이 난다는 상태도 계산으로 보였다(violating_the_order_deadlocks).

 오름차순을 지킬 때 (A < B)            규율을 어길 때
 흐름 1   A 를 쥠 → B 를 원함          흐름 1   A 를 쥠 → B 를 원함
 흐름 2   A 를 원함 (기다림)           흐름 2   B 를 쥠 → A 를 원함
 → 흐름 1 이 B 를 잡고 진행한다        → 서로를 기다린다 (교착)

정직하게 — 도구가 이 규율을 강제하지 않는다. 그래서 이것은 “이렇게 쓰면 안전하다” 이지 “컴파일러가 막아 준다” 가 아니다. 검사로 만들려면 잠금에 정적 순서를 붙여야 한다. 그리고 락 자체의 명세(잡으면 자원을 받는다)는 교착을 막지 않는다. “잡으면 받는다” 이지 “반드시 잡힌다” 가 아니기 때문이다. 락을 두 번 잡고 한 번 놓으면 둘째 잡기는 영원히 오지 않는다.

수학. 굶주림 없음(LowentFair.v 의 no_starvation)

협력형 라운드로빈 스케줄러에서 준비된 태스크는 자기 앞의 수 + 1 걸음 안에 반드시 돈다. “언젠가” 가 아니라 유계다. 귀납의 측정치가 대기열의 길이가 아니라 자리인 것이 요점이다 — 회전은 길이를 보존하므로. 회전이 없으면 굶는다는 것도 증명했다.

한계는 분명하다. 협력형은 양보를 가정한다. yield 없이 끝없이 도는 태스크 앞에서 스케줄러가 할 수 있는 것은 없다. 우선순위와 차단도 이 모델 밖이다.

흔한 오해. 락을 쓰면 교착도 막아 준다

락의 명세는 “잡으면 자원을 받는다” 이지 “반드시 잡힌다” 가 아니다. 교착 자유(no_deadlock)는 모든 흐름이 잠금을 오름차순으로만 잡는다는 규율 위에서만 성립하고, 이 판의 도구는 그 규율을 강제하지 않는다. 락을 두 번 잡고 한 번 놓으면 둘째 잡기는 영원히 오지 않는다. 증명이 주는 것은 “이렇게 쓰면 안전하다” 는 설계 규칙이고, 그 규칙을 지키는 일은 아직 사람의 몫이다.

47.6 약한 메모리에서 빌린 증명 — `spsc`#

Iris 의 언어(heap_lang)는 순차 일관성 모델이다. 약한 기억 차례를 적은 코드를 증명하려면 RC11 위의 Iris 논리인 iRC11·gpfsl 이 필요하다. LowentIRC11.v 가 그 위에서 첫 정리를 세웠다 — release 쓰기와 acquire 읽기로 짠 메시지 전달 프로그램은 RC11 에서 읽는 쪽이 반드시 데이터를 본다. 순차 일관성을 가정하지 않는다. 46장의 E4 가 실행 하나에서 프로그램 전체로 올라갔다.

그 도구로 표준 라이브러리 모듈을 하나 세웠다.

examples/ch47/ring.low

module ring .
rem run: main

use spsc .

proc main input k cap atomic . input al cap allocator . output u8 . effects atomic alloc .
do
  let gc option mut slice u8 be alloc_bytes al capacity 16 .
  let gb option mut slice u8 be alloc_bytes al capacity 32 .
  let go option mut slice u8 be alloc_bytes al capacity 8 .
  guard is_some gc . else return 255 .
  guard is_some gb . else return 254 .
  guard is_some go . else return 253 .
  var ctl mut slice u64 be view_array u64 (some_value gc) .
  var buf mut slice u64 be view_array u64 (some_value gb) .
  var out mut slice u64 be view_array u64 (some_value go) .
  let a u64 be spsc.spsc_push k ctl buf 10 .
  let b u64 be spsc.spsc_push k ctl buf 32 .
  let got u64 be spsc.spsc_pop k ctl buf out .
  guard eq got 1 . else return 252 .
  let first u64 be index out 0 .
  let again u64 be spsc.spsc_pop k ctl buf out .
  return narrow u8 (add first (index out 0)) .
end

실행 결과

$ lowentc --run main ring.low
main() = 42

생산자는 칸을 먼저 채우고 그다음에 색인을 release 로 공개한다. 소비자는 그 색인을 acquire 로 읽은 뒤에야 칸을 읽는다. lowent_spsc_push_is_correct· lowent_spsc_pop_is_correct 가 이 짝이 RC11 에서 옳다고(가득·빔 판정 포함) 말한다.

 생산자                                   소비자
 buf[i] ← x          (칸을 먼저 채운다)
 tail ← i+1  release ─────────────────▶   tail  acquire  로 i+1 을 보면
                                          buf[i] 를 읽는다 → 반드시 x 를 본다 (RC11 에서)

실제 사례. 빌렸다는 것의 뜻

알고리즘 수준의 증명은 gpfsl 의 circ_buff 이고, mp_instance_gen_inv 도 gpfsl 의 것이다. 이 저장소가 한 일은 “우리가 방출하는 기억 차례가 그 명세가 요구하는 바로 그것” 임을 진술하고 잇는 것이다. 그래서 신뢰 기반에 gpfsl 과 Iris 개발판이 더해진다. 다시 짓지 않은 이유는 하나다 — 같은 것을 두 벌 두면 갈린다. 그리고 그래서 하나만 넣었다. MPSC·MPMC·seqlock 은 빌릴 근거가 없고, 근거 없이 넣으면 표준 라이브러리가 “검증됐다고 적혀 있으나 아무도 검증하지 않은 것” 의 창고가 된다. “무겁다” 고 적어 두었던 이 작업을 실제로 재 보니 대부분이 도구 조립이었고 진짜 위험은 없었다. 재 보기 전에는 비용을 모른다.

문. 증명된 락이 있는데 이 판에서 lock 은 왜 없는가?

답. 증명한 것은 Iris 의 언어로 쓴 CAS 스핀락이고, 실제 런타임의 락이 그것과 같다는 것은 검증되지 않았다 — 이 파일과 구현 사이의 가장 큰 간극이다. 그리고 나누어 가지는 자물쇠 상태 타입은 아직 짓지 않았다(E-LOCK-NOTYET, 26장). 증명이 먼저 있고 구현이 나중에 오는 자리다. 없는 것을 받아들이고 나중에 짓는 대신 없다고 말한다.

47.7 증명하지 않은 것#

락 모델은 순차 일관성이다. 약한 기억 차례는 heap_lang 락 증명에 없다. 다만 기본 차례가 seq_cst 이므로(46장) 기본값으로 쓰는 level 3 코드는 그 모델 안에 있고, 약한 차례를 적은 코드만 iRC11 의 몫으로 남는다. 가둠이 여기서도 선다.
구현이 이 스핀락이라는 보장이 없다.
two_threads_spec 은 정확한 합계를 말하지 않는다.
교착 자유는 사람이 지키는 규율에 기댄다. 굶주림 없음은 양보를 가정하고, 우선순위·차단은 밖이다.
우리 컴파일러가 spsc 의 그 프로그램을 낸다는 보장은 없다. 기억 차례의 1 대 1 방출과 차례를 바꾸지 않음은 시험으로 확인한다.
빌린 증명은 신뢰 기반에 들어간다. 두 확인기(Coq 8.20.1 · Rocq 9.2)가 같은 답을 내어 확인기 자체의 결함 가능성을 줄이지만, gpfsl 이 필요한 둘은 Rocq 9.2 에서만 확인된다.

복습 정리

분리논리의 ∗ 는 서로 다른 조각을 뜻해 국소 추론을 주고, 락은 “열려 있으면 자원이 불변식 안에, 잠겨 있으면 잠근 흐름의 손에” 라는 불변식 한 줄과 유령 토큰으로 증명된다. 토큰은 둘일 수 없고, 잡으면 토큰과 자원을 받으며, 놓으려면 둘 다 반납한다. rwlock 의 배타성은 직접 증명과 빌린 증명 두 가지로 확인했고, 오름차순 잠금은 교착하지 않으며 라운드로빈은 유계 안에 태스크를 돌린다. 약한 메모리의 프로그램 논리를 빌려 spsc 를 확인했고, 그 대가로 신뢰 기반이 늘었다.

← 이전목차로다음 →