26 Tasks and channels — exchange between bound flows

26.1 Flows are bound to blocks#

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 0 .
  task_group do
    let h1 task u64 spawn square 5 . .
    let h2 task u64 spawn square 6 . .
    let a u64 await h1. . .
    let b u64 await h2. . .
    set r. add a. b. . .
  end .
  return r. .
end .

test join_any_order schedule explore_interleavings .
do
  var r u64 0 .
  task_group do
    var h1 task u64 spawn square 5 . .
    var h2 task u64 spawn square 6 . .
    let a u64 await h1. . .
    let b u64 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 ==

• task_group do … end . binds the flows made inside it into one. Where the block ends, all bound flows end, and none leave with any still running.
• spawn square 5 makes a flow running square 5 and gives that flow’s handle. The handle’s type is task u64 — the type of the value the flow will give (square’s output) is part of the type, and await gives a value of that type.
• await h1. . waits until that flow ends and gives its result. While waiting, other flows progress.

Drawn on a time axis, the lifetimes look like this.

drive       ──┬── task_group do                                   end ──┬──▶ continues
              │                                                         │
flow h1       │   spawn ├─── square 5 runs ─┤ done                      │
flow h2       │       spawn ├─── square 6 runs ───────┤ done            │
              │                     await h1 ▲    await h2 ▲            │
              └─ where the block opened                where it closed ─┘
                  flows live only between these two lines --- none is left when end is passed

A flow cannot outlive the block that made it. So making a flow outside a binding place is rejected.

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
  let h task u64 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>`

A flow made and forgotten survives after the program ends, touches things already gone, or produces failures nobody reads. When a block holds the lifetime, those three vanish by grammar — there is no place to forget.

test join_any_order schedule explore_interleavings in the same file runs every ordering of the two flows and checks that the answers agree. “2 interleavings agree, exhaustive” in the result line says so.

26.1.1 An empty handle — 0#

A handle may start at 0: that is how a place is left empty before it is given a flow. No other number can be a handle — a number does not point at a flow (var h task u64 7 . is refused).

module handle_zero .
rem run: both
rem trap: forgot

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

rem a handle may start empty, at 0 --- wait on it after it is given a flow
proc both output u64 . effects state .
do
  var a task u64 0 .
  var b task u64 0 .
  task_group do
    set a. spawn square 5 . .
    set b. spawn square 6 . .
  end .
  return add await a. . await b. . . .
end .

rem ✘ waits on a handle left empty --- it stops instead of picking another flow
proc forgot output u64 . effects state .
do
  var a task u64 0 .
  var b task u64 0 .
  task_group do
    set b. spawn square 6 . .
  end .
  return await a. . .
end .

$ lowentc --run both handle_zero.low
both() = 61
$ lowentc --run forgot handle_zero.low
== ir diagnostics (1) ==
0:0 E-VM-HANDLE-ZERO: `await` on handle 0 — this `task` was never given a flow (0 is the handle that points at nothing; assign `spawn <op>` to it first)

• both leaves two handles empty at 0, gives them flows inside the block, then waits: 25 plus 36 is 61.
• forgot waits on a without ever giving it a flow. The run stops right there (E-VM-HANDLE-ZERO). A channel (chan T) is the same — putting into or taking from a channel that is 0 stops.

Actors are the same (chapter 25). var s sink 0 . is an actor not spawned yet, and sending it a message with send or spawn send stops. Spawn it first with set s. spawn actor sink . .. No other number goes into an actor place either.

0 plays the part of the null pointer in other languages. Being able to leave a place empty is convenient, but using the empty thing must stop on the spot rather than pick up something else. So the handles spawn and channel give count from 1, and every place that uses a handle checks for 0.

26.2 Channels — containers with an order#

A channel is a container for putting and taking values between flows. Values come out in the order put in, and the number it can hold is fixed.

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 chan u64 . input n u64 . output u64 . effects concurrent .
do
  return chsend ch. n. . .
end .

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

proc drive output u64 . effects state .
do
  var ch chan u64 channel u64 . .
  var s sink 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 chan u64 channel u64 . .
  var s sink 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 ==

• channel u64 makes a channel — its type is chan u64 (the type of the values it holds is part of the type). chsend ch. n. . puts in (n must be a u64) and chrecv ch. . takes out (it gives a u64).
• A flow taking from an empty channel stops, and so does a flow putting into a full one. A stopped flow continues when its counterpart comes.
• Two consumers and two producers are bound in one group. Whatever the ordering, both 10 and 32 go into sink and the result is 42.

“58 interleavings agree, exhaustive” in the test line means all 58 orderings in which the four flows stop and continue were run, and every one answered 42. Concurrency defects usually show only in rare orderings, so tests that run a few times do not catch them. For a small group, running every ordering is the sure way.

Channel operations are the concurrent effect, because their completion depends on another flow’s progress.

module pure_chan .
rem expect: E-EFFECT

proc producer input ch chan 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

A producer written as effects none calls chsend and is rejected for not declaring concurrent and wait. With this effect in the head, the fact that the op cannot be used on a machine without an operating system — which has no executor to run partner flows — shows at translation time.

26.3 Deadlocks you can see from what is written#

A binding place that makes only one flow, where that flow waits for a partner, is rejected.

module alone .
rem expect: E-CONC-ALONE

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

proc lonely output u64 . effects state concurrent .
do
  var ch chan u64 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)

Waiting without a partner cannot end in any ordering. It is reported at translation rather than waiting for a hang.

If every bound flow only receives and none sends, it is rejected too.

module deadlock .
rem expect: E-CONC-DEADLOCK

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

proc stuck output u64 . effects state .
do
  var ch chan u64 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)

26.4 Flows and memory#

Tasks run side by side. So two rules apply when a task uses a root from chapter 18 or an allocator from chapter 20.

First, an op that carves from a root cannot be spawned as a task.

module mistake_taskregion .
rem expect: E-ALLOC-TASK

proc worker input k u64 . output u64 . effects alloc .
do
  var n u64 0 .
  region r arena do
    let g option mut slice u8 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 ✘ spawning, as a task, an op that carves from a root
    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)

Each root has one cursor, and regions are rewound in order. If two tasks open regions in turn, one side’s end rewinds bytes the other side still uses. A lock cannot fix it, because rewinding relies on order, not on locking. So spawning as a task an op whose effects include alloc or heap is refused with E-ALLOC-TASK.

Second, an allocator whose cursor does not move atomically cannot be handed to a task.

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 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 spawn actor allocs.bump_bytes . .
  let z usize send b. init buf. . .
  task_group do
    rem ✘ handing an allocator whose cursor is not moved atomically to two tasks
    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)

Two tasks reserving from the same b race over one cursor. If the allocator’s reserve does not declare atomic, it is E-ALLOC-SHARED. What is refused is the sharing — handing one allocator to two tasks, or handing it to a task and still using it beside them. Spawning a separate allocator for each task works. Another way is to hand over bytes and create the allocator inside the task, which is what follows.

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 the task receives bytes, not an allocator; the allocator is created inside the task
proc user input piece mut slice u8 . output u64 . effects state .
do
  var a allocs.bump_bytes spawn actor allocs.bump_bytes . .
  let room usize send a. init piece. . .
  let g option mut slice u8 send a. reserve 4 . .
  if is_some g. . do
    return cast u64 send a. used . . .
  end .
  return 0 .
end .

proc share input buf mut slice u8 . output u64 . effects state .
do
  rem split the buffer into two pieces that do not overlap and give one to each task
  var r u64 0 .
  task_group do
    let h1 task u64 spawn user subslice buf. 0 8 . . .
    let h2 task u64 spawn user subslice buf. 8 16 . . .
    let a u64 await h1. . .
    let b u64 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 splits the buffer into two pieces that do not overlap and gives one to each task. Each task spawns an allocator on its own piece and uses 4 bytes; adding the two answers gives 8. Because the pieces do not overlap, there is no cursor to race over and no bytes to be rewound.

26.5 What does not exist yet#

Channels without an end (channel … unbounded) are not accepted (E-CHAN-UNBOUNDED). This is decided, not pending — how much memory such a channel uses cannot be read from the source. A bounded channel makes the sender wait when it is full, and that wait is visible in the text.

Lock state shared by several flows (lock, rwlock) is not accepted yet (E-LOCK-NOTYET). One could accept what does not exist and build it later, but then programs written meanwhile would find that what seemed to work does not. It is more honest to say it does not exist. Handling the same memory atomically from several flows is covered in chapter 27.

module lock .
rem expect: E-LOCK-NOTYET

rem ✘ lock state shared between flows; the name is in the canon but it is not accepted yet
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 id u64 .`) or write the underlying type

lock u64 is a type named in the canon, so the tool does not call it “a type that does not exist”. Instead E-LOCK-NOTYET says “not built yet”. Until then, when a count must be shared, use atomic operations (chapter 27) or an actor (chapter 25).

26.6 Common mistakes#

module mistake_crossed .
rem trap: crossed

proc relay input inbox chan u64 . input outbox chan u64 . output u64 . effects concurrent .
do
  let x u64 chrecv inbox. . .
  return chsend outbox. x. . .
end .
proc crossed output u64 . effects state .
do
  var a chan u64 channel u64 . .
  var b chan u64 channel u64 . .
  task_group do
    rem ✘ both start by receiving --- no flow puts in the first value
    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

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 0 .
  task_group do
    rem ✘ the same variable is lent for writing to two flows
    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)

module sharedvar_fixed .
rem run: count2

rem each flow returns its share, and the grouping side combines them after `await`
fn one output u64 .
do
  return 1 .
end .

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

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

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 keeps only the first value received --- the answer depends on arrival order
    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 chan u64 . input n u64 . output u64 . effects concurrent .
do
  return chsend ch. n. . .
end .
proc consumer input ch chan u64 . input s first_seen . output u64 . effects state concurrent .
do
  let x u64 chrecv ch. . .
  let y u64 chrecv ch. . .
  let a u64 send s. put min x. 1000 . . .
  return send s. put min y. 1000 . . .
end .
proc drive output u64 . effects state .
do
  var ch chan u64 channel u64 . .
  var s first_seen 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 chan u64 channel u64 . .
  var s first_seen 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 ==

26.7 This chapter’s syntax at a glance#