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 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 ==

• 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.
• 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
  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>`

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.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 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 ==

• channel u64 makes a channel. chsend ch n puts in and chrecv ch takes out.
• 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 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 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)

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 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)

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 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 ✘ 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 . . 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 ✘ 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 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 split the buffer into two pieces that do not overlap and give one to each task
  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 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) and lock state shared by several flows (lock, rwlock) are not accepted yet (E-CHAN-UNBOUNDED, 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 str slice u8 .`) 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 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 ✘ 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 be 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 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

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 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 ==

26.7 This chapter’s syntax at a glance#