Paralever

paralever

Proving output equivalence of parallel programs with sequential programs — in Lean 4

Anirudh Gupta

IISc Bengaluru · ISP-I · 4th-year BTech

19 October 2026

The fundemental Question for (truly) Parallelizing programs

paralever { [0] := 3; [1] := 4; %0 := [0]; [2] := %0 * %0; %1 := [1]; [3] := %1 * %1; %2 := [2]; %3 := [3]; [4] := %2 + %3 }nine statements, one core

→parallelize

paralever { [0] := 3; [1] := 4; parallel { %0 := [0]; [2] := %0 * %0 } | { %1 := [1]; [3] := %1 * %1 }; %2 := [2]; %3 := [3]; [4] := %2 + %3 } For both codes Output State = [3,4,9,16,25].

We parallelize programs for GPU/TPU, etc. targetting True Parallelism in most cases. The primary question that arises:

Is par = seq correct? under every schedule

seq — the statements run one after another, on one core. par — the branches of a parallel block run at the same time, and the block ends when all of them have.

Overview

Background — Hoare triples, ∗-disjointness, and what CSL's soundness theorem gives you
Our claim — independent branches can be run either way, and the answer does not change
Programs as data — one branching constructor, and a footprint computed from the syntax
The proof — four pieces, and the schedule appears in exactly one of them
The language — memory, registers, one fork, and a rejected program that explains itself
Examples — a sum, a matmul, a merge sort, a neural net — one check each
Automatic parallelization — a ;-chain in, a proved-equivalent tree out
MLIR — a benchmark in C gets a verdict without being translated by hand

Part 1 · Background

Hoare triples, ∗-disjointness, and what Concurrent Separation Logic (CSL)'s soundness theorem gives you

Why Hoare triples are not enough?

Consider the below counterexample:

C₁ : [p] := 5; y := [p]write to [p], then read it back

C₂ : [p] := 8write to the same [p]

Let p points at xso both commands write the cell holding x

{true} C₁ {y = 5}

{true} C₂ {true}

{true} C₁; C₂ {y = 5}by sequencing, y = 5

{true} C₁ ∥ C₂ {y = 5}false · a schedule runs C₂ between the write and the read, leaving y = 8

A triple {P} C {Q} says that if P holds and C terminates then Q holds. It quantifies over the starting state and over nothing else — in particular not over what another thread does while C runs.
So the first triple is proved as though its command ran alone. y := [p] reads back the value the command itself wrote, which is true of every run in which nothing else touches [p].
The schedule that runs C₂ between that write and that read does touch [p], so the assumption the proof was built on no longer holds, and y ends at 8.
A triple has no way to say this cell is mine, so it cannot exclude that schedule. Ownership is the missing notion, and it is what separation logic adds.

Separation Logic's `∗`-disjointness

l ↦ vthe heap cell l holds v · exclusive

P ∗ P′the heap splits into two disjoint-domain pieces, one satisfying each

{P} C {Q} {P′} C′ {Q′}

{P ∗ P′} C ∥ C′ {Q ∗ Q′}

C modifies no variable free in P′, C′, Q′, and conversely · O'Hearn, CONCUR 2004

l ↦ v says the heap is exactly one cell, l, and it holds v. Holding it is exclusive: no other assertion standing beside this one may mention l.
P ∗ P′ says the heap splits into two pieces whose domains are disjoint, one satisfying each side. The existence of that split is part of the claim, not a remark about it.
Each premise of the rule mentions one thread, and the conclusion holds for every interleaving. Disjointness is what pays for that step: neither thread can reach a cell the other owns, so there is nothing for an interleaving to disturb.
O'Hearn states this as two hypotheses — a thread accesses only what it owns, and at every moment the state partitions into the parts owned by each thread and by each resource.

Sharing comes back as a loan, and the rules are sound by a trace semantics

{(P ∗ RI₃) ∧ B} C {Q ∗ RI₃}

{P} with r when B do C {Q}

each resource name r carries an invariant RI₃ · two with regions for the same r never overlap in time

r is a resource: a name for a region of the heap that no thread owns. Every r carries an invariant RI_r, the assertion describing the states that region is allowed to be in.
Outside a region a thread knows nothing about those cells. with r when B do C lends RI_r to the thread on entry; C may break it while it runs, and has to restore it before the region ends.
RI_r must be precise, meaning it pins down one sub-heap rather than any of several. Without that the hand-back is undefined — the thread would not know how much of the heap it is returning.
Brookes proves both rules sound in a semantics of action traces in which a racing step is a catastrophic error, so a program with a race proves nothing.

Parallel Decomposition · Brookes, CONCUR 2004, Thm. 21

If a trace of C₁ ∥ C₂ runs from a state split as σ₁ ∗ σ₂ and the components' footprints stay separate, then that trace is an interleaving of a trace of C₁ from σ₁ and a trace of C₂ from σ₂, and the final states recombine as σ₁′ ∗ σ₂′.

The heap splits, and that split is also the hypothesis: it must already hold of σ. Two threads reading a₀ have no such split, and C₁; C₂ is never mentioned.

The conclusion is about the states, not only the traces: each thread's final heap σᵢ′ is what that thread alone produces from its own half, and σ′ is their disjoint union. That is what makes the disjoint-concurrency rule sound — Q₁ holds of σ₁′ and Q₂ of σ₂′, so Q₁ ∗ Q₂ holds of σ′. The premise is a heap already written as σ₁ ∗ σ₂ with each thread confined to its own half, and two threads that both read a₀ cannot be divided that way: whichever half holds a₀, the other thread's local run steps outside its heap. Our hypothesis asks for no split, only Bernstein independence, and our conclusion is the one this lemma does not state — that C₁ ∥ C₂ and C₁; C₂ reach the same outcomes, in both directions, under every schedule.

∗ forbids a shared read that nothing can go wrong with

Each side needs a₀ ↦ u, so the conclusion needs (a₀ ↦ u) ∗ (a₀ ↦ u) ⇒ false.
A resource r serializes the two reads instead of allowing them.
Fractions do allow them: a₀ ↦_{1/2} u each, carried through every lemma.
Bernstein checks writes only, so read-read is no conflict.

“there is no way to prove the obviously valid formula ⊢ {z ↦ 1} x:=[z] ∥ y:=[z] {x = y = 1 ∧ z ↦ 1}, since the logic requires both processes to ‘need’ to own the heap cell denoted by z, separately. Nevertheless, the trace semantics handles this issue (and this example) correctly, so here is a place where the semantics is ahead of the logic.” Brookes, A semantics for concurrent separation logic, CONCUR 2004

To dereference a₀ the left premise must hold a₀ ↦ u and the right premise the same cell, and one cell does not split into two pieces that each contain it — so the rule does not apply, to a program whose answer no schedule can change. Handing a₀ to a resource takes it out of both preconditions, but then every read sits inside with r do … and two such regions never overlap in time; matmul would put each element it reads into a critical region and give up the parallelism it was written for. Fractional permission is the real repair, and it moves the cost into the specifications: a fraction for every shared cell, threaded through every lemma.

This is O'Hearn's own argument, used there to show that [10]:=42 ∥ [10]:=6 has no derivable triple; pointed at reads it rejects a deterministic program instead. The claim is not that CSL cannot verify this — with fractions it can. The claim is about the shape of the obligation, and matrix multiplication is this example at scale: every row of A is read by every thread in a row block.

Part 2 · Our claim

Independent branches can be run either way, and the answer does not change

One theorem about two programs, with a hypothesis the kernel evaluates — rather than a bound on one program's postcondition.

What the literature proves, and what it leaves open

O'HearnCONCUR'04

{P₁}C₁{Q₁}, {P₂}C₂{Q₂} ⇒ {P₁∗P₂} C₁∥C₂ {Q₁∗Q₂}

a rule about triples — says nothing about program equality

BrookesCONCUR'04 §5–7

a trace of C₁∥C₂ from σ₁∗σ₂ with separate footprints is an interleaving of traces of C₁ and C₂

projects one trace — not equality of outcome sets

Apt & Olderogtextbook

C₁, C₂ share no variables ⇒ C₁∥C₂ = C₁;C₂

excludes shared reads, so excludes matmul; on paper

this workLean 4

wfB s = true ⇒ execPar s ∥≡ execSeq s — equality of outcome sets, arbitrary programs, kernel-checked

the corollary everyone uses and nobody states

Independence is Bernstein, computed from the syntax

@[simp, grind .]
def Indep (f₁ f₂ : Footprint) : Prop :=
  Disjoint f₁.writes f₂.writes ∧ Disjoint f₁.writes f₂.reads ∧ Disjoint f₂.writes f₁.reads

w₁∩w₂ = w₁∩r₂ = w₂∩r₁ = ∅ — shared reads are allowed
∗ would forbid them, and so forbid matmul: disjoint C[i*n+j], overlapping rows
footprintOf is a fold over the syntax, so the check is decide, not a proof

reads 0,1 · writes 2thread 1

reads 0,1 · writes 3thread 2

→indepB = true

acceptedsame cells read, different cells written

`WellFormed` is that check at every `par`, along the run

def WellFormed {τ : Type} : ParM τ → State → Prop
  | .pure _,      _ => True
  | .read l k,    σ => WellFormed (k (σ l)) σ
  | .write l v k, σ => WellFormed (k ()) (σ.update l v)
  | .par cs k,    σ =>
      let r := runChilds cs σ
      IndepAll (childFootprints cs σ) ∧ WellFormedChilds cs σ ∧ WellFormed (k r.1) r.2

accesses p σ is the footprint of running p from σ: the cells it reads and the cells it writes, as two lists.
A par node asks for three things — the children's own footprints are pairwise independent, each child is itself well-formed, and so is the continuation from the heap the children leave.
A read or write is never a condition; it only advances the heap the next check is measured against. All of the content sits at par nodes.
Checking the outermost par alone is unsound, which is why the recursion goes to the bottom of the tree.

Independent branches agree with `p; q` under every schedule

theorem par_seq_eq {s : ParProg} (h : wfB s = true) (ρ : Regs) (σ : State) :
    ParSeqEq (execPar s ρ) (execSeq s ρ) σ := bys:ParProgh:s.wfB = trueρ:Regsσ:State⊢ s.execPar ρ ∥≡ s.execSeq ρ from σ

ParSeqEq p q σ — the two reach the same outcome set from σ, not one trace
hypothesis is a Bool the kernel evaluates; conclusion quantifies over schedules
time_le rides along: the parallel reading never needs more rounds

The schedule does not appear in the obligation. Proved once, every program afterwards pays one decide on a footprint rather than a proof about interleavings.

Part 3 · Programs as data

One branching constructor, and a footprint computed from the syntax

ParM is an inductive type, so a program is a tree Lean can take apart; the obligation is a Bool on two lists of addresses.

`seq` is a spine; `par` is the only node that branches

Same leaves, same order, one node different. paralever { s₁; …; sₙ } is right-nested seq, so every program is a spine until a parallel block puts a fork in it.

Nobody states what a program touches — `footprintOf` evaluates it

#eval ParProg.footprintOf (matmul 2) { reads := [0, 4, 1, 6, 0, 5, 1, 7, 2, 4, 3, 6, 2, 5, 3, 7], writes := [8, 9, 10, 11] }two lists of addresses, obtained by reduction — not an annotation, not a lemma

accesses p σ is the footprint a run actually has. It depends on σ, so a claim about it is a claim about every heap.
footprintOf s reads the same two lists off the syntax tree and mentions no heap at all, so Lean evaluates it.
execPar_accesses_sub is the one thing that needed proving, and it is proved once for all programs: the computed lists contain the cells any run touches.

theorem execPar_accesses_sub (s : ParProg) (ρ : Regs) (σ : State) :
    (accesses (execPar s ρ) σ).Sub (footprintOf s) := execPar_accesses_sub_all.1 s ρ σ

`wfB` checks every `par`, not just the top

parallel { [0] := 1 } | { parallel { [1] := 2 } | { %0 := [1] } }outer footprints {0} and {1} are disjoint — a top-level check passes

▼

the inner `par` writes and reads `[1]` concurrently`wfB` recurses, so it rejects this

def wfB : ParProg → Bool
  | .load _ _  => true
  | .store _ _ => true
  | .set _ _   => true
  | .seq a b   => wfB a && wfB b
  | .par ss    => indepAllB (threadFootprints ss) && wfAllB ss
  | .label _ s => wfB s
  | .loadAt _ _ _  => true
  | .storeAt _ _ _ => true
  -- either branch may run, so both must be well-formed
  | .ifElse _ t e  => wfB t && wfB e

A check that only looked at the outermost fork would be unsound, which is why wfB is defined by recursion on the whole tree.

Races stop at `wrong`, so the hypothesis is load-bearing

[0] := 1 ∥ %0 := [0]one write, one read, one cell

→run

wrongabsorbing — Reynolds' grainless semantics

→so

wfB = falsemeasured, not assumed

racy programs are excluded, not silently assumed away — so the atomic grain is irrelevant
standing obligation: exhibit p, q where the conclusion fails, so the hypothesis is not free
the loop-carried case A[i] := A[i-1] + 1 must stay unprovable

Part 4 · The proof

Four pieces, and the schedule appears in exactly one of them

Where the difficulty actually is, and the program on which this equality is false.

The proof is four steps, and only one is about schedules

ParM is a nested inductive, so Lean's induction refuses it: every step runs through ParM.mutualInduction, and the N-ary case is an induction on the children list.

The difficulty, on two children

p = write 0 1 q = read 1 (λv. write 2 v)disjoint: p writes {0}, q reads {1} and writes {2}

→two readings

runSeq measures q at σ[0↦1]after p has run

a real schedule may run q at σbefore p has run

these are different heaps, so the two readings of q are a priori different runs
independence is what makes them agree: q reads [1], p writes [0], so the cell q looks at holds the same value in both
the induction therefore carries the footprint along with the equality — one level down, the footprint conjunct is what pins the replayed heap to the right one

The theorem is that every reachable terminal configuration of a well-formed par is the same one, and runSeq names it. The schedule enters the proof here and nowhere else.

Every configuration a schedule reaches computes the same `runSeq`

theorem wellFormed_canonical {τ : Type} (p : ParM τ) :
    ∀ σ r σ', WellFormed p σ → (Reaches (.run p σ) (.run (.pure r) σ') ↔ (r, σ') = runSeq p σ) :=
  wellFormed_canonical_all.1 p

One step leaves runSeq P σ unchanged, and can only shrink the footprint — step_combined.
One step keeps WellFormed, whichever branch moved — WellFormed_preserved.
Iterate along the whole chain: every reachable P', σ' has runSeq P' σ' = runSeq P σ — runSeq_invariant_chain.
At a .pure r endpoint runSeq is (r, σ'), which gives (r, σ') = runSeq P σ: the →.
For ←, run child 1 to completion, then child 2, then step into the continuation — reachesChilds_canonical.

Step 1 is where independence does the work, and it is the only hard case. The branch that moves second is replayed against a heap runSeq never measured it from. step_locality says a step replays unchanged between two heaps that agree outside a set of cells; Indep says the branch that moved writes nothing the other one reads or writes, so the two heaps do agree outside that set; and pinning the replayed heap down exactly needs the footprint conjunct of this very induction, one level down. That is why step_combined proves the outcome and the footprint together rather than as two lemmas — each half needs the other.

The ← direction needs no induction hypothesis about schedules at all: it exhibits one schedule. Running a child to completion is this same theorem one level down, which is why the two halves are mutually inductive.

`wfB` gives well-formedness at every heap, by one induction

theorem wfB_wellFormed {s : ParProg} (h : wfB s = true) (ρ : Regs) (σ : State) :
    WellFormed (execPar s ρ) σ := wfB_wellFormed_all.1 s h ρ σ

Induction over the syntax. load, store, set are trivial — only par carries a condition.
At a par: indepAllB held of the computed footprints, and Indep is antitone, so it holds of the real ones at σ — indepAll_childFootprints.
The sequential side has no par node, so its WellFormed is True by structure — wfB_wellFormedSeq_all.
Hand-written ParM instead of a ParProg: WellFormed_par_intro asks for the same three obligations, proved rather than decided.

This is the only place the quantifier over heaps is discharged, and it is discharged once, in the library: σ is universally quantified in the statement, so a program's own obligation never mentions a heap. That is what makes by decide sufficient afterwards.

The antitonicity step is the one worth saying aloud. execPar_accesses_sub gives accesses (execPar s ρ) σ ⊆ footprintOf s, and Indep.mono_left/mono_right say independence survives shrinking either side — so a bound that passes the test is enough, and a data-dependent address contributing its whole array is sound for exactly this reason.

Examples/SharedReads.lean is the hand-proved route: wellFormed_minmax discharges the three obligations for findMin ∥ findMax, where both branches read all three input cells.

Where this equality is false: one shared resource

observer = write 1 7 (λ_. read 0) mutator = write 0 99Examples/Racy.lean · σ₀ has cell 0 = 1

→par

y = 99mutator ran first · par_reaches

→seq

y = 1only outcome · seq_runSeq

put both accesses inside with r do … and CSL proves the program, with RI_r = ∃v. 10 ↦ v; by Brookes's corollary it is race free
race freedom is strictly weaker than determinism: the ∥ rule joins postconditions with ∗, which records no ordering — the rule is designed to forget the schedule
so ParM has no resource, no lock, and no unstructured fork, and the conclusion would be false if it had — not_parSeqEq proves the failure, not_indepAll refutes the hypothesis

Both sides terminate normally here and simply disagree, which is the case a reader is entitled to worry about.

`max` at a fork is derived, not assumed

theorem time_le {s : ParProg} (h : wfB s = true) (ρ : Regs) (σ : State) :
    time (execPar s ρ) σ ≤ time (execSeq s ρ) σ := time_execPar_le_all.1 s ρ σ h

work counts memory operations and is unchanged by forking — work_par_eq_seq
time counts rounds, where a round advances every ready child by one step
nothing in the cost semantics stipulates max at a fork: it falls out of the same independence hypothesis, on the same Bool — and time_par_lt_seq_single makes the inequality strict when both branches do work

Conflating work with time is the usual mistake. Parallelism buys nothing in total operations, and the theorem says so.

Part 5 · The language

Memory, registers, one fork — and the check run on user code

ParProg is the surface syntax a user writes; wfB is the same obligation, decided.

The language: memory, registers, and one fork

[l] := e %n := [l] %n := e parallel { … } | { … } if (c) { … } else { … } for i in n { … } parfor i in n { … } while (c) in n { … }`[` and `%` reserve no tokens — surface syntax is global in Lean

literal address [2] := %0 · footprint is exact

computed address A[B[i]] · footprint is the whole array

branch if c {…} else {…} · footprint is the branch union

Over-approximation costs precision, never soundness: execPar_accesses_sub proves the computed footprint contains every cell actually touched, at every heap.

Question c: a user-written `parallel` is checked, not trusted

parallel { [0] := 1 } | { %0 := [0]; [1] := %0 }store x on one core, load x on another

→decide

wfB = false
block [·,·] = truethe only legal placement is in sequence

this is the configuration the whole data-race literature is about
our rewrite can never build it: a RAW edge puts the two in one thread
when the user writes it, wfB is the checker — and rejects

A rejected program explains itself

the scan is the obligation, so an empty site list is the race-freedom proof — a false negative would be a bug in raceSites, not a tuning matter
a wrong guess in phase 2 cannot produce a wrong claim: follow_sound turns any schedule that replays into a Reaches proof, so a bad guess merely finds nothing
aiming is what makes it cheap — on three 8, three threads where the middle one is innocent, blind search takes 2.7 s and the aimed search 2 ms

step:thread action state 0:T0 write [10] ← 1 10↦1, 9↦0, 20↦0 1:T1 write [20] ← 1 10↦1, 9↦0, 20↦1 2:T1 write [9] ← 2 pending 2:T0 write [9] ← 1 pending Parallel aborts at Step 2. Reason: T0, T1 write to: {9}. Parallel: 9↦1 Sequential: 9↦2`explainProg late σ₀` · the counterexample is an execution, so the report is one

A data race, and the report it produces

def late : Prog :=
  .par (.seq (.wr 10 1) (.seq (.wr 11 1) (.wr 9 1)))
       (.seq (.wr 20 1) (.seq (.wr 21 1) (.wr 9 2)))

#evalstep:thread  action          state
0:T0         write [10] ← 1  10↦1, 11↦0, 9↦0, 20↦0, 21↦0
1:T0         write [11] ← 1  10↦1, 11↦1, 9↦0, 20↦0, 21↦0
2:T1         write [20] ← 1  10↦1, 11↦1, 9↦0, 20↦1, 21↦0
3:T1         write [21] ← 1  10↦1, 11↦1, 9↦0, 20↦1, 21↦1
4:T1         write [9] ← 2   pending
4:T0         write [9] ← 1   pending
Parallel aborts at Step 4. Reason: T0, T1 write to: {9}.
Parallel: 9↦1
Sequential: 9↦2
 IO.println (explainProg late σ0)

the race report as the infoview renders it

assets/race-report.png

Both sides do real work before colliding on their last write, so the race is not at the first step — which is what makes aiming the search worth having. wellFormedB is false, and the report is the interleaving that realizes it.

Part 6 · Examples

Four programs, in increasing order of what they need

A read-only sum, then overlapping reads, then recursion, then an in-place update — and the same two lines discharge every one of them.

A sum: shared reads, and nothing written twice

def sumRangeSeq (chunks : ChunkPlan) : ParM (List Int) := ParM.seqAll (chunks.map sumRange)

/-! ### par -/

def sumRangePar (chunks : ChunkPlan) : ParM (List Int) := ParM.parAll (chunks.map sumRange)

one thread per chunk, each folding .read l over its own locations — no thread writes anything, so Bernstein's three clauses are vacuous and ∗-disjointness would still have to split the array
wellFormed_sumRangePar holds for any ChunkPlan, including uneven ones, and any state — no decide, so it does not care how long the array is
strictly fewer rounds once two chunks are nonempty (time_lt), at identical work

chunks = [[0,1,2], [3], [4,5,6,7]]uneven on purpose

→runSeq

[6, 4, 26]by decide, on A = [1..8]

The obligation is a Bool the kernel evaluates; par_seq_eq supplies the rest.

A matmul: the reads overlap heavily, and that is the point

def matmul (n : Nat) : ParProg :=
  ParProg.parEach (gridIdx n n) fun ij =>
    ParProg.block
      ([ paralever { %2 := 0 } ]
        ++ (List.range n).map (fun k => paralever {
              %0 := [ij.1 * n + k];
              %1 := [n * n + (k * n + ij.2)];
              %2 := %2 + %0 * %1 })
        ++ [ paralever { [n * n + n * n + (ij.1 * n + ij.2)] := %2 } ])

parallel { thread 0 { t2 := 0; t0 := M[0]; t1 := M[4]; t2 := (t2 + (t0 * t1)); t0 := M[1]; t1 := M[6]; t2 := (t2 + (t0 * t1)); M[8] := t2; } thread 1 { t2 := 0; t0 := M[0]; t1 := M[5]; t2 := (t2 + (t0 * t1)); t0 := M[1]; t1 := M[7]; t2 := (t2 + (t0 * t1)); M[9] := t2; } … }what it lowers to at n = 2 — threads 0 and 1 both read M[0] and M[1], row 0 of A

The accumulator is a register, so a thread's whole write set is the one cell C[i,j]. That is what lets different cells read overlapping rows and columns — and it is the program ∗-disjointness rejects outright.

example : ParProg.wfB (matmul 2) = true := by⊢ (matmul 2).wfB = true decideAll goals completed! 🐙
example : ParProg.wfB (matmul 3) = true := by⊢ (matmul 3).wfB = true decideAll goals completed! 🐙

/-- …and the equivalence follows with nothing further to supply. -/
theorem par_seq_eq_2 (ρ : Regs) (σ : State) :
    ParSeqEq (ParProg.execPar (matmul 2) ρ) (ParProg.execSeq (matmul 2) ρ) σ :=
  ParProg.par_seq_eq (byρ:Regsσ:State⊢ (matmul 2).wfB = true decideAll goals completed! 🐙) ρ σ

A merge sort: the same recursion twice, `parPair` against `seqPair`

def mergeSortPure : List Int → List Int
  | [] => []
  | [x] => [x]
  | x :: y :: rest =>
      let xs := x :: y :: rest
      let mid := xs.length / 2
      mergePure (mergeSortPure (xs.take mid)) (mergeSortPure (xs.drop mid))

def mergeSortPar (N : Nat) : Nat → Nat → ParM Unit
  | lo, hi =>
      if _h : hi - lo ≤ 1 then .pure ()
      else
        let mid := lo + (hi - lo) / 2
        ParM.bind (ParM.parPair (mergeSortPar N lo mid) (mergeSortPar N mid hi)) (fun _ =>
          ParM.bind (mergeStep mid hi N (hi - lo) lo mid lo) (fun _ =>
            copyBack N (hi - lo) lo lo))

mergeSortSeq is the same definition with seqPair for parPair — nothing else differs
here the obligation cannot be decided: the recursion is in N, lo, hi, so independence comes from an interval argument — the two halves touch [lo,mid) and [mid,hi), which are disjoint
mergeSortPar_wellformed N lo hi (hi ≤ N) σ holds for every range and every heap, and seq_eq_par follows for the whole recursion rather than the top split

#eval on σ₄ = [5,3,8,1] agrees with mergeSortPure [5,3,8,1] — the pure function is the spec, and the check is a #guard in the file.

A neural net: layers in sequence, threads in parallel, weights updated in place

/-- Forward pass: convolution, ReLU, dense layer. -/
def forward : ParProg :=
  ParProg.block
    [ ParProg.conv1dK 6 3 X CW C
    , ParProg.mapK 6 C Rl (fun v => AExp.max v (.lit 0))
    , ParProg.denseK 2 6 W2 Rl B2 Y ]

/-- One SGD step: forward, then the error, then an in-place weight update with learning rate
`1 / lrDen`. The update's thread `(i,j)` reads and writes `W[i,j]` *in place* — admissible only
because each thread owns its own cell. -/
def trainStep (lrDen : Int) : ParProg :=
  ParProg.block
    [ forward
    , ParProg.zipK 2 Y T E (fun y t => y - t)
    , ParProg.outerUpdateK 2 6 W2 E Rl lrDen ]

every conv1dK thread reads the whole weight array and its own window — two kinds of read sharing at once, and neither costs anything, because Indep constrains writes only
the layout is declared, not addressed: Layout.of assigns the bases, so the disjointness the net depends on holds by construction — §5 of the file shows the bug that used to be writeable
trainStep's update thread (i,j) reads and writes W[i,j] in place, which is admissible exactly because each thread owns its own cell

82memory operations, either way

23rounds, parallel

82rounds, sequential

36squared error after 4 epochs, from 1224

forward_par_seq_eq and forward_time_le are both by decide on the same Bool.

Part 7 · Automatic parallelization

A ;-chain in, a proved-equivalent tree out

The analysis is untrusted and the gate is proved, so the pass needs no hypothesis — and the depth it reaches is measured against the dependence DAG's own lower bound.

Question a: dependences come from one scoreboard pass

unit i reads l edge lastWriter[l] → i · then readers[l] += i RAW · W ∩ R

unit i writes l edge lastWriter[l] → i WAW · W ∩ W

…and edge r → i for every r ∈ readers[l], then lastWriter[l] := i, readers[l] := [] WAR · R ∩ W

Bernstein's three clauses are the three kinds of edge. The DAG's longest path (critical) is a lower bound on the depth of any schedule, so it is what says whether a plan is optimal rather than merely better.

The DAG's longest path (critical) is a lower bound on the depth of any schedule, so it is what says whether a plan is optimal rather than merely better.

A fork discards register writes, so the unit is a segment

| .par ss, ρ => ParM.bind (ParM.parAll (execParAll ss ρ)) (fun _ => .pure ρ)the continuation gets the PRE-fork register file — `Prl/Lang/Core.lean`

▼

a register written inside a thread is gone at the joinboth readings agree, so it is NOT a race — `wfB` cannot see it

▼

the unit is a register-closed segment, not a statement`atoms`: cut only where no register is live — `liveIn`, must-kill `regKills`

Found by testing a rewrite that gave M[12],M[13] = 0,0 where the original gave 3,4. A load and the store consuming its register are one segment and are never split across a fork.

A plan is stages of threads, in program order

Because no unit moves, planUnits (plan us) = us is a structural theorem — proved by induction on the pass, not checked at run time — and the soundness proof needs no commutation argument.

The pass is one fold, and the three cases are the three dependences

worked on `[0]:=1; %0:=[0]; [1]:=%0; [2]:=3; %1:=[2]; [3]:=%1` — two chains written interleaved
`u₁`	—	new thread · `cur = [u₁]`
`u₂`	conflicts with `cur`	extend · `cur = [u₁,u₂]`
`u₃`	independent of everything	new thread · `stage = [[u₁,u₂]]`
`u₄`	conflicts with `cur`	extend · `cur = [u₃,u₄]`
`parallel { u₁; u₂ } \| { u₃; u₄ }` — depth 3, sequential 6, bound 3

Greedy prefix grouping gets 5 here: one conflicting unit ends its group even when everything after it is free.

`rewrite_sound`: seq = par for the rewrite, with no hypothesis

theorem rewrite_sound (p : ParProg) (ρ : Regs) (σ : State) :
    (runSeq (execPar (rewrite p) ρ) σ).2 = (runSeq (execSeq p ρ) σ).2 := byp:ParProgρ:Regsσ:State⊢ (runSeq ((rewrite p).execPar ρ) σ).snd = (runSeq (p.execSeq ρ) σ).snd

execPar and execSeq agree under runSeq — execPar_runSeq_all
execSeq of a par restores the register file, so a chain of forks never advances it: every thread of the whole plan runs at the initial registers — stages_seqAll
threads in order, each at the initial ρ, are the chain, when no register flows between them — fork_heap
a chain of blocks runs like the flat chain — runSeq_block_map
the plan's units are the program's statements — plan_units, atoms_flatten, runSeq_flatten

Step 2 carries the proof: a fork restores ρ, so a chain of forks leaves the top-level plan in the situation fork_heap already handles, one level up. rewrite checks its own plan and returns p unchanged if the check fails — which is why the theorem needs no hypothesis.

The pass on one program: the old tree and the new one

Two independent chains, written interleaved. The pass finds four units, one stage, two threads: quality ex1 = (3, 3, 6) and optimalB ex1 — depth 3 against a sequential 6, and 3 is the dependence DAG's critical path, so this is optimal rather than merely better. Greedy prefix grouping gets 5, because one conflicting unit ends its group even when everything after it is free.

The round trip: `paralever` in, `paralever` out

paralever { [0] := 1; %0 := [0]; [1] := %0; [2] := 3; %1 := [2]; [3] := %1 }input — one `;`-chain

▼ rewrite

paralever { parallel { [0] := 1; %0 := [0]; [1] := %0 } | { [2] := 3; %1 := [2]; [3] := %1 } } -- units 4 stages 1 threads 2 -- depth 3 (sequential 6, lower bound 3) optimal true committed trueoutput — `surface` emits what `paralever { … }` parses

lang → tree → tree → lang, closed. evalTask (rewrite p) = evalTaskSeq p is gated per program on real threads, on top of the theorem.

Measured: the pass reaches the lower bound, except where nothing can

program	depth	sequential	bound L	optimal
two chains, interleaved	3	6	3	✓
the N	8	12	7	—
merge sort, n = 4	12	16	12	✓
loop-carried chain	6	6	6	✓

L is the dependence DAG's critical path — a bound for any schedule, so ✓ is a certificate
the N's 7 needs a₃ concurrent with a₂'s write of [1]: wfB of that tree is false
so 8 is the floor for a race-free fork–join rewrite, and the gap is the shape, not the scheduler

Merge sort: the pass recovers a recursion tree it never saw

divide-and-conquer DAGs are series-parallel — no N — so the plan attains the bound
atoms threw the recursion away with the ;-chain: the tree comes back from footprints alone
splitting the merge per output cell gives depth 9, at work 16 → 24 — the trade, measured

Part 8 · MLIR

One front end, so a benchmark is not translated by hand

Hand-translating a benchmark suite is the dominant threat to validity for anything measured on one, because the translation is part of what is measured and is itself unverified.

MLIR as the one front end

N languages against one converter, instead of one front end per language — and stage 1 is replaceable, so a hand-written .mlir feeds the same interface
generic form, not each dialect's assembly: --mlir-print-op-generic prints every op the same way, so one reader covers affine, memref, arith and func
not LLVM IR — unstructured br and phi nodes have no encoding in an inductive ParM, and going through a loop structurizer destroys the affine maps the lowering depends on

MLIR.lower is a Lean function, so the translation is an object we can state a theorem about. The target is footprint preservation, which turns "trust the translator" into a proof obligation.

An affine map is already a footprint function

"affine.store"(%v, %A, %i, %j) {map = affine_map<(d0, d1) -> (d0, d1)>}the map applied to (i, j) is the subscript — no analysis, no inference

▼

Layout.at "A" [i, j] = A.base + i·cols + jrange-checked against its own buffer, because `Layout.at` is total

▼

wr (i, j) = [that cell]which is exactly what `wfB_parFor_of_lists` asks for

loops are unrolled at lowering time, so the subscript is a literal Nat and the footprint stays exact — proportional to the number of accesses, not to the size of the array
that matters for evaluability, not only precision: indepB is quadratic in list length, so an over-approximated footprint on a large array is unevaluable rather than merely imprecise
unrolling has a ceiling — decide on wfB (matmul n) is 6.6 s at n = 8 and 19 s at n = 10, and native_decide is prohibited — so about a hundred threads, and past that a kernel lemma at symbolic n

Layout.of places buffers in consecutive ranges, so array disjointness is discharged once by the allocator rather than once per pair.

One pilot, end to end: `doall-no.mlir`

"affine.parallel"() ({ ^bb0(%i: index): %0 = "affine.load"(%A, %i) {map = ...} %1 = "affine.load"(%B, %i) {map = ...} %2 = "arith.addi"(%0, %1) "affine.store"(%2, %C, %i) {map = ...} }) {upperBoundsMap = ... (8)}C[i] := A[i] + B[i], generic form

→MLIR.lower

parallel { thread 0 { t0 := M[0]; t1 := M[8]; M[16] := (t0 + t1); } thread 1 { t0 := M[1]; t1 := M[9]; M[17] := (t0 + t1); } … thread 7 { t0 := M[7]; t1 := M[15]; M[23] := (t0 + t1); } }one thread per point of the index box

layout A[8]@0, B[8]@8, C[8]@16 reads 16 cells writes 8 cells footprint exact verdict wfB true, wellFormedB true sites 0 values exact in Int`Lowered.report` — the whole story about one benchmark

The subscript is a literal Nat because the loop is unrolled at lowering time, so the footprint stays exact rather than becoming the whole array. C = [11, 22, 33, 44, 55, 66, 77, 88] on the threaded run, and runTask_eq is what makes it sound to look at that heap at all.

Two runs: the verdict over `Int`, the reference over `ℚ`

MLIR/Lower.leanLayout × ParProg, over `Int` — the verdict

MLIR/Eval.leanheap : Loc → Scalar, `Int` and `Rat` — the reference

→cell by cell

differential execution`progCells` against `refCells`

the verdict depends on no value: footprintOf and indepB never inspect a Val, so a memref<8xf64> occupies the same eight cells as a memref<8xi32> and gets the same verdict
floating point becomes Rat, not Real — every finite IEEE value is m · 2ᵉ, so Rat is a superset of the floats rather than an approximation, and it is computable, so a gate can run
the reference interpreter is allowed to evaluate a par in one canonical order, and what licenses that is par_seq_eq itself

MLIR.Corpus.summary	expressible	unsupported	confusion	over-approx	round trip
seven labelled pilots	7/7	[]	tp=3 fp=0 fn=0 tn=4	`indirect-yes`	✓

No false negatives is not luck: raceSites_nil_iff makes the scan complete for the obligation. stencil-f64-no is the Bernstein case — neighbouring threads share two of three read cells, which ∗ rejects outright and Indep accepts without a clause.

Kernels: symbolic obligations where `decide` dies

surface matmul, `wfB` at n	6	8	10	12
`decide` — pairwise over n² threads	1.5 s	6.3 s	19.3 s	49.3 s
`wfB_parFor_of_lists` — symbolic in n	0.16 s	0.16 s	0.16 s	0.16 s

fitted exponent 5.1 — Θ(n²) threads × Θ(n) cells, pairwise
11 kernels have a ∀ n obligation; each also decides at a concrete n, so the routes are checked to agree
the scheduler must emit kernel shape, not an unrolled par list — a Lower bug otherwise

Limits

registers cannot be renamed away — yet. noRegFlow is on raw read sets, stronger than the liveness atoms establishes, so a chain reusing %0 is declined and returned sequential
memory cannot be renamed at all. A Loc is reached by a computed address, so the cell is the name — privatization, the commonest OpenMP clause, is out of reach
footprints over-approximate. A[B[i]] reports the whole array; whileAtMost reports the branch union — conservative, never unsound
ParM is inductive, so while true is unrepresentable; and whether order preservation itself costs depth is open

Conclusions

One theorem, then arithmetic. wfB s = true ⇒ execPar s ∥≡ execSeq s, every schedule, arbitrary programs, kernel-checked — so each program pays decide, not a proof about interleavings
The rewrite is proved, not checked. rewrite_sound has no hypothesis: the pass is untrusted, the gate is proved, and the plan's order preservation makes the bookkeeping structural
Optimal where fork–join allows. Depth meets the DAG critical path on interleaved chains and on merge sort; the N's gap of 8 vs 7 is the shape, and the 7-tree is racy

534 build jobs · 0 sorries · github.com/AnirudhG07/paralever · contact@shemeka.in

References

Bernstein, Analysis of programs for parallel processing, IEEE TEC, 1966.
O'Hearn, Resources, concurrency and local reasoning, CONCUR 2004.
Brookes, A semantics for concurrent separation logic, CONCUR 2004, §5–§7.
Reynolds, Toward a grainless semantics for shared-variable concurrency, FSTTCS 2004.
Apt & Olderog, Verification of Sequential and Concurrent Programs, Springer.
Valdes, Tarjan & Lawler, The recognition of series parallel digraphs, SIAM J. Comput. 11(2):298–313, 1982.
Graham, Bounds on multiprocessing timing anomalies, SIAM J. Appl. Math., 1969.