Black-White Bakery Algorithm Made RW-Safe

Lamport’s Bakery algorithm is a well-known, simple, and elegant solution to the mutual exclusion problem for N ≥ 2 concurrent/parallel processes. However, the algorithm generates an unbounded number of tickets, even when only 2 processes are arbitrated. Various proposals in the literature were introduced to bound the number of tickets. Anyway, almost all these proposals prove to be correct when operated with atomic registers (AR) only. They become incorrect when working with non-atomic registers (NAR), as may occur in embedded hardware platforms with multi-port memory and relaxed memory-bus control, such as microcontrollers, FPGA-based systems, or specialized network devices. A notable solution with bounded tickets is Taubenfeld’s Black-White Bakery (BWB) algorithm. BWB relies on tickets which are couples <number,mycolor> where mycolor can be Black or White and number ranges in [0, N]. BWB, too, was confirmed, through informal reasoning, it is correct with AR only. The original contribution of this paper is a reformulation of BWB, which is formally modelled and exhaustively verified by timed automata in the Uppaal toolbox. In the reformulation, a ticket’s couple is coded as a single integer, and decoded and processed according to the BWB logic. The reformulated BWB remains fully correct with AR regardless of the number N of processes, but it is also correct with NAR for N = 2 processes. As a further original contribution, the paper demonstrates that the BWB version for 2 processes can be embedded in a general, state-of-the-art solution, based on a binary tournament tree (TT), to become AR/NAR correct, that is, RW-safe, for any number of processes. However, due to model complexity, the correctness of the TT versions of BWB, that is, based on atomic and non-atomic registers, is mainly studied by stochastic simulation of the formal model reduced to actors in Java.