5. Principles of Model Checking. Baier_ Joost (2008) (5. Principles of Model Checking. Baier_ Joost (2008).pdf), страница 13

Alternatively,another (more concrete) mutual exclusion algorithm could be selected that resolves thisscheduling issue explicitly. A prominent example of such algorithm has been provided in1981 by Peterson [332].Example 2.25.Peterson’s Mutual Exclusion AlgorithmConsider the processes P1 and P2 with the shared variables b1 , b2 , and x. b1 and b2 areBoolean variables, while x can take either the value 1 or 2, i.e., dom(x) = { 1, 2 }. Thescheduling strategy is realized using x as follows.

If both processes want to enter thecritical section (i.e., they are in location waiti ), the value of variable x decides which ofthe two processes may enter its critical section: if x = i, then Pi may enter its criticalsection (for i = 1, 2). On entering location wait1 , process P1 performs x := 2, thus givingprivilege to process P2 to enter the critical section.

The value of x thus indicates whichprocess has its turn to enter the critical section. Symmetrically, P2 sets x to 1 whenstarting to wait. The variables bi provide information about the current location of Pi .More precisely,bi = waiti ∨ criti .bi is set when Pi starts to wait. In pseudocode, P1 performs as follows (the code for processP2 is similar):46Modelling Concurrent SystemsPG1 :PG2 :noncrit1noncrit1b1 := true; x := 2b1 := falsewait1b2 := falsex=1 ∨ ¬b2crit1b2 := true; x := 1wait1x=2 ∨ ¬b1crit1Figure 2.9: Program graphs for Peterson’s mutual exclusion algorithm.P1loop forever...b1 := true; x := 2;wait until (x = 1 ∨ ¬b2 )do critical section odb1 := false...(* noncritical actions *)(* request *)(* release *)(* noncritical actions *)end loopProcess Pi is represented by program graph PGi over Var = { x, b1 , b2 } with locationsnoncriti , waiti , and criti , see Figure 2.9 above.

The reachable part of the underlying transition system TSPet = TS(PG1 ||| PG2 ) has the form as indicated in Figure 2.10 (page 47),where for convenience ni , wi , ci are used for noncriti , waiti , and criti , respectively. Thelast digit of the depicted states indicates the evaluation of variable x. For convenience, thevalues for bi are not indicated. Its evaluation can directly be deduced from the locationof PGi . Further, b1 = b2 = false is assumed as the initial condition.Each state in TSPet has the form loc1 , loc2 , x, b1 , b2 . As PGi has three possible locationsand bi and x each can take two different values, the total number of states of TSPet is 72.Only ten of these states are reachable.

Since there is no reachable state with P1 and P2being in their critical section, it can be concluded that Peterson’s algorithm satisfies themutual exclusion property.In the above program, the multiple assignments b1 := true; x := 2 and b2 := true; x := 1are considered as indivisible (i.e., atomic) actions. This is indicated by the brackets Parallelism and Communicationn1 , n2 , x = 247n1 , n2 , x = 1n1 , c2 , x = 1c1 , n2 , x = 2w1 , n2 , x = 2n1 , w2 , x = 1w1 , w2 , x = 1w1 , w2 , x = 2c1 , w2 , x = 1w1 , c2 , x = 2Figure 2.10: Transition system of Peterson’s mutual exclusion algorithm.and in the program text, and is also indicated in the program graphs PG1 and PG2 .We like to emphasize that this is not essential, and has only been done to simplify thetransition system TSPet .

Mutual exclusion is also ensured when both processes performthe assignments bi := true and x := . . . in this order but in a nonatomic way. Note that, forinstance, the order “first x := . . ., then bi := true” does not guarantee mutual exclusion.This can be seen as follows. Assume that the location inbetween the assignments x := . . .and bi := true in program graph Pi is called reqi . The state sequencenoncrit1 , noncrit2 ,req2 ,noncrit1 ,req2 ,req1 ,req2 ,wait1 ,req2 ,crit1 ,wait2 ,crit1 ,crit2 ,crit1 ,x = 1,x = 1,x = 2,x = 2,x = 2,x = 2,x = 2,b1b1b1b1b1b1b1= false,= false,= false,= true,= true,= true,= true,b2b2b2b2b2b2b2= false= false= false= false= false= true= trueis an initial execution fragment where P1 enters its critical section first (as b2 = false)after which P2 enters its critical section (as x = 2).

As a result, both processes aresimultaneously in their critical section and mutual exclusion is violated.2.2.3HandshakingSo far, two mechanisms for parallel processes have been considered: interleaving andshared-variable programs. In interleaving, processes evolve completely autonomously48Modelling Concurrent Systems• interleaving for α ∈/ H:α→1 s1s1 −−αs1 , s2 −−→ s1 , s2 αs2 −−→2 s2αs1 , s2 −−→ s1 , s2 • handshaking for α ∈ H:αα→1 s1 ∧ s2 −−→2 s2s1 −−αs1 , s2 −−→ s1 , s2 Figure 2.11: Rules for handshaking.whereas according to the latter type processes “communicate” via shared variables.

Inthis subsection, we consider a mechanism by which concurrent processes interact via handshaking. The term “handshaking” means that concurrent processes that want to interacthave to do this in a synchronous fashion. That is to say, processes can interact only ifthey are both participating in this interaction at the same time—they “shake hands”.Information that is exchanged during handshaking can be of various nature, ranging fromthe value of a simple integer, to complex data structures such as arrays or records.

Inthe sequel, we do not dwell upon the content of the exchanged messages. Instead, anabstract view is adopted and only communication (also called synchronization) actionsare considered that represent the occurrence of a handshake and not the content.To do so, a set H of handshake actions is distinguished with τ ∈ H. Only if bothparticipating processes are ready to execute the same handshake action, can messagepassing take place.

All actions outside H (i.e., actions in Act \ H) are independent andtherefore can be executed autonomously in an interleaved fashion.Definition 2.26.Handshaking (Synchronous Message Passing)Let TSi = (Si , Acti , →i , Ii , APi , Li ), i=1, 2 be transition systems and H ⊆ Act1 ∩ Act2with τ ∈ H. The transition system TS1 H TS2 is defined as follows:TS1 H TS2 = (S1 × S2 , Act1 ∪ Act2 , →, I1 × I2 , AP1 ∪ AP2 , L)where L(s1 , s2 ) = L1 (s1 ) ∪ L2 (s2 ), and where the transition relation → is defined bythe rules shown in Figure 2.11.Notation: TS1 TS2 abbreviates TS1 H TS2 for H = Act1 ∩ Act2 .Parallelism and CommunicationRemark 2.27.49Empty Set of Handshake ActionsWhen the set H of handshake actions is empty, all actions of the participating processescan take place autonomously, i.e., in this special case, handshaking reduces to interleavingTS1 ∅ TS2 = TS1 ||| TS2 .The operator H defines the handshaking between two transition systems.

Handshakingis commutative, but not associative in general. That is, in general we haveTS1 H (TS2 H TS3 ) = (TS1 H TS2 ) H TS3for H = H .However, for a fixed set H of handshake actions over which all processes synchronize, theoperator H is associative. LetTS = TS1 H TS2 H . .

. H TSn ,denote the parallel composition of transition systems TS1 through TSn where H ⊆ Act1 ∩. . . ∩ Actn is a subset of the set of actions Acti of all transition systems. This form ofmultiway handshaking is appropriate to model broadcasting, a communication form inwhich a process can transmit a datum to several other processes simultaneously.In many cases, processes communicate in a pairwise fashion over their common actions.Let TS1 . . . TSn denote the parallel composition of TS1 through TSn (with n > 0) whereTSi and TSj (0 < i = j n) synchronize over the set of actions Hi,j = Acti ∩ Actj such/ { i, j }. It is assumed that τ ∈ Hi,j .

The formal definitionthat Hi,j ∩ Actk = ∅ for k ∈of TS1 . . . TSn is analogous to Definition 2.26. The state space of TS1 . . . TSn resultsfrom the Cartesian product of the state spaces of TSi . The transition relation → is definedby the following rules:• for α ∈ Acti \ (Hi,j ) and 0 < i n:0<jni=jα→ i sisi −−αs1 , . . . , si , . . . , sn −−→ s1 , . . . , si , .

. . sn • for α ∈ Hi,j and 0 < i < j n:αα→ i si ∧ sj −−→ j sjsi −−αs1 , . . . , si , . . . , sj , . . . , sn −−→ s1 , . . . , si , . . . , sj , . . . , sn 50Modelling Concurrent SystemsAccording to the first rule, components can execute actions that are not subject to handshaking in a completely autonomous manner as in interleaving. The second rule states thatprocesses TSi and TSj (i = j) have to perform every handshaking action in Acti ∩ Actjtogether. These rules are in fact just generalizations of those given in Figure 2.11.Example 2.28.Mutual Exclusion by Means of an ArbiterAn alternative solution to the mutual exclusion problem between processes P1 and P2(as before) is to model the binary semaphore that regulates access to the critical sectionby a separate parallel process that interacts with P1 and P2 by means of handshaking.For simplicity, we ignore the waiting phase and assume that Pi simply alternates infinitelyoften between noncritical and critical sections.

Assume (much simplified) transition systemrepresentations TS1 and TS2 with just two states: criti and noncriti . The new process,named Arbiter, mimics a binary semaphore (see Figure 2.12). P1 and P2 communicatewith the Arbiter via handshaking over the set H = { request, rel }. Accordingly, the actionsrequest (requesting to access the critical section) and rel (to leave the critical section) haveto be executed synchronously with the Arbiter.