# Verifying Mutual Exclusion Algorithms with Non-Atomic Registers
## 4 Modeling Non-Atomic Registers in Uppaal
### Modeling Flickering in SWMR Registers  
Three techniques were developed. In the first one (\(Simple\) technique), the writer first assigns a non-deterministic value to the register, belonging to the type of the variable, followed by the assignment of the true value. This corresponds to a non-atomic write operation [32; 33; 34] (e.g., [34] page 3). The technique (see Figure 4) is exemplified in the model of Figure 2, when the process \(i\) exits the NCS and has to establish the value 1 (true) in the output variables \(a[i]\) and \(w[i]\) and again, before while_P4, 0 (false) in \(a[i]\). The yellow part of the three commands in Figure 4 expresses the non-deterministic selection of a bit value and its assignment to the temporary variable \(v\), whose lifetime is restricted to the command itself. Figure 4: An excerpt of using the \(Simple\) flickering between NCS and the while_P4 location of Figure 2.  
Figure 3: An Uppaal snapshot witnessing correctness of the model in Figure 2.  
_Simple_ flickering allows an overlapping read, e.g., of \(a[i]\) to acquire the non-deterministic value instead of the true value. Despite its simplicity, the technique permits multiple readers to actually achieve different values of the register. In fact, due to concurrency and interleaving of process actions (it is recalled that all the execution paths in the state graph are automatically analyzed by the exhaustive model checker), a reader can obtain the previous value, another the non-deterministic (flickering) value, another one the effective written value. The simple flickering technique was adopted, e.g., in [11; 14]. The second technique (_Loop_ technique) [32] is used, e.g., in [29]. In this case, the writer realizes a loop of non-deterministic assignments to the register (see Figure 5) before writing the true value. The _Loop_ proposal assumes the loop eventually terminates. As a consequence, this technique aims to ensure that multiple readers can achieve, during an overlapping write, a possible different flickering value. The use of the _Loop_ technique causes no problem in the Uppaal model of a mutual exclusion algorithm. The model checker, indeed, can consider what happens for any duration of the loop. The third proposed technique in this paper is the _Decoration_ one, which reproduces the intents of the _Loop_ mechanism by first decorating the model with boolean variables (0 false, 1 true) to indicate whether a given register is actually under writing or not. For example, in the model of Figure 2, the boolean arrays \(wa[pid]\), \(ww[pid]\) and \(ws[pid]\) are introduced (all false initially), which correspond to the output variables \(a[pid]\), \(w[pid]\), and \(s[pid]\), respectively. When the writer, e.g., of \(a[i]\) wants to assign a value to \(a[i]\), it puts true to the corresponding decoration variable \(wa[i]\) and assigns the value to \(a[i]\). Then, following this step, \(wa[i]\) is reset to false to reflect the writing to \(a[i]\) is finished. The technique gives the reader the responsibility of checking the value of \(wa[i]\). If it is true, the reader generates and uses a non-deterministic value \(v\) for the register (see Figure 6). Otherwise, the actual value of the register is used. This paper advocates the use of the _Decoration_ technique for rendering flickering. It has general applicability and can reduce the non-determinism degree in the model: a non-deterministic choice \(v\) is only used when the corresponding output variable is effectively under writing, as witnessed by the associated decoration variable \(w?[.]\). It can be expected a reduction both in the memory space required by the state graph and  
Figure 5: An excerpt of using _Loop_ flickering between NCS and the while_P4 location of Figure 2.  
Figure 6: An excerpt of using flickering _by Decoration_ in the model of Figure 2.  
(see also later in this paper). To reduce model cluttering, in Figure 6, instead of two distinct edges (see the connection, e.g., between while_P4 and P5), an equivalent disjunction is used in the guard of a single edge.