### TLA+ Specifications and Proofs for Deconstructing the Bakery to Build a Distributed State Machine

In his paper Deconstructing the Bakery to Build a Distributed State Machine, Leslie Lamport introduces a generalization of the well-known Bakery algorithm for mutual exclusion and then derives the algorithm for implementing a distributed state machine from the paper Time, Clocks, and the Ordering of Events in a Distributed System as a refinement of that generalized algorithm. The paper uses pseudo-code descriptions to introduce the algorithms and contains rigorous, but informal proofs of their correctness. The paper, as well as specifications written in PlusCal, are available from Lamport's Web site.

This page provides machine-checked proofs for the deconstructed and the distributed Bakery algorithms introduced in Lamport's paper. The specifications are minor variations of those written by Leslie Lamport and available on his site. Specifically, they differ in the following ways:

• I moved a few definitions of operators that are common to the two algorithms to a separate module and proved a few lemmas about these operators. Also, the operators Nodes and OtherNodes of the distributed Bakery algorithm have been renamed to Procs and OtherProcs, which are the names used in the deconstructed Bakery algorithm.
• In addition to Lamport's specification of the deconstructed Bakery algorithm, I use a variant in which ticket numbers are chosen atomically. In particular, that version is used for the proof that the distributed Bakery algorithm refines the deconstructed Bakery algorithm, given that the distributed algorithm draws ticket numbers atomically.
Only safety properties of the algorithms are proved. The first step is to prove type correctness of the algorithms (based on more precise statements of type correctness than those defined in the original specifications). Then, we prove an inductive invariant for each algorithm. For the deconstructed Bakery algorithm, this is the invariant I provided in Lamport's specifications, although we prepare its proof by showing two auxiliary inductive invariants. For the distributed Bakery algorithm, we define an inductive invariant that in particular tracks the sending and reception of messages between the different processes. Finally, we show mutual exclusion of the deconstructed Bakery algorithm, and also that every step of the distributed Bakery algorithm can be mapped to a (possibly stuttering) step of the deconstructed Bakery algorithm.