Verifying Mutual Exclusion Algorithms with Non-Atomic Registers

The work described in this paper develops a formal method for modeling and exhaustive verification of mutual exclusion algorithms. The process is based on timed automata and the Uppaal model checker. The technique was successfully applied to several mutual exclusion algorithms, mainly under the atomic memory model, when the read and write operations on memory cells (registers) are atomic or indivisible. The original contribution of this paper consists of a generalization of the approach to support modeling mutual exclusion algorithms with non-atomic registers, where multiple read operations can occur on a register simultaneously to a write operation on the same register, thus giving rise to the flickering phenomenon or multiple write operations can occur at the same time on the same register, hence determining the scrambling phenomenon. The paper first clarifies some consistency rules of non-atomic registers. Then, the developed Uppaal-based method for specifying and verifying mutual exclusion algorithms is presented. The method is applied to the correctness assessment of a sample mutual exclusion solution. After that, non-atomic register consistency rules are rendered in Uppaal to be embedded in the specification methodology. The paper goes on by presenting different mutual exclusion algorithms that are studied using non-atomic registers. Algorithms are also investigated in the context of a tournament tree organization that can provide standard and efficient mutual exclusion solutions for N>2 processes. The paper compares the proposed techniques for handling non-atomic registers and reports about their application to many other mutual exclusion solutions.