27 Parallel loops and atomic operations

27.1 Declaring that a loop may be split#

module split .
rem run: double_all [1,2,3,4,5,6]
rem run: total [1,2,3,4,5,6]

proc double_all input s mut slice u8 . output u64 . effects none .
  parallel s split .
do
  var i u64 be 0 .
  while lt i (len s) . do
    set (index s i) (wrap_mul (index s i) 2) .
    set i (add i 1) .
  end
  return len s .
end

fn total input s slice u8 . output u64 .
  parallel s split .
  reduce acc add .
do
  var acc u64 be 0 .
  var i u64 be 0 .
  while lt i (len s) . do
    set acc (add acc (widen u64 (index s i))) .
    set i (add i 1) .
  end
  return acc .
end

$ lowentc --run double_all split.low [1,2,3,4,5,6]
double_all([2,4,6,8,10,12]) = 6
  arg0 (written) = [2,4,6,8,10,12]
$ lowentc --run total split.low [1,2,3,4,5,6]
total([1,2,3,4,5,6]) = 21
  arg0 (written) = [1,2,3,4,5,6]

• double_all’s head has parallel s split . — a declaration that “this loop may be split into pieces of s run by several together”. Each step reads and writes only index s i, its own element.
• total accumulates a sum. The accumulator acc lives across steps, so as is it cannot be split. reduce acc add . states “accumulate per piece, then combine with add”.

In pictures, this is what the two declarations allow.

 split --- each piece touches only its own share
   s:  [ 0 1 2 3 | 4 5 6 7 | 8 9 10 11 ]
         piece A    piece B    piece C        ← all three may run at once without touching each other

 reduce acc add --- gather per piece, then combine
   piece A: acc_A = 0+1+2+3      = 6  ─┐
   piece B: acc_B = 4+5+6+7      = 22 ─┼─ add ─▶ acc = 66
   piece C: acc_C = 8+9+10+11    = 38 ─┘

add gives the same answer however it is grouped (it is associative), so any split matches the sequential result. Floating-point addition is not, so it cannot be split with reduce (see “The combining operation must be associative” below).

When the processor confirms such a declaration, it reports W-PAR-OK, and that note contains something important: the VM still runs sequentially. That is a correct implementation because a theorem is proven that, under the splittable conditions, the parallel result is bit-for-bit identical to the sequential result (chapter 45). Native code really does split into pieces and run them on several threads. The two back ends agreeing is a measurement of that theorem.

27.2 The three conditions the processor checks#

module par_read .
rem expect: E-PAR-READ

proc relative input s mut slice u8 . output u64 . effects none .
  parallel s split .
do
  var i u64 be 0 .
  while lt i (len s) . do
    set (index s i) (wrap_sub (index s i) (index s 0)) .
    set i (add i 1) .
  end
  return len s .
end

$ lowentc --check par_read.low
par_read.low:9:0 E-PAR-READ: a splittable loop may only read its OWN element of the split slice — reading another index creates a cross-iteration dependence (Bernstein: rd ∩ wr = ∅)

This loop subtracts the first element from every element. If the first piece changes index s 0 first, the first element other pieces read has already changed. Even run sequentially, the loop has the defect of subtracting 0 after the first step, and splitting makes that defect depend on ordering.

module par_carry .
rem expect: E-PAR-CARRY

fn total input s slice u8 . output u64 .
  parallel s split .
do
  var acc u64 be 0 .
  var i u64 be 0 .
  while lt i (len s) . do
    set acc (add acc (widen u64 (index s i))) .
    set i (add i 1) .
  end
  return acc .
end

$ lowentc --check par_carry.low
par_carry.low:10:0 E-PAR-CARRY: a splittable loop may not write a local that lives across iterations (a loop-carried dependence) — declare it: `reduce <acc> <op> .`

It accumulated into acc without reduce. The diagnostic says exactly how to fix it.

27.3 The combining operation must be associative#

When gathering with reduce, the shape of the tree that combines pieces changes depending on how they were split. If the operation is associative, the shape does not change the answer; if not, it does.

module par_assoc .
rem expect: E-PAR-ASSOC

fn diff input s slice u8 . output u64 .
  parallel s split .
  reduce acc sub .
do
  var acc u64 be 1000 .
  var i u64 be 0 .
  while lt i (len s) . do
    set acc (sub acc (widen u64 (index s i))) .
    set i (add i 1) .
  end
  return acc .
end

$ lowentc --check par_assoc.low
par_assoc.low:4:0 E-PAR-ASSOC: this reduction operator is not associative, so the shape of the reduction tree changes the result — a split tree is not deterministic (★ nonassoc_shape_matters, Qed — docs/proofs/coq/LowentPar.v)
par_assoc.low:4:0 W-PAR-OK: this loop satisfies the Bernstein conditions and may be split (DET-1 proves the parallel result is bit-identical to the sequential one — docs/proofs/coq/LowentPar.v). Execution is still sequential, which is a VALID implementation precisely because of that theorem

sub is not associative: (1000 − 1) − 2 and 1000 − (1 − 2) differ. Both propositions — associative means the shape does not matter, non-associative means the shape changes the result — are proven in Coq, and the diagnostic cites the theorem’s name. Floating-point addition also depends on order, so it is blocked separately (E-PAR-FLOAT).

27.4 Atomic operations#

Sometimes split pieces must update one place together, such as adding counts from each piece into a shared counter. With plain add, two threads read the same value, add separately and write, and one addition is lost. An atomic operation is indivisible — other flows cannot see its middle.

module atomic_counter .
rem run: main

proc count_par input k cap atomic . input data slice u8 . input counter mut slice u64 .
  output void .
  effects atomic .
  parallel data split .
do
  var i u64 be 0 .
  while lt i (len data) . do
    atomic_add counter 0 1 .
    set i (add i 1) .
  end
  return .
end

proc main input k cap atomic . input al cap allocator . output u8 . effects atomic alloc .
do
  let g option mut slice u8 be alloc_bytes al capacity 8 .
  guard is_some g . else return 1 .
  var cells mut slice u64 be view_array u64 (some_value g) .
  atomic_store cells 0 0 .
  count_par k "abcdefghij" cells .
  return narrow u8 (atomic_load cells 0) .
end

$ lowentc --run main counter.low
main() = 10

• atomic_add counter 0 1 atomically adds 1 at position 0 of the slice counter. A place is addressed by slice and index.
• count_par splits data and updates the shared counter. It counted ten bytes, so the result is 10.
• Atomic operations are the atomic effect and require receiving cap atomic. main receives cap atomic at the entry point.
• view_array u64 views the 8 allocated bytes as a slice of one u64 without copying (chapter 13).

Declaring the atomic effect without the capability is rejected.

module nocap .
rem expect: E-ATOMIC-NOCAP

proc bump input s mut slice u64 . output u64 . effects atomic .
do
  atomic_add s 0 1 .
  return atomic_load s 0 .
end

$ lowentc --check nocap.low
nocap.low:4:0 E-ATOMIC-NOCAP: this op declares the `atomic` effect but receives NO `cap atomic`. Like `io`, `alloc` and `heap`, `atomic` is an effect you are HANDED the right to: `input k cap atomic .` (§7.2 (6))

Atomic operations are not free. Used on a value only one flow touches, they only slow things down. So they are not the default; they are chosen by name, and their cost is written in the head’s effects and capabilities.

27.5 Memory orderings#

Appending order <name> to an atomic operation decides what other flows see and when.

The strongest is the default because it is the easiest to reason about. It is proven that when every access is seq_cst you may think sequentially. Weakening is a choice made in writing by someone who knows its value.

Combinations that mean nothing for an operation are rejected.

Using four of the orders with the operations they pair with looks like this.

module orders .
rem run: main

rem without an order it is seq_cst; every flow sees one and the same order
rem acq_rel for an operation that reads and writes (atomic_swap), release for a write, acquire for a read
proc main input k cap atomic . input al cap allocator . output u8 . effects atomic alloc .
do
  let g option mut slice u8 be alloc_bytes al capacity 8 .
  guard is_some g . else return 250 .
  var cells mut slice u64 be view_array u64 (some_value g) .
  atomic_store cells 0 5 order seq_cst .
  let old u64 be atomic_swap cells 0 7 order acq_rel .
  atomic_store cells 0 (add old 10) order release .
  return narrow u8 (atomic_load cells 0 order acquire) .
end

$ lowentc --run main orders.low
main() = 15

atomic_store … order seq_cst writes 5, atomic_swap … order acq_rel, which reads and writes, swaps in 7 and returns the old 5, order release writes 15, and order acquire reads it back, so 15 is returned. A pairing that does not match is refused.

module order_bad .
rem expect: E-ATOMIC-ORDER

proc peek input k cap atomic . input s mut slice u64 . output u64 . effects atomic .
do
  return atomic_load s 0 order release .
end

$ lowentc --check order_bad.low
order_bad.low:6:0 E-ATOMIC-ORDER: this memory ordering is not valid for this atomic op (a load cannot be `release`, a store cannot be `acquire`, a fence cannot be `relaxed`) — RFC-0018 §6.1

What would a read release? C leaves such combinations undefined. A write cannot be acquire, and a fence (atomic_fence), which only sets order, cannot be relaxed.

27.6 Lanes — computing several values at once#

Where parallel splits a loop across flows, vec holds several values as one value within a single flow and computes them at once (SIMD). vec u32 4 is a value with four lanes holding four u32s, and the lane count is part of the type. Whether the machine computes the lanes at once or one by one, the answer is the same (canon 6.2.11).

module lanes .
rem run: capped_sum [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]
rem run: extremes [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]
rem run: turned [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0] [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
rem run: lanes_here

rem read four lanes as one value, press lanes above 5 down to 5, and add them all
proc capped_sum input b slice u8 . output u32 . effects none .
  requires ge (len b) 16 .
do
  var xs slice u32 be view_array u32 b .
  var v vec u32 4 be load xs 0 .
  var lim vec u32 4 be splat 5 .
  var over mask 4 be gt v lim .
  var capped vec u32 4 be select over lim v .
  return reduce_add capped .
end

rem across the lanes: the largest, the smallest, and the product of all
proc extremes input b slice u8 . output u32 . effects none .
  requires ge (len b) 16 .
do
  var xs slice u32 be view_array u32 b .
  var v vec u32 4 be load xs 0 .
  return add (mul (reduce_max v) 1000) (add (mul (reduce_min v) 100) (reduce_mul v)) .
end

rem reverse the lanes, rotate by one, and write them to memory
proc turned input b slice u8 . input out mut slice u8 . output u32 . effects none .
  requires ge (len b) 16 .
  requires ge (len out) 16 .
do
  var xs slice u32 be view_array u32 b .
  var ys mut slice u32 be view_array u32 out .
  var v vec u32 4 be load xs 0 .
  var r vec u32 4 be reverse v .
  var t vec u32 4 be rotate r 1 .
  store ys 0 t .
  return reduce_add t .
end

rem how many u32 lanes this machine handles at once --- a translation-time number
fn lanes_here output u64 .
do
  return native_lanes u32 .
end

$ lowentc --run capped_sum lanes.low [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]
capped_sum([1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]) = 14
  arg0 (written) = [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]
$ lowentc --run extremes lanes.low [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]
extremes([1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]) = 9289
  arg0 (written) = [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]
$ lowentc --run turned lanes.low [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0] [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
turned([1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0], [3,0,0,0,9,0,0,0,1,0,0,0,7,0,0,0]) = 20
  arg0 (written) = [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]
  arg1 (written) = [3,0,0,0,9,0,0,0,1,0,0,0,7,0,0,0]
$ lowentc --run lanes_here lanes.low
lanes_here() = 4

• load xs 0 reads four lanes starting at position 0 of the slice. store ys 0 t writes the other way.
• splat 5 fills every lane with 5. The lane count comes from the type of the name it is stored in (vec u32 4).
• Comparing vecs, as in gt v lim, gives a mask mask 4 holding true or false per lane. select over lim v picks lim in lanes where the mask is on and v where it is off. Choosing per lane without a branch (if) lets the machine do it in one instruction.
• reduce_add, reduce_max, reduce_min and reduce_mul gather the lanes into one. Pressing [1,9,3,7] down to 5 gives [1,5,3,5], whose sum is 14.
• reverse reverses the order of the lanes, and rotate r 1 rotates them by one. [7,3,9,1] rotated, [3,9,1,7], was written to memory.
• native_lanes u32 gives, at translation time, how many u32 lanes this machine handles at once. Choosing that lane count only computes more at once; the answer is the same.

A mask can also read or write just some of the lanes.

module masked .
rem run: keep_big [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0] [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
rem run: read_big [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]

rem write only the lanes above 5 --- places of masked-out lanes are left untouched
proc keep_big input b slice u8 . input out mut slice u8 . output u64 . effects none .
  requires ge (len b) 16 .
  requires ge (len out) 16 .
do
  var xs slice u32 be view_array u32 b .
  var v vec u32 4 be load xs 0 .
  var lim vec u32 4 be splat 5 .
  var m mask 4 be gt v lim .
  store_masked out 0 v m .
  return 0 .
end

rem read only the lanes that are on, and put the default 100 in the others
proc read_big input b slice u8 . output u32 . effects none .
  requires ge (len b) 16 .
do
  var xs slice u32 be view_array u32 b .
  var v vec u32 4 be load xs 0 .
  var lim vec u32 4 be splat 5 .
  var m mask 4 be gt v lim .
  var fallback vec u32 4 be splat 100 .
  var r vec u32 4 be load_masked xs 0 m fallback .
  return reduce_add r .
end

$ lowentc --run keep_big masked.low [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0] [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
keep_big([1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0], [0,0,0,0,9,0,0,0,0,0,0,0,7,0,0,0]) = 0
  arg0 (written) = [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]
  arg1 (written) = [0,0,0,0,9,0,0,0,0,0,0,0,7,0,0,0]
$ lowentc --run read_big masked.low [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]
read_big([1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]) = 216
  arg0 (written) = [1,0,0,0,9,0,0,0,3,0,0,0,7,0,0,0]

store_masked out 0 v m writes only at the places of the lanes that are on (9 and 7) and leaves the others untouched. load_masked xs 0 m fallback reads only the lanes that are on and puts the default 100 in the others. This is the shape for handling the tail when fewer than four slots remain at the end of a slice.

Watch two things. First, splat takes its lane count from the declared type, so it cannot be written inline in an expression. Second, adding lanes and adding a slice are different ops — lanes are reduce_add, a float slice is sum_neumaier or sum_seq. Until 2026-09-17 the latter were spelled sum and sum_fast, while the canon used those same names for “add all the lanes”. One name meant two things, so the names were split (canon 6.3.7.1).

module mistake_splatinline .
rem expect: E-VEC-SPLAT

fn capped input b slice u8 . output u32 .
do
  var xs slice u32 be view_array u32 b .
  var v vec u32 4 be load xs 0 .
  rem ✘ `splat` written inline --- nothing says how many lanes
  var over mask 4 be gt v (splat 5) .
  return reduce_add (select over v v) .
end

$ lowentc --check mistake_splatinline.low
mistake_splatinline.low:9:0 E-VEC-SPLAT: `splat` fills every lane of a vector, and how many lanes there are comes from the declared type — inside an expression there is nothing to say it, so the value is read as a plain scalar and the surrounding comparison stops matching its `mask` type. Bind it first, with the lane count written down: `var lim vec u32 4 be splat 5 .`, then use `lim`
mistake_splatinline.low:9:0 E-TYPE-VAR: the initializer's type does not match the declared type — expected `mask`, found `bool`

27.7 Saying how a place is used — access#

The access <name> <mode> . clause writes in the head whether the op only reads an input place or only writes it. Callers and the scheduler rely on that promise.

module access .
rem run: peek [9,8,7]

rem access data shared_read says this op only reads data, a promise that several tasks may hold it together
fn peek input data slice u8 . output u64 .
  access data shared_read .
do
  return widen u64 (index data 0) .
end

$ lowentc --run peek access.low [9,8,7]
peek([9,8,7]) = 9
  arg0 (written) = [9,8,7]

shared_read means “only reads”. With no write there is no race, so several tasks may hold the same place together. write_only means “only writes”, so a buffer not yet filled may be passed. The tool checks both modes against the body. The remaining modes such as sequential are kernel scheduling hints that constrain nothing yet, and writing one makes W-NOT-YET say so.

27.8 Common mistakes#

module mistake_sharedwrite .
rem expect: E-PAR-WRITE

proc count_par input data slice u8 . input counter mut slice u64 . output void . effects none .
  parallel data split .
do
  var i u64 be 0 .
  while lt i (len data) . do
    rem ✘ every piece reads, adds to and writes the same place `index counter 0`
    set (index counter 0) (wrap_add (index counter 0) 1) .
    set i (add i 1) .
  end
  return .
end

$ lowentc --check mistake_sharedwrite.low
mistake_sharedwrite.low:10:0 E-PAR-WRITE: a splittable loop may only write its OWN element `index <s> <i>` — this write can collide with another iteration (Bernstein: wr ∩ wr = ∅)

module mistake_floatreduce .
rem expect: E-PAR-FLOAT

fn mean input s slice f64 . output f64 .
  parallel s split .
  rem ✘ the result of float addition depends on how it is grouped
  reduce acc add .
do
  var acc f64 be 0.0 .
  var i u64 be 0 .
  while lt i (len s) . do
    set acc (add acc (index s i)) .
    set i (add i 1) .
  end
  return acc .
end

$ lowentc --check mistake_floatreduce.low
mistake_floatreduce.low:9:0 E-PAR-IDENTITY: the accumulator this reduction starts from is not the IDENTITY of its operator, so a split answer is not the sequential one: every piece starts again from that value and it is counted once per piece (measured: sequential 121, native split 621). DET-1 promises a split is bit-identical — that holds only from the identity (`add`/`bit_or`/`bit_xor` → 0, `mul` → 1, `max` → 0 on an unsigned width). Start from the identity and add the offset once, after the loop
mistake_floatreduce.low:9:0 E-PAR-FLOAT: a FLOAT reduction cannot be split: float addition is not associative, so the tree shape changes the result and the answer would depend on the schedule (★ nonassoc_shape_matters, Qed). Use the sequential `sum` (Neumaier) — determinism is part of the meaning, not a detail
mistake_floatreduce.low:4:0 W-PAR-OK: this loop satisfies the Bernstein conditions and may be split (DET-1 proves the parallel result is bit-identical to the sequential one — docs/proofs/coq/LowentPar.v). Execution is still sequential, which is a VALID implementation precisely because of that theorem

module mistake_reduceinit .
rem expect: E-PAR-IDENTITY

fn total input s slice u8 . output u64 .
  parallel s split .
  reduce acc add .
do
  rem ✘ the accumulator starts at 100 --- once split, every piece starts at 100
  var acc u64 be 100 .
  var i u64 be 0 .
  while lt i (len s) . do
    set acc (add acc (widen u64 (index s i))) .
    set i (add i 1) .
  end
  return acc .
end

$ lowentc --check mistake_reduceinit.low
mistake_reduceinit.low:9:0 E-PAR-IDENTITY: the accumulator this reduction starts from is not the IDENTITY of its operator, so a split answer is not the sequential one: every piece starts again from that value and it is counted once per piece (measured: sequential 121, native split 621). DET-1 promises a split is bit-identical — that holds only from the identity (`add`/`bit_or`/`bit_xor` → 0, `mul` → 1, `max` → 0 on an unsigned width). Start from the identity and add the offset once, after the loop
mistake_reduceinit.low:4:0 W-PAR-OK: this loop satisfies the Bernstein conditions and may be split (DET-1 proves the parallel result is bit-identical to the sequential one — docs/proofs/coq/LowentPar.v). Execution is still sequential, which is a VALID implementation precisely because of that theorem

module mistake_noloop .
rem expect: E-PAR-NOLOOP

proc smooth input s mut slice u8 . output u64 . effects none .
  parallel s split .
do
  var i u64 be 0 .
  rem ✘ a loop to split must have the shape `while lt i (len s)` --- and this one reads a neighbouring element too
  while lt (add i 1) (len s) . do
    set (index s i) (div (wrap_add (index s i) (index s (add i 1))) 2) .
    set i (add i 1) .
  end
  return len s .
end

$ lowentc --check mistake_noloop.low
mistake_noloop.low:4:0 E-PAR-NOLOOP: the `parallel` clause names a slice, but no `while lt <i> (len <slice>) . do … end` loop was found to split. That clause is a CLAIM — DET-1 proves a split is bit-identical only when there IS a loop to split — so with no loop the compiler verifies NOTHING while the annotation still tells every reader it was checked. An unchecked promise is the lie PRINCIPLES.md §0 is about; the same judgement already refused `mailbox unbounded` and `bounded 0`. Delete the clause (it means nothing here) or write the loop it describes

module mistake_access .
rem expect: E-ACCESS-MODE

rem ✘ declared write_only yet it reads; the place may not be filled yet
proc bad_fill input out mut slice u8 . . output u64 . effects state .
  access out write_only .
do
  let x u8 be index out 0 .
  return widen u64 x .
end

$ lowentc --check mistake_access.low
mistake_access.low:5:0 E-ACCESS-MODE: `access <p> write_only` says this op never READS that place — but it does. A write_only place may be uninitialised: reading it is reading garbage, and the declaration is what told the caller it was safe
mistake_access.low:7:1 W-EFFECT-OVER: this op DECLARES `state` but never PERFORMS it. A declared effect is a cost the caller must budget for (a pure caller cannot call an `io` op). Drop it, or — if a future version will perform it — say so (RFC-0007)

module max_gather .
rem run: biggest [3,9,2,7]
rem `max` is associative too, with 0 as its identity, so it can be split and gathered
fn biggest input s slice u8 . output u64 .
  parallel s split .
  reduce best max .
do
  var best u64 be 0 .
  var i u64 be 0 .
  while lt i (len s) . do
    set best (max best (widen u64 (index s i))) .
    set i (add i 1) .
  end
  return best .
end

$ lowentc --run biggest max_gather.low [3,9,2,7]
biggest([3,9,2,7]) = 9
  arg0 (written) = [3,9,2,7]

27.9 This chapter’s syntax at a glance#