45 Proofs about races and parallelism — discipline instead of a memory model

45.1 The Bernstein condition — an answer from 1966#

Let R and W be the set of places read and set of places written by a task. Two tasks are independent in three lines.

W₁ ∩ W₂ = ∅      the two do not write the same place
W₁ ∩ R₂ = ∅      one does not read what the other writes
R₁ ∩ W₂ = ∅      nor the reverse

Three lines saying intersections are empty are all there is. R₁ ∩ R₂ is not in the condition — reading the same place together is fine. A race is defined as “two tasks touch the same place and at least one writes”. The usual definition adds “the two accesses are not ordered”, but at level 1 that holds automatically. Between tasks after flows split and before they rejoin, there are no ordering edges at all.

The processor’s diagnostic quotes this condition directly.

module par_overlap .
rem expect: E-PAR-WRITE

rem every piece writes the first cell --- what remains depends on who went last
proc stamp input s mut slice u64 . output u64 . effects none .
  parallel s split .
do
  var i u64 be 0 .
  while lt i (len s) . do
    set (index s 0) i .
    set i (add i 1) .
  end
  return len s .
end

$ lowentc --check par_overlap.low
par_overlap.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 = ∅)
par_overlap.low:10: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 = ∅)

Every piece writes the first element, so wr ∩ wr = ∅ broke, and reading another piece’s element broke rd ∩ wr = ∅ too. chapter 27′s three conditions — read only your own share, write only your own share, do not write places living across iterations — are the Bernstein condition.

45.2 Independence means no races, and the condition is necessary#

The second theorem is the mark of an honest proof. Proving only “satisfying the condition is safe” leaves the theorem true even if the condition is overly strict — a condition that lets nothing pass is also safe. So a counterexample is proven alongside: loosen the condition and it really breaks. One theorem, one counterexample — a method this part uses in many places.

Without races, the well-known DRF-SC theorem (Adve–Hill) applies and the program behaves with sequential consistency. That is, you need not imagine orders jumbled up.

45.3 Between actors there is always a message#

The chain of argument runs like this. A place is owned by exactly one actor. Only the owner accesses it. Ownership moves only by message. But the two accesses come from different actors. Therefore an ownership transfer happened between them. A message is an edge fixing before and after, and two accesses with a fixed order are by definition not a race. The most common mistake with actors — sending a reference by message and continuing to use it on the sending side — is stopped because it is an ownership transfer and the sender loses that place (chapter 25′s handoff).

The connection to chapter 42 is the point. Enforcing “only one name writes” within one flow becomes exactly “two tasks do not overlap”. One safety rule pays off in two places.

45.4 Containment — where heavy tools are needed#

level 1 (split loops)          ─┐
level 2 (actor isolation)       ─┤→ no races by discipline → DRF-SC → think sequentially
level 3 (atomics · locks)       ─┘→ races really exist     → a memory model is needed

45.5 No races is not the same as deterministic#

Running twice on the same input can give different answers. Even without races. If several cores add floating-point numbers in parts and combine them, the last bits change when the order of combining changes. Each touched only its own share, so there is no race. Yet the answers differ.

This language’s claim is strong. The result of level 1 parallelism is bit-for-bit identical to the sequential result. No approximation, no tolerance. The conditions establishing that claim were proven to be exactly three (LowentPar.v). Determinism is not a matter of races but of the Bernstein condition. The same condition gives a different conclusion.

The counterexample is two tasks writing 1 and 2 to the same place. Depending on order, the answer is 2 or 1.

DET-2 is the theorem that swapping two non-conflicting tasks gives the same result. The proof is induction on adjacent swaps. If adjacent pairs can be swapped, repeating that reaches “any rearrangement that keeps the conflict order” — the same idea as a sorting algorithm. It gives the scheduler maximal freedom without losing determinism, and freedom is performance.

DET-3′s counterexample is subtraction. (5 − 3) − 1 = 1 while 5 − (3 − 1) = 3. If the operation is not associative the language must fix the tree shape, and if the scheduler changes the tree with the number of cores, the result depends on the schedule. The proof did not import IEEE floating point as axioms; it showed “if non-associative, the shape matters” generally, using subtraction as the representative non-associative operation. That is why reduce acc sub is rejected with E-PAR-ASSOC and floating-point addition with E-PAR-FLOAT (chapter 27).

45.6 What is not proven#

• The DRF-SC theorem itself is cited. “Without races it behaves with sequential consistency” is a well-known theorem; what was proven here is that our discipline satisfies its premise (no races).
• The theorems do not verify the implementation. Level 1 parallelism is implemented, but what the theorems pin down are the conditions the implementation must keep. Whether it keeps them is backed empirically by back-end cross-checks.
• The model assumes static read and write sets. With pointers those sets are hard to know in advance; in practice the type system must guarantee them. “Local” is an assumption, not a check.
• The state model is a “place → value” function. Real memory with alignment, aliasing and partial writes was not modelled. Floating point itself (rounding, NaN, −0) was not covered either.