# Verifying Mutual Exclusion Algorithms with Non-Atomic Registers
## 1 Introduction  
The mutual exclusion problem [1; 2; 3] arises each time \(N\) concurrent/parallel processes (or threads) have to access in read/write to a shared resource \(R\). For predictability of \(R\) evolution, only one process at a time must be allowed to use \(R\). The code segment executed by a process when using \(R\) constitutes its _critical section_ (CS). Several algorithms (protocols) have been proposed in the literature for solving the mutual exclusion problem. In this paper, the interest is on algorithms that are based on software mechanisms only, that is, without the support of special hardware instructions like _test-and-set_. Each particular protocol (see Algorithm 1) consists of a (hopefully minimal) number of _shared communication variables_ (registers), suitably initialized, and a _prologue_ section where the process signals its interest in accessing the resource and starts competing with peers. The process remains (waits) in the prologue until the conditions on the shared variables permit it to enter its critical section. Waiting is normally achieved by \(busy-waiting\) loops, with the process actively checking selected variables until an awake situation is sensed which enables it to exit from the busy-waiting. After the critical section, an _epilogue_ section is executed, which resets registers, thus allowing other competing processes to possibly resume movement toward their critical section. In the non-critical section (NCS) the process executes actions independent from the resource \(R\). For generality, in the NCS the process can also terminate its execution. The first \"pure\" software solution to the mutual exclusion problem was due to [PERSON] [4; 5] and was concerned with the handling of \(N=2\) processes. [PERSON] proposed a solution [6] for \(N>2\) processes, although with a possible unbounded waiting time for a competing process. [PERSON] [7], [PERSON] [8], and [PERSON] and [PERSON] [9], respectively, developed improved solutions to the [PERSON]'s algorithm to ensure a bounded waiting time for a competing process, possibly linear in \(N\), e.g., [9]. A more simple and elegant solution than [PERSON]'s algorithm for \(N=2\) processes and a general solution for \(N>2\) processes were proposed by [PERSON] in [10]. All such algorithms were mainly studied using atomic registers and through informal mathematical reasoning. Atomic registers have indivisible read/write operations. That is, it is not possible that such operations can overlap on the same register. In addition, informal reasoning has great difficulty in assessing the general properties of a mutual exclusion algorithm. This is due to the intrinsic non-determinism or interleaving that characterizes the execution order of actions of concurrent/parallel processes, which almost always is impossible to predict. This can explain, for example, the different conjectures about the waiting time of a competing process in [PERSON]'s algorithm for \(N>2\) processes [11]. As observed by [PERSON] in [1], studying the correctness of a mutual exclusion algorithm by assuming atomic read/write operations on registers is a way of achieving mutual exclusion by relying on a lower-level mechanism of mutual exclusion. On the other hand, the widespread diffusion of multi-port memory devices [12] (e.g., cell phones and similar low-cost hardware devices) mandates to adopt mutual exclusion solutions that can tolerate multiple simultaneous read/write operations on the same register. Therefore, the more general context where to check properties of mutual exclusion algorithms is that of working with non-atomic registers and their associated consistency rules. This paper significantly extends previous authors' work [11; 13; 14; 15] aimed at the development of a formal method for modeling and verification of mutual exclusion algorithms based on timed automata [16] and model checking [17; 18], using the Uppaal toolbox [19; 20; 21] for the practical experiments.