This project was done to illustrate the technique of proving a concurrent algorithm using the proof assistant PVS, see W.H. Hesselink: Mechanical verification of Lamport's Bakery algorithm. Science of Computer Programming 78 (2013) 1622-1638. Slides are available. The PVS specification consists of two files, one for safety and one for liveness. This is proved in a PVS dump file, which can be inspected with PVS (version 5.0). The algorithm has been extended to allow infinitely many processes using concurrently extendable arrays. This is verified in a second dump file, which is only a minor modifcation of the first one. A paper about it appeared in Science of Computer Programming 78 (2013) 1622-1638.
In September 2014, I gave a new progress proof of the Bakery algorithm for N processes in which the progress is quantified by means of bounded Unity. The throughput factor is linear in N, whereas the individual delay is quadratic in N. The PVS dump file for this new proof also contains the theory of bounded Unity.
In 2004, G. Taubenfeld wrote "The Black-White Bakery Algorithm and related bounded-space, adaptive, local-spinning and FIFO algorithms." This appeared in the Proceedings of the DISC 2004, volume 3274 of LNCS, pages 56-70. In September 2015, I verified the adaptive version of the algorithm, Figure 3, in my paper "Correctness and concurrent complexity of the Black-White Bakery Algorithm", to appear in Formal Aspects of Computing (2016). The PVS dumpfile is available.
Taubenfeld's BW Bakery Algorithm is an elegant algorithm, but it is not a concurrent program because it treats all variables as shared and does not obey the principle of single critical reference. My concurrent program of 2015 faithfully represents Taubenfeld's algorithm, but the encoding of mycolor in the last bit gives awkward waiting conditions. November 2020, I developed a new version with a more natural encoding and simpler waiting conditions, in the PVS dumpfile.
Lamport's Bakery Algorithm needs unbounded tickets. Taubenfeld's bakery algorithm uses tickets bounded by 2N, where N is an upper bound of the number of competing threads, but it requires a complicated juggling of the tickets. Recently, Alex Aravind proposed a bakery algorithm for mutual exclusion with tickets that can be two's complement machine integers with wrap-around, together with an extension for group mutual exclusion. We have proved that the algorithm for mutual exclusion is correct if the number of available machine integers is more than 4N. Correctness is proved with the PVS dumpfile. In the version for group mutual exclusion, the distances between tickets can get larger than in the version for mutual exclusion, because the threads in a session (although having the same forum) may have different tickets. This algorithm has been proved to be correct if the number of machine integers is more than 8N + 8. This is proved in the PVS dumpfile. A paper with these two algorithms is in preparation.
Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink