# Verifying Mutual Exclusion Algorithms with Non-Atomic Registers
## 6 Conclusions  
This paper proposes techniques for specifying register flickering and scrambling in mutual exclusion algorithms executing in non-atomic memory [22]. The techniques are embedded into a formal methodology for modeling and exhaustive verification of mutual exclusion protocols. The methodology is based on timed automata [16] and the Uppaal model checker [19; 20; 21].  
With respect to similar formal methods, e.g., based on process algebra and model checking [22], this paper argues the proposed approach is more intuitive yet powerful to use.  
Several examples were thoroughly modeled and verified using the consistency rules of non-atomic registers described in this paper. Observed results comply with results reported in [22]. Some solutions were also extended for them to be used in the context of the tournament tree (TT) organization [11; 14; 27]. TT provides a standard and efficient way of supporting mutual exclusion for \(N>2\) processes by relying on particular solutions for \(N=2\) processes used as the arbitration unit. As an original result of this paper, although [PERSON]'s algorithm [25] was proved by our work to be incorrect with both atomic and non-atomic registers, its version for \(N=2\) processes, modified according to the indications  
\begin{table}
\begin{tabular}{l c c c c c c} \hline \hline  & \multicolumn{2}{c}{\(Simple\)} & \multicolumn{2}{c}{\(Loop\)} & \multicolumn{2}{c}{\(Decoration\)} \\  & \multicolumn{2}{c}{**Flickering**} & \multicolumn{2}{c}{**Flickering**} & \multicolumn{2}{c}{**Flickering**} \\ \hline
**Query** & **ET (s)** & **MU (GB)** & **ET (s)** & **MU (GB)** & **ET (s)** & **MU (MB)** \\ \hline A[]!deadlock & 439 & 4 & 1431 & 4 & 15 & 147 \\ \hline A[] (sum(:pid)Process(i).CS) \(<=1\) & 312 & 4 & 888 & 4 & 10 & 149 \\ \hline sup(Process(tp).L): \(\{\)qp\(\}\) & 379 & 5 & 1087 & 4 & 14 & 185 \\ \hline \hline \end{tabular}
\end{table}
Table 2: Model checking efficiency of the TT-D2 algorithm with the three flickering techniques and \(N=5\) processes.  
\begin{table}
\begin{tabular}{l c c c} \hline \hline  & \multicolumn{2}{c}{\(Decoration\)} \\  & \multicolumn{2}{c}{**Flickering**} & \\ \hline
**Query** & **Result** & **ET (s)** & **MU (GB)** \\ \hline A[]!deadlock & satisfied & 176 & 1 \\ \hline A[] (sum(:pid)Process(i).CS) \(<=1\) & satisfied & 119 & 1 \\ \hline sup(Process(tp).L): \(\{\)qp\(\}\) & 7 & 135 & 1 \\ \hline \hline \end{tabular}
\end{table}
Table 3: Model checking efficiency of the TT-D2 algorithm with the \(Decoration\) technique and \(N=6\) processes.  
in [31], is not only fully correct with non-atomic registers but exploited as the arbitration unit in TT is capable of furnishing correct mutual exclusion for \(N>2\) processes.  
The paper also reports some experimental results concerning the verification efficiency of three flickering techniques. The so-called _Decoration_ technique, which is a novel contribution of this paper, emerged to be the best one in all the carried-out experiments.  
Ongoing and future work will be geared to the following points: first, to continue applying the developed non-atomic register consistency techniques to other mutual exclusion algorithms; second, to make a detailed experimental comparison of the proposed method with the approach described in [22]; third, to consider the modeling of further consistency rules of non-atomic registers as proposed, e.g., in [35].  
This research received no external funding.  
Data Availability Statement: Data are contained within the article.  
The author declare no conflict of interest.