# Proving Properties of [PERSON]'s Algorithm for Mutual Exclusion of N Processes
## 1 Introduction  
In his paper [1], [PERSON] reveals the way in which he invented the first mutual exclusion algorithm for two processes. The solution was prepared, in a few days, in response to a [PERSON] well-stated problem, of which the proponent and others were very doubtful of its practical solvability, about how to orchestrate two processes (machines), using only software means, in such a way that they never access some shared data simultaneously. The code fragment for accessing/modifying shared data is called the process of _critical section_. [PERSON]'s solution was formulated in 1960, and [PERSON] made it public in 1962 [2, 3]. [PERSON] stressed the mutual exclusion solution had to fulfill the following additional properties: (a) absence of deadlocks among the competing processes; (b) absence of starvation which in turn means bounded waiting for a process willing to enter its critical section; (c) the solution should be independent from the relative speed of processes; and (d) read/write operations on shared variables should be indivisible. The last requirement concerns the use of atomic registers. Nowadays [4, 5, 6, 7], considering the use of multi-port memory, low-cost devices like cell phones [8] and similar hardware,where multiple read/write operations on the same register can occur simultaneously, it is felt that the operation of a mutual exclusion algorithm should be correct also in the presence of non-atomic registers. Another requirement often added to the above specifications is that (d), a process not interested in the critical section, should not forbid another process to enter its critical section. [PERSON]'s algorithm for two processes represents the fundamental solution on which many subsequent proposals were developed. Two specific variants of the basic [PERSON]'s algorithm are described in [9; 10]. A mutual exclusion algorithm for \(N\geq 2\) processes was designed by [PERSON] in [11], although the author himself recognized the possibility for a competing process to suffer unbounded waiting. Better solutions for \(N\geq 2\) processes were presented by [PERSON] [12], [PERSON] [13], and [PERSON] and [PERSON] [14], with a guarantee of bounded waiting, e.g., linear in the number \(N\) of waiting processes. [PERSON] in [15] proposed a more compact and elegant solution than the [PERSON]'s basic algorithm and a more general solution for \(N\geq 2\) processes. The correctness of many proposed mutual exclusion algorithms was mainly based on atomic registers and informal mathematical arguments. However, intuitive reasoning, except for simple cases, cannot predict all the possible interleaving of actions that can occur in a nondeterministic concurrent/parallel system. This is testified, for example, by the different indications of the overtaking factor for a competing process in [PERSON]'s solution for \(N>2\) processes (see [16]). Formal modeling and verification approaches are now widely recognized as an essential tool for the assessment of the properties of a mutual exclusion solution. For example, the use of assertions and theorem provers was advocated in [5; 10], whereas the use of model checkers with an exhaustive verification of the execution states of the processes of a concurrent system regulated by a mutual exclusion protocol was explored, e.g., in [6; 7]. The work described in this paper relies on the use of Timed Automata (TA) [17] in the context of the Uppaal model checker [18; 19; 20] because process modeling and interactions are felt more intuitively when expressed graphically using TA instead of using, e.g., process algebra as in mCRL2 [6; 21]. On the other hand, the Uppaal support of (a subset of) the Timed Computational Tree Logic (TCTL) [18] is simple yet powerful for capturing and checking properties (queries) of a TA-based mutual exclusion model. A unique feature of our TA-based approach is the possibility of investigating the interaction between timed and concurrent aspects in a model.