and left hands (respectively), while P1 would eat with F1 and F2, and P2 with F2 and F0. Clearly, when one philosopher ‘chows,’ the other two have to lick their lips, patiently waiting their turn. It is assumed that despite their advanced state of learning, they are disallowed from trying to eat with one fork or reach across the table for the disallowed fork. In order to pick up a fork, a philosopher sends a message to the fork through the appropriate channel. For example, to acquire F0 or F1, respectively, P0 would send an are_you_free request message through channel C5 or C0, respectively. Such a request obtains a “yes” or a “no” reply. If the reply is “yes,” the philosopher acquires the fork; otherwise he retries (if for the left fork) or gives up the already acquired left fork and starts all over (if for the right fork). Consequently, the deadlock due to all the philosophers picking up their left forks and waiting for their right forks does not arise in our implementation. After finishing eating, a philosopher puts down the two forks he holds by sequentially issuing two release messages, each directed at the respective forks through the appropriate channels.
Figure 21.2 describes how the above protocol is described in the Promela modeling language. Consider the init section where we create channels c0 through c5. Each channel is of zero size and carries mtype messages. Communication through a channel of size 0 occurs through rendezvous wherein the sender and the receiver both have to be ready in order for the communication to take place. As one example, consider when proctype phil executes its statement lf!are_you_free. We trace channel lf and find that it connects to a philosopher’s left-hand side fork. This channel happens to be the same as the rp channel as far as fork processes are concerned (rp stands for the ‘right-hand philosopher’ for a fork). These connections are specified in the init section. Hence, proctype fork must reach rp?are_you_free statement at which time both lf!are_you_free and rp?are_you_free execute jointly. As a result of this rendezvous, proctypes phil as well as fork advance past these statements in their respective codes.
Continuing with the init section, after “wiring up” the phil and fork processes, we run three copies of phil and three copies of fork in parallel (the atomic construct ensures that all the proctype instances start their execution at the same time). The never section specifies the property of interest, and will be described in Sections 21.4.1 and 22.1. Now we turn our attention to the proctypes phil and fork.
Proctype phil consists of one endless outer do/od loop, inside which are two sequential do/od loops. The first of these loops has as its first statement lf!are_you_free. This statement acts as a guard, in the sense that the execution of this statement allows the subsequent statement to be engaged in — in our example, this happens to be a nested if/fi statement (sequencing is indicated by ->; in Promela, one may use -> and ; interchangeably to denote sequencing). An if/fi offers a selection of guards, and nondeterministically selects one of the arms that can execute (a do/od is like an if/fi with a goto leading back to the beginning). Hence, if lf?yes rendezvous with rp!yes, the first inner do/od loop breaks, and the second do/od loop is engaged. In this, the guard is rf!are_you_free. If the reply obtained is rf?yes, the philosopher in question can begin eating. To indicate that a philosopher has successfully started eating, we set a progress flag to 1 and
then to 0. The attainment of progress=1 will be monitored by a never automaton. The forks are released and the execution continues with another iteration of the outer do/od loop. Notice that if the second arm of the if/fi statement is chosen (through lf?no), the lf!are_you_free is retried. Therefore, phil repeatedly requests its left fork, and if/when successful, requests its right fork. If a rf?no is obtained when requesting the right fork, notice that the already acquired left fork is released via lf!release and the whole process is restarted.
The process of acquiring both forks in the manner described above is based on two-phase locking—an algorithm known to be able to avoid deadlocks. The idea is (i) to acquire all the required resources in some sequential order, and (ii) when some resource is found unavailable, instead of holding on to all the resources acquired thus far and waiting for the unavailable resource (which can cause deadlocks), we release all the resources acquired thus far and restart the acquisition process. It is easy to see that while this approach avoids deadlocks, it can introduce livelocks. To detect the livelock in our example, we employ a property automaton expressed in the never section of a Promela model. Our property automaton (or “never” automaton) is designed to check whether the progress bit is set to true infinitely often. Even if one phil proctype violates this assertion—meaning that it only sets progress true a finite number of times—we want the bug to be reported. We describe this property automaton as well as how it finds the liveness violation in the next section. In Chapter 22, we explain the relationship between property automata as well as linear-time temporal logic assertions.
