# Proving Properties of [PERSON]'s Algorithm for Mutual Exclusion of N Processes
## 3 [PERSON]'s Mutual Exclusion for Any Number of Processes  
In [1], [PERSON] proposed a fair mutual exclusion algorithm for \(N\geq 2\) processes. Fairness is based on a linked list of precedence. After completing its critical section, the process places itself at the bottom of the list, and lower ranking competing processes are moved one place up in the list. Since the list is consulted concurrently by processes,  
Figure 2: The Dekker-2 model using non-atomic registers and the Decoration technique. movements in the list are tricky. In particular, moves are carried out in such a way that all processes in the list continue to be visible to all the other processes. The process is placed at the bottom and temporarily occurs twice in the list. Due to this operation, the bottom is not used as the list end. The penultimate element is effectively the last element, and the bottom is the next element to it. The algorithm uses the following shared communication variables with the shown initialization:  
int top = N, penult = 2;  
int[0, 2] c[1..N] // all 0 initially  
int[0, N] next[1..N]; // for all j in [1..N], next[j] = j - 1  
The \(c[]\) array is analogous to the \(flag[]\) array of Dekker-2. However, instead of the two Boolean values 0 (false) and 1 (true), three values are now used to express the status of a process \(i\). When c[\(i\)]=0, the process is not interested in the critical section. The value c[\(i\)] = 1 denotes the process that starts competing (ready status). Finally, when c[\(i\)] = 2, the process is \(up\) to enter its critical section. All the communication variables are output or behave as output variables. Each \(c[. ]\) variable is associated with a distinct process that has the responsibility of writing its status information in it. The process can change the \(top\), \(penult\), and \(next\) variables at its abandoning of the critical section. All the variables, though, can be checked concurrently by all the processes. Algorithm 3 reproduces in pseudo-code [PERSON]'s algorithm for \(N\geq 2\) processes (Dekker-N). A competing process \(i\) acquires permission to enter its critical section when _predecessor_ processes, from the top of the \(next[]\) list up to the one immediately before \(i\), are found in the status of being not interested in the critical section (\(c[pre]==0\)). Such a situation must be assessed twice: with \(c[i]=1\) and then with \(c[i]=2\). After that, the process \(i\) must wait until _posterior_ processes (from \(next[i]\) to penultimate) are at most in the ready status (\(c[post]<2\)). On exiting from its critical section, the process \(i\) is placed at the bottom of the list, provided \(i\) is not already the bottom. If required, process \(i\) becomes the next \(bottom\), and the previous \(bottom\) is established as the penultimate of the list. After that, if the process \(i\) was the \(top\), the \(top\) variable is updated to the next element of \(i\). Otherwise, the previous \(i\) will have the next \(i\) as the next element. Finally, process \(i\) sets its status to not interested in the critical section (\(c[i]=0\)), and the NCS is re-entered. Dekker-N will be first reduced to Uppaal under atomic registers, and its properties, including fairness, will be investigated. Then, the algorithm will be adapted to work with non-atomic registers, and its correctness will be deeply verified.