# Proving Properties of [PERSON]'s Algorithm for Mutual Exclusion of N Processes
## 3 [PERSON]'s Mutual Exclusion for Any Number of Processes
### Transforming Dekker-N into Uppaal by Using Atomic Registers  
The following are the basic global declarations of the Dekker-N Uppaal model:  
\[\text{const int N = 4; //example  typedef int[1, N] pid;  typedef int[0, 2] value;  //shared communication variables  pid top = N, penult = 2;  value c[pid]; //all zero by default  pid next[pid]; //all 1 by default  urgent broadcast Chan synch;  clock x[pid];  
As one can see, the \(next[]\) list was changed, with respect to [1], to have only process indexes in [1, N] as values. In fact, the \(next[1]\) value is immaterial and can be assigned itself as the next value. This provision reduces the number of possible values of \(next[]\), which in turn tends to improve the burden of the model checker.  
The Uppaal model is organized in two timed automata: \(Bootstrapper\) and \(Process\).  
_Bootstrapper_ (see Figure 3) is a parameterless automaton that has the responsibility of model initialization. Its initial location is purposely declared as committed. This way its exiting edge will certainly be taken _before_ any other edge in the \(Process\) models. Recall that \(Process\) locations (see, e.g., Figure 1) are normal or urgent locations. The function initialize() is detailed in Figure 4. The \(Bootstrapper\), after the edge with initialize(), enters an anonymous normal location from which it will take no part in the subsequent model evolution.  
Figure 5 shows the _Process_ automaton equipped with the sole parameter: _const__pid__i_. Atomic registers are automatically ensured by the atomic actions of Uppaal TA-based modeling language. Atomic actions are executed one at a time and in any order. Consequently, considering that only one communication variable can be accessed/modified in a guarded command, only one write or read operation can occur at any time.  
A notable point in Figure 5 is the introduction of the busy waiting BW location that precedes the first loop on the predecessor processes when \(c[i]==1\). This provision was made to reduce the partial order degree in the state graph that inevitably would accompany the continuous checking, in the model, of communication variables by chained urgent  
Figure 4: The initialize() function.  
Figure 5: The Process automaton of Dekker-N based on atomic registers.  
Figure 3: The Bootstrapper automaton.  
locations. From BW, the _Process_ automaton tentatively exits when there is a chance all the predecessor processes of \(i\) are in the not interested status: \(c[pre]==0\). Toward this, the try() function of Figure 6 was prepared, which optimistically checks the exiting condition from BW. Optimism is related to the fact that multiple shared communication variables are simultaneously checked. However, model concurrency and nondeterminism are correctly ensured given that _Process_\(i\), after abandoning the BW location through the synchronization on the urgent and broadcast _synch_ channel, evaluates one-at-a-time the single variables of the try() loop, and it immediately re-enters BW if any predecessor is found in the ready status (\(c[pre]>0\)).  
In Figure 5, it is worth noting the provision to reset as soon as possible local variables after their use. This action can improve model checking by ensuring variables return to their default status.  
The system configuration of the Dekker-N model is achieved by the following declaration: system Bootstrapper, Process; which automatically creates one instance of the _Bootstrapper_ and \(N\) instances of the _Process_ automaton indexed by the integers in [1, N].