The boulangerie algorithm is a variant of the bakery algorithm published in
Under the Hood of the Bakery Algorithm: Mutual Exclusion as a Matter of Priority
by Yoram Moses and Katia Patkin
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
The source file of the bakery algorithm specification and its pretty-printed pdf version.
Boulanger.tla
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.