# Verifying Mutual Exclusion Algorithms with Non-Atomic Registers
## 1 Introduction
Previous work mainly addressed the correctness assessment of mutual exclusion solutions using atomic registers and a preliminary technique for dealing with non-atomic registers. The original contribution of the current paper is to propose more general techniques to ensure the consistency of non-atomic registers [22]. The new techniques are rendered in the Uppaal modeling method, and their practical usefulness is demonstrated by modeling examples. The new proposed techniques address specifically non-atomic registers where multiple writers and multiple readers (MWMR) can overlap their execution on the same register, or a single writer and multiple readers (SWMR) can access a register simultaneously. The MWMR case can cause the value of the register to be _scrambled_[22; 23], that is, writing in it a non-deterministic value belonging to the register type domain, which can be acquired by readers. The SWMR case is the source of the _flickering_ phenomenon [22; 23], where each distinct overlapping reader can obtain a non-deterministic valuation of the register value. Different mutual exclusion solutions are considered for modeling and correctness assessment. As an example, the paper shows that [PERSON]'s algorithm proposed in [24] is correct under atomic registers but becomes incorrect when using non-atomic registers. Inaddition, the improved solution reported in [25], designed to ensure a linear waiting time for a competing process and which admits a reduced shared data space, effectively guarantees a linear _overtaking factor_ (the number of times competing processes can bypass a given waiting process and precede it in entering their critical section), but, for \(N>2\) processes, it does not fulfill mutual exclusion properties even with atomic registers. From the algorithm in [25], a version for \(N=2\) (S2) processes is derived in this paper, and its correctness is demonstrated using either atomic or non-atomic registers. Both the Peterson for \(N=2\) processes (P2) [10] and the Szymanski algorithm for \(N=2\) processes are then exploited, separately, as the arbitration unit in a standard and efficient tournament tree (TT)-based solution [11; 14; 26; 27], thus addressing \(N>2\) processes. As an original result of this paper, it is shown that whereas TT-P2 is incorrect when both scrambling and flickering of non-atomic registers are admitted, the TT-S2 solution, which can only be affected by flickering, represents a fully correct mutual exclusion algorithm also with non-atomic registers. The paper compares the model checking efficiency of three proposed flickering techniques for non-atomic registers with the so-called _Decoration_ technique, which is a novel proposal of this paper, that emerges as the best one for application generality, flexibility, and execution performance. The formal modeling approach developed in this paper is similar to the process algebra method based on the mCRL2 model checker [28], described in [22]. However, this paper argues that the presented approach is more intuitive to use because it rests on processes modeled graphically by timed automata, which are more amenable to understanding and preliminary debugging activities. Visual modeling and exhaustive model checking, that is, systematically investigating all the possible (hopefully finite) execution paths/states in a model, represent the strength of the developed formal method. The paper is structured as follows. Section 2 describes the consistency rules of non-atomic registers. Section 3 presents the basic formal method, centered on Uppaal, for modeling and verification of mutual exclusion algorithms. A few timed computational tree logic (TCTL) queries are suggested for checking the properties of a mutual exclusion solution. Section 4 proposes some techniques for modeling scrambling and flickering, respectively, in MWMR/SWMR non-atomic registers. The techniques are rendered in Uppaal to be easily integrated within the basic formal method described in Section 3.