Two processes, one critical section

Two processes want to use one critical section. Their steps can be interleaved, so checking whether the other process is interested is not enough by itself. Peterson’s algorithm uses an interest flag for each process and a shared turn variable to coordinate entry.

The model

The Lean model makes every shared read and write a separate atomic step under sequential consistency. In particular, another process can take a step between the two reads in a waiting test.

Mutual exclusion means that distinct processes never occupy their critical sections together. The source also studies progress: when a pending request eventually leads to entry.

This transcription writes the acting process’s own identity to turn; it waits while the peer’s flag is true and turn still names itself. Both processes use the same fixed short-circuit read order. Either initial turn value is permitted.

The program counter records an unfavorable first read at betweenReads. That observation can become stale before the second read. Critical completion is a separate private step; the flag remains true until the following exit write.

The browser implementation is tested against a separate transition table and exhaustive reachable-state checks. It does not run Lean, and interacting with it does not prove the Lean theorems.

Read the pinned atomic-step specification, safety theorem peterson_mutual_exclusion, and progress theorem peterson_global_progress.

Assumptions and limits

• Safety requires no fairness assumption.
• Conditional global progress requires weak fairness for continuously enabled protocol work and eventual completion by each critical occupant. It guarantees some new entry after a pending observation, not entry by a named requester or a delay bound. Choosing buttons does not enforce fairness.
• This stepper covers two processes making one passage each. It has no restart, repeated-use mode, or n-process extension.
• The results do not establish correctness under weak memory or refinement to compiled code.

Source and attribution

These notes summarize the linked repository; they are not an independent proof review. Erik Peterson initiated and directed the project. The research, prose, tooling, and Lean proofs were generated by AI models. The repository reports Lean acceptance and reviews by separate AI agents; those reviews are fallible and can share errors. Lean acceptance applies to the encoded propositions, not historical fidelity to the original paper. The work has not received independent human mathematical review.

Algorithm and modelsProof guideVerification