next.png up.png previous
Next: An Assertional Language for Up: Constraint Multiset Rewriting Previous: The language


An example: The Ticket Mutual Exclusion Protocol

The ticket protocol is a mutual exclusion protocol designed for multi-client systems operating on a shared memory. The protocol is based on a first-in first-served access policy. The algorithm is given in Fig.1 (where we use $P~{\bf \vert}~Q$ to denote the interleaving parallel execution of $P$ and $Q$, and $\langle\cdot\rangle$ to denote atomic fragments of code).
Figure 1: The Ticket Protocol: $n$ is a parameter of the protocol.
\begin{figure*}
{\footnotesize\centerline{$
\begin{array}{cc}
\begin{array}{l...
...rray}\right.\\
~~~~{\bf end.}
\end{array}
\end{array}
$\ }}
\end{figure*}
The protocol works as follows. Initially, all clients are thinking, while $t$ and $s$ store the same initial value. When requesting the access to the critical section, a client stores the value of the current ticket $t$ in its local variable $a$. A new ticket is then emitted by incrementing $t$. Clients wait for their turn until the value of their local variable $a$ equals the value of $s$. After the elaboration inside the critical section, a process releases it and the current turn is up.pngdated by incrementing $s$. During the execution, the global state of the protocol consists of the current values of $s$, $t$, and of the local variables of $n$ processes. As remarked in [10], even for $n=2$ (only 2 clients), the values of the local variables of individual processes as well as $s$ and $t$ may get unbounded. This implies that any instance of the scheme of Fig. 1 gives rise to an infinite-state system. The algorithm is sup.pngposed to work for any value of $n$, and it should also work if new clients enter the system at running time. Multiset rewriting allows us to give an accurate and flexible encoding of the ticket protocol. Let us first consider a single shared resource controlled via the counters $t$ and $s$ as described in Section 2.3. The infinite collection of admissible initial states consists of all configurations with an arbitrary but finite number of thinking processes and two counters having the same initial value ($t=s$). The specification is shown in Fig. 2. The initial configuration is the predicate $init$, the seed of all possible runs of the protocol. The counters are represented here via the atoms $count(t)$ and $turn(s)$. Thinking clients are represented via the propositional symbol $think$, and can be generated dynamically via the second rule. The behavior of an individual client is described via the third block of rules of Fig. 2, in which the relation between the local variable and the global counters are represented via DC-constraints. Finally, we allow thinking processes to terminate their execution as specified via the last rule of Fig. 2. The previous rules are independent of the current number of clients in the system. Note that in our specification we keep an explicit representation of the data variables; furthermore, we do not out any restrictions on their values. As a consequence, there are runs of our model in which $s$ and $t$ grow without any bound as in the original protocol. A sample run of a system with 2 clients (as in [10]) is shown in Fig. 3.
Figure 2: Ticket protocol for multi-client, single-server system, with an example of run.
\begin{figure*}
\centerline{\small
$
\begin{array}{c}
\begin{array}{c}
{\bf...
...~ & \epsilon & true
\end{array}\end{array}
\end{array}
$
}
\end{figure*}
Figure 3: Example of run.
\begin{figure*}
\centerline{\small
$
\begin{array}{c}
\begin{array}{c}
init...
...(10)~\vert~turn(9)~\vert~think
\end{array}
\end{array}
$
}
\end{figure*}
Let us consider now an open system with an arbitrary but finite number of shared resources, each one controlled by two local counters $s$ and $t$. We specify this scenario by associating a unique identifier to each resource and to use it to stamp the corresponding pair of counters. Furthermore, we exploit non-determinism in order to simulate the capability of each client to choose which resource to use. The resulting specification is shown in Fig 4. We have considered an open system in which new clients can be generated dynamically via a demon process. The process $demon(n)$ maintains a local counter $n$ used to generate a new identifier, say $id$, and to associate it to a newly created resource represented via the pair $count(id,t)$ and $turn(id,s)$. A thinking process non-deterministically chooses which resource to wait for by synchronizing with one of the counters in the system (the first rule of the third block in Fig. 4). After this choice, the algorithm behaves as usual w.r.t. to the chosen resource $id$. The termination rules can be specified as natural extensions of the single-server case. Note that in this specification the sources of infiniteness are the number of clients, the number of shared resources, the values of resource identifiers, and the values of tickets. An example of run is shown in Fig. 5.
Figure 4: Ticket protocol for multi-server, multi-client systems.
\begin{figure*}
\centerline{\footnotesize
$
\begin{array}{c}
\begin{array}{c...
...ue
\end{array}
\end{array}
\smallskip\\
\end{array}
$
}
\end{figure*}
Figure 5: Example of run.
\begin{figure*}
\centerline{\footnotesize
$
\begin{array}{c}
\begin{array}{c...
...\vert~think(3)~\vert~demon(5).
\end{array}
\end{array}
$
}
\end{figure*}

next.png up.png previous
Next: An Assertional Language for Up: Constraint Multiset Rewriting Previous: The language
Giorgio Delzanno 2003-02-03