Formal verification of mutual exclusion algorithms in anonymous memory

This paper applied a formal method based on timed automata and the Uppaal toolbox to the specification and verification of mutual exclusion algorithms operating on anonymous memory. Anonymous memory is a challenging variation of shared memory where common variables (registers) do not have globally agreed-upon names. Instead, each process has its own view and naming for the shared registers. In addition, the cooperating/competing processes are supposed to be symmetric, that is, they execute the same code, and process identifiers are unknown. A recent proposal of Taubenfeld's mutual exclusion algorithm with $ \mathrm{m}\ge 7 $ ($ \mathrm{m} $ odd) shared anonymous registers was chosen as a concrete case study. Such an algorithm was informally studied by the authors together with the establishment of some possibility and impossibility results. This paper's first contribution was to confirm the correctness of the algorithm for $ \mathrm{N} = 2 $ processes when atomic registers are used. The solution no longer holds for a smaller number of registers, e.g., $ \mathrm{m} = 5 $, or when non-atomic registers are used. The paper also showed that for $ \mathrm{N} > 2 $, the algorithm violates the mutual exclusion. To extend the use of the algorithm to $ \mathrm{N} > 2 $ processes, this paper developed a novel organization where the basic solution for two processes is used as the arbitration unit in a binary, standard state-of-the-art tournament tree. Some timed variations of the model were considered, which permit the study of the algorithm under model checking and/or statistical model checking, for various values of the number N of processes.