# Verifying Mutual Exclusion Algorithms with Non-Atomic Registers
## 5 Modeling Examples with Non-Atomic Registers
### Tournament Tree-Based Mutual Exclusion Solutions
#### 5.3.2 The TT-S2 Algorithm  
The TT-S2's solution, which uses the adapted Szymanski algorithm [25] for 2 processes (see Figure 2) as the arbitration strategy, is presented in Figure 13. The model rests on the 3 bit per process output registers _bit_\(a[findex]\), _bit_\(w[findex]\), _bit_\(s[findex]\) SWMR safe registers (all initialized to 0). For simplicity, in Figure 13, flickering is rendered by the _Loop_ technique. The model was also prepared by using the \(Simple\) and the _Decoration_ flickering techniques as well. Figure 14 shows the TT-S2 model according to the _Decoration_ technique. The models in Figures 13 and 14 were found fully correct, from all the mutual exclusion properties, with the overtaking factor being \(ov=2^{\lceil\log_{2}N\rceil}-1\). Concerning the TT's solution based on the Lycklama and Hadzilacos (LH) algorithm [15] for \(N=2\) processes, the TT-S2's algorithm uses fewer shared space variables: 3 bit per process for TT-S2 instead of 4 bit per process required by TT-LH2 [15]. Figure 12: The TT-P2 algorithm with scrambling and flickering based on the _Decoration_ technique. The correct behavior of TT-S2 was also confirmed when flickering is expressed by the \(Simple\) technique. The TT-S2 models were verified until \(N=5\). Table 1 collects the execution time (\(ET\)) in sec, and the memory usage (\(MUI\)) in GB required by the model checker in the case \(N=5\), with the non-critical section (NCS) supposed to have a 0 duration. After having checked that the model behaves correctly with NCS which has an arbitrary duration (also infinite to model process termination), setting NCS to a 0 duration ensures maximal process competition (a process that exits the CS immediately re-enters to compete). TT-S2 was separately studied in the three cases of formulation of register flickering and for the three basic TCTL queries [20] (see also Section 3.2) devoted to checking the absence of deadlocks (satisfied), the mutual exclusion correctness (satisfied), and the assessment of the overtaking factor (\(ov=7\) when \(N=5\)). Figure 13: The TT-S2 formal model based on the SWMR safe registers \(a[]\), \(w[]\), \(s[]\) with flickering expressed by the \(Loop\) technique. As one can see from Table 1, the \(Simple\) and \(Loop\) techniques imply similar verification performances. The two flickering techniques are outperformed by the \(Decoration\) technique, which ensures a reduced verification time and a lower memory usage. It should be noted that the extra variables \(w?[. ]\) introduced by the \(Decoration\) technique do not cause a degradation of the model checking work because they normally stay at their false default value. As another significant case, the basic [PERSON]'s algorithm for \(N=2\) processes [4; 5; 14] used as the arbitration unit in a tournament tree (TT-D2) was considered. TT-D2 admits \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} & \multicolumn{2}{c}{Flickering} \\ \hline
**Query** & **ET (s)** & **MU (GB)** & **ET (s)** & **MU (GB)** & **ET (s)** & **MU (GB)** \\ \hline A[]!deadlock & 1554 & 16 & 1596 & 12 & 797 & 7 \\ \hline A[] (sum(!-pid)Process(i).CS) \(\Leftarrow\) 1 & 1120 & 16 & 1213 & 12 & 543 & 7 \\ \hline sup(Process(tp).L): x[tp] & 1509 & 19 & 1627 & 14 & 751 & 9 \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Model checking efficiency of the TT-S2 algorithm with the three flickering techniques and \(N=5\) processes. Figure 14: The TT-S2 formal model based on the SWMR safe registers \(a[]\), \(w[]\), and \(s[]\) with flickering expressed by the \(Decoration\) technique. both output variables (\(bool\ flag[findex]\), one per node of the TT) and non-output variables (\(finder\ turn[findex]\), one per ancestor node).