Formal Analysis of Bakery-Based Mutual Exclusion Algorithms

Lamport’s Bakery algorithm (LBA) represents a general and elegant solution to the mutual exclusion (ME) problem posed by Dijkstra in 1965. Its correctness is usually based on intuitive reasoning. LBA rests on an unbounded number of tickets, which prevents correctness assessment by model checking. Several variants are proposed in the literature to bound the number of exploited tickets. This paper is based on a formal method centered on Uppaal for reasoning about general shared-memory ME algorithms. A model can (hopefully) be verified by the exhaustive model checker (MC), and/or by the statistical model checker (SMC) through stochastic simulations. To overcome the scalability problems of SMC, a model can be reduced to actors and simulated in Java. The paper formalizes LBA and demonstrates, through simulations, that it is correct with atomic and non-atomic memory registers. Then, some representative variants with bounded tickets are studied, which prove to be accurate with atomic registers, or which confirm their correctness under atomic or non-atomic registers.