# Proving Properties of [PERSON]'s Algorithm for Mutual Exclusion of N Processes
## 2 Modeling a Mutual Exclusion Algorithm
### Extending the Dekker-2 Model to Non-Atomic Registers  
Due to the widespread diffusion of multi-port memory, low-cost devices like phone-cells and similar hardware equipment [8; 29], nowadays, a mutual exclusion algorithm is required to behave correctly without guaranteeing that the read and write operations on the same register are always atomic or indivisible. The problem is then to check the correctness of an algorithm in the presence of non-atomic registers, too. According to [4; 6], a first scenario/pattern is the so called Single Writer Single Reader (SWSR), where a read operation can co-occur with a write operation on the same register. SWSR can affect the behavior of Dekker-2, because of the use of output-only shared communication variables, namely, that a variable is only written by one process and read by the partner. Reading a variable during a write gives rise to the _flickering_ phenomenon [4; 6; 10]. Specifically, the reader achieves a nondeterministic value of the variable, belonging to the variable type domain. The SWSR pattern generalizes to the Single Writer Multiple Reader (SWMR) case when, as in the Dekker-N algorithm studied later in this paper, shared registers are still output variables, and a single writer can be in access of a register simultaneously to multiple reader processes. In this case, each concurrent reader can receive a possibly different nondeterministic value chosen in the type domain of the register. In the worst case Multiple Writer Multiple Reader (MWMR) scenario, simultaneous write operations on the same non-output variable determines the _scrambled_ register value [4; 6; 10]. Reading a variable affected by scrambling returns a nondeterministic value in the type domain of the variable. A mutual exclusion algorithm is said to be W-Safe [10] if it is immune to the possible flickering effects of the shared registers. The algorithm is called RW-Safe [10] when it is robust concerning both flickering and scrambling. In a recent paper [7], all the above-introduced patterns of non-atomic registers are modelled in Uppaal using three techniques: the _Simple_, the _Loop_, and the _Decoration_ techniques. In the Simple case, the writer first assigns the variable a nondeterministic value; then, this is followed by the assignment of the effective value. This way a read can effectively return the previous value, the flickered value, or the new value of the variable. In the Loop technique [6; 10], the writer first executes a loop, which eventually terminates. At each iteration, a nondeterministic value is temporarily assigned to the variable. At the loop termination, the effective value is assigned to the variable. A reader can then achieve the previous value, any flickered value, or the final assigned value to the variable. The Decoration technique decorates the model by adding Boolean variables _vx_, one for each shared communication variable \(x\), which indicate whether \(x\) is under writing or not. The writer first sets the decoration variable to true, then it assigns the effective value to the variable. In the next action, the decoration value is reset to false. Depending on the values of \(wx\) variables, a reader can access the last assigned value to the variable or a nondeterministic (flickered or scrambled) value. The three techniques are equivalent in practical use, although they have different repercussions on the state graph and the model checker. The Simple technique was used, e.g., in [16; 22]. The Decoration technique is more efficient. The decoration variables remain almost always at their default false value, except, temporarily, when a write operation is accomplished. In the rest of this paper, Decoration will be used for studying models under non-atomic registers. Figure 2 shows a modification of the Dekker-2 model according to the Decoration technique and the SWSR pattern of use of non-atomic registers. Three global variables were added, namely, \(bool\ wf[1,2]\) and \(bool\ wt\), which are associated with the \(flag[1,2]\) and the \(turn\) variables, respectively.