44 효과의 증명 — “무엇을 할 수 있나” 를 타입에 적기

먼저 알아야 할 것

15장 효과 · 효과는 호출을 따라 번지고, 순수함은 차례 바꾸기·기억하기·지우기를 허락한다

16장 권한 · 효과는 무슨 일인지, 권한은 누가 허락했는지를 적는다

39장 수학 도구상자 · 격자와 join

돌아보기

15장에서 fn 과 proc 을 가르는 기준은 무엇이었고, 순수하다는 약속은 처리기에게 무엇을 허락했는가?

답. fn 은 바깥에 자국을 남기지 않고 proc 은 적은 효과만큼 남긴다. 순수한 op 은 같은 인자에 같은 답을 내므로 처리기가 호출의 차례를 바꾸거나, 결과를 기억하거나, 쓰이지 않는 호출을 지워도 된다. 이 장은 그 약속이 정말로 지켜진다는 증명 — 그리고 그 증명이 왜 순환 논증이 아닌지 — 를 다룬다.

이 장의 필요성과 맥락

40·43장은 “메모리를 어떻게 만지나” 였다. 이 장은 “무엇을 할 수 있나” 다. effects none 은 강한 약속이다 — 전역을 읽지도, 할당하지도, 화면에 쓰지도, 기다리지도 않는다. 그 약속을 최적화기가 믿고 호출을 지우는데 실제로는 파일을 썼다면, 관측할 수 있는 동작이 사라진다. 효과 체계는 메모리 안전을 주지 않는다. 대신 다른 종류의 안전 — 최적화의 정당성, 감사할 수 있음, 작은 기계에서의 거절 — 을 준다. 그 안전이 선언을 믿는 데서 오므로, 선언이 실제를 덮는다는 정리가 필요하다.

이 장이 끝나면

효과가 원자의 집합이고 부분집합 순서로 격자를 이룬다는 것, 전파와 게이팅이 한 격자의 두 연산이라는 것을 알게 된다. 처리기가 강제하는 네 규칙 (전파 · 순수성 · 원자의 집합 · 멈춤은 효과가 아니다)을 예제로 확인하고, 권한이 효과의 짝으로서 주는 감쇠와 국소 감사를 익힌다. 효과 건전성 정리가 순환이 아닌 까닭, 효과에 기댄 네 최적화가 적법하다는 증명과 그 반례도 보게 된다.

이 장에서 답할 질문

예약된 낱말을 매개변수 이름으로 쓰면 왜 효과 진단이 아니라 이름 진단이 나오는가?

44.1 효과는 원자의 집합이다#

효과는 원자의 집합이다. effects io alloc . 처럼 여러 원자를 가질 수 있다. 그러면 자연스러운 순서가 하나 있다 — ε₁ ⊑ ε₂ 는 ε₁ ⊆ ε₂, 곧 “ε₁ 이 ε₂ 보다 적게 한다” 이다. 부분집합 관계는 격자를 이루고, join 은 합집합이며, none(빈 집합)이 가장 아래다.

무엇	격자 연산	뜻
전파	`⊔`(합집합)	내가 부르는 것들의 효과를 모두 모으면 내 효과다
게이팅	`⊆`(부분집합)	선언한 것보다 적게 하는 것은 괜찮다

표 44.1 — 격자 하나가 하는 두 가지 일

40장의 타입 격자와 같은 모양이다. 다른 문제에 같은 수학이 답한다. 그리고 작은 기계의 판정이 ⊆ 한 번이 된다. 힙이 없는 기계에서 alloc 하는 코드는 번역되면 안 되는데(30장), 효과 선언이 있으면 “이 op 의 효과가 이 등급이 감당하는 집합에 들어가는가” 를 물으면 끝이다.

            {io, alloc}
             ▲       ▲
            {io}     {alloc}
             ▲       ▲
              none

 전파    f 가 g(effects io)와 h(effects alloc)를 부르면
         effects(f) ⊇ {io} ⊔ {alloc} = {io, alloc}      모자라면 E-EFFECT
 게이팅  힙 없는 보드가 감당하는 집합에 alloc 이 없으면
         {io, alloc} ⊄ 그 집합                          그 보드로는 번역되지 않는다

io 를 {read, write} 로 쪼개는 계층 격자도 쓸 수 있다. 이 언어는 지금 평면을 쓴다. 계층으로 얻는 정밀도는 권한 쪽에서 이미 얻을 수 있고, 평면은 ⊆ 판정이 간단해 비용이 보인다. 정밀도를 두 곳에서 표현하면 그 둘이 어긋나기 시작한다.

44.2 처리기가 강제하는 네 규칙#

규칙 1 — 전파. f 가 g 를 부르면 effects(f) ⊇ effects(g) 여야 한다. 아니면 E-EFFECT(fn 이면 E-EFFECT-CALC)다. effects none 이라 적힌 op 이 몰래 파일을 쓰는 일을 막는다(15장).

규칙 2 — 순수성. fn 이 호출자의 버퍼에 쓰면 E-EFFECT-PURITY 다. fn 은 값을 계산하고 proc 은 일을 한다. 판정의 기준이 낱말의 모양이면 구멍이 난다. 한때 액터의 핸들러가 proc 이 아니라는 이유로 순수로 세어져, 액터 상태를 고치면서 effects none 을 선언해도 아무도 반대하지 않았다. 같은 죄인데 한쪽은 잡히고 한쪽은 안 잡혔다.

규칙 3 — effects 절은 원자의 집합이다.

examples/ch44/effect_dup.low

module effect_dup .
rem expect: E-EFFECT-DUP

proc shout input out cap io . output u64 . effects io io . do
  return write_out out 1 "hi\n" .
end

실행 결과

$ lowentc --check effect_dup.low
effect_dup.low:4:0 E-EFFECT-DUP: an effect atom appears more than once in the `effects` clause — the row is a SET, not a list. A repeat says nothing the first one didn't, and the reader has to decide it's noise (RFC-0057 E3)

examples/ch44/effect_typo.low

module effect_typo .
rem expect: E-EFFECT-UNDEF

proc ping input out cap io . output u64 . effects netwrok . do
  return 0 .
end

실행 결과

$ lowentc --check effect_typo.low
effect_typo.low:4:0 E-EFFECT-UNDEF: unknown effect (the vocabulary is closed: none/alloc/heap/io/wait/concurrent/lock/atomic/unsafe/device/page_fault/blocking/cancel/detach/panic/state) — a typo here silently declares the op PURE

같은 원자를 두 번 적으면 거절된다. 집합에 중복은 뜻이 없고, 읽는 사람이 그것이 잡음인지 판단해야 한다. 없는 원자는 오타로 잡힌다 — 진단이 말하듯 오타가 조용히 지나가면 그 op 은 순수하다고 선언한 것이 된다. 당연해 보이는 규칙이지만, 구현이 절의 첫 낱말 하나만 읽던 때가 있었다. 그때 effects io alloc 은 io 로만 등록되었고 둘째 원자부터는 적어도 없는 것과 같았다. 선언을 읽는 코드의 결함은 선언 체계 전체를 무력하게 만든다.

규칙 4 — 멈춤은 효과가 아니다. 이 장에서 가장 생각할 거리다.

examples/ch44/trap_not_effect.low

module trap_not_effect .
rem run: pick [1,2,3] 1
rem trap: pick [1,2,3] 7

rem 범위를 벗어나면 멈추지만, 이 op 은 여전히 순수한 fn 이다
fn pick input s slice u8 . input i u64 . output u8 . do
  return index s i .
end

실행 결과

$ lowentc --run pick trap_not_effect.low [1,2,3] 1
pick([1,2,3], 1) = 2
  arg0 (written) = [1,2,3]
$ lowentc --run pick trap_not_effect.low [1,2,3] 7
== ir diagnostics (1) ==
0:0 E-VM-BOUNDS: slice index out of bounds (panic)

index s i 는 범위를 벗어나면 멈춘다. 그러면 pick 은 panic 효과를 가져야 하는가? 아니다. panic 은 명시적인 panic "…" 만 센다. 멈출 가능성은 계약이 말하는 것이지 효과가 말하는 것이 아니다. index 의 위험은 requires lt i (len s) 로 없앨 수 있고 실제로 처리기가 그 검사를 지운다(41장). 효과 표시는 지워지지 않는다. 없앨 수 있는 것을 효과로 표시하면 그 표시는 영원히 남고, 거의 모든 op 이 panic 을 갖게 되어 표시가 뜻을 잃는다.

 op 을 끝내는 것           어디에 적나                 지워지나
 panic "…"  (의도)         effects panic               아니다 — 늘 남는다
 범위 밖 index (위반)      requires lt i (len s)       증명되면 검사가 지워진다

흔한 오해. 멈출 수 있는 op 은 순수하지 않다

효과는 “이 op 이 무엇을 하는가” 이고 계약은 “언제 안전한가” 다. 둘을 섞지 않았기 때문에 panic 표시가 여전히 정보를 가진다. panic 이 붙어 있으면 그 op 은 의도적으로 프로그램을 끝낼 수 있다는 뜻이다. 범위 밖 색인은 의도가 아니라 계약 위반이고, 계약이 그 자리를 맡는다.

44.3 권한 — 효과의 짝#

효과가 “무슨 종류의 일을 하나” 라면, 권한은 “그 일을 할 권리를 어디서 받았나” 다. cap io 를 인자로 받아야 화면에 쓸 수 있고, 아무 데서나 전역으로 꺼내 쓰지 못한다. 이 객체-권한 모형이 두 가지를 준다.

감쇠(attenuation). 받은 권리를 좁혀서 넘길 수 있다. 평면 효과 격자로 못 하는 정밀도를 여기서 얻는다.
국소 감사. op 의 서명만 보면 무엇에 손댈 수 있는지 전부 보인다. 숨은 전역 통로가 없다는 것이 요점이다.

주는 것	어떻게
최적화의 정당성	`effects none` 이면 차례 바꾸기·공통 부분식 제거·지우기가 관측 동작을 바꾸지 않는다
감사할 수 있음	`io` 를 하는 코드를 선언에서 찾을 수 있다
등급과 프로파일 게이팅	작은 기계에서 `alloc` 하는 op 을 번역 오류로 막는다
놀람이 없음	순수하다고 적힌 것이 정말 순수하다

표 44.2 — 효과 체계가 주는 안전

44.4 효과 건전성 — 순환이 아니다#

examples/ch44/recursive.low

module recursive .
rem run: main

proc stars input out cap io . input n u64 . output u64 . effects io .
  requires le n 10 .
do
  if eq n 0 . do
    return write_out out 1 "\n" .
  end
  let w u64 be write_out out 1 "*" .
  return add w (stars out (sub n 1)) .
end

proc main input out cap io . output u8 . effects io .
do
  return narrow u8 (stars out 5) .
end

실행 결과

$ lowentc --run main recursive.low
*****
main() = 6

stars 는 자기를 부르는 재귀이고 effects io 를 선언한다. 처리기는 호출 자리에서 피호출자의 본문을 다시 걷지 않고 선언을 쓴다. 언뜻 순환처럼 보인다 — 선언이 선언을 믿는다.

수학. 효과 건전성(LowentEffect.v 의 effect_sound)

prog_ok P = true -> lookup P f = Some (d, b) -> performs P (ECall f) a -> In a d. 검사를 통과한 프로그램에서 op f 를 부르면, 실제로 일어나는 모든 효과는 f 가 선언한 것 안에 있다. 호출 깊이와 무관하다. 순환이 아닌 까닭은 귀납이 프로그램이 아니라 실행에 대한 것이기 때문이다. 효과가 하나 일어나면 그것은 어떤 유한한 호출 깊이에서 일어나고, 그 깊이에 대한 귀납이 닫힌다. 그래서 재귀도, 상호 재귀도, 끝나지 않는 재귀도 따로 다룰 것이 없다. 자기를 부르는 op 이 검사를 통과하고, io 가 실제로 일어나며, alloc 은 일어날 수 없다는 예제가 증명 파일에 함께 있다.

44.5 효과에 기댄 최적화는 적법하다#

효과 건전성 위에 최적화의 적법성이 선다. 효과 층에서는 순수한 조각의 자리를 바꿔도(pure_calls_commute), 지워도(dropping_pure_is_legal) 일어나는 효과가 같다. 값 층까지 올린 증명이 LowentOpt.v 다. 값·상태·출력 열을 가진 모델에서 차례 바꾸기, 공통 부분식 제거, 결과 기억, 죽은 코드 제거가 넷 다 적법함을 증명했다.

열쇠는 한 줄이다 — 값은 읽는 칸에만 달렸다(value_depends_only_on_reads). 그리고 전제가 장식이 아님을 반례로 보였다. 효과 있는 조각의 차례를 바꾸면 값이 14 에서 7 로 바뀌고, 출력하는 조각을 지우면 출력이 준다. 정리 하나에 반례 하나 — 반례가 없으면 조건이 과하게 엄격해도 정리는 참이다.

문. 예약된 낱말을 매개변수 이름으로 쓰면 왜 효과 진단이 아니라 이름 진단이 나오는가?

답. 한때는 반대였다. 매개변수 이름을 원시 포인터 낱말인 raw 로 쓰면 효과 추론이 조용히 오염되어 “순수하다고 선언했는데 효과를 수행한다” (E-EFFECT-CALC)가 떴다. 진짜 까닭은 “예약된 낱말을 이름으로 썼다” 인데 진단은 순수성을 가리켰다. 프로그래머를 엉뚱한 곳으로 보내는 진단이 가장 나쁘다. 그래서 그 낱말들을 E-NAME-BUILTIN 으로 넘겨 같은 죄에 진단 하나만 남겼다. 증명이 정하는 것은 무엇을 거절하나이고, 사람이 만나는 것은 왜 거절했나다 — 후자가 틀리면 전자의 값이 절반으로 준다.

44.6 증명하지 않은 것#

구현이 모델과 같다는 것은 시험과 두 백엔드 대조가 받치는 경험적 대응이다(50장).
task_group 이 concurrent 를 흡수하는 규칙은 ⊆ 규율이 아니라 요구의 해소라 모델 밖이다.
효과 기반 최적화에서 호출 경계(순수 판정을 op 경계로 올리는 일)와 멈추는 시점은 밖이다.
평면 격자의 정밀도 한계. io ⊑ {read, write} 같은 정련은 하지 않았고, 그것을 권한 감쇠로 대신하는데 둘이 같은 정밀도를 준다는 논증은 없다.
effect-row 다형성이 없다. “호출자의 효과를 그대로 물려받는 op” 을 쓸 수 없어, 고차 op 은 효과를 가장 넓게 선언해야 한다.
일부 원자는 어휘만 있다. page_fault·blocking·cancel·detach 따위는 선언할 수 있어도 그것을 일으키는 연산이 아직 없어, 그 원자의 전파는 실전 검증이 얇다.

복습 정리

효과는 원자의 집합이고 부분집합 순서로 격자를 이루며, 전파는 합집합, 게이팅은 부분집합 판정이다. 처리기는 전파 · 순수성 · 원자의 집합(중복과 오타 거절) · 멈춤은 효과가 아님의 네 규칙을 강제하고, 권한이 효과의 짝으로 감쇠와 국소 감사를 준다. 효과 건전성은 실행에 대한 귀납이라 재귀가 있어도 순환이 아니며, 그 위에서 차례 바꾸기·공통 부분식 제거·기억·죽은 코드 제거가 반례와 함께 적법함이 증명되었다.

← 이전목차로다음 →