19 소유 — 없앨 책임은 하나에게
먼저 알아야 할 것
돌아보기
18장의 영역은 값들을 한꺼번에 걷는다. 그런데 파일 핸들처럼 하나씩, 그리고 닫다가 실패할 수 있는 자원은 영역만으로 다룰 수 있는가?
답. 영역은 바이트를 한꺼번에 되감을 뿐이라서, 파일을 닫거나 버퍼를 비우는 일은 하지 못한다. 그리고 닫기가 실패하면 그 실패를 받을 자리가 영역의 end 에는 없다. 그런 자원에는 값마다 없앨 책임을 지는 소유가 필요하다. 이 장이 그것을 다룬다.
이 장의 필요성과 맥락
이 장이 끝나면
owned t 가 무엇이고 drop 이 무엇을 하는지 알게 된다. 옮긴 값을 다시 쓰거나 두 번 없애면 거절되고, 갈래마다 소유 상태가 다르면 거절되는 이유를 익힌다. 없애기가 해제(실패 없음)와 완결(실패할 수 있음) 두 갈래라는 것, 완결이 필요한 값을 자동으로 버리면 왜 거절되는지 보게 된다. 이 언어의 메모리 안전이 어느 강도로 보장되는지도 정리한다.이 장에서 답할 질문
- 소유가 없는 값은 넘길 때 어떻게 되는가?
19.1 owned 와 drop#
owned t 는 소유를 가진 값이다. 소유를 가진 값은 정확히 한 번 없애져야 한다.
examples/ch19/sink.low
module sink .
rem run: use_once 5
type buffer u8 .
fn consume input h owned buffer . output u8 .
do
drop h .
return 0 .
end
fn use_once input v u8 . output u8 .
do
var h owned buffer be v .
return consume h .
end
실행 결과
$ lowentc --run use_once sink.low 5
use_once(5) = 0
consume 은 owned buffer 를 받아 drop h . 로 없앤다. use_once 는 var h owned buffer be v . 로 소유 값을 만들어 consume 에 넘긴다. 넘기는 순간 소유가 옮겨진다. 이제 h 를 없앨 책임은 consume 에 있고, use_once 는 h 를 더 쓸 수 없다.
use_once consume
┌──────────────────┐ 넘긴다(옮김) ┌──────────────────┐
│ h ──▶ [ 버퍼 ] │ ───────────────▶ │ h ──▶ [ 버퍼 ] │ ── drop h . → 없어진다
└──────────────────┘ └──────────────────┘
이제 h 는 빈 이름이다 없앨 책임은 여기 하나뿐
(다시 쓰면 E-OWN-MOVED)열쇠 하나짜리 사물함에 빗대면 쉽다. 열쇠를 건네면 내 손에는 열쇠가 없다. 사물함을 비울(없앨) 사람은 언제나 열쇠를 쥔 한 사람뿐이다. 그래서 «두 사람이 비운다»(두 번 해제)도, «아무도 안 비운다»(해제 누락)도, «건넨 열쇠로 또 연다» (옮긴 뒤 사용)도 생길 수 없다.
옮긴 값을 다시 쓰면 거절된다.
examples/ch19/moved.low
module moved .
rem expect: E-OWN-MOVED
type buffer u8 .
fn consume input h owned buffer . output u8 .
do
drop h .
return 0 .
end
fn reuse input h owned buffer . output u8 .
do
let a u8 be consume h .
let b u8 be consume h .
return add a b .
end
실행 결과
$ lowentc --check moved.low
moved.low:15:0 E-OWN-MOVED: this `owned` value was already MOVED (consumed) — using it again is use-after-move, which SPEC-004 §4.8 has always called a compile error and which nothing enforced. To keep using it, either CONSUME AND PUT IT BACK (`set <name> <new value>` re-initialises the place — that is how a handle threads through a loop), or borrow it LOCALLY with `ref h`. ☞ borrowing across an OP BOUNDARY is not lowered yet (E-IR-UNSUP says so at the call site), so `f (ref h)` is not a way out today
두 번 없애도 거절된다.
examples/ch19/twice.low
module twice_drop .
rem expect: E-OWN-MOVED
type buffer u8 .
fn twice input h owned buffer . output u8 .
do
drop h .
drop h .
return 0 .
end
실행 결과
$ lowentc --check twice.low
twice.low:9:0 E-OWN-MOVED: this `owned` value was already MOVED (consumed) — using it again is use-after-move, which SPEC-004 §4.8 has always called a compile error and which nothing enforced. To keep using it, either CONSUME AND PUT IT BACK (`set <name> <new value>` re-initialises the place — that is how a handle threads through a loop), or borrow it LOCALLY with `ref h`. ☞ borrowing across an OP BOUNDARY is not lowered yet (E-IR-UNSUP says so at the call site), so `f (ref h)` is not a way out today
진단은 이것이 명세가 늘 오류라고 불러 온 자리이고 한때는 아무것도 강제하지 않았다고 적는다. 지금은 번역이 막는다.
문. 소유가 없는 값은 넘길 때 어떻게 되는가?
답. 베껴진다. u64 나 point 같은 값은 넘기면 복사되고 원래 이름도 계속 쓸 수 있다. 소유가 있는 값만 옮겨진다. 베끼기의 비용이 걱정되는 큰 값은 ref 로 빌려 넘긴다(12장). 그리고 값을 만드는 식이 놓일 자리가 비어 있고, 도중에 실패하지 않으며, 그 자리가 그 값만의 것이면 값은 목적지에 곧바로 만들어진다. 중간 임시값도, 옮기는 복사도 없다. 이 세 조건은 소스만 보고 셀 수 있다.
19.2 갈래가 만나는 자리#
if 로 갈라졌다가 다시 만나는 자리에서, 소유 상태는 모든 길에서 같아야 한다.
examples/ch19/join.low
module join .
rem expect: E-OWN-JOIN
type buffer u8 .
fn maybe input h owned buffer . input c bool . output u8 .
do
if c . do
drop h .
end
return 0 .
end
실행 결과
$ lowentc --check join.low
join.low:8:0 E-OWN-JOIN: this `owned` value is CONSUMED on one path of this branch but still LIVE on another where they merge — Lowent requires the ownership state to be STATICALLY consistent at a join (RFC-0044 §9.3): no hidden drop-flag decides it at runtime. Consume it on EVERY path, or make it conditionally owned (`?owned`)
c 가 참인 길에서는 h 가 없어졌고 거짓인 길에서는 살아 있다. 두 길이 만난 뒤 h 가 살아 있는지를 아무도 말할 수 없다.
if c
┌─────┴─────┐
drop h (그대로 둔다)
h: 없음 h: 있음
└─────┬─────┘
두 길이 만나는 자리 --- h 는 있나, 없나? → 한 가지로 말할 수 없으니 거절어떤 언어는 이 자리에 숨은 “없앴는지 표시하는 깃발” 을 두지만, Lowent 는 소유 상태가 정적으로 한 가지이기를 요구한다. 두 길 모두에서 없애거나, 두 길 모두에서 넘기면 된다.
같은 원리로, 묶음의 owned 칸 하나를 옮긴 뒤 묶음 전체를 다시 옮기면 거절된다(E-OWN-PARTIAL). 받는 쪽은 온전한 묶음을 받았다고 여기는데 그 안의 한 칸은 이미 남의 것이다.
19.3 해제와 완결#
없애는 일은 두 갈래다.
| 갈래 | 예 | 다루는 법 |
|---|---|---|
| 해제 | 메모리를 돌려준다 | 실패가 없으므로 수명이 끝나는 자리에서 조용히 일어나도 된다 |
| 완결 | 파일을 닫는다, 버퍼를 비운다, 거래를 커밋한다 | 실패할 수 있으므로 저자가 적어서 불러야 한다 |
표 19.1 — 없애는 일의 두 갈래
해제는 삼킬 실패가 없다. 완결은 조용히 일어나면 그 실패를 건네줄 자리가 없다. 기준은 하나다 — 끝내는 일이 실패할 수 있는가.
| 값의 종류 | 넘기면 | 끝나면 |
|---|---|---|
소유가 없는 값(u64 · point …) | 베껴진다. 원래 이름도 계속 쓴다 | 할 일이 없다 |
owned, 해제만 필요 | 옮겨진다. 원래 이름은 빈다 | 수명이 끝나는 자리에서 조용히 해제된다 |
owned, 완결이 필요 | 옮겨진다. 원래 이름은 빈다 | 저자가 완결 op 을 적어서 불러야 한다(아니면 E-OWN-INCOMPLETE) |
표 19.2 — 값이 넘겨질 때와 끝날 때 — 한눈에
어떤 타입이 완결을 요구하는지는 프로그램 자신이 선언한다. 그 타입을 owned 로 받아 result 를 돌려주는 op 이 있으면, 그것이 “이것을 끝내는 일은 실패할 수 있다” 는 선언이다. 새 낱말은 없다.
examples/ch19/complete.low
module complete .
rem run: session 3
type journal u64 .
enum flush_error do
disk_full .
end
fn finish input j owned journal . output result u8 flush_error .
errors disk_full eq j 0 .
do
rem 빈 일지는 쓸 자리가 없었다는 뜻이다 --- 그래서 이 갈래가 실제로 난다
guard ne j 0 . else do
drop j .
return error disk_full .
end
drop j .
return ok 0 .
end
fn session input n u64 . output result u8 flush_error .
errors disk_full .
do
var j owned journal be n .
return finish j .
end
실행 결과
$ lowentc --run session complete.low 3
session(3) = ok 0
finish 가 owned journal 을 받아 result 를 돌려주므로 journal 은 완결이 필요한 타입이 된다. session 은 finish j 를 불러 끝내고, 그 결과(실패할 수도 있는)를 자기 결과로 돌려준다. 완결을 부르지 않고 범위를 벗어나게 두면 거절된다.
examples/ch19/incomplete.low
module incomplete .
rem expect: E-OWN-INCOMPLETE
type journal u64 .
enum flush_error do
disk_full .
end
fn finish input j owned journal . output result u8 flush_error .
errors disk_full .
do
drop j .
return ok 0 .
end
fn forget input j owned journal . output u8 .
do
return 0 .
end
실행 결과
$ lowentc --check incomplete.low
incomplete.low:11:0 W-ERRORS-UNRAISED: this `errors` clause names a failure the body never returns. The clause is read as a promise about what this op can do, and the callers write their handling from it — a branch that can never be taken is dead code the reader cannot tell from live code. Return it (`return error <variant>`), forward one (`try`), or remove the clause
17:0 E-OWN-INCOMPLETE: this value is dropped automatically at the end of scope — but the program itself declares an op that takes this type `owned` BY VALUE and returns a `result`: finishing it CAN FAIL. An automatic drop is a RELEASE (total, non-suspending), and it has nowhere to hand you that failure — it would SWALLOW it. A fallible finish (flush/commit/close) is a COMPLETION and must be EXPLICIT: call it and handle the `result`. If you really mean to discard the value and its failure, say so with `drop`. RFC-0058
진단의 말대로, 자동으로 없애는 것은 해제이고 해제에는 실패를 돌려줄 곳이 없으므로 그 실패를 삼키게 된다. 플러시·커밋·닫기 같은 실패할 수 있는 끝내기는 저자가 적어서 불러야 한다.
흔한 오해. 소멸자(destructor)가 알아서 파일을 닫아 주면 편하다
Drop 은 범위를 벗어날 때 자원을 닫는다. 닫기가 실패하면? 소멸자는 값을 돌려줄 수 없으므로 실패를 무시하거나 프로그램을 멈춘다. 디스크가 가득 차서 마지막 버퍼를 쓰지 못한 사실이 조용히 사라지는 자리다. Lowent 는 이 편의를 해제에만 허락하고, 완결은 적게 한다. 정말로 값과 그 실패를 함께 버리려면 drop 으로 버린다고 말한다 — 진단도 그렇게 안내한다. 조용히 사라지는 것과 저자가 버리기로 적은 것은 다른 일이다.19.4 운영체제가 치워 주기를 기대하지 않는다#
많은 프로그램이 “어차피 프로세스가 끝나면 운영체제가 치운다” 에 기댄다. Lowent 는 그 기대를 하지 않는다. 없애기를 잊은 것을 번역에서 잡으므로, 운영체제가 없는 환경 — 프로세스가 끝나지 않는 펌웨어 — 에서도 같은 코드가 성립한다.
19.5 메모리 안전은 어느 강도로 보장되나#
“메모리 안전” 이라는 말은 무엇이 어떻게 안전한지 밝혀야 뜻이 있다. 이 언어는 강도를 갈라 적는다.
| 규칙 | 강도 | 뜻 |
|---|---|---|
| 차용의 배타 · 참조 탈출 금지 | 정적 + 증명됨 | 번역이 막고, 규칙의 건전성은 Coq 로 증명되었다(순차 모델) |
| 소유의 한 번 없애기 · 영역 탈출 금지 | 정적 | 번역이 막는다 |
| 슬라이스 경계 · 계약 | 동적 | 실행 중 검사하고, 증명되면 검사가 사라진다 |
| 세대 핸들의 늘어진 참조 | 동적 | 실행 중 세대를 비교한다(34장) |
표 19.3 — 메모리 규칙과 그 강도
그러니 이 언어를 “전면 정적 안전” 이라고 부르면 틀린다. 정적으로 막는 것, 실행 중에 막는 것, 증명된 것을 섞은 설계다. 무엇이 증명되었고 증명과 컴파일러 사이에 어떤 틈이 있는지는 42·50장이 다룬다.
19.6 흔한 실수#
반례. 반복 안에서 소유 값을 넘긴다
examples/ch19/mistake_loopmove.low
module mistake_loopmove .
rem expect: E-OWN-MOVED
type buffer u8 .
fn consume input h owned buffer . output u8 .
do
drop h .
return 0 .
end
fn three_times input v u8 . output u8 .
do
var h owned buffer be v .
var i u64 be 0 .
while lt i 3 . do
rem ✘ 첫 바퀴에서 옮겨 간 `h` 를 둘째 바퀴가 또 넘긴다
let a u8 be consume h .
set i (add i 1) .
end
return 0 .
end
실행 결과
$ lowentc --check mistake_loopmove.low
mistake_loopmove.low:16:0 E-OWN-MOVED: this `owned` value is CONSUMED inside a LOOP and never put back — the SECOND iteration would be a use-after-move. A loop body must end the way it began: consume it and REASSIGN the place (`set <name> …`, which re-initialises it), or move the consumption out of the loop
첫 바퀴에서 consume h 가 소유를 가져가면 둘째 바퀴의 h 는 이미 남의 것이다. 번역은 바퀴를 하나씩 따라가지 않고도 “바퀴 몸이 시작할 때와 다른 모양으로 끝난다” 를 보고 E-OWN-MOVED 로 거절한다. 고치는 길은 둘이다. 넘기기를 반복 밖으로 빼거나, 넘긴 자리를 set 으로 새 값으로 다시 채워 바퀴가 같은 모양으로 끝나게 한다.
examples/ch19/loopmove_fixed.low
module loopmove_fixed .
rem run: three_times 5
type buffer u8 .
fn consume input h owned buffer . output u8 .
do
drop h .
return 1 .
end
fn three_times input v u8 . output u8 .
do
var h owned buffer be v .
var n u8 be 0 .
var i u64 be 0 .
while lt i 3 . do
set n (add n (consume h)) .
rem 넘긴 자리를 새 값으로 다시 채운다 --- 바퀴가 시작할 때와 같은 모양으로 끝난다
set h v .
set i (add i 1) .
end
drop h .
return n .
end
실행 결과
$ lowentc --run three_times loopmove_fixed.low 5
three_times(5) = 3
반례. 읽기만 했다고 생각하고 옮긴다
examples/ch19/mistake_readmove.low
module mistake_readmove .
rem expect: E-OWN-MOVED
type buffer u8 .
fn peek input h owned buffer . output u8 .
do
rem ✘ 값을 꺼내 담는 것도 옮기기다 --- 그 뒤의 `drop h` 는 옮긴 값을 없앤다
let v u8 be h .
drop h .
return v .
end
실행 결과
$ lowentc --check mistake_readmove.low
mistake_readmove.low:10:0 E-OWN-MOVED: this `owned` value was already MOVED (consumed) — using it again is use-after-move, which SPEC-004 §4.8 has always called a compile error and which nothing enforced. To keep using it, either CONSUME AND PUT IT BACK (`set <name> <new value>` re-initialises the place — that is how a handle threads through a loop), or borrow it LOCALLY with `ref h`. ☞ borrowing across an OP BOUNDARY is not lowered yet (E-IR-UNSUP says so at the call site), so `f (ref h)` is not a way out today
let v u8 be h . 는 h 를 들여다보는 것이 아니라 v 로 옮기는 것이다. 소유가 있는 값은 이름에 담는 순간 옮겨 가므로 뒤의 drop h 는 옮긴 값을 없애려는 셈이다. 들여다보기만 하려면 같은 op 안에서 ref h 로 빌린다. 진단이 적은 대로 op 경계를 넘는 빌림은 이 판에서 아직 낮춰지지 않는다.
반례. 다른 이름에 담으면 사본이 생긴다고 믿는다
examples/ch19/mistake_twonames.low
module mistake_twonames .
rem expect: E-OWN-MOVED
type buffer u8 .
fn consume input h owned buffer . output u8 .
do
drop h .
return 0 .
end
fn both input h owned buffer . output u8 .
do
rem ✘ 다른 이름에 담으면 사본이 생긴다고 믿었다 --- 소유는 `h2` 로 옮겨 갔다
var h2 owned buffer be h .
let a u8 be consume h2 .
let b u8 be consume h .
return 0 .
end
실행 결과
$ lowentc --check mistake_twonames.low
mistake_twonames.low:17:0 E-OWN-MOVED: this `owned` value was already MOVED (consumed) — using it again is use-after-move, which SPEC-004 §4.8 has always called a compile error and which nothing enforced. To keep using it, either CONSUME AND PUT IT BACK (`set <name> <new value>` re-initialises the place — that is how a handle threads through a loop), or borrow it LOCALLY with `ref h`. ☞ borrowing across an OP BOUNDARY is not lowered yet (E-IR-UNSUP says so at the call site), so `f (ref h)` is not a way out today
u64 같은 값은 다른 이름에 담으면 베껴진다. 소유가 있는 값은 베껴지지 않고 옮겨 간다. 사본이 둘이면 누가 없앨지 정할 수 없고, 둘 다 없애면 두 번 없애기가 되기 때문이다. var h2 owned buffer be h . 뒤로 소유자는 h2 하나다.
흔한 오해. drop 을 적지 않으면 샌다
examples/ch19/implicit_release.low
module implicit_release .
rem run: keep_or_drop 5 1
rem run: keep_or_drop 5 0
type buffer u8 .
rem `c` 가 거짓인 길은 `drop` 없이 떠난다 --- 해제는 실패가 없으므로 수명이 끝나는 자리에서 조용히 일어난다
fn keep_or_drop input v u8 . input c u8 . output u8 .
do
var h owned buffer be v .
guard eq c 1 . else return 0 .
drop h .
return 1 .
end
실행 결과
$ lowentc --run keep_or_drop implicit_release.low 5 1
keep_or_drop(5, 1) = 1
$ lowentc --run keep_or_drop implicit_release.low 5 0
keep_or_drop(5, 0) = 0
c 가 0 인 길은 drop 없이 떠나지만 거절되지 않고 새지도 않는다. 메모리를 돌려주는 해제는 실패할 수 없으므로 수명이 끝나는 자리에서 조용히 일어난다. 저자가 반드시 적어야 하는 것은 실패할 수 있는 완결뿐이다(incomplete.low). 다만 갈래가 다시 만나는 자리에서는 소유 상태가 같아야 한다(join.low). 떠나 버리는 길은 만나지 않으므로 해당하지 않는다.
19.7 이 장의 문법 한눈에#
| 모양 | 뜻 | 왜 이렇게 |
|---|---|---|
input h owned buffer . · var h owned buffer be v . | 소유를 가진 값 | 없앨 책임이 이름 하나에 있다 |
consume h | 넘기면 소유가 옮겨 간다 | 옮긴 뒤에는 쓸 수 없다 — E-OWN-MOVED |
drop h . | 지금 없앤다고 적는다 | 두 번 없애기는 거절된다 |
set h v . (옮긴 뒤) | 옮겨 간 자리를 다시 채운다 | 반복 몸이 같은 모양으로 끝난다 |
if 뒤 갈래마다 다른 소유 상태 | 거절(E-OWN-JOIN) | 숨은 “없앴나” 깃발을 두지 않는다 |
fn finish input j owned journal . output result … | 이 타입의 끝내기는 실패할 수 있다는 선언 | 새 낱말 없이 완결을 선언한다 |
| 완결을 부르지 않고 범위를 떠남 | 거절(E-OWN-INCOMPLETE) | 끝내기의 실패를 삼키지 않는다 |
| 완결이 필요 없는 값을 적지 않고 떠남 | 조용히 해제된다 | 해제는 실패가 없다 |
표 19.4 — 소유의 문법 — 모양 · 뜻 · 왜 이렇게 생겼나
복습 정리
owned t 는 정확히 한 번 없애져야 하고, 넘기면 옮겨진다. 옮긴 값을 다시 쓰거나 두 번 없애면, 그리고 갈래마다 소유 상태가 다르면 거절된다. 없애기는 실패 없는 해제와 실패할 수 있는 완결로 나뉘며, 완결이 필요한 타입은 그것을 owned 로 받아 result 를 돌려주는 op 이 선언한다. 완결이 필요한 값을 자동으로 버리면 거절된다. 메모리 규칙은 정적·동적· 증명됨으로 강도를 갈라 이해한다.