# Proving Properties of [PERSON]'s Algorithm for Mutual Exclusion of N Processes
## 3 [PERSON]'s Mutual Exclusion for Any Number of Processes
### The Dekker-N Model with Non-Atomic Registers  
Figure 8 shows Dekker-N model decorated for using non-atomic registers. The following global declarations were added:  
//decoration variables--all false initially  
bool wt, //true when writing to top  
wp; //true when writing to penult  
bool wc[pid], //true when writing to c[. ],  
wn[pid]; //true when writing to next[.] \begin{table}
\begin{tabular}{c c c c} \hline \hline
**N** & **ov** & **ET (Sec)** & **M** \\ \hline
2 & 1 & 0 & 19 MB \\
3 & 2 & 0.3 & 27 MB \\
4 & 3 & 147 & 2.8 GB \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Observed overtaking bound for the model in Figure 5. \begin{table}
\begin{tabular}{c c c c} \hline \hline
**N** & **ov** & **ET (Sec)** & **M** \\ \hline
2 & 1 & 0 & 19 MB \\
3 & 2 & 0.3 & 27 MB \\
4 & 3 & 147 & 2.8 GB \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Observed overtaking bound for the model in Figure 5 with the NCS urgent location. Figure 7: Snapshot of the Uppaal model checker when Dekker-N of Figure 5 is verified with N = 3. The existence of only output shared communication variables implies that the model in Figure 8 takes care only of variable flickering due to the SWMR pattern. The model in Figure 8 was preliminarily debugged using the symbolic simulator of Uppaal. It emerged that due to flickering, the contents of the _next_ list can temporarily become cyclic; thus, the try() function can enter an infinite loop during the evaluation of predecessor processes. As a consequence, the try() function was modified according to Figure 9. A _visited_\(]\) array was introduced, and a possible loop in the _next_ list was discovered. Under these circumstances, try() terminates by returning false. After that, the model was verified with the model checker by first assuming NCS is a normal location. For \(N=2\), the model of Figure 8 was found to be W-Safe and fully correct. The result complies with the author's expectation stated in [1] that the mutual exclusion solution, when reduced to operate with two processes, would be equivalent to [PERSON]'s algorithm for two processes (see Sections 2.2 and 2.5). The experimental results confirm that the property holds both with atomic and non-atomic registers. The next verification step was to check the model in Figure 8 for \(N>2\). Unfortunately, already for \(N=3\), the decorated model loses the fundamental mutual exclusion property because more than one process can enter simultaneously the critical section (see Figure 10). In addition, the query that checks for the overtaking bound becomes inconclusive. Figure 8: The Dekker-N model with non-atomic registers. In the light of the observed results, the Dekker-N model was found to be incorrect for \(N>2\) when non-atomic registers are used. The model was then studied by making some changes (see Figure 11). In particular, considering the role played by the _top_ common variable, the provision of fencing _top_ was added, thus ensuring it behaves as a regular atomic variable. Reading _top_ will always return either the previous or the newly assigned value, but never a flickered value. Fencing is supposed to be supported by some low-level hardware mechanism that controls the access to the _top_ variable and enforces that  
Figure 10: Verification snapshot of the Dekker-N model with non-atomic registers for N = 3. Figure 9: The try() function adapted for working with flickering. read/write operations on _top_ are indivisible. In Figure 11, the _wt_ variable was eliminated, and any read to _top_ returns the last value stored in the variable. With these changes, Dekker-N becomes correct also with non-atomic registers. However, the adapted model suffers from state explosions when \(N=4\). The verification process was then continued by turning NCS into an urgent location. Correct behavior, that is, satisfaction of all the mutual exclusion properties, including fairness, was then observed until \(N=5\).