Paralever: A Language That Proves Your Parallel Program Is Your Sequential Program

Published on Oct 17, 2026

·

~ 42 min read

Here is a program that squares two numbers in parallel and adds the squares.

Every snippet in this post is the live Lean, highlighted by the compiler that checked it: hover a name for its type, or switch the panel to Infoview to click through goal states and #eval output the way you would in the editor.

Below the program is the proof that running it with both threads at once computes exactly what running it one thread after the other computes, under every schedule the machine might pick.

The entire contribution of the person writing that program is by decide. There is no proof about interleavings, no invariant, no ownership discipline, and no separation-logic derivation. The independence condition is a closed Boolean expression, so Lean's kernel evaluates it; par_seq_eq is a theorem proved once, for all programs, that turns the true into the equality.

Making that line typecheck took a particular set of decisions, and those are the subject here. The project is Paralever, a Lean 4 library still under active development, with no sorry and no native_decide behind any theorem quoted below. The central proof gets a sketch of its shape rather than a walkthrough; the space goes to the decisions it forced instead — why independence is Bernstein's criterion rather than separating conjunction, why a tree of forks cannot express every dependence graph, what the language looks like, what happens when your program does have a race, and how a sequential program gets parallelised with a proof attached.

The claim a parallel loop makes

When you replace a loop with a parallel loop, you make a claim: the two programs compute the same thing. The claim is almost always left informal, and when somebody does formalize it, they formalize it for one program at a time. Two obstacles explain why.

The first is combinatorial. A parallel program with k threads of m steps each admits on the order of (km)!/(m!)^k schedules. The obvious proof strategy — show the output is the same for every interleaving — therefore stops working almost immediately; four threads of ten steps each already give more than 10^19 of them. Any argument that inspects schedules one at a time is finished before it starts, and the proof below never inspects one.

The second obstacle is that the claim is awkward even to state. It equates a nondeterministic program with a deterministic one, so you cannot write it as an equality of results until you have said what the results of the nondeterministic program are. Paralever answers with a relation: ParSeqEq p q σ says p and q reach exactly the same (result, final heap) pairs from σ. It is an equality of outcome sets, so it needs no choice of scheduler to make sense.

Where the theorem comes from, and the corollary nobody states

The theory this rests on is concurrent separation logic, and the honest account of the relationship is more interesting than "we mechanized CSL".

Separation logic exists because a Hoare triple cannot say "the cell at the address held by p", so the rule for mutating the heap carries a disjointness condition the assertion language cannot express. Sequentially that is an inconvenience. Under concurrency it is unsoundness, because two component proofs can each be valid while their composition is false. The points-to assertion l ↦ v and the separating conjunction ∗ exist to turn that side condition into an assertion.

O'Hearn's rule for disjoint concurrency, from CONCUR'04, is the one everything here descends from. Its premises mention each thread in isolation:

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

Brookes justified that rule, in the same year, with a Parallel Decomposition Lemma: in a race-free execution, an interleaved trace factors into one trace per component. Now notice what follows. If every trace factors, then the interleaving contributed nothing, and so every schedule produces the same answer — including the fully sequential one. Non-interference is proved once, and schedules stop mattering.

Brookes never writes that corollary down, and it is worth being precise about why, because it is not an oversight. In full CSL, with resources and ownership transfer, the equality is false. Two threads may legitimately communicate through a protected cell, and sequentializing them changes what the program does. The smallest instance is two lines: let the resource invariant be ∃v. 10 ↦ v, and run with r do [10] := [10]+1 against with r do y := [10]. CSL proves this program, since both branches preserve the invariant — and yet the parallel version can finish with y = 0 (right process first) or y = 1 (left process first), while the sequential composition finishes only with y = 1. Both terminate normally.

That example is worth sitting with, because it says something sharper than "resources are out of scope": race freedom does not imply determinism. Every access to cell 10 happens inside a critical region, so no two accesses ever overlap in time and the program is race free in exactly Brookes' sense — and parallel still differs from sequential. Race freedom is what CSL's soundness theorem delivers, and it is strictly weaker than the property proved here. The two coincide only in the fragment without synchronization, where the only way to be race free is to have non-conflicting footprints in the first place. So the equality holds only in that fragment, and isolating it was not what Brookes or O'Hearn were trying to do; soundness was the right theorem for the system they were building.

So the gap is not an unproved conjecture. Apt and Olderog (1997) state the equality on paper, under the far stronger hypothesis that the components share no variables at all. Deterministic Parallel Java (OOPSLA 2009) asserts it for a Java-like calculus but formalizes only the sequential commutativity it would follow from; PolCert (TASE 2024) mechanises it in Coq for affine loop nests; Blom, Darabi, Huisman and Safari (STTT 2021) built this exact architecture with no proof assistant. It is nowhere stated at Bernstein strength, for an arbitrary program, machine-checked.

The trade Paralever makes is explicit: by giving up interference entirely, it gets a two-sided equality instead of a one-sided refinement, a per-program obligation that is decidable arithmetic instead of a separation-logic proof, and a cost theorem about the same object. What it gives up is every program that needs a lock. That program is not merely out of scope, it is a program for which the central theorem is false, which is a much more useful thing to know.

Why not separating conjunction: Bernstein, and matrix multiplication

Separating conjunction is the obvious candidate for the independence condition, and it is the wrong one. P₁ ∗ P₂ asserts that the two threads own disjoint pieces of the heap, which means neither of them may so much as read a cell the other reads. Bernstein's criterion, from his 1966 Analysis of Programs for Parallel Processing in IEEE Transactions on Electronic Computers, asks for three intersections to be empty instead of one:

w₁ ∩ w₂ = ∅            the two threads write no common cell
w₁ ∩ r₂ = ∅            neither writes a cell the other reads
w₂ ∩ r₁ = ∅

There is deliberately no clause on r₁ ∩ r₂. Shared reads are allowed, and that single difference is what decides which programs the library can talk about.

Matrix multiplication is the example that forces the issue. Parallelize it over output cells and each task writes its own C[i*n+j], so the writes are disjoint and that part is fine. But the tasks computing C[i][j] and C[i][j'] both read the whole of row i of A. Under ∗-disjointness this kernel is rejected, despite being obviously safe. Under Bernstein it is admitted. That pattern — disjoint writes over heavily shared reads — is not an edge case; it is the shape of the dense linear-algebra kernels, convolutions and attention blocks that dominate GPU and TPU workloads.

∗-disjointness Bernstein
threads write disjoint cells required required
one thread writes what another reads forbidden forbidden
both threads read the same cell forbidden allowed
widening a read set can make a proof unsound can never create a conflict
matrix multiplication by output cell rejected admitted

That last-but-one row is what makes the whole approach computable. Since all three clauses are the emptiness of an intersection and no clause mentions r₁ ∩ r₂, enlarging a read set can never manufacture a conflict. The library is therefore free to over-approximate a footprint whenever it cannot compute one exactly, and the result stays sound. Under ∗ the same move is unsound, because there enlarging a footprint enlarges the ownership being claimed.

The criterion also has a second reading. Take Bernstein's three clauses as conditions that are violated rather than satisfied, and they are the three dependence edges every compiler textbook lists:

w₁ ∩ r₂ ≠ ∅   is a read-after-write dependence    (RAW, a true dependence)
w₁ ∩ w₂ ≠ ∅   is a write-after-write dependence   (WAW, an output dependence)
r₁ ∩ w₂ ≠ ∅   is a write-after-read dependence    (WAR, an anti-dependence)

One definition, used twice. As a predicate it is the hypothesis of the equivalence theorem; as a graph builder it is a dependence analysis. The automatic parallelizer spends it in both directions at once, which is why Bernstein's criterion is the one a compiler person would have picked anyway.

The construction, and how Task fits in

There is a reasonable objection to all of this: Lean already has real parallelism, so why invent a language? The answer is that Task is where a Paralever program runs, but it cannot be where the theorem lives, and the reason is one line of its definition:

structure Task (α : Type u) : Type u where pure :: get : α

@[noinline, extern "lean_task_spawn"]
protected def Task.spawn (fn : Unit → α) (prio := .default) : Task α := ⟨fn ()⟩

So (Task.spawn f).get = f () holds by rfl. Parallel and sequential are literally the same term. All the actual parallelism is an @[extern] runtime override that the kernel cannot see, so a theorem about interleaving proved at that level is not hard to prove — it is vacuous, because there is no interleaving in the model to reason about.

That is the whole justification for ParM, the type the theorem is actually about. Four of its design decisions are forced rather than preferred, and each has a consequence worth stating:

  • par is our own constructor, whose meaning is fixed by the interpreter rather than by Lean. This is exactly why the theorem is not a definitional identity.
  • ParM is inductive, so only terminating programs are expressible. while true cannot be written down. Lean 4 has no native coinductive types, so this is a permanent boundary rather than a gap waiting to be closed.
  • Races go to an absorbing wrong state, following Reynolds' grainless semantics (FSTTCS 2004). A racy program has no behaviour at all rather than a badly-specified one, which is what makes the choice of atomic grain irrelevant and keeps racy programs excluded instead of quietly assumed away.
  • par is N-ary and heterogeneous, carrying a type-indexed spine of children rather than a list, because List (ParM α) with a constructor-local α is rejected outright by Lean's kernel. The type index is what keeps each child's result type static. The cost is that Lean's induction tactic refuses ParM, so every proof in the library goes through a hand-written recursor, and the N-ary theorems are proved by induction on the child list.

How Task is actually used

Task is the backend, and it is the whole point of the exercise: a verified program that never runs on more than one core has proved something about nothing. runTask interprets a ParProg by spawning one real Lean Task per thread of every parallel block, running everything else on the calling thread.

The second theorem there is the one that matters. runTask_eq says that when wfB s = true, the heap left by the real-threads run is exactly the heap left by the canonical sequential run. The operating system can schedule those threads however it likes, and the work-stealing scheduler inside the Lean runtime can make different choices on different runs; none of it changes the answer, because the obligation has already ruled out every way the choice could matter.

The third theorem is what makes benchmarking honest. runTask_eq_runTaskSeq puts the threaded run and the single-threaded run on the two sides of an equation, so both go through the same interpreter and a stopwatch between them measures scheduling and nothing else. A speedup table built this way cannot be an artefact of the two sides computing different things, which is the usual way such tables mislead.

What the proof is, without the proof

Two moves carry the theorem. The first is getting the obligation right, because checking independence at the top level of a program is not enough, and the counterexample is small. Take par (wr 5 1) (wr 5 2) against wr 100 0. The first program races with itself on cell 5, but its footprint is {writes: [5]}, the second's is {writes: [100]}, and those are disjoint. Top-level independence says nothing whatsoever about what is nested inside. So WellFormed is recursive: Bernstein is checked at every par node in the term, against the heap that node actually sees along the reference run.

The second thing is the move that avoids the schedule explosion entirely. Instead of quantifying over interleavings, prove that a well-formed program has exactly one reachable outcome, and that this outcome is computed by an ordinary function:

theorem wellFormed_canonical (p : ParM τ) (σ : State) (h : WellFormed p σ) (r : τ) (σ' : State) :
    Reaches (.run p σ) (.run (.pure r) σ') ↔ (r, σ') = runSeq p σ

runSeq is an ordinary function and Reaches is the real nondeterministic small-step relation, so the theorem says the relation's entire image is that function's single value.

Canonical outcomes collapse every schedule to one value Many distinct schedules of a well-formed program fan out from one starting heap, and all of them terminate at the single outcome computed by runSeq. A racy program instead has schedules that end in the absorbing wrong state. run p σ runSeq p σ wrong every schedule the machine might pick well-formed: one outcome, computed by a function racy only

Once that is proved, the headline equivalence is three rewrites: apply the lemma to the parallel side, apply it to the sequential side, and observe that the two sides have the same canonical run, which is true by unfolding definitions and needs no independence hypothesis at all. The N-ary case is not a corollary of the binary one; it is the other way round, because the induction over children already happened inside the canonical-outcomes proof.

All the genuine difficulty sits in one case of one lemma — the par case, which is Brookes' decomposition lemma mechanized against an operational semantics instead of a trace model. Where the independence hypothesis is actually spent is narrower than you would guess. The step relation re-checks for conflicts at every step, so any step that does not crash is automatically non-racing at that instant, for free, however deeply nested it is. Independence is needed in one place only: when the right branch of a fork moves before the left one, its real starting heap is the joint state rather than the reference point the theorem is stated against, and only Bernstein guarantees that replaying the step against that reference point gives the same answer.

Trees: why fork–join cannot match a dependence DAG

Can every dependence graph be written as a tree of forks? The literature mostly leaves the question implicit, and the answer turns out to be the standing limitation of the entire approach.

A paralever program is a tree. You fork, the threads run, they join, and then you fork again; there is no construct that lets one thread wait on, signal, or lock against another. The dependences of that program, on the other hand, form a directed acyclic graph: instruction i must follow instruction j whenever their footprints violate one of Bernstein's three clauses. These are not the same class of object, and the mismatch costs real time.

Fork–join trees are exactly the series-parallel graphs, which is to say the graphs you can build from single nodes using only two operations.

The only two ways to build a fork-join tree Series composition stacks one subtree above another under a seq node. Parallel composition places subtrees beside one another under a par node. Every fork-join program is some combination of these two, and nothing else. seq a b par a b series parallel span adds span is the max every fork-join program is these two operations and nothing else

Not every DAG can be built that way, and the smallest one that cannot is called the N. It has four units where i₃ depends on both i₁ and i₂, while i₄ depends only on i₂, which leaves i₁ and i₄ with no relationship at all.

The N: a dependence DAG no fork-join tree can match On the left, the N-shaped dependence DAG with four units of span 6, 1, 3 and 7; its critical path through i1 and i3 is 9. On the right, the best fork-join tree, which must run i2 first and then fork i4 against the chain i1 then i3, giving a span of 10. The extra round is the cost of the tree shape. i₁ · 6 i₂ · 1 i₃ · 3 i₄ · 7 the dependence DAG critical path i₁ → i₃ = 9 i₁ and i₄ are unrelated: nothing orders them, either way round seq i₂ par i₁ i₄ i₃ best fork-join tree = 10 embed

Why no tree manages it: i₄ has to be placed either in parallel with i₁ or after it. If it is in parallel with i₁, then it cannot also wait for i₂, because a join is the only thing that orders anything and joining for i₂ would close the fork i₁ is inside. If it is after i₁, it has waited for a unit it does not depend on. Either way the tree has imposed an ordering the dependences never asked for.

With i₁ and i₄ made long, the cost is measurable in the library's own cost semantics. Every number in this table is a #guard that Lean evaluates, over four units of span 6, 1, 3 and 7:

shape of the long N span
sequential 17
par[i₁,i₂]; par[i₃,i₄] — stage by stage, which is what the pass emits 13
par[i₁, (i₂;i₄)]; i₃ — nested 11
i₂; par[i₄, (i₁;i₃)] — nested, and the best any tree does 10
the dependence DAG's critical path 9

Nesting is worth going from 13 down to 10, so a better scheduler genuinely helps. The remaining gap from 10 to 9 is irreducible, and I want to be careful about what makes it irreducible, because there are two different reasons a tree can fail to reach the bound and they are easy to confuse. In this program the 10-span tree is perfectly race-free — wfB returns true on it — so the gap is the tree shape alone and nothing else. In a shorter variant of the same N shape, the tree that would reach the bound of 7 pairs i₁;i₃ against i₂;i₄, which puts i₃'s read of a cell beside i₂'s write of it; there wfB returns false by decide, and the floor of 8 is enforced by the race rather than by the shape. Having both cases in the library is what stops "fork–join cannot reach the critical path" from being an appeal to Valdes, Tarjan and Lawler's series-parallel recognition paper (SIAM J. Comput. 11(2), 1982) and makes it a checked fact about specific programs.

The N also rules out a whole class of solutions. No online scheduler can be optimal here, because one that has forked i₁ against i₂ and then joined in order to run i₃ has already destroyed i₂'s thread by the time i₄ shows up. Building the dependence graph, by contrast, is online and nearly linear: each instruction is compared against the last writer of the cells in its own footprint, never against all of its predecessors.

What the tree restriction buys is worth stating, since it is not pure loss. Because a schedule here is an order-preserving partition of the instruction sequence, the fact that the plan's units are the program's statements is structural — it holds by how the plan was built, not by a run-time check. A scheduler that reordered units instead would need a commutation theorem saying independent statements may be transposed, and that theorem is not proved anywhere in this development. Order preservation is what let the whole proof go through with no such lemma.

Two things here are genuinely open. Recognising series-parallel digraphs takes linear time, but no algorithm for embedding an arbitrary DAG into one is known to bound the increase in critical path by a constant factor, and there is no hardness proof for the exact minimum-depth embedding either. Separately, whether order preservation itself ever costs span — as opposed to merely being convenient to prove — I do not know.

The language

ParM is a type of programs rather than a language anyone writes, because its effect nodes carry Lean functions as continuations. A ParM term cannot be printed past its first read, since whatever comes after a read is a function of the value read, and its footprint has to be obtained by simulating the program against a heap, since the addresses a continuation will touch are not visible in the term. Both are tolerable while programs are assembled by hand out of combinators. Neither survives contact with a compiler, which hands you instructions rather than closures.

ParProg is the same programs with their computations as data: a first-order inductive type with load and store for memory, set for register arithmetic, seq, par over a list of threads, ifElse, and loadAt/storeAt for an address computed at run time. It introduces no new semantics and adds no axiom. Instead it comes with two interpretations back into ParM — execPar sends par to the real fork constructor, and execSeq sends it to the corresponding chain of binds — so every theorem about the language still bottoms out in the theorem from the last section. What the layer buys is that the three things a user actually wants become computations instead of proofs:

The four layers a Paralever program passes through Surface syntax elaborates downward into ParProg, the first-order data layer where the footprint is a fold and the obligation is a Boolean. ParProg has two interpretations into ParM, execPar sending par to the real fork constructor and execSeq sending it to a chain of binds. ParM is interpreted by the nondeterministic small-step relation Reaches, which is the layer the metatheorem is stated about. paralever { … } ParProg ParM Reaches execPar execSeq what you write data: printable, footprint by a fold, obligation is a Bool closures: what the metatheorem is about every schedule, nondeterministically the two interpretations are what `par_seq_eq` equates nothing below ParProg is new: no axiom, no extra semantics

The surface language reserves very little. Memory is [l], a register is %n, and the only parallel form is a block of threads written parallel { … } | { … }, with parfor for one thread per index; there are also if/else and while … in. A program is a ;-chain, so paralever {s₁; …; sₖ} is right-nested seq and the term is a spine with one statement per rung. The single branching node is the par, and it is the only place independence is ever asked for.

Registers are thread-private. A par node hands every thread a copy of the register file and discards whatever the threads leave in it. That is why a thread writes its result rather than returning one, and it is the reason the independence obligation is about memory alone.

Here is the program from the matmul discussion, where all three threads read the same cell:

Cell 2 appears twice in the read list because two threads read it, and that is exactly the situation ∗ would reject. The footprint is rfl rather than decide because footprintOf is a fold over the syntax, so Lean computes it by unfolding definitions.

One piece of language-design trivia is worth recording, because it cost real time. In Lean, a syntax "foo" declaration reserves foo as a token for the entire project, so no declaration anywhere can then be named foo. Writing syntax "r " broke an unrelated test file, and a memory form written mem l made def mem impossible — which is the obvious name for a memory layout. Memory is now written [l], which reserves nothing at all.

Three ways to discharge the obligation

"Does it scale?" is the fair question, and the honest answer has three tiers.

decide on a concrete program. This is the headline experience and it is genuinely free, but it reduces concrete lists inside the kernel, so it scales with the program's size rather than with the difficulty of the argument. Measured on matrix multiplication:

n threads by decide
2 4 under a second
4 16 0.8 s
6 36 2.0 s
8 64 6.6 s
10 100 19 s

These are single-run elaboration times from one laptop on Lean 4.34.0, so read them as a growth curve rather than as absolute figures. So the ceiling is around a hundred threads, which is fine for a kernel and useless for a real array.

A lemma at symbolic n. When decide runs out you prove the obligation once for every size. The library ships a kernel vocabulary — an elementwise map, a broadcast, a reduction, a grid of reductions, a transpose, a 1-D stencil, a convolution with weights in memory, a dense layer, a bias add, an outer-product weight update — and each one carries a wfB lemma quantified over its sizes rather than checked at one of them.

Three things in those proofs are worth pointing out. The hypotheses are all range inequalities like bias + rows ≤ out, which is to say: the only thing the author must supply is a layout in which the output block starts after the input block ends. The conclusion is ∀ n, so the surface matmul kernel is well-formed at every size, where decide had given up at n = 10. And the dense layer is the matmul argument in miniature — every thread reads all of x, so ∗-disjointness rejects it and Bernstein does not, which is the whole reason the criterion was chosen.

Two tactics recur, and both were learned the hard way. A cell index like i * cols + j is nonlinear, so it has to be bounded with lin_lt before anything linear can be said about it. And the closing arithmetic goal goes to grind, not omega: Loc is an abbrev for Nat, omega does not see through it, and reports "no usable constraints" on goals that are in fact closed.

Over-approximation, where exactness is impossible. An access through a computed address reports the whole array as its footprint, and a conditional reports the union of both branches. This is where the antitonicity of Indep from earlier pays for itself: a widened read set can never create a conflict, so the result is conservative and never unsound. The price is precision, and it is a real price — A[B[i]] serialises, so histograms and sparse matrix-vector products are outside the method's reach.

The Lean embedding makes two smaller things possible. The same Boolean that discharges the obligation also licenses running the program on real threads, so a wall-clock benchmark compares two runs whose answers are equal by theorem. And when a program does have a race, #race p σ renders the counterexample as a widget in the editor, which is the subject of the next section.

When it fails: finding the race, and reading it

A rejection is not much use on its own. If the independence check fails, what a user is owed is the execution that proves it, and producing one is a search. The architecture is the one a validator uses: the search is untrusted and may return anything or give up, but what it returns is a schedule, and a schedule is checked by replaying it through the semantics.

The two phases of the race search Phase one walks the program tree and collects every fork whose children fail Bernstein, together with the cells that witness the failure; it is linear in the program. An empty result is itself the race-freedom proof and phase two never runs. A non-empty result names the conflicting cells, and phase two performs a bounded depth-first search aimed at them, returning a schedule. Replaying that schedule through follow yields a Reaches proof, so an unreplayable schedule claims nothing. p, σ phase 1 · scan walks the tree, linear empty ⇒ WellFormed holds. That list IS the proof; phase 2 never runs. phase 2 · search bounded, aimed at those cells Schedule untrusted — a guess Reaches proof or the replay fails and nothing is claimed non-empty, and it names the conflicting cells follow_sound Phase 1 is the obligation, so it cannot miss a race. Phase 2 is a heuristic that cannot lie: every schedule it returns is checked against the real `step`.

The division of labour is the part worth noticing. Phase 1 is not a conservative approximation that might warn spuriously: raceSites p σ = [] holds if and only if the program is well-formed. An empty result is a proof of race-freedom and a non-empty result is a genuine failure of the obligation, never a warning to triage. That is possible only because the obligation is itself decidable — phase 1 is Bernstein, evaluated.

Mechanically, getting the races out of a program is four steps and no search. Walk the term. At every par node, compute each child's footprint — the pair of read and write lists, by the same fold the obligation uses. Intersect the three Bernstein ways for each pair of siblings: writes against writes, writes against the other's reads, reads against the other's writes. Keep every pair whose intersection is non-empty, together with the cells in it, and recurse into the children. The result is one record per racing pair, naming the two footprints and the witnessing cells, and the whole walk is linear in the size of the program.

Here is the smallest interesting failure: two threads that each do some private work and then both write cell [9].

raceSites returns one record, and it is specific: the left child writes [10] and [9], the right writes [20] and [9], and the conflict is [9]. That is the whole diagnosis, and it comes out of an evaluation rather than an exploration. Phase 2 then has somewhere to aim.

In the editor you do not read that as text. #race p σ renders the counterexample as a widget in the infoview, which is the same report laid out as cards — one per executed step, with the changed cell highlighted, the two pending actions that clash shown side by side, and the abort line underneath:

That panel is not a picture of the widget. It is the widget's own Html value, the one #race hands the infoview, serialised to a page — so if the report ever changes shape, this changes with it.

Phase 2 is where the heuristics live, and because follow checks its output, no heuristic can make a false claim; at worst it fails to find something. That freedom matters, because the obvious search order is the worst possible one. A race needs two threads poised at conflicting accesses at the same instant, and the move that destroys that position is letting a thread run through its conflicting access — which is what a left-to-right search tries first. Since phase 1 already names the conflicting cells, the fix is to try those moves last, which is a reordering rather than a restriction, so nothing becomes unfindable:

program steps blind aimed
lateRace 200 405 257 ms 82 ms
lateRace 500 1005 3.5 s 494 ms
three 8 31 2.7 s 2 ms
three 60 187 — 34 ms

Same caveat as above: single runs on one machine, with — meaning the blind search was still running when I stopped it rather than that it returned nothing.

three is the case that makes the point. It forks three threads where the middle one is innocent, and blind, that innocent thread multiplies the backtracking: eight writes on each side already cost 2.7 seconds, and at twenty the blind search no longer finishes. Aimed, sixty writes take 34 milliseconds, because there is no backtracking left to multiply. The innocent thread's moves are never flagged so it simply runs, and the two guilty threads stop at their conflicting writes.

What comes out is an execution, so the report is one:

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

Two threads share step 2, and that is not a formatting accident: the check rejects the pair for being ready at the same instant, so the two actions genuinely belong to one step. Nothing else in the trace has two rows at one number, which is what makes the clash visible at a glance, and the values are shown because write [9] ← 2 against write [9] ← 1 is the contradiction.

The subtlest case is a read racing against a write, where both orderings leave the same heap and the executions differ only in what the reading thread observes. A report comparing final heaps would call that race harmless, which is why read observations are tracked too.

AutoPar: a chain in, a tree and a theorem out

Everything so far assumes you wrote the parallel block yourself. The analysis also runs in the other direction: given a sequential program, where could the forks go?

The first attempt at this is instructive, because it fails in a way no independence criterion could catch. Take the chain

[10] := 1;  [11] := 2;  %0 := [10]; %1 := [11]; [12] := R0+R1;  %2 := [11]; [13] := R2*2

A scheduler working statement by statement puts the two loads in one stage and the store consuming them in the next, by which point the fork has discarded the registers. The original leaves M[12] = 3 and M[13] = 4; the proposal leaves 0 and 0 — and the independence check returns true throughout. It is not wrong to: register writes do not survive a join in the sequential reading either, so the two readings agree and no race occurs.

The moral is not that the check is too weak. It is that memory and register dependences need opposite treatment, because a memory dependence is discharged by sequencing two statements and a register dependence is destroyed by sequencing them across a fork. So the unit of scheduling is not a statement but a register-closed segment: a load and the store consuming its register are one unit, never split. The pass is then four steps.

The automatic parallelizer, end to end A sequential chain of statements is cut into register-closed segments by units, grouped into an order-preserving two-level partition of stages and threads by plan, emitted as one parallel block per stage, and printed back as surface text. The theorem rewrite_sound connects the original chain to the emitted tree directly, and holds for every program because the gate is checked inside rewrite itself. a `;`-chain units plan ParProg paralever { … } the sequential program register-closed segments, never split across a fork stages × threads, order preserving by construction one parallel block per stage surface text again — the round trip closes rewrite_sound no hypothesis The gate lives inside `rewrite`, which returns the chain unchanged when the plan fails it.

units cuts the chain into segments, plan groups them into an order-preserving two-level partition of stages and threads, emit builds one parallel block per stage, and then a gate decides whether to commit. The theorem is this:

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

There is no hypothesis, and it holds for every program. That is possible because the gate lives inside rewrite, which returns the program unchanged when the check fails — the analysis is untrusted and the gate is proved, which is the same architecture as the race search. A second theorem carries well-formedness through the rewrite, which feeds the metatheorem and lifts this from the reference run to every schedule.

The depth it achieves comes with a certificate rather than an estimate. The dependence DAG is built in a single scoreboard pass — this is where Bernstein's three clauses get spent as the three kinds of edge — and its critical path is a lower bound on the depth of any schedule of those units, fork–join or otherwise. So "optimal" is a checked claim:

program threads × stages depth bound sequential optimal
two independent chains, written interleaved 2 × 1 3 3 6 yes
the N (short variant) 4 × 2 8 7 12 no
merge sort, four elements 3 × 2 12 12 16 yes
A[i] := A[i-1] + 1 1 × 1 6 6 6 yes

Two rows are doing real work. Merge sort is handed a flat ;-chain with the recursion already thrown away, and the pass recovers a two-stage tree that attains the bound — it reconstructs a recursion tree it never saw, because divide-and-conquer dependence DAGs happen to be series-parallel. And the loop-carried chain is the anti-vacuity case: A[i] := A[i-1] + 1 is genuinely sequential, and what the table shows is that the pass does not pretend otherwise.

The gate is also stricter than it needs to be, and the cost is measurable. It asks that no thread read a register an earlier thread writes, as a condition on raw read sets, which is stronger than the liveness the segmentation has already established. On a chain that reuses %0 across segments, the pass computes a plan of one stage and three threads at depth 2 — equal to the lower bound — and then throws it away for a sequential depth of 6. Fixing this properly means merging the children's register files at the join rather than discarding them, guarded by Bernstein on registers. Registers admit that and memory cells do not, because a cell is reached by a computed address, so the cell is its name.

Where the programs come from: MLIR

Everything above is about programs written in Paralever's own language, which is a problem if the goal is to say anything about code people actually wrote. The plan is one converter rather than one front end per language, and it is the next piece of work rather than a result I can report.

The interface is MLIR in its affine, scf and memref dialects, as text, so anything emitting that text feeds the converter: cgeist for C and C++, flang for Fortran, the upstream SCF-to-affine pass, or a hand-written .mlir file. This matters because hand-translating a benchmark suite is the dominant threat to validity here — the translation is itself part of what is being measured, and it is unverified.

The interface is deliberately not LLVM IR, which is the choice a compiler person will want justified. LLVM IR has unstructured control flow and phi nodes, and since ParM is inductive, arbitrary jumps are not representable in it at all; consuming LLVM IR would mean writing a loop structurizer first. Worse, lowering that far destroys the information the translation depends on, because the affine maps are gone by the time a loop has become a control-flow graph. At the affine level the correspondence is unusually close:

MLIR Paralever
affine.for with constant bounds parfor
affine.load / affine.store plus its affine map load / store at a literal cell
memref.global / memref.alloc a layout's buffer declaration
scf.if ifElse
omp.parallel / omp.wsloop the par node

The load-bearing alignment is the second row: an affine map is exactly the per-thread footprint function that the symbolic kernel lemmas ask for. A store to A[i, j] under the map (i,j) ↦ i*M + j gives the thread's write set directly, and the side conditions become the arithmetic goals the library already discharges.

The converter will be a Lean library and not a script, which is the part of the design I would defend hardest, and it is the same bet I made in PastaLean, where the Python-to-Lean translation is a Lean function for exactly this reason. A Lean function is an object you can state a theorem about, and the theorem to aim at is footprint preservation: every access the MLIR program performs lies inside the bound the produced program reports. That turns "trust the translator" from a caveat into a proof obligation, where a script emitting text could only ever have its output checked, never characterised.

What it is good for, and what it cannot do

The case for caring is the matmul shape. Disjoint writes over shared reads is what dense kernels, convolutions and attention blocks look like, and it is exactly the pattern that ∗-disjointness rejects and Bernstein admits. Checking a hand-written OpenMP pragma is the same obligation.

The sharper argument is about failure profiles. The OMPar paper (Kadosh et al., 2024) measures two conventional auto-parallelizers against ground-truth labels on the HeCBench suite and reports AutoPar at 71% precision with 17% recall and Intel's ICPC at 90% precision with 25% recall; of the 109 benchmarks AutoPar transformed, 63 passed compilation and 42 passed output verification. Its own LLM-based tool scored 67% accuracy on a 55-loop subset because it proposed parallelizing all 18 loops labelled non-parallelizable — though the authors then re-examined those labels and concluded 11 of the 18 were themselves wrong, which raised the score to 87% and is a fair reminder that the ground truth in this area is not solid either.

A tool whose wrong proposals fail to typecheck sits somewhere else on that spectrum entirely. It will refuse far more programs than it should, and when it does accept one, there is nothing left to verify afterwards. Those are very different things to be wrong about, and which one you want depends on whether a missed parallelization or a silently miscompiled one is the more expensive mistake.

Proving that parallel is also faster

"Same output" does not by itself explain why anyone runs the parallel version, so the cost side is proved as well — and it is a second theorem out of the same Bool, not a benchmark.

Two quantities are counted. Work is the number of memory operations along the run. Span is the number of rounds, where one round advances every thread that is ready, which is the standard work-span pair from Blelloch's cost model. The distinction is the one most easily got wrong: chunking a sum across eight threads still performs the same additions, so a correct parallelism result has to say that work is unchanged and only span falls.

The middle theorem, time_le, is the cost counterpart of par_seq_eq: for every program the check accepts, the parallel reading takes no more rounds than the sequential one. The third is the strict version — when both branches actually do something, the parallel reading takes strictly fewer rounds.

What makes those worth proving is how max enters. Most cost models simply stipulate that a fork costs the maximum of its branches, which makes "parallel is faster" true by unfolding a definition written to say so. Here the round relation never mentions max at all; it just advances every ready thread and collects the writes. The max is then recovered as a theorem, and its hypothesis is independence. An earlier version of the cost file did define span with a max at the fork and was therefore circular, which is how the distinction got noticed.

The lead program measures out as you would expect: nine memory operations either way, and nine rounds sequentially against seven in parallel, because the two squaring threads share their rounds instead of queueing. Both numbers are #eval in the snippet above, so neither is a claim about a machine.

Branches that interfere share no round and get no max, and the library exhibits that case too, which is what stops the cost theorem from holding for reasons unrelated to independence.

The limits are these, and none of them is hedged.

  • Locks, critical sections, atomics and barriers are not modelled, so a program whose race-freedom comes from a lock reads as racy here. That is the resource case from earlier, where the central equality is not merely unproved but false.
  • Unbounded loops are permanently out, because ParM is inductive and Lean 4 has no coinductive types.
  • Computed addresses cost precision. A[B[i]] reports the whole array, so scatters serialise.
  • There is no floating point. Footprints never inspect values, so every race verdict is unaffected; what suffers is numerical reproduction, so anything needing square roots has no honest encoding.
  • The span model is idealised: unlimited cores, no scheduling overhead, no memory hierarchy, unit cost per operation, and span zero for a computation that touches no memory at all. A proof that span decreases is not a proof that a program runs faster, and the repository's wall-clock numbers are observations rather than theorems.

What is next

Three things remain, in the order I would do them. Make registers survive the join, which removes the restriction that currently sends register-reusing chains back to sequential. Settle what the fork–join shape actually costs, where the N is the smallest witness and both the embedding bound and the hardness question are open. And build the MLIR converter, with footprint preservation as the theorem and DataRaceBench — 96 C and 166 Fortran microbenchmarks whose labels are in the filenames — as the first corpus.

The thing worth keeping from all of this is narrower than the theorem. What was missing was never a proof technique; it was a statement, for arbitrary programs with shared reads, machine-checked. The way to get it was to stop reasoning about schedules altogether and prove instead that a well-formed program has exactly one reachable outcome, computed by a function. Equivalence is then two lines, and by decide is the user's whole share of the work.

The code is at github.com/AnirudhG07/paralever.