Projects & explorations

Peterson’s algorithm

category: projects

Lean models and proofs for a classic mutual exclusion algorithm.

Two processes want to use the same critical section. Each can read and write shared variables, but their steps may be interleaved. Peterson’s algorithm coordinates access using two flags and a turn variable.

Project source Explore the algorithm

Two processes, one critical section

category: explorations

The model treats shared reads and writes as separate atomic steps under sequential consistency. Progress depends on explicit fairness and completion assumptions.

Choose each atomic step and share the resulting trace.