# Verifying Mutual Exclusion Algorithms with Non-Atomic Registers
## 3 Uppaal Modeling with Atomic Registers
The dwell time in a normal location can be constrained by attaching to it an _invariant_ (see the CS location with the invariant \(x[i]\leq 1\) in Figure 1). The process can remain in the location provided the invariant (a logical condition built on data or clocks) continues to be satisfied. An urgent location must be abandoned without time passage. Among the current urgent locations of a set of processes, Uppaal ensures they will be exited in a non-deterministic order. Therefore, for a proper reproduction of the concurrency of the actions of multiple processes, actions can be purposely attached to the edge commands exiting from urgent locations. This way action interleaving and partial order of a concurrent/parallel execution are naturally ensured. It is worth noting that exiting from a normal location with an enabled guard and urgent output synchronization (see, e.g., the AWP11 location in Figure 1) is equivalent to exiting from an urgent location. Thus, non-determinism regulates the execution of all types of urgent actions. The model in Figure 1 is time-dependent in the following aspects. In the non-critical section (NCS), which is also the initial location, a process can remain an arbitrary time, also infinite. This way, process termination gets naturally modeled. In the critical section (CS) location, the dwell time is constrained to be exactly 1 time unit. This choice was adopted to measure the overtaking factor (_ov_) of processes easily. Each process is associated with a clock \(x[i]\), which is reset just before entering the CS. A target process (_tp_) can be established and its clock \(x[tp]\) observed for measuring the _ov_. All the times the process \(tp\) starts competing, its clock \(x[tp]\) is reset (through the \(reset(i)\) function). Then, \(x[tp]\) gets incremented as competing processes gain the CS before \(tp\). Finally, the maximum value of \(x[tp]\) is measured just before \(tp\) enters its CS (see the \(L\) location in Figure 1). Busy-waiting situations are required in the P11, P22, and P31 points of the Prologue section and the E0 point of the Epilogue of the mutual exclusion protocol (see Algorithm 1). Whereas an internal spin-lock of a process running on a separate core can be practically tolerated, it should conveniently be avoided in an Uppaal model for verification efficiency (by reducing the number of distinct execution paths to be analyzed). The adopted solution consists of introducing a normal location (see AWP11, AWP22, AWP31, and AWE0 in Figure 1) for each busy waiting. Instead of immediate looping, the exit from the location is controlled by a guard function like \(tryAll()\) in AWP11. This function checks \"optimistically\" (by possibly simultaneously consulting multiple shared variables) if a potential exit from the busy waiting location is possible. If yes, the urgent and asynchronous _synchl_ signal is used to force the exiting without further time passage. However, following the exit from the busy waiting location, the effective evaluation of the await (possibly complex) condition is carried out, component by component. At any moment the condition for abandoning the busy-waiting would be found to be false, the busy-waiting location is immediately re-entered. Algorithm 3 collects all the try functions used in Figure 1.  
```
bool tryAll(\(\{\)  bool tryAny\(\{\)  int j;  int j;  for(j = 1; j <= N; ++j)  for(j = 1; j <= N; ++j)  if(flag[j] > 2)  if(flag[j]==4)  return false;  return true;  return false;  return true;  return true;  return false; } //tryAll //tryAny //tryInf
```  
**Algorithm 3** The try functions of the model in Figure 1.