Supplemental Material


Deconstructing the Bakery to Build a Distributed State Machine

Leslie Lamport
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:

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.
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 this web page.