# Proving Properties of [PERSON]'s Algorithm for Mutual Exclusion of N Processes
## 2 Modeling a Mutual Exclusion Algorithm
### TCTL Verification Queries of Dekker-2  
A model like Dekker-2 of Figure 1 can preliminarily be studied (debugging) using the Uppaal symbolic simulator [20], which permits one to observe graphically the evolution of the process instances and the corresponding values of the global and local data declarations, when selected or randomly chosen transitions occur. The simulator can reveal some bad properties. For example, a deadlocked state can be reached, but one cannot conclude the model is correct. Model correctness can only be determined by exhaustive verification based on the preliminary creation of the (hopefully finite) model _state graph_[18; 19]. The state graph is a timed transition system, where nodes represent the possible execution states of the model, and the arcs denote the possible timed or instantaneous transitions between states. Each node contains a _data part_ and a _time constraint part_. The data part depends on the sizes and the values of the global and local data declarations. The time constraint part is a clock inequality system that describes all the possible time instants at which the state node can be reached. Proving properties of a model rests on the model checker that systematically traverses all the execution paths in the state graph, which is strongly influenced by the nondeterminism degree of nodes, that is, the number of possible exiting transitions at each node.  
Property checking of the Dekker-2 model can be practically accomplished by issuing TCTL queries [18] as noted in the following. First of all, Dekker-2 makes no hypothesis on the relative speed of processes.  
1. _Mutual exclusion_. At most one process at a time can enter its critical section. The following query can be used.  
A[] (sum(i:pid)Process(i).CS) \(<=1\)  
This asks if it is always true (or invariantly) that in all the states of the state graph the number of processes simultaneously found in their CS location is less than or equal to 1.  
Dekker-2 satisfies the mutual exclusion property.  
2. _Absence of deadlocks_. One of the following TCTL queries can be issued.  
A[]!deadlock  
E\(<>\) deadlock  
The first query asks the model checker to assess if invariantly that there is no deadlocked state in the state graph. The second query demands to verify if there _exists_ at least one deadlocked state in the state graph. The absence of deadlocks is confirmed by the first query that gets satisfied, or, equivalently, by the second query that terminates unsatisfied.  
Dekker-2 has no deadlock.  
3. _Absence of starvation_. A competing process should always wait for a bounded time before achieving the permission to enter its critical section. The following _suprema_ query [21] can be issued.  
sup[ Process(tp).L ] : x[tp]  
This query asks to determine the maximum value of the clock x[tp] when the process tp is found in the L location (see Figure 1) that immediately precedes CS.  
Dekker-2 guarantees 1 is the maximum waiting time for a competing process (_overtaking bound_), thus confirming the algorithm is fair.  
4. _Liveness_ 1. Every process eventually enters its critical section. For Dekker-2 the following queries can be used:  
E\(<>\) Process(1).CSE<> Process(2).CS  
Both queries are satisfied, thus giving more arguments to the mutual exclusion property and to the absence of starvation.  
5. _Liveness_ 2. A process in its NCS should not forbid other processes to enter the critical section. The following query can be used.  
E<> exists(i:pid)Process(i).NCS && exists(j:pid)Process(j).CS  
This query asks if there exists at least one state where some process \(i\) is in its NCS whereas some other process \(j,j\
eq i\), is in its CS.  
Based on the responses to the above-described TCTL queries, Dekker-2 was found a correct mutual exclusion algorithm when atomic registers are used. All the experiments are carried out on a Win11 Pro desktop platform with Dell XPS 8940, Intel i7-10700 (eight physical + eight virtual cores), [EMAIL_ADDRESS] GHz, and 32 GB RAM.