# Proving Properties of [PERSON]'s Algorithm for Mutual Exclusion of N Processes
## 2 Modeling a Mutual Exclusion Algorithm
### Reducing Dekker-2 on to Uppaal  
Figure 1 (see also [22]) shows the Uppaal model [18; 19; 20] of \(Process(i)\) when atomic registers are used. \(Process\) is a parameterized template model (automaton) with one single parameter: \(const\)\(pid\)\(i\); where \(pid\) is a sub-range type for the integers from 1 to N:  
const int N = 2; //number of processes typedef int[1, N] pid;At the system configuration time, two instances of Process will automatically be created and denoted as Process(1), and Process(2), which share global declarations for types and variables. The primitive types int, bool, and clock; arrays data structures of these types and channels; and an array of channels are available. Each Process instance owns its local declarations.  
Shared communication variables are introduced in the global environment of the Uppaal model.  
A process instance is a state machine composed of _locations_ (circle in Figure 1) and _edges_ (arrows in Figure 1) that connect locations. Each edge hosts a _guarded command_ that is made up of three optional attributes: (1) a _guard_ (Boolean expression, true by default if it is missing, green colored), (2) a channel _synchronization_ (azure colored), and (3) an _update_ part (blue colored) that is an ordered list of assignments to variables and clock resets. The guarded command is the _atomic unit_ of concurrency in Uppaal models. Like in Petri nets Petri (2017), an enabled command _can_ be taken, but it is not forced to do it. Different locations can be used to provide the time behavior to a model. Time is usually expressed using clock variables (see the clock \(x[i]\) in Figure 1). Clocks can be reset in an update section of a command. Then, they all grow at the same rate as the global time of a model. They measure the _relative time_ elapsed from their last reset. In a normal location (see NCS in Figure 1), the automaton can stay an arbitrary, possibly infinite, time. The dwell time of a normal location can be constrained by the use of an _invariant_ (see the invariant \(x[i]<=1\) attached to CS in Figure 1). An urgent location (flagged with an internal U) must be abandoned immediately, without any time passage. Another kind of location to be exited without time passage is the committed one (Han, 2018), which is similar to an urgent location. However, committed locations have priority and are guaranteed to be abandoned before urgent locations.  
Interactions between TA can be based on unicast or broadcast channels. A unicast channel can have a sender that executes the send signal operation (symbol!) and a receiver that can accept the synchronization signal (symbol?) sent by a sender. Unicast channels obey to _rendezvous_. Only when both sender and receiver are ready to communicates, a synchronization can be taken. The first process that arrives to the synchronization point has to wait for the partner to arrive. Broadcast channels have one sender and zero, one, or multiple receivers. The sender of a broadcast channel never waits for receivers to be ready. This way, such kind of channels are useful for one-way, asynchronous interactions. Figure 1 uses one single broadcast channel _synch_ that purposely has one sender and no receiver. Channels can be declared to be urgent (e.g., the _synch_ channel in Figure 1). In this case, an enabled synchronization must be taken without time passage. Among the actions that can be executed at the same time, the order of execution is nondeterministic. For example, it is nondeterministic when exiting from the location BW in Figure 1 with \(turn!=j\) (_synch_  
Figure 1: Uppaal model for Dekker-2 (2017).  
being urgent), especially when this occurs simultaneously from an urgent location in the partner model.