Supplemental Material

for

Deconstructing the Bakery to Build a Distributed State Machine

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.