Statistical Model Checking of Lamport’s Bakery Mutual Exclusion Algorithm

This work develops a formal method for modelling and verifying concurrent/parallel systems, focusing on mutual exclusion algorithms. Formal modelling is based on Uppaal timed automata. Verification is usually based on model checking, that is, the exhaustive analysis of all the execution states and state paths of the system model. However, in cases where model checking is impossible to apply for state explosions, statistical model checking based on simulations can be used. As a concrete example, the paper formalizes Lamport’s bakery mutual exclusion algorithm, which cannot be studied by model checking for the large amount of data it generates. Properties of the algorithm are then investigated by statistical model checking. The algorithm is separately modelled and verified with atomic and non-atomic registers. The paper demonstrates that the algorithm remains correct also when it is employed on low-cost devices like cell phones, which depend on multi-port memory with relaxed control on the simultaneous accesses to the same non-atomic register.