12 빌리기 — ref 와 mut_ref

12.1 두 가지 빌림#

참조는 다른 곳에 있는 값을 가리킨다. 두 갈래뿐이고, 이름이 곧 권한이다.

• ref t — 읽기 빌림. 여럿이 동시에 가질 수 있다. 이것으로는 값을 바꿀 수 없다.
• mut_ref t — 쓰기 빌림. 한 값에 대해 한 번에 하나만 있을 수 있고, 그동안 읽기 빌림도 있을 수 없다.

도서관 책에 빗대면 쉽다. 여럿이 한꺼번에 열람(읽기)할 수는 있지만, 책에 고쳐 적으려면(쓰기) 혼자 빌려 가야 하고, 그동안은 아무도 열람하지 못한다. 고치는 동안 누가 읽으면 반쯤 고친 내용을 보게 되기 때문이다.

module borrow .
rem run: use_sum 7
rem run: use_bump 7

struct big do
  a u64 .
  b u64 .
  c u64 .
  d u64 .
end

fn total input v ref big . output u64 .
  requires le (field v a) 1000 .
  requires le (field v b) 1000 .
  requires le (field v c) 1000 .
  requires le (field v d) 1000 .
do
  return add (add (field v a) (field v b)) (add (field v c) (field v d)) .
end

fn use_sum input x u64 . output u64 .
  requires le x 1000 .
do
  let v big be make big do a x . b 2 . c 3 . d 4 . end .
  return add (total (ref v)) (total (ref v)) .
end

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

proc use_bump input start u64 . output u64 .
  requires lt start 1000 .
do
  var n u64 be start .
  let r u64 be bump (mut_ref n) .
  return add n r .
end

$ lowentc --run use_sum borrow.low 7
use_sum(7) = 32
$ lowentc --run use_bump borrow.low 7
use_bump(7) = 16

• total 은 네 칸짜리 big 을 베끼지 않고 ref big 으로 빌려 읽는다. field v a 는 참조를 거쳐 칸을 읽는다.
• use_sum 은 같은 값을 ref v 로 두 번 빌려 넘긴다. 읽기 빌림은 여럿이어도 된다.
• bump 는 mut_ref u64 를 받아 set p … 로 호출자의 값을 바꾼다. 참조가 가리키는 값은 deref p 로 읽는다.
• use_bump 는 var n 을 mut_ref n 으로 빌려준다. bump 가 돌아온 뒤 n 은 8 이다.

빌리는 쪽이 ref x 나 mut_ref n 을 부르는 자리에 적는다는 점이 중요하다. 호출을 읽는 사람은 그 자리만 보고도 이 호출이 n 을 바꿀 수 있다는 것을 안다.

12.2 쓰기 권한은 한 방향으로만 좁아진다#

읽기 빌림으로 쓰려 하면 거절된다.

module ref_write .
rem expect: E-TYPE-REF

proc reset input p ref u64 . output u64 .
do
  set p 0 .
  return 0 .
end

$ lowentc --check ref_write.low
ref_write.low:6:0 E-TYPE-REF: write through a shared ref (declare mut_ref)

반대 방향도 막힌다. 읽기로만 받은 값을 mut·mut_ref·owned 를 받는 자리에 넘기면 E-TYPE-ARGMUT 으로 거절된다. 쓸 수 있는 것을 읽기로 건네는 것은 되지만, 읽기만 되는 것을 쓸 수 있는 자리로 건넬 수는 없다. 어떤 값을 읽기로 받은 쪽은 자기가 보는 동안 그 값이 바뀌지 않는다고 믿을 수 있어야 하고, 그 믿음은 아무도 몰래 쓰기 권한을 얻지 못할 때에만 선다.

12.3 읽기 여럿 또는 쓰기 하나#

같은 값에 대한 빌림이 겹칠 때가 문제다. 쓰기 빌림 둘이 겹치면 거절된다.

module excl .
rem expect: E-EXCL

proc set_both input a mut_ref u64 . input b mut_ref u64 . output void .
do
  set a 1 .
  set b 2 .
end

proc confused output u64 .
do
  var n u64 be 0 .
  set_both (mut_ref n) (mut_ref n) .
  return n .
end

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

set_both 의 본문은 a 와 b 가 서로 다른 값이라고 믿는다. 같은 n 을 두 번 빌려주면 그 믿음이 깨지고, 남는 값이 1 인지 2 인지는 쓰는 차례에 달린다. 읽기와 쓰기가 겹쳐도 거절된다.

module stale .
rem expect: E-EXCL

proc look_then_write output u64 .
do
  var n u64 be 0 .
  let r ref u64 be ref n .
  set n 5 .
  return deref r .
end

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

r 로 n 을 읽기로 빌린 채 n 에 5 를 쓰면, r 을 읽는 쪽은 자기가 본 값이 언제 바뀌었는지 알 수 없다.

같은 값 n 에 대한 빌림을 시간 순으로 늘어놓으면 규칙이 한눈에 보인다.

 시간 →          ①        ②        ③        ④        ⑤
 ref r1 n     ├─────────────────┤                          읽기 둘은 겹쳐도 된다
 ref r2 n              ├─────────────────┤
 mut_ref w n                                   ├────────┤  쓰기는 혼자일 때만
 ──────────────────────────────────────────────────────────────
 ✘ ref r n    ├──────────────────────────┤
   set n 5                   ●                             읽는 동안 값이 바뀐다  → 거절
 ✘ mut_ref a n ├──────────────┤
   mut_ref b n        ├──────────────┤                     쓰기 둘이 겹친다      → 거절

이 두 모양 — 다른 흐름이 동시에 고치는 것, 읽는 중에 값이 바뀌는 것 — 은 소스를 읽어서는 찾기 어려운 결함이라 규칙으로 없앤다.

12.4 빌림은 빌려준 값보다 오래 살 수 없다#

op 안의 지역을 가리키는 참조를 op 밖으로 돌려주면 거절된다.

module escape .
rem expect: E-ESCAPE

fn leak output ref u32 .
do
  let here u32 be 42 .
  return ref here .
end

$ lowentc --check escape.low
7:0 E-ESCAPE: reference to a local escapes the op (dangling)

만약 이 코드가 번역된다면, 돌려받은 참조는 이미 사라진 값을 가리킨다. 그 참조를 읽으면 무슨 값이 나올지 아무도 모른다. Lowent 는 이것을 실행해 보고 아는 것이 아니라 번역할 때 안다. 빌림은 그것을 연 블록 밖으로 나갈 수 없고(E-BORROW-ESCAPE), 빌려준 값이 옮겨졌는데 빌림이 남아 있어도 거절된다(E-EXCL-MOVED).

값을 op 밖으로 내보내야 한다면 참조가 아니라 값을 돌려주거나, 호출자가 넘긴 저장소에 담는다. 호출자보다 오래 사는 저장소가 필요하면 영역을 쓴다(18장).

12.5 mut ref slice 는 없다#

슬라이스에는 mut ref 를 붙이지 않는다.

module mref_slice .
rem expect: E-MREF-SLICE

proc shrink input p mut ref slice u8 . output u64 .
do
  return 0 .
end

$ lowentc --check mref_slice.low
mref_slice.low:4:0 E-MREF-SLICE: `mut ref slice` gives nothing that `mut slice` does not — the elements are already writable through a plain `mut slice` (the descriptor is copied, the bytes are shared). The ONLY thing it adds is replacing the caller's descriptor, which silently changes the length behind the caller's back. Say the new slice with a RETURN VALUE instead (SPEC-004 §4.4a: the windows through which someone else can change your local are listed, and this one is closed)

mut slice 를 넘기면 원소는 이미 쓸 수 있다. 슬라이스 값 {시작, 길이} 는 베껴 가지만 가리키는 바이트는 같기 때문이다. 그러니 mut ref slice 가 더 주는 능력은 하나뿐이다 — 호출자 쪽 슬라이스의 길이와 시작을 몰래 바꾸는 것. 그러면 호출자의 반복문은 자기 코드 어디에도 대입이 없는데 길이가 달라진다. 새 슬라이스는 돌려주면 된다.

module head .
rem run: first_two [9,8,7,6]

fn take_front input p slice u8 . input n u64 . output slice u8 .
  requires le n (len p) .
do
  return subslice p 0 n .
end

fn first_two input xs slice u8 . output u64 .
  requires ge (len xs) 2 .
do
  let front slice u8 be take_front xs 2 .
  return len front .
end

$ lowentc --run first_two head.low [9,8,7,6]
first_two([9,8,7,6]) = 2
  arg0 (written) = [9,8,7,6]

take_front 는 앞쪽 n 개를 가리키는 새 슬라이스를 돌려준다. 길이가 달라졌다는 사실이 반환값과 let front 에 드러난다.

12.6 흔한 실수#

module mistake_nomutref .
rem expect: E-TYPE-ARG

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

proc use_bump input start u64 . output u64 .
  requires lt start 1000 .
do
  var n u64 be start .
  rem ✘ 부르는 자리에 `mut_ref` 를 빠뜨렸다 --- 참조가 아니라 수 7 이 넘어간다
  let r u64 be bump n .
  return add n r .
end

$ lowentc --check mistake_nomutref.low
mistake_nomutref.low:15:0 E-TYPE-ARG: this op takes a BORROW here (`ref` / `mut_ref`), and a plain value was passed. Take the borrow at the call — `mut_ref <name>` — so the reader sees where the callee may write. It used to pass `--check` and stop at run time with `E-VM-TYPE: deref needs a reference`

module mistake_noderef .
rem expect: E-TYPE-REFVAL

fn twice input p ref u64 . output u64 .
do
  rem ✘ `p` 는 수가 아니라 수를 가리키는 참조다 --- `deref p` 로 읽어야 한다
  return add p p .
end

fn double input x u64 . output u64 .
  requires le x 1000 .
do
  let n u64 be x .
  return twice (ref n) .
end

$ lowentc --check mistake_noderef.low
mistake_noderef.low:7:0 E-TYPE-REFVAL: a BORROW is being used where a number is expected. `ref t` / `mut_ref t` names a place, not the value in it — read it with `deref <name>` (and write through it with `set <name> …`). It used to pass `--check` and stop at run time with `E-VM-TYPE`, which blamed the arithmetic instead of the missing read

module mistake_letmutref .
rem expect: E-TYPE-ARGMUT

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

proc use_bump input start u64 . output u64 .
  requires lt start 1000 .
do
  rem ✘ `let` 으로 지은 이름인데 쓰기로 빌려준다
  let n u64 be start .
  bump (mut_ref n) .
  return n .
end

$ lowentc --check mistake_letmutref.low
mistake_letmutref.low:14:0 E-TYPE-ARGMUT: a WRITE borrow (`mut_ref`) was taken of a name that cannot be written: a `let` binding (or a shared input). `let` says the value does not change (§6.5.1) — if a borrow could change it, the reader who checked that name once would be wrong, and the borrow makes the change invisible at the call site. Bind it with `var`, or take a read borrow (`ref`)

module copyparam .
rem run: use_inc 7

proc inc input x u64 . output u64 .
  requires lt x 1000 .
do
  rem `x` 는 호출자가 넘긴 값의 사본이다 --- 여기서 무엇을 해도 호출자의 변수에 닿지 않는다
  var y u64 be x .
  set y (add y 1) .
  return y .
end

proc use_inc input start u64 . output u64 .
  requires lt start 1000 .
do
  var n u64 be start .
  let r u64 be inc n .
  rem `n` 은 그대로 7 이다 --- 바꾸게 하려면 `mut_ref n` 으로 빌려준다
  return n .
end

$ lowentc --run use_inc copyparam.low 7
use_inc(7) = 7

module seqborrow .
rem run: use_twice 7

proc bump input p mut_ref u64 . output void .
  requires lt (deref p) 1000 .
do
  set p (add (deref p) 1) .
end

proc use_twice input start u64 . output u64 .
  requires lt start 900 .
do
  var n u64 be start .
  rem 첫 빌림은 이 호출이 끝날 때 돌아온다 --- 그래서 다음 줄에서 또 빌릴 수 있다
  bump (mut_ref n) .
  bump (mut_ref n) .
  return n .
end

$ lowentc --run use_twice seqborrow.low 7
use_twice(7) = 9

12.7 이 장의 문법 한눈에#