42 소유와 차용의 증명

42.1 두 기계와 세 사건#

같은 규칙을 보는 기계가 둘 있다. 정적 기계는 컴파일할 때 살아 있는 빌림의 목록을 들고, 겹치는 빌림을 만들려 하면 거절한다. 동적 기계는 실행 중에 자리마다 빌림 스택을 두고, 무효가 된 빌림을 쓰면 멈춘다. 이 장의 정리는 두 기계가 서로 어긋나지 않는다는 것이다.

증명을 위해 프로그램을 세 종류 사건의 나열로 줄인다. 전체 언어 대신 본질만 남긴 작은 대상을 만드는 것이 증명의 첫 기술이다.

동적 기계는 규칙 다섯으로 정의된다. 빌림을 만들면 스택에 쌓고(D1), 빌림으로 읽으면 그 위의 쓰기 빌림만 버리고 읽기 빌림은 남기며(D2), 빌림으로 쓰면 그 위를 전부 버린다(D3). 소유자가 읽으면 쓰기 빌림을 모두 무효로 하고(D4), 소유자가 쓰면 스택을 비운다(D5). D2 와 D3 의 차이가 요점이다 — 읽기는 여러 독자가 공존해도 문제가 없지만, 쓰기 뒤에는 위의 이름들이 낡은 값을 보므로 더는 쓸 수 없어야 한다. 그리고 소유자가 다시 손대는 것 자체를 오류로 만들지 않고, 그 뒤에 죽은 빌림을 쓰려 할 때 잡는다.

사건 넷을 차례로 먹이면 자리 x 의 스택이 이렇게 바뀐다.

 사건                        스택 (아래 → 위)
 Create r1 x 읽기    D1      r1
 Create w2 x 쓰기    D1      r1 w2
 Use r1 읽기         D2      r1          r1 위의 쓰기 빌림 w2 를 버린다
 Use w2 쓰기                 → 위반      w2 는 이미 스택에 없다

정적 기계는 둘째 사건에서 이미 거절한다. 읽기 빌림 r1 이 살아 있는데 같은 자리에 쓰기 빌림을 만들기 때문이다.

42.2 중심 정리#

                 ┌─▶ 정적 기계 (살아 있는 빌림 목록) ── 초록 ──────┐
 사건 나열 evs ──┤                                                 │ 정리 A
                 └─▶ 동적 기계 (자리마다 빌림 스택) ── 위반 없음 ◀─┘

 정적 초록 ⇒ 동적 위반 없음      (증명됨)
 동적 위반 없음 ⇒ 정적 초록      (참이 아니다 — 정적 검사는 보수적이다)

대우가 실용적인 뜻을 선명하게 한다. 번역을 통과한 코드에서 실행 중에 차용 위반을 보는 일은 없다. “번역은 됐는데 돌려 보니 빌림이 깨졌다” 는 조합 자체가 이 모델 안에서는 일어날 수 없다.

반대 방향 — 동적으로 안전하면 정적으로도 통과한다 — 은 참이 아니고 참일 필요도 없다. 정적 검사는 보수적이라 실제로는 안전한 프로그램도 거절할 수 있다. 안전 쪽으로 틀리는 것은 불편이고, 위험 쪽으로 틀리는 것은 재앙이다. 41장의 구간 분석과 같은 비대칭이다.

증명은 불변식 보존이고, 불변식이 둘 필요했다.

• INV — 정적으로 살아 있는 빌림은 동적 스택에도 있고, 대상 자리와 쓰기 여부가 일치한다.
• SINV — 같은 자리에 살아 있는 서로 다른 빌림 둘은 모두 읽기 빌림이다.

SINV 가 왜 필요했는가. 빌림으로 쓰면(D3) 스택의 위를 전부 버리는데, 버려진 것 가운데 정적으로는 아직 살아 있는 빌림이 있으면 INV 가 깨진다. “쓰기 빌림은 하나뿐” 이라는 규칙이 겹침을 막으므로, 쓰기를 하는 빌림과 같은 자리에 살아 있는 다른 빌림은 없다. 직관은 “겹치면 위험하니까” 라고 말하지만, 증명은 더 정확한 이유를 준다 — 그 규칙이 없으면 두 기계의 대응이 무너진다. 규칙을 느슨하게 하면 정확히 어디가 깨지는지 증명이 가리킨다.

나머지는 자료구조에 대한 지루한 보조정리다 — “담은 자리에서 꺼내면 담은 것이 나온다”(get_set_same), “다른 자리는 바뀌지 않는다” (get_set_other), “스택의 위를 버려도 그 태그는 남는다”(in_pop_above). 증명이 길어지는 곳은 늘 흥미로운 곳이 아니라 이런 곳이다.

42.3 거절되는 모양, 통과하는 모양#

정리가 막는 것을 코드의 모양으로 옮기면 이렇다. 네 모양 모두 12장의 예제로 실제 진단을 보았다.

42.4 모델을 넓히다가 구현의 결함을 찾았다#

평평한 모델은 자리를 번호로 봤다. 실제 언어는 더 복잡하다. 모델을 두 번 넓혔고, 두 번 다 정리 A 를 다시 증명했다.

칸(place). 평평한 모델에서 x.a 와 x.b 는 둘 다 그냥 x 라서, 서로 다른 칸의 쓰기 빌림 둘이 충돌하는 것으로 나온다. 실제 규칙은 통과시킨다. 증명이 구현을 따라가지 못하면 그 증명은 다른 언어에 대한 것이다. 그래서 자리를 경로로 일반화하고, 자리의 같음을 겹침(“한쪽이 다른 쪽의 접두사다”)으로 바꿨다. 정리와 불변식의 구조는 그대로였다. 좋은 추상을 골랐으면 확장이 이렇게 국소적으로 끝난다.

op 경계. 사건 언어에는 호출이 없었다. 그래서 op 이 인자로 받은 빌림을 그대로 참조로 돌려주어 빌림을 세탁하는 모양이 모델 밖에 있었다. 구현이 그것을 실제로 겪었다 — 정적 검사가 돌려받은 참조를 원래 빌림과 같은 것으로 알아보지 못해 통과시켰다. 결함을 고친 뒤 그 이야기를 정리로 옮겼다.

그때까지 그것은 “우리가 겪었다” 는 이야기였다. 이야기는 잊히고 리팩터링에 지워진다. 이제 그것은 정리다. 누가 그 검사를 지우면 증명이 깨진다. 이것이 이 저장소에서 증명이 하는 가장 값진 일이다.

42.5 모델과 구현 사이#

정리는 종이 위의 두 기계에 대한 것이다. 그 기계가 실제 컴파일러와 같은지는 유계 전수 모델 검사가 받친다. 자리 둘·태그 넷 이하·길이 7 이하의 모든 사건 나열 10,490,024 개를 구현의 정적 검사와 동적 기계에 먹여 판정이 모델과 같은지 본다. 위반은 0 이다. 옵트인으로 길이 9 의 13 억 개도 돌렸고 위반 0 이다.

봉투를 열한 배 넓히는 데 든 비용이 1 초가 되지 않았다. “비싸서 못 한다” 고 적기 전에 재 봐야 한다. 그래도 길이 10 이상은 모른다 — 그리고 그것을 적는 것이 이 절의 일이다.

반복의 분기 합류는 정리 밖이고, 반복 체커가 90,376 형태 × 반복 1 … 3 을 전수 확인한다(43장). 이것들은 “증명됨” 이 아니라 “전수 검사됨” 이다.

42.6 증명하지 않은 것#

• 모델은 직선 사건 나열이다. 갈래와 반복이 없다. 실제 컴파일러는 제어 흐름을 따라 빌림의 생사를 계산하는데, 정리 A 는 그 계산이 옳다는 것을 말하지 않는다. 그것이 43장의 주제다.
• 태그가 신선하다고 가정한다. 구현은 태그를 재사용하지 않지만 그 사실 자체는 증명 밖이다.
• 메모리 자체를 모델링하지 않았다. 사건 모델은 “누가 접근할 권리가 있나” 만 본다. 그 권리 체계가 해제 후 사용 같은 실제 메모리 안전으로 이어지는 단계는 별도다.
• 순차 단편에 대한 정리다. 여러 흐름으로의 확장은 45장의 데이터 경합 정리가 맡는다.