This repository is a source-guided study of the mutual-exclusion algorithms in Gary L. Peterson's 1981 paper, “Myths about the mutual exclusion problem”. It contains Lean models and proofs for the paper's two-process algorithm, both for one passage and for repeated requests, and for the paper's finite n-process construction.
Mutual exclusion means that distinct processes never occupy their critical sections together. The proofs make every shared read and write a separate atomic step under sequential consistency, so they account for interleavings between the two reads in the two-process waiting test. They cover both fixed read orders used uniformly by the processes.
The public claim contract names six result families:
Peterson.peterson_mutual_exclusion: one-passage safety for two processes, with either initialturnvalue.Peterson.peterson_global_progress: a pending one-passage request leads to some new entry under explicit protocol fairness and critical-work completion premises.Peterson.Repeated.repeated_mutual_exclusion: safety across arbitrarily many requests and private restarts.Peterson.Repeated.repeated_request_entry: every repeated request reaches its own entry under the same two kinds of liveness premise.Peterson.NProcess.arbitrary_mutual_exclusion, supported bylevel_capacity: one-passage safety for every finite process count at least two, using individually atomic ascending peer scans.Peterson.Repeated.repeated_overtaking_bound, its zero-before-turn, after-turn, and bounded-service refinements, and the universal sharpness witnessrepeated_overtaking_sharp: a repeated request can be overtaken by at most one peer entry; zero occur before itsturnwrite, and one is attainable for every reviewed parameter choice.
Safety claims require no fairness. Progress and bounded service require weak fairness for continuously enabled protocol work plus eventual completion by a critical-section occupant. The overtaking count is an entry count, not a time, step, or read bound. The n-process result makes no progress or repeated-use claim. None of the results establishes weak-memory correctness or refinement to compiled code.
The algorithm and models relates the program counters and events to the source algorithms. The proof guide explains the six results and why their assumptions differ. Verification gives build and theorem-inspection commands. Related work records the narrow library and comparison work.
The reconstruction used an author-marked electronic restoration of the paper; identity with the publisher's version has not been established. The paper, images, and transcriptions are not redistributed here.
With elan installed, run from the repository root:
lake build Peterson.Verification Peterson.NProcessVerificationThe project pins Lean v4.34.0-rc2, CSLib, Mathlib, and the full transitive
dependency graph. STATUS.md distinguishes prior development checks
from qualification of a particular exported tree.
Erik Peterson initiated and directed this project. The research, prose, tooling, and Lean proofs are model-generated. Lean checked the proofs, and separate AI agents reviewed each model and theorem boundary against the source. Those reviews are fallible and can share errors. Lean's acceptance establishes the encoded propositions, not historical source faithfulness. There has been no independent human mathematical review.
Licensed under MIT.