5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 22
Текст из файла (страница 22)
The sticks aremodeled as independent processes (called Stick i ) with which the philosophers synchronizevia actions request and release; see the right part of Figure 3.2 that represents the processof stick i. A stick process prevents philosopher i from picking up the ith stick whenphilosopher i+1 is using it.92Linear-Time Propertiesthinkreleasei irequestireleasei1irequesti i1iavailablewait forwait forleft stickright stickrequesti irequesti1i1ireqi ireli i reli ioccupiedeatreleaseireqi i11occupiedreleasei ireturn thereturn theleft stickright stickFigure 3.2: Transition systems for the ith philosopher and the ith stick.The complete system is of the form:Phil 4 Stick 3 Phil 3 Stick 2 Phil 2 Stick 1 Phil 1 Stick 0 Phil 0 Stick 4This (initially obvious) design leads to a deadlock situation, e.g., if all philosophers pickup their left stick at the same time.
A corresponding execution leads from the initial statethink 4 , avail 3 , think 3 , avail 2 , think 2 , avail 1 , think 1 , avail 0 , think 0 , avail 4 by means of the action sequence request 4 , request 3 , request 2 , request 1 , request 0 (or anyother permutation of these 5 request actions) to the terminal statewait 4,0 , occ 4,4 , wait 3,4 , occ 3,3 , wait 2,3 , occ 2,2 , wait 1,2 , occ 1,1 , wait 0,1 , occ 0,0 .This terminal state represents a deadlock with each philosopher waiting for the neededstick to be released.A possible solution to this problem is to make the sticks available for only one philosopherat a time.
The corresponding chopstick process is depicted in the right part of Figure 3.3.In state available i,j only philosopher j is allowed to pick up the ith stick. The abovementioned deadlock situation can be avoided by the fact that some sticks (e.g., the first,the third, and the fifth stick) start in state available i,i , while the remaining sticks start instate available i,i+1 .
It can be verified that this solution is deadlock- and starvation-free.Deadlock93thinkreli ireqireli1ireqi i1iavailableiwait forwait forleft stickright stickreqi ireqi1ireli1i1reqi ioccupiedeatreli ioccupiedreli ireturn thereturn theleft stickright stickreqi ireli iavailablei11Figure 3.3: Improved variant of the ith philosopher and the ith stick.A further characteristic often required for concurrent systems is robustness against failureof their components. In the case of the dining philosophers, robustness can be formulatedin a way that ensures deadlock and starvation freedom even if one of the philosophers is“defective” (i.e., does not leave the think phase anymore).1 The above-sketched deadlockand starvation-free solution can be modified to a fault-tolerant solution by changing thetransition systems of philosophers and sticks such that philosopher i+1 can pick up the ithstick even if philosopher i is thinking (i.e., does not need stick i) independent of whetherstick i is in state available i,i or available i,i+1 .
The corresponding is also true when the rolesof philosopher i and i+1 are reversed. This can be established by adding a single Booleanvariable xi to philosopher i (see Figure 3.4). The variable xi informs the neighboringphilosophers about the current location of philosopher i. In the indicated sketch, xi is aBoolean variable which is true if and only if the ith philosopher is thinking. Stick i ismade available to philosopher i if stick i is in location available i (as before), or if stick iis in location available i+1 while philosopher i+1 is thinking.Note that the above description is at the level of program graphs.
The complete system isa channel system with request and release actions standing for handshaking over a channelof capacity 0.1Formally, we add a loop to the transition system of a defective philosopher at state think i .94Linear-Time Propertiesxi : truethinkreqi iwaitxi : truereqixi : falseavailableifalls xireqi i1i1reqi iwaitoccupiedoccupied......xiavailableireqi i111Figure 3.4: Fault-tolerant variant of the dining philosophers.3.2Linear-Time BehaviorTo analyze a computer system represented by a transition system, either an action-based ora state-based approach can be followed. The state-based approach abstracts from actions;instead, only labels in the state sequences are taken into consideration.
In contrast,the action-based view abstracts from states and refers only to the action labels of thetransitions. (A combined action- and state-based view is possible, but leads to moreinvolved definitions and concepts. For this reason it is common practice to abstract fromeither action or state labels.) Most of the existing specification formalisms and associatedverification methods can be formulated in a corresponding way for both perspectives.In this chapter, we mainly focus on the state-based approach. Action labels of transitionsare only necessary for modeling communication; thus, they are of no relevance in thefollowing chapters.
Instead, we use the atomic propositions of the states to formulatesystem properties. Therefore, the verification algorithms operate on the state graph of atransition system, the digraph originating from a transition system by abstracting fromaction labels.Linear-Time Behavior3.2.195Paths and State GraphLet TS = (S, Act, →, I, AP, L) be a transition system.Definition 3.3.State GraphThe state graph of TS, notation G(TS), is the digraph (V, E) with vertices V = S andedges E = {(s, s ) ∈ S × S | s ∈ Post(s)}.The state graph of transition system TS has a vertex for each state in TS and an edgebetween vertices s and s whenever s is a direct successor of s in TS for some action α.
Itis thus simply obtained from TS by omitting all state labels (i.e., the atomic propositions),all transition labels (i.e., the actions), and by ignoring the fact whether a state is initialor not. Moreover, multiple transitions (that have different action labels) between statesare represented by a single edge. This seems to suggest that the state labels are no longerof any use; later on, we will see how these state labels will be used to check the validity ofproperties.Let Post∗ (s) denote the states that are reachable in state graph G(TS) from s. This notionis generalized toward sets of states in the usual way (i.e., pointwise extension): for C ⊆ SletPost∗ (s).Post∗ (C) =s∈CThe notations Pre∗ (s) and Pre∗ (C) have analogous meaning.
The set of states that arereachable from some initial state, notation Reach(TS), equals Post∗ (I).As explained in Chapter 2, the possible behavior of a transition system is defined by anexecution fragment. Recall that an execution fragment is an alternating sequence of statesand actions. As we consider a state-based approach, the actions are not of importance andare omitted. The resulting “runs” of a transition system are called paths. The followingdefinitions define path fragments, initial and maximal path fragments, and so on.
Thesenotions are easily obtained from the same notions for executions by omitting the actions.Definition 3.4.Path FragmentA finite path fragment π of TS is a finite state sequence s0 s1 . . . sn such that si ∈ Post(si−1 )for all 0 < i n, where n 0. An infinite path fragment π is an infinite state sequences0 s1 s2 . . . such that si ∈ Post(si−1 ) for all i > 0.We adopt the following notational conventions for infinite path fragment π = s0 s1 . .
.. Theinitial state of π is denoted by first(π) = s0 . For j 0, let π[j] = sj denote the jth state of96Linear-Time Propertiesπ and π[..j] denote the jth prefix of π, i.e., π[..j] = s0 s1 . . . sj . Similarly, the jth suffix ofπ, notation π[j..], is defined as π[j..] = sj sj+1 . . .. These notions are defined analogouslyπ ) = sn denote the lastfor finite paths. Besides, for finite path π = s0 s1 . . . sn , let last(state of π, and len(π ) = n denote the length of π. For infinite path π these notions aredefined by len(π) = ∞ and last(π) = ⊥, where ⊥ denotes “undefined”.Definition 3.5.Maximal and Initial Path FragmentA maximal path fragment is either a finite path fragment that ends in a terminal state, oran infinite path fragment.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
