Peterson’s algorithm
Animated interleavings, atomic memory accesses, and the invariants behind mutual exclusion.
Different execution orders. At most one process in the critical section.
The two reads in the waiting test can observe memory at different times.
The invariant excludes simultaneous entry under every valid schedule.
A pending request can be overtaken by at most one peer entry.
At most n − k processes can have passed level k without clearing Q.
Code and manual execution
N-process filter lock
N-process mutual exclusion
Animation starts when this chapter is active.
Model details
Each action is atomic: write Q, write TURN, read one peer Q cell, or read TURN. A marker crosses a boundary only when the model records that level as passed.
At level k, at most n − k processes remain past the boundary before clearing Q. The final level therefore admits at most one.
Lean proofs and model assumptions
Each shared read and write is individually atomic under sequential consistency. Both processes use the same fixed read order. These animations show selected valid schedules; the Lean safety proof covers every reachable state in the model.
Safety does not require fairness. Eventual entry additionally requires weak fairness for continuously enabled protocol steps, including exit writes, and completion of critical work. The overtaking bound counts peer entry events, not time or steps. The n-process theorem covers one-passage safety only.
The browser model is a tested TypeScript transcription, not a Lean proof checker. The results do not establish weak-memory or compiled-code correctness.
Erik Peterson initiated and directed the project. AI models generated the research, prose, tooling, and proofs. Lean checked the proofs; separate AI agents reviewed the model and theorem boundaries. These reviews are fallible, and the source interpretation has not received independent human mathematical review.