# Proving Properties of [PERSON]'s Algorithm for Mutual Exclusion of N Processes
## 2 Modeling a Mutual Exclusion Algorithm
### Semantic Aspects of a Reduced Uppaal Model  
A fundamental concern of a mutual exclusion algorithm like Dekker-2 reduced in Uppaal as shown in Figure 1 is the proper reproduction of nondeterminism and action interleaving of concurrent/parallel processes. From this point of view, process actions are purposely embedded in the guarded commands of the exiting edges of urgent locations. Therefore, the duration of atomic actions is zero time units. Regardless of the memory model, no more than one shared communication variable can be accessed in a single command. This constraint does not apply to local variables. Multiple local variables, supposed to be held in CPU registers, can be operated together in the same command without problems. A reduced model, such as Dekker-2 in Figure 1, is both concurrent and time sensitive. Time is allowed to pass in the NCS, CS, and busy waiting locations like BW. Exiting from NCS (which is also the initial location) is modelled by a spontaneous edge. This way a process can spend an arbitrary time in doing actions unrelated to the critical section. An infinite time in NCS models process termination. It has to be verified that a process in NCS should never forbid other processes from entering their critical section. Busy waiting can be modelled by a normal location as BW in Figure 1 or by a looped urgent location like L. The former solution is preferable from the model checker point of view, because it reduces the nondeterminism (or partial order) degree of the nodes of the state graph [18; 19]. When the awaited condition holds (\(turn!=j\)), the BW is abandoned without time passage through the urgent synchronization \(synch!\). More generally, exiting from a busy waiting location can be guarded by a \(try()\) function that, optimistically, checks a complex condition based on multiple shared communication variables. In this case, the exiting is immediately followed by the evaluation, step-by-step and non-deterministically, of the compound condition. At any step that would contradict the exiting from the busy waiting location, the latter is immediately re-entered. The second solution with L urgent generates a zero-cycle [22; 28] in the model (logically present also in Algorithm 1), which is an infinite series of returns in L in zero time. However, in a concrete implementation of Algorithm 2, actions could not have a zero duration, and the zero-cycle in the model has the effect of compromising model liveness. It is possible, virtually, that a process in L never will reach the CS. However, the analysis of the model in the time domain will confirm the full correctness of Dekker-2. Timing is also used in the CS (critical section) location. First of all, the particular duration of the dwell time of a process in CS does not matter. During a critical section, concurrent competing processes can execute as many atomic and instantaneous actions of the mutual exclusion protocol as they want, or they can wait in a busy waiting location like BW. The adopted Uppaal approach purposely assumes a critical section consumes one time unit. This way, by using a clock variable per process (see the global array \(x[]\) in Figure 1, which has one clock for each process instance), which gets reset just before entering a CS, it becomes possible to assess the overtaking bound, that is the number of times a competing process is by-passed by competing partners, by checking the maximum value of the clock of a process when it finds itself in L (a location immediately preceding CS). In the case of an unfair mutual exclusion algorithm, and the continual arrival of competing processes (e.g., the NCS duration is always 0 time units), the overtaking factor can become infinite. For an (almost) fair algorithm, even under the worst case arrivals of processes, the waiting time in L for any competing process is finite, and the overtaking factor bounded. As a consequence, the particular duration of NCS, which occurs in parallel with the critical sections, does not affect the overtaking bound.