A lock that lets exactly one thread into the critical section at a time. Two threads, one shared flag — and the whole question is: over every way their steps can interleave, can both ever be inside at once? The engine enumerates the entire interleaving space exhaustively: an atomic acquire is safe over all 8 reachable states; make the acquire non-atomic and a race appears in 4 steps. Down the center, data flows: two threads go in, the model checker runs, the verdict comes out. The blue team builds the lock; the red team breaks its atomicity.
source Dijkstra, Cooperating Sequential Processes (EWD123, 1965) — the paper that named the critical section and the mutual-exclusion problem — cs.utexas.edu/~EWD/…/EWD123.html. Manuscript, AMBER. Rendered, not quoted.
Each thread is a tiny program over one shared flag locked. The correct lock makes acquire atomic: a single indivisible step that reads-and-sets in one shot (hardware test-and-set / compare-and-swap).
| at | step | enabled when | effect |
|---|---|---|---|
| 0 | acquire | locked = 0 | locked ← 1, enter |
| 1 | ▓ in CS | always | locked ← 0, leave |
| 2 | done | — | terminal |
The checker explores every reachable global state (pc0, pc1, locked). Live:
The mutex is the lock that serializes the critical section — correct only when the acquire is truly atomic. Hardware gives that atom directly (test-and-set); in pure software you build it from ordinary reads and writes.
That software construction is the neighbouring sphere: the-peterson's algorithm wins mutual exclusion for two threads with only loads and stores plus a turn variable — no atomic instruction. Same guarantee, one layer down. Each sphere is the next one's premise.
The blue team's live check: re-run the exhaustive explorer over the active lock and over both reference locks, and confirm mutual exclusion. If red makes the acquire non-atomic, this badge is where it goes red.
The inputs are two identical threads — T0 and T1 — each wanting the same critical section, and one shared bit locked (0 = free, 1 = held). A schedule is any interleaving of their atomic steps; there is no global clock, so every merge of the two step-sequences is a legal run.
The invariant we demand of the whole space: at most one thread in the critical section in every reachable state. That is what you feed the panel below.
Step either thread by hand, or auto-run. Every verdict is computed live from the transition rules over the real reachable-state graph — never looked up.
What the machine proves, exhaustively: an atomic lock enforces mutual exclusion across all 8 reachable states — both-in-CS is unreachable, and it is deadlock-free. Drop atomicity (read-then-set as two steps) and a 4-step race puts both threads inside. The lock also gives progress: a waiter is blocked only while the holder is inside, and is enabled the instant it releases.
The blue witness (left) confirms this live; the red team (right) attacks the one thing that makes it work — the atom.
Worse, the atom itself is an assumption: pure-software locks (Peterson, Dekker) are correct only under sequential consistency. Real CPUs and compilers reorder memory, so without fences/barriers the store-then-load ordering the proof relies on can be observed out of order — and the lock silently breaks. assumed: the model here is sequentially consistent.
"A boolean flag is enough to lock." Cut. A plain read the flag, then set it races — two threads both read 0 and both enter. Mutual exclusion needs the read-and-set to be one atomic step. (That is exactly the tamper below.)
"Disabling interrupts makes any code a critical section." Cut, corrected. True on a uniprocessor only; on SMP the other cores keep running. You still need a real lock across cores.
"Peterson's algorithm works on modern hardware as written." Cut. It assumes sequential consistency; without memory fences, store/load reordering breaks mutual exclusion.
The red team's move: make the acquire non-atomic — split it into read the flag then, separately, set the flag. Now an interleaving lets both threads read "free" before either sets it. The blue witness (window 7) is watching.