Deconstructing the Bakery to Build a Distributed State Machine
Last modified 7 January 2022
The paper for which this web page provides supplemental material can
be found here. It contains a sequence of
five algorithms, each informally derived from the preceding one.
Further details of these algorithms are available as indicated here:
Stephan Merz has turned the informal proof from the expanded
version of the paper into a machine-checked TLA+ proof.
He also wrote a TLA+ proof that the distributed bakery algorithm
implements the deconstructed bakery algorithm.
Those proofs can be found on
- An expanded version of the paper
This version has an appendix containing a detailed informal
proof that the deconstructed
bakery algorithm satisfies mutual exclusion.
- Precise specifications of algorithms
- PlusCal specifications of what I consider to be the two most
interesting of the paper's five algorithms: The deconstructed bakery
algorithm and the distributed bakery algorithm. The specification of
the deconstructed algorithm also includes a formal definition of the
invariant that appears in the appendix of the expanded version of the
paper. Here are links to the source files and pretty-printed pdf
versions of these specifications:
Deconstructed Bakery: source pdf
Distributed Bakery: source pdf
The specification of the deconstructed bakery should be read first.