Lowent 매뉴얼←↑→

26 태스크와 채널 — 묶인 흐름끼리 주고받기

먼저 알아야 할 것

15장 효과 · concurrent 는 wait 을 딸고 온다
25장 액터 · 상태를 가두고 메시지를 한 번에 하나씩 처리한다
2장 첫 프로그램 · test 블록은 --test 로 돈다

돌아보기

15장에서 concurrent 와 wait 은 무엇으로 갈렸는가?

답. wait 은 누구의 도움 없이도 언젠가 깨어나는 기다림(커널·장치가 깨운다)이고, concurrent 는 같은 프로그램의 다른 흐름이 진행해야 끝나는 기다림이다. 그래서 concurrent 를 적으면 wait 을 함께 적은 것이 된다. 이 장은 그 “다른 흐름” 을 만들고, 흐름끼리 값을 주고받는 법을 다룬다.

이 장의 필요성과 맥락

액터(25장)는 상태를 가두는 모양이었다. 그러나 일을 여러 흐름에 나누고 결과를 모으거나, 생산자와 소비자가 값을 넘겨받는 모양은 액터만으로 적기 번거롭다. 흐름을 다루는 흔한 결함은 셋이다 — 만들어 놓고 잊은 흐름, 짝이 없어 영원히 기다리는 흐름, 서로를 기다리는 교착. Lowent 는 흐름의 수명을 블록에 묶어 첫째를 문법으로 없애고, 둘째와 셋째 가운데 적힌 것만 봐도 알 수 있는 경우를 번역에서 거절한다. 그리고 여러 흐름의 모든 차례를 시험하는 도구를 준다.

이 장이 끝나면

task_group 안에서 spawn <op> 으로 흐름을 만들고 await 로 결과를 받는 법을 익힌다. 흐름이 자기를 만든 블록보다 오래 살지 못한다는 규칙을 알게 된다. channel·chsend·chrecv 로 값을 주고받고, 채널 연산이 concurrent 효과인 까닭을 이해한다. 짝 없는 기다림과 보내는 쪽이 없는 교착이 번역에서 거절되는 모습, 그리고 schedule explore_interleavings 시험이 가능한 모든 차례를 돌려 보는 모습을 보게 된다.

이 장에서 답할 질문

  1. task_group cancel_on_error 는 무엇을 하는가?

26.1 흐름은 블록에 묶인다#

examples/ch26/await.low

module awaiting .
rem run: drive
rem test

fn square input n u64 . output u64 .
  requires le n 1000 .
do
  return mul n n .
end

proc drive output u64 . effects state .
do
  var r u64 be 0 .
  task_group do
    var h1 u64 be spawn square 5 .
    var h2 u64 be spawn square 6 .
    let a u64 be await h1 .
    let b u64 be await h2 .
    set r (add a b) .
  end
  return r .
end

test join_any_order schedule explore_interleavings .
do
  var r u64 be 0 .
  task_group do
    var h1 u64 be spawn square 5 .
    var h2 u64 be spawn square 6 .
    let a u64 be await h1 .
    let b u64 be await h2 .
    set r (add a b) .
  end
  expect eq r 61 .
end

실행 결과

$ lowentc --run drive await.low
drive() = 61
$ lowentc --test await.low
  [PASS] join_any_order  (schedule: 2 interleavings agree, exhaustive)
== tests: 1 run, 1 passed, 0 FAILED ==

흐름의 수명을 시간 축에 그리면 이렇다.

drive       ──┬── task_group do                                   end ──┬──▶ 계속
              │                                                         │
흐름 h1       │   spawn ├─── square 5 돈다 ─┤ 끝                        │
흐름 h2       │       spawn ├─── square 6 돈다 ───────┤ 끝              │
              │                     await h1 ▲    await h2 ▲            │
              └─ 블록이 열린 자리                     블록이 닫힌 자리 ─┘
                  흐름은 이 두 선 안에서만 산다 --- end 를 지날 때 남은 흐름은 없다

흐름은 자기를 만든 블록보다 오래 살지 못한다. 그래서 묶는 자리 밖에서 흐름을 만들면 거절된다.

examples/ch26/scope.low

module scope .
rem expect: E-SPAWN-SCOPE

fn square input n u64 . output u64 .
  requires le n 1000 .
do
  return mul n n .
end

proc loose output u64 . effects state .
do
  var h u64 be spawn square 5 .
  return await h .
end

실행 결과

$ lowentc --check scope.low
scope.low:12:0 E-SPAWN-SCOPE: spawning a task (`spawn <op>`) is only allowed inside a `task_group` (RFC-0009 D3-b SC1: no task may outlive its group). Wrap it in `task_group do … end`, or if you meant an actor instance write `spawn actor <T>`

흐름을 만들어 놓고 잊으면 그것은 프로그램이 끝난 뒤에도 남거나, 이미 없어진 것을 만지거나, 아무도 읽지 않는 실패를 낸다. 블록이 수명을 쥐면 그 셋이 문법으로 사라진다 — 잊을 자리가 없기 때문이다.

같은 파일의 test join_any_order schedule explore_interleavings 는 두 흐름이 도는 모든 차례를 돌려 보고 답이 같은지 확인한다. 결과 줄의 “2 interleavings agree, exhaustive” 가 그것이다.

문. task_group cancel_on_error 는 무엇을 하는가?

답. 묶인 흐름 하나가 오류로 끝나면, 아직 시작하지 않았거나 기다리는 형제들을 그 오류로 끝난 것으로 처리한다. 다만 취소는 되감지 않는다. 이미 일을 낸 흐름의 효과는 되돌아가지 않고, 앞으로 할 일을 하지 않게 할 뿐이다. 어느 형제가 취소되었는지는 차례에 달려 있고, 명세는 그 차례를 정하지 않는다. 오류 자체는 await 로 드러난다.

26.2 채널 — 차례 있는 그릇#

채널은 흐름 사이에 값을 넣고 빼는 그릇이다. 넣은 차례대로 나오고, 담을 수 있는 수가 정해져 있다.

examples/ch26/chan.low

module chan .
rem run: drive
rem test

actor sink do
  state do
    v u64 .
  end
  proc put input n u64 . output u64 . effects state .
    requires le n 1000 .
  do
    set v (wrap_add v n) .
    return v .
  end
  fn get output u64 .
  do
    return v .
  end
end

proc producer input ch u64 . input n u64 . output u64 . effects concurrent .
do
  return chsend ch n .
end

proc consumer input ch u64 . input s sink . output u64 . effects state concurrent .
do
  let x u64 be chrecv ch .
  return send s put (min x 1000) .
end

proc drive output u64 . effects state .
do
  var ch u64 be channel u64 .
  var s sink be spawn actor sink .
  task_group do
    spawn consumer ch s .
    spawn consumer ch s .
    spawn producer ch 10 .
    spawn producer ch 32 .
  end
  return send s get .
end

test every_interleaving schedule explore_interleavings .
do
  var ch u64 be channel u64 .
  var s sink be spawn actor sink .
  task_group do
    spawn consumer ch s .
    spawn consumer ch s .
    spawn producer ch 10 .
    spawn producer ch 32 .
  end
  expect eq (send s get) 42 .
end

실행 결과

$ lowentc --run drive chan.low
drive() = 42
$ lowentc --test chan.low
  [PASS] every_interleaving  (schedule: 58 interleavings agree, exhaustive)
== tests: 1 run, 1 passed, 0 FAILED ==

시험 줄의 “58 interleavings agree, exhaustive” 는 네 흐름이 멈추고 이어 가는 차례 58 가지를 모두 돌려 보았고 답이 모두 42 였다는 뜻이다. 동시성 결함은 대개 드문 차례에서만 드러나서 몇 번 돌려 보는 시험으로는 잡히지 않는다. 작은 그룹이라면 모든 차례를 도는 편이 확실하다.

채널 연산은 concurrent 효과다. 완결이 다른 흐름의 진행에 달려 있기 때문이다.

examples/ch26/pure_chan.low

module pure_chan .
rem expect: E-EFFECT

proc producer input ch u64 . output u64 . effects none .
do
  return chsend ch 1 .
end

실행 결과

$ lowentc --check pure_chan.low
pure_chan.low:5:1 E-EFFECT: this op performs `concurrent`, `wait`, which its `effects` clause does not declare — add it to `effects …`, or stop calling what needs it

effects none 으로 적은 생산자가 chsend 를 부르자 concurrent·wait 을 선언하지 않았다고 거절된다. 이 효과가 머리에 있으면, 운영체제가 없어 동료 흐름을 돌려 줄 실행기가 없는 기계에서 이 op 을 쓸 수 없다는 것이 번역할 때 드러난다.

26.3 적힌 것만 봐도 아는 교착#

묶는 자리가 흐름을 하나만 만들고 그 흐름이 짝을 기다리면 거절된다.

examples/ch26/alone.low

module alone .
rem expect: E-CONC-ALONE

proc consumer input ch u64 . output u64 . effects concurrent .
do
  return chrecv ch .
end

proc lonely output u64 . effects state concurrent .
do
  var ch u64 be channel u64 .
  task_group do
    spawn consumer ch .
  end
  return 0 .
end

실행 결과

$ lowentc --check alone.low
alone.low:12:0 E-CONC-ALONE: this `task_group` spawns exactly ONE task, and that task needs a PEER to finish (`concurrent` — a `chrecv` on an empty channel, or a `chsend` on a full one). There is no peer: the parent is waiting on the group. This is not "might be slow" — NO interleaving completes, so it is a provable deadlock, and the compiler can see it here instead of letting it die at runtime. Spawn the other side in the same group, or use `wait` I/O, which the KERNEL wakes and which needs no peer (RFC-0022 D-A)

짝이 없는 기다림은 어떤 차례로도 끝나지 않는다. 돌려 보고 매달리기를 기다리지 않고 번역할 때 말한다.

묶인 흐름들이 모두 받기만 하고 아무도 보내지 않아도 거절된다.

examples/ch26/deadlock.low

module deadlock .
rem expect: E-CONC-DEADLOCK

proc consumer input ch u64 . output u64 . effects concurrent .
do
  return chrecv ch .
end

proc stuck output u64 . effects state .
do
  var ch u64 be channel u64 .
  task_group do
    spawn consumer ch .
    spawn consumer ch .
  end
  return 0 .
end

실행 결과

$ lowentc --check deadlock.low
deadlock.low:12:0 E-CONC-DEADLOCK: this `task_group`'s tasks wait to RECEIVE (`chrecv`) but NOTHING sends. There is no `chsend` anywhere in this self-contained module (no `use` imports), and the channels are created locally — the enclosing op takes no parameters, so no caller can feed them either. Every task blocks on an empty channel while the parent waits on the group: NO interleaving completes, so it is a PROVABLE deadlock the compiler names here instead of letting it die at runtime (E-VM-DEADLOCK). Add a producer (`chsend`), or a task that sends, in the same group (RFC-0022 D-A — the multi-member sibling of E-CONC-ALONE)

흔한 오해. 교착 검사가 있으니 이 언어에서는 교착이 일어나지 않는다

이 검사는 적힌 것만 봐도 아는 교착만 잡는다. 두 흐름이 서로 다른 채널을 엇갈려 기다리는 교착, 조건에 따라서만 생기는 교착은 번역이 잡지 못한다. 그런 교착은 실행 중에 모든 흐름이 멈추면 처리기가 E-VM-DEADLOCK 으로 말하고, 작은 경우는 explore_interleavings 시험이 모든 차례를 돌며 찾아낸다. 잡지 못하는 교착이 있다는 사실은 이 규칙이 무엇을 약속하는지 분명히 하는 것이다.

26.4 흐름과 메모리#

태스크는 서로 곁에서 돈다. 그래서 18장의 뿌리와 20장의 할당기를 태스크에서 쓸 때는 규칙이 둘 붙는다.

첫째, 뿌리에서 깎는 op 을 태스크로 띄울 수 없다.

examples/ch26/mistake_taskregion.low

module mistake_taskregion .
rem expect: E-ALLOC-TASK

proc worker input k u64 . output u64 . effects alloc .
do
  var n u64 be 0 .
  region r arena do
    let g option mut slice u8 . . be alloc_bytes r capacity 1000 .
    if is_some g . do
      set n k .
    end
  end
  return n .
end

proc two_workers input al cap allocator . output u64 . effects alloc state .
do
  task_group do
    rem ✘ 뿌리에서 깎는 op 을 태스크로 띄운다
    spawn worker 1 .
    spawn worker 2 .
  end
  return 0 .
end

실행 결과

$ lowentc --check mistake_taskregion.low
20:0 E-ALLOC-TASK: this spawns a TASK whose op takes memory from a ROOT (its effects include `alloc` or `heap`). A root has one cursor, and regions rewind it in order — two tasks interleaving would rewind each other's bytes (measured on the VM's green threads: `region reset needs its own mark`; native tasks are real threads). Give the task an allocator over borrowed bytes instead (RFC-0112 D11)
21:0 E-ALLOC-TASK: this spawns a TASK whose op takes memory from a ROOT (its effects include `alloc` or `heap`). A root has one cursor, and regions rewind it in order — two tasks interleaving would rewind each other's bytes (measured on the VM's green threads: `region reset needs its own mark`; native tasks are real threads). Give the task an allocator over borrowed bytes instead (RFC-0112 D11)

뿌리마다 커서는 하나이고, 영역은 차례대로 되감긴다. 두 태스크가 영역을 번갈아 열면 한쪽의 end 가 다른 쪽이 아직 쓰는 바이트를 되감는다. 자물쇠로도 고칠 수 없다. 되감기가 기대는 것은 잠금이 아니라 차례이기 때문이다. 그래서 효과에 alloc·heap 이 있는 op 을 태스크로 띄우면 E-ALLOC-TASK 로 거절한다.

둘째, 커서를 원자적으로 옮기지 않는 할당기를 태스크에 건넬 수 없다.

examples/ch26/mistake_taskshared.low

module mistake_taskshared .
rem expect: E-ALLOC-SHARED

use allocs .

proc user input a allocs.bump_bytes . output u64 . effects state .
do
  let g option mut slice u8 . . be send a reserve 4 .
  if is_some g . do
    return 1 .
  end
  return 0 .
end

proc share input buf mut slice u8 . output u64 . effects state .
do
  var b allocs.bump_bytes be spawn actor allocs.bump_bytes .
  let z u64 be send b init buf .
  task_group do
    rem ✘ 커서를 원자적으로 옮기지 않는 할당기를 두 태스크에 건넨다
    spawn user b .
    spawn user b .
  end
  return 0 .
end

실행 결과

$ lowentc --check mistake_taskshared.low
21:0 E-ALLOC-SHARED: the same ALLOCATOR is in play in two places at once here, and its `reserve` does not move its cursor atomically (no `atomic` effect): it is handed to more than one task, or handed to a task and still used beside it. Two of them reserving race on one cursor. Give each task its OWN allocator over its own bytes — two `spawn actor` instances, each `init`ed on a disjoint slice — or use one whose `reserve` is atomic (RFC-0112 D11)

두 태스크가 같은 b 에서 reserve 하면 커서 하나를 두고 경합한다. 할당기의 reserve 가 atomic 을 적지 않았으면 E-ALLOC-SHARED 다. 무는 것은 나눠 쓰는 것이다 — 같은 할당기를 태스크 둘에 건네거나, 태스크에 건넨 채 곁에서 또 쓰는 것. 따로 띄운 할당기를 태스크 마다 하나씩 주는 것은 통한다. 또 하나의 길은 바이트를 넘기고 할당기는 태스크 안에서 만드는 것이며, 아래가 그것이다.

examples/ch26/taskshared_fixed.low

module taskshared_fixed .
rem run: share [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]

use allocs .

rem 태스크가 받는 것은 할당기가 아니라 바이트다. 할당기는 태스크 안에서 만든다
proc user input piece mut slice u8 . . output u64 . effects state .
do
  var a allocs.bump_bytes be spawn actor allocs.bump_bytes .
  let room u64 be send a init piece .
  let g option mut slice u8 . . be send a reserve 4 .
  if is_some g . do
    return send a used .
  end
  return 0 .
end

proc share input buf mut slice u8 . output u64 . effects state .
do
  rem 버퍼를 겹치지 않는 두 조각으로 나눠 태스크마다 하나씩 준다
  var r u64 be 0 .
  task_group do
    var h1 u64 be spawn user (subslice buf 0 8) .
    var h2 u64 be spawn user (subslice buf 8 16) .
    let a u64 be await h1 .
    let b u64 be await h2 .
    set r (add a b) .
  end
  return r .
end

실행 결과

$ lowentc --run share taskshared_fixed.low [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
share([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]) = 8
  arg0 (written) = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]

share 는 버퍼를 겹치지 않는 두 조각으로 나눠 태스크마다 하나씩 준다. 각 태스크는 자기 조각 위에 할당기를 띄워 4 바이트를 쓰고, 두 답을 더하면 8 이다. 조각이 겹치지 않으니 경합할 커서도, 되감길 바이트도 없다.

26.5 아직 없는 것#

끝이 없는 채널(channel … unbounded)과 여러 흐름이 나누어 가지는 자물쇠 상태(lock·rwlock)는 아직 받아들이지 않는다 (E-CHAN-UNBOUNDED·E-LOCK-NOTYET). 없는 것을 받아들이고 나중에 짓는 길도 있지만, 그러면 그 사이에 쓴 프로그램이 되는 줄 알았다가 안 되는 것을 겪는다. 없으면 없다고 말하는 편이 정직하다. 여러 흐름이 같은 메모리를 원자적으로 다루는 길은 27장이 다룬다.

examples/ch26/lock.low

module lock .
rem expect: E-LOCK-NOTYET

rem ✘ 흐름끼리 나누는 자물쇠 상태 — 이름은 정본에 있지만 아직 받지 않는다
fn read_count input c lock u64 . output u64 . do
  return 0 .
end

실행 결과

$ lowentc --check lock.low
lock.low:5:0 E-LOCK-NOTYET: `lock t` / `rwlock t` / `shared_read t` are level-3 shared-state types that SPEC-008 §74 names but this compiler DOES NOT IMPLEMENT: no lock is taken, no release happens. Writing one tells every reader the state is lock-protected while NOTHING checks that — an unchecked safety claim is the lie PRINCIPLES.md §0 is about. ★ And today there is nothing for a lock to protect against: execution is cooperative on ONE OS thread and actor delivery is SEQUENTIAL, so such a lock could never even be exercised. This is refused for the same reason as `mailbox unbounded` and `bounded 0`. Use an `actor` (sequential delivery IS the mutual exclusion) or the `atomic_*` ops, whose memory ordering IS real (RFC-0018 §6.1). These types come back when real OS threads do
lock.low:5:0 W-NOT-YET: this type NAME is accepted but carries NO MEANING yet: lowering cannot read it, so every op in its signature falls to the interpreter (~80x). The answer stays right, so no oracle will ever see this. Declare it (`type str slice u8 .`) or write the underlying type

lock u64 은 정본에 이름이 있는 타입이라 “없는 타입” 이라고 말하지 않는다. 대신 E-LOCK-NOTYET 으로 “아직 짓지 않았다” 고 말한다. 그 사이에 나누어 쓸 수가 필요하면 원자 연산(27장)이나 액터(25장)를 쓴다.

26.6 흔한 실수#

반례. 두 흐름이 서로에게서 받기부터 한다

examples/ch26/mistake_crossed.low

module mistake_crossed .
rem trap: crossed

proc relay input inbox u64 . input outbox u64 . output u64 . effects concurrent .
do
  let x u64 be chrecv inbox .
  return chsend outbox x .
end
proc crossed output u64 . effects state .
do
  var a u64 be channel u64 .
  var b u64 be channel u64 .
  task_group do
    rem ✘ 둘 다 받기부터 한다 --- 첫 값을 넣어 줄 흐름이 없다
    spawn relay a b .
    spawn relay b a .
  end
  return 0 .
end

실행 결과

$ lowentc --run crossed mistake_crossed.low
== ir diagnostics (1) ==
0:0 E-VM-DEADLOCK: the scheduler is stuck — every remaining task is blocked on a channel (a `chrecv` on an empty channel or `chsend` on a full one) and none can wake another. This is a real deadlock, not a tool limit: no interleaving completes

relay a b 는 a 에서 받아 b 로 넘기고, relay b a 는 그 반대다. 둘 다 받기부터 하므로 누구도 첫 값을 넣지 못한다. 흐름이 둘이고 채널이 엇갈려서, 적힌 것만 봐서는 교착인지 알 수 없으므로 번역은 통과한다. 실행하면 모든 흐름이 멈춘 것을 처리기가 보고 E-VM-DEADLOCK 으로 알린다. 엇갈린 기다림을 만들지 않으려면 흐름마다 “누가 먼저 보내는가” 를 정해 두고, 가능하면 값이 한 방향으로만 흐르게 짠다.

반례. 두 흐름에 같은 변수를 쓰기로 빌려준다

examples/ch26/mistake_sharedvar.low

module mistake_sharedvar .
rem expect: E-EXCL

proc bump input p mut_ref u64 . output void . effects state .
do
  set p (add (deref p) 1) .
end
proc race output u64 . effects state .
do
  var n u64 be 0 .
  task_group do
    rem ✘ 두 흐름에 같은 변수를 쓰기로 빌려준다
    spawn bump (mut_ref n) .
    spawn bump (mut_ref n) .
  end
  return n .
end

실행 결과

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

두 흐름이 같은 n 을 동시에 올리면 데이터 경합이다. 쓰기 빌림은 하나여야 한다는 규칙(12장)이 흐름 사이에서도 그대로라서 E-EXCL 로 거절된다. 첫 줄의 W-EFFECT-OVER 는 이 장의 주제와 상관없는 이 판의 결함이다(mut_ref 로 쓰는 것을 state 로 세지 않는다). 흐름은 자기 몫을 돌려주고, 합치는 일은 묶는 쪽이 await 뒤에 한다.

examples/ch26/sharedvar_fixed.low

module sharedvar_fixed .
rem run: count2

rem 흐름은 자기 몫을 돌려주고, 합치는 일은 묶는 쪽이 `await` 뒤에 한다
fn one output u64 .
do
  return 1 .
end

proc count2 output u64 . effects state .
do
  var n u64 be 0 .
  task_group do
    var h1 u64 be spawn one .
    var h2 u64 be spawn one .
    let a u64 be await h1 .
    let b u64 be await h2 .
    set n (add a b) .
  end
  return n .
end

실행 결과

$ lowentc --run count2 sharedvar_fixed.low
count2() = 2

흔한 오해. 한 번 돌려서 맞으면 동시성 코드도 맞다

examples/ch26/order_dependent.low

module order_dependent .
rem run: drive
rem test-fail

actor first_seen do
  state do
    v u64 .
  end
  proc put input n u64 . output u64 . effects state .
    requires le n 1000 .
  do
    rem 처음 받은 값만 남긴다 --- 답이 도착 차례에 달린다
    if eq v 0 . do set v n . end
    return v .
  end
  fn get output u64 .
  do
    return v .
  end
end
proc producer input ch u64 . input n u64 . output u64 . effects concurrent .
do
  return chsend ch n .
end
proc consumer input ch u64 . input s first_seen . output u64 . effects state concurrent .
do
  let x u64 be chrecv ch .
  let y u64 be chrecv ch .
  let a u64 be send s put (min x 1000) .
  return send s put (min y 1000) .
end
proc drive output u64 . effects state .
do
  var ch u64 be channel u64 .
  var s first_seen be spawn actor first_seen .
  task_group do
    spawn consumer ch s .
    spawn producer ch 10 .
    spawn producer ch 32 .
  end
  return send s get .
end
test first_is_ten schedule explore_interleavings .
do
  var ch u64 be channel u64 .
  var s first_seen be spawn actor first_seen .
  task_group do
    spawn consumer ch s .
    spawn producer ch 10 .
    spawn producer ch 32 .
  end
  expect eq (send s get) 10 .
end

실행 결과

$ lowentc --run drive order_dependent.low
drive() = 32
$ lowentc --test order_dependent.low
  [FAIL] first_is_ten
         E-SCHED-NONDET: this test PASSES under some message-delivery orders and FAILS under others (diverged at interleaving 1 of 8 explored) — its result DEPENDS on the order the scheduler delivers messages. A deterministic actor program must give the SAME result under EVERY interleaving (RFC-0009 D6 — the actor analogue of a data race). Fix the handler so order does not matter, or serialize with `drain`
== tests: 1 run, 0 passed, 1 FAILED ==

first_seen 은 처음 받은 값만 남긴다. drive 를 돌리면 32 가 나오고, 다른 차례라면 10 이 나온다. 한 번 돌려 본 결과는 그 한 차례의 답일 뿐이다. schedule explore_interleavings 시험은 여덟 가지 차례를 모두 돌려 보고, 답이 차례에 따라 갈린다는 것을 E-SCHED-NONDET 으로 알린다. 결정적인 프로그램은 모든 차례에서 같은 답을 내야 한다. 받은 값을 모두 더하는 chan.low 의 sink 처럼, 차례가 달라도 결과가 같도록 처리기를 짠다.

26.7 이 장의 문법 한눈에#

모양뜻왜 이렇게
task_group do … end흐름들을 블록에 묶는다 — 끝에서 모두 끝난다만들어 놓고 잊은 흐름이 문법으로 사라진다
var h1 u64 be spawn square 5 .흐름을 만들고 핸들을 받는다묶는 자리 밖이면 E-SPAWN-SCOPE
await h1그 흐름의 결과를 기다려 받는다기다리는 동안 다른 흐름이 나아간다
task_group cancel_on_error do … end오류 하나에 형제를 취소한다취소는 되감지 않는다
var ch u64 be channel u64 .크기가 정해진 차례 있는 그릇끝없는 채널은 아직 없다 — E-CHAN-UNBOUNDED
chsend ch n · chrecv ch넣기 · 빼기 — 차거나 비면 멈춘다concurrent 효과 — 완결이 남에게 달렸다
짝 없는 기다림 · 보내는 쪽 없는 받기번역에서 거절(E-CONC-ALONE · E-CONC-DEADLOCK)적힌 것만 봐도 아는 교착
test … schedule explore_interleavings . do … end가능한 모든 차례를 돌려 답을 맞댄다드문 차례의 결함을 시험이 찾는다
태스크 op 의 효과에 alloc·heapE-ALLOC-TASK뿌리의 되감기는 차례에 기댄다 — 잠금으로 못 지킨다
원자적이지 않은 할당기를 spawn 인자로E-ALLOC-SHARED바이트 조각을 넘기고 할당기는 태스크 안에서 만든다
lock t · rwlock t · shared_read tE-LOCK-NOTYET이름은 정본에 있다 — 짓지 않은 것을 받아 주지 않는다

표 26.1 — 태스크와 채널의 문법 — 모양 · 뜻 · 왜 이렇게 생겼나

복습 정리

task_group 안에서 spawn <op> 은 흐름을 만들고 핸들을 주며, await 가 결과를 받는다. 흐름은 자기를 만든 블록보다 오래 살지 못하므로 묶는 자리 밖의 spawn 은 거절된다. channel·chsend·chrecv 는 크기가 정해진 차례 있는 그릇이고 채널 연산은 concurrent 효과다. 짝 없는 기다림과 보내는 쪽이 없는 교착은 번역에서 거절되고, schedule explore_interleavings 시험은 모든 차례를 돌려 답을 맞댄다.