Model (Proctype) And Property (Never) Automata

Model (proctype) and property (never) automata: A typical Promela model consists of multiple proctypes and one never automaton. The proctypes are concurrent processes whose atomic statements interleave in all possible ways. The collection of proctypes represents the “system” or “model.” Formally, one can say that the asynchronous or interleaving product of the model automata represents the set of all behaviors of interest. A never or property automaton observes the infinite runs of this interleaving product (all model runs). Conceptually, after every move of the model (a move of one of the constituent proctypes), one move of the property automaton is performed to check whether the model automaton move left the system in a good state. Formally, one can say that the synchronous product of the model and property automata are performed. In Figure 21.2, the property automaton represents the complement5 of the desired property—hence, the keyword never. One of the desired properties in our example is that progress is infinitely often set true. This means that infinitely often, every philosopher gets to eat. If there is even one philosopher who, after a finite amount of eatings, is never allowed to eat again, we certainly would like to know that. The never automaton accepts a run (or a computation) if the run visits one of the final states infinitely. The never automaton defined in Figure 21.2 can nondeterministically loop in its initial do/od loop. In fact, it can even stay in its initial state if progress is false. However, it may also choose to go to the final state labeled accept when progress is false. Here, it can continue to visit accept so long as progress is false. Hence, this never automaton accepts only an infinite sequence of progress being false—precisely when our desired liveness property is violated.

When we ran the description in Figure 21.2 through the SPIN model checker (which is a model checker for descriptions written in Promela), it quickly found a liveness violation which indicates that, indeed, there exists at least one philosopher who will starve forever. SPIN produces a message sequence chart (MSC) corresponding to this error; this is shown in Figure 21.3.

An MSC displays the “lifelines” (time lines of behaviors) of all the processes participating in the protocol. Ignoring the never and init lifelines that are at the left extremity, the main lifelines shown are vertical lines tracing the behaviors of various process instances, specifically phi1:1, fork:2, phi1:3, fork:4, phi1:5, and fork:6. Reading this MSC, we find out how the bug occurs:

Fig. 21.3. Message sequence chart showing liveness violation bug

• phil:5 acquires fork:4 by sending it an are_you_free message and obtaining a yes reply (the channel names have been converted into internal channel numbers in this MSC). It also acquires fork:6 in the same manner.
• phil:1 attempts to acquire fork:6 by sending an are_you_free and obtaining a no repeatedly. This is a liveness violation because phil:1 is starving.