Deconstructing the Bakery to Build a Distributed State Machine

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.

This page provides the following resources:

- Lamport's paper presenting the algorithms and an informal proof that the deconstructed Bakery algorithm satisfies mutual exclusion.
- A first module contains basic declarations and operator definitions that are
used for both algorithms, as well as lemmas about these operators.

[ TLA+ module | PDF ] - The following modules contain the specification of the deconstructed Bakery
algorithm, corresponding to figure 3 of Lamport's paper, and a proof that
the algorithm ensures mutual exclusion. This is the
atomic

version of the deconstructed Bakery algorithm, corresponding to the pseudo-code shown in figure 3 of the paper.

[ PlusCal specification | PDF | TLA+ proof of mutual exclusion | PDF ] - The following modules contain the specification of the distributed Bakery
algorithm, corresponding to figure 4 of Lamport's paper, and a proof that
this algorithm refines (the safety part of) the generalized Bakery algorithm
whose specification appears above.

[ PlusCal specification | PDF | TLA+ proof of refinement | PDF ] - In the following variant of the deconstructed Bakery algorithm,
processes choose their ticket numbers non-atomically. This is the PlusCal
specification that is provided on Lamport's page, and we prove that
this variant also ensures mutual exclusion. I believe that one could
prove that a non-atomic variant of the distributed Bakery algorithm refines
this variant of the generalized Bakery algorithm, but I have not checked this.

[ PlusCal specification | PDF | TLA+ proof of mutual exclusion | PDF ]

Stephan Merz