Correctness and concurrent complexity of the Black-White Bakery Algorithm
Wim H. Hesselink · Formal Aspects of Computing · 2016
Abstract Lamport’s Bakery Algorithm (Commun ACM 17:453–455, 1974 ) implements mutual exclusion for a fixed number of threads with the first-come first-served property. It has the disadvantage, however, that it uses integer communication variables that can become arbitrarily large. Taubenfeld’s Black-White Bakery Algorithm (Proceedings of the DISC. LNCS, vol 3274, pp 56–70, 2004 ) keeps the integers bounded, and is adaptive in the sense that the time complexity only depends on the number of competing threads, say N . The present paper offers an assertional proof of correctness and shows that the concurrent complexity for throughput is linear in N , and for individual progress is quadratic in N . This is proved with a bounded version of UNITY, i.e., by assertional means.