# Verifying Mutual Exclusion Algorithms with Non-Atomic Registers
## 3 Uppaal Modeling with Atomic Registers  
The following summarizes the formal approach adopted in this work for modeling and verification by model checking of a mutual exclusion algorithm reduced onto the timed automata language of the Uppaal toolbox [19; 20; 21]. The goal is to clarify the basic modeling infrastructure based on atomic registers, on top of which the operation of non-atomic registers will subsequently be embedded. The reader is referred to [11; 13] for more details about the rationale of the transformation of a mutual exclusion solution into an Uppaal model. A concurrent system with \(N\) processes is represented by a network of \(N\) Process(\(i\)) instances (timed automata), whose unique identifier \(i\) ranges from 1 to \(N\). The processes execute the same algorithm and interact with one another through the _shared communication variables_ used by the mutual exclusion protocol. Under atomic modeling, any single access (read/write) to a shared communication variable constitutes an _atomic action_. Therefore, a boolean expression involving multiple shared variables has to be evaluated component-by-component. An exception to the above rule is represented by the management of local variables of a process. Multiple local variables, supposedly held in hardware registers, can be operated simultaneously. [PERSON]'s algorithm for \(N\geq 2\) processes, proposed in [24] (page 624, Figure 2), is chosen for demonstration purposes (see Algorithm 2). It is based on output variables only: \(flag[i]\), \(1\leq i\leq N\). The solution follows the metaphor of a waiting room with two doors: _door_in_ and _door_out_. Initially, the _door_in_ is open and the _door_out_ is closed. Each process can be in one of 5 states (values 0.4 of \(flag[i]\)). State 0 means the process is not interested in the critical section. In state 1, the process wants to enter the waiting room. All the processes that want to enter the waiting room at the same time are allowed to pass through the _door_in_. In state 2, a process checks if other external processes want to enter. If no other processes are sensed, the process closes the _door_in_, passes to state 3, and the _door_out_ is opened. From the waiting room, processes exit the _door_out_ according to the order of their IDs. In state 4 the process exits the waiting room and enters the CS. When finishing with the CS, the process switches again to the state 0. At the time the last process exits from its CS, the initial door situation is re-installed. The **await0** condition at the E0 line takes into account the correction suggested in [31] (page 675). The Algorithm 2 was analyzed informally by the author in [24], and a linear overtaking factor (that is the maximal number of times a process in the waiting room will be by-passed by other competing processes) was predicted: \(ov=N-1\), as a direct consequence of enforcing an exit order from the waiting room directly dependent on the process IDs. Figure 1 shows a transformation of [PERSON]'s algorithm of the generic \(Process(i)\) in an Uppaal-timed automaton model made of _locations_, _edges_, and _clocks_. Time can be controlled by _clock_ variables, which measure relative amounts of elapsed time. A clock can be reset. After a reset, the clock grows at the same rate as all the clocks in the model. Edges are annotated by _guarded commands_. Guards (green-colored in Figure 1) are logical conditions that enable an edge to be possibly taken. A command can contain a synchronization on an urgent broadcast (asynchronous) channel _synch_! (azure-colored) that constrains the edge to be exited as soon as the guard evaluates to true. A command can also have an update part (blue-colored), which consists of an ordered list of assignments and clock resets. Locations can be normal (see NCS, AWP11, and so forth) or urgent (flagged with an internal U). The automaton (_Process_ instance) can remain in a normal location for an arbitrary time.