|
|
|
The Boulangerie Algorithm in PlusCal/TLA+
Leslie Lamport
Last modified on 21 July 2015
|
The boulangerie algorithm is a variant of the bakery algorithm published in
Yoram Moses and Katia Patkin:
Under the Hood of the Bakery Algorithm:
Mutual Exclusion as a Matter of Priority
22nd International Colloquium on Structural Information
and Communication Complexity (SIROCCO 2015).
I had already written a PlusCal version of the bakery algorithm
for the TLA+ Hyperbook, along with
a formal
proof that it satisfies mutual exclusion. The proof
was checked
with TLAPS,
the TLA+ proof system.
Just for fun, I decided to modify the algorithm and the proof
for the boulangerie algorithm. Here are the two
algorithms and their proofs:
Bakery.tla
Bakery.pdf
- The source file of the bakery algorithm specification
and its pretty-printed pdf version.
Boulanger.tla
Boulanger.pdf
- The source file of the boulangerie algorithm specification
and its pretty-printed pdf version. Comments at the
beginning of the file describe the process of writing the algorithm
and constructing the proof.
|
|
Back
|