43 되풀이와 고정점 — “몇 번을 돌든” 을 증명하기

43.1 두 번째 회차에서 깨진다#

module loop_stale .
rem expect: E-EXCL

proc drift input n u64 . output u64 .
  requires le n 100 .
do
  var x u64 be 1 .
  let r ref u64 be ref x .
  var i u64 be 0 .
  var seen u64 be 0 .
  while lt i n . do
    set x (add x 1) .
    set seen (deref r) .
    set i (add i 1) .
  end
  return seen .
end

$ lowentc --check loop_stale.low
12:0 E-EXCL: exclusivity violation: overlapping borrow/owner access (readers-XOR-writer)
12:0 E-EXCL: exclusivity violation: overlapping borrow/owner access (readers-XOR-writer)

반복 밖에서 만든 읽기 빌림 r 을 반복 안에서 쓰면서, 같은 반복 안에서 소유자가 x 에 쓴다. 1 회차는 문제가 없어 보인다. 그러나 그 쓰기가 r 을 죽이고, 2 회차의 deref r 이 죽은 빌림을 쓴다. 한 번 돌 때는 멀쩡하고 두 번째에 터지는 모양이다. 처리기는 이것을 번역에서 거절한다.

module loop_fresh .
rem run: drift 5

proc bump input p mut_ref u64 . output u64 .
do
  set p (add (deref p) 1) .
  return deref p .
end

proc drift input n u64 . output u64 .
  requires le n 100 .
do
  var x u64 be 1 .
  var i u64 be 0 .
  var seen u64 be 0 .
  while lt i n . do
    set seen (bump (mut_ref x)) .
    set i (add i 1) .
  end
  return seen .
end

$ lowentc --run drift loop_fresh.low 5
drift(5) = 6

반대로 빌림이 반복 안에서 태어나 안에서 끝나면 회차마다 신선하고, 회차 사이에 낡은 것이 남지 않는다. “반복 안에서 만들고 반복 안에서 끝내라” 는 흔한 조언에 증명이 붙은 것이다.

43.2 고정점이면 몇 번이든#

여기서 함수 f 는 “반복 몸을 한 번 도는 것” 이고, 값 x 는 정적 검사기의 상태(살아 있는 빌림 목록)다. 몸을 한 번 돌아도 정적 상태가 그대로면 그것이 고정점이다. 그러면 귀납법이 선다.

0 번 돌면 안전하다.                                      기초 --- 아무 일도 안 했다
상태 L 에서 안전하게 한 번 돌면 상태가 다시 L 이다.        보존
─────────────────────────────────────────────
따라서 몇 번을 돌아도 안전하다.                          ∀k

도미노를 세울 때 조각의 간격이 모두 같아야 하는 것과 같다. 상태가 회차마다 달라지면 “다음 조각” 을 논증할 수 없다. 상태가 되돌아오니까 같은 논증을 끝없이 다시 쓸 수 있다.

고정점에 닿지 않는 코드도 있다. 회차마다 빌림이 하나씩 늘고 죽지 않아 반복 밖으로 새면 정적 상태가 자란다. 그런 코드는 정리의 전제를 만족하지 않고, 처리기가 거절한다. 빌림이 몸 안에서 태어나 몸 안에서 죽으면 상태가 되돌아온다 — 그것이 보통의 코드다.

43.3 위험한 모양은 하나뿐이다#

증명을 하며 알아낸 사실이 있다. 반복에서 빌림이 깨지는 방식은 한 가지뿐이다.

pre 에서 만든 빌림 τ 를 body 에서 쓰고, 동시에 body 안에 소유자 접근 own(x) 가 있다.
  → i 회차의 own(x) 가 τ 를 죽인다.
  → i+1 회차의 use(τ) 가 위반을 낸다.

정적 규칙 하나가 정확히 그 짝 — 반복을 넘어 사는 빌림 × 몸의 소유자 접근 — 을 거절하고, 정리 B 의 증명은 “그 하나로 충분하다” 를 보인다. 다른 위험은 없다. 이것이 증명의 실용적 산출물이다. 규칙이 모자라면 결함이 새고, 넘치면 정상 코드가 막히는데, 몇 개가 맞는지를 논증이 정했다.

43.4 신선한 토큰 — 이름 문제를 없애는 한 수#

반복의 진짜 골치는 이름 충돌이다. 1 회차의 r 과 2 회차의 r 은 소스에서 같은 이름인데 실행에서는 다른 빌림이다. 보통 이것을 다루려면 “태그 재명명” 이라는 장치를 만든다.

이 증명은 그 장치를 만들지 않았다. 대신 모델이 실행할 때마다 새 토큰을 발행한다. 정적 태그 t 는 환경을 거쳐 “지금의 토큰” 을 가리키고, 그 토큰은 회차마다 새 번호다. 그러면 지난 회차의 토큰은 아무도 가리키지 않으므로 저절로 무효가 된다. 이것은 억지가 아니다 — 구현이 실제로 신선한 태그를 발행한다. 모델이 구현을 따라간 덕에 증명이 짧아졌다. 증명이 어려우면 모델을 다시 보라. 어려움의 절반은 잘못된 표현에서 온다.

증명에는 42장의 INV·SINV 에 불변식이 하나 더 붙는다.

• FRESH — 발행된 토큰은 모두 next 보다 작다.

이것이 없으면 새 토큰이 옛 토큰과 같은 번호를 받을 수 있고, 그러면 죽은 빌림이 되살아난다. 증명에서 가장 무서운 종류의 구멍이다 — 안전 쪽이 아니라 위험 쪽으로 틀린다.

43.5 중첩 반복 — 함수를 관계로#

module nested .
rem run: tri 4

proc bump input p mut_ref u64 . output u64 .
do
  set p (add (deref p) 1) .
  return deref p .
end

rem 안쪽 반복은 바깥 회차마다 다른 횟수로 돈다(0, 1, 2, 3 번)
proc tri input n u64 . output u64 .
  requires le n 100 .
do
  var x u64 be 0 .
  var i u64 be 0 .
  while lt i n . do
    var k u64 be 0 .
    while lt k i . do
      let seen u64 be bump (mut_ref x) .
      set k (add k 1) .
    end
    set i (add i 1) .
  end
  return x .
end

$ lowentc --run tri nested.low 4
tri(4) = 6

안쪽 반복은 바깥 회차마다 0, 1, 2, 3 번 돈다. 빌림 mut_ref x 는 안쪽 몸 안에서 태어나 끝나므로 어느 회차에서도 안전하다.

평평한 정리 B 는 unroll body k — “모든 회차가 똑같이 돈다” — 를 강요한다. 실제 프로그램은 그렇지 않다. 중첩 반복의 증명(LowentNest.v)은 프로그램을 나무(NLeaf·NSeq·NLoop)로 두고, 펼침을 함수가 아니라 관계로 적었다.

첫 회차가 상태를 바꾸는 반복도 들어온다. b ; loop b 로 한 번 벗기면 그 뒤로는 고정점이 된다(peeled_loop_is_safe).

43.6 증명하지 않은 것#

• 갈래(if)의 합류는 정리 B 안에 없다. 모델은 (pre, body) 두 직선 나열이다. 합류의 정확성은 위의 전수 검사가 받친다.
• 고정점에 닿는 과정은 모델 밖이다. 정리는 닿은 뒤를 말한다.
• 반복이 끝나는지는 다루지 않는다. 정리는 “돌면 안전하다” 이지 “끝난다” 가 아니다. 무한 반복은 펌웨어의 주 반복처럼 이 언어에서 정당한 프로그램이다. 그래서 도구가 스스로 만든 시험을 돌릴 때는 걸음 예산을 둔다(41장) — 종료를 보장할 수 없으니 도구가 멈출 줄 알아야 한다.