TLA+ Specifications and Proofs for Deconstructing the Bakery to Build a Distributed State Machine

In his paper 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:

Only safety properties of the algorithms are proved. The first step is to prove type correctness of the algorithms (based on more precise statements of type correctness than those defined in the original specifications). Then, we prove an inductive invariant for each algorithm. For the deconstructed Bakery algorithm, this is the invariant I provided in Lamport's specifications, although we prepare its proof by showing two auxiliary inductive invariants. For the distributed Bakery algorithm, we define an inductive invariant that in particular tracks the sending and reception of messages between the different processes. Finally, we show mutual exclusion of the deconstructed Bakery algorithm, and also that every step of the distributed Bakery algorithm can be mapped to a (possibly stuttering) step of the deconstructed Bakery algorithm.

This page provides the following resources:

Stephan Merz