Supplemental Material
for
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 prettyprinted 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 machinechecked 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.