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

Thedepicted transition system is actually the transition systemTS = TrLight1 ||| TrLight2that originates from interleaving.For program graphs PG1 (on Var1 ) and PG2 (on Var2 ) without shared variables (i.e.,Var1 ∩ Var2 = ∅), the interleaving operator, which is applied to the appropriate transitionsystems, yields a transition systemTS(PG1 ) ||| TS(PG2 )that describes the behavior of the simultaneous execution of PG1 and PG2 .2.2.2Communication via Shared VariablesThe interleaving operator ||| can be used to model asynchronous concurrency in which thesubprocesses act completely independent of each other, i.e., without any form of messagepassing or contentions on shared variables.

The interleaving operator for transition systemsis, however, too simplistic for most parallel systems with concurrent or communicatingcomponents. An example of a system whose components have variables in common—shared variables so to speak—will make this clear.Example 2.20.The Interleaving Operator for Concurrent ProcessesRegard the program graph for the instructions α and β of the parallel programx + 1x2·x ||| x := :=action αaction βwhere we assume that initially x = 3. (To simplify the picture, the locations have beenskipped.) The transition system TS(PG1 ) ||| TS(PG2 ) contains, e.g., the inconsistent statex=6, x=4 and, thus, does not reflect the intuitive behavior of the parallel execution ofα and β:x=3αx=6αx=3|||βx=4=x=3, x=3x=6, x=3ββx=3, x=4x=6, x=4α40Modelling Concurrent SystemsThe problem in this example is that the actions α and β access the shared variable xand therefore are competing.

The interleaving operator for transition systems, however,“blindly” constructs the Cartesian product of the individual state spaces without considering these potential conflicts. Accordingly, it is not identified that the local states x=6and x=4 describe exclusive events.In order to deal with parallel programs with shared variables, an interleaving operator willbe defined on the level of program graphs (instead of directly on transition systems). Theinterleaving of program graphs PG1 and PG2 is denoted PG1 ||| PG2 . The underlyingtransition system of the resulting program graph PG1 ||| PG2 , i.e., TS(PG1 ||| PG2 ) (seeDefinition 2.15, page 34) faithfully describes a parallel system whose components communicate via shared variables. Note that, in general, TS(PG1 ||| PG2 ) = TS(PG1 ) ||| TS(PG2 ).Definition 2.21.Interleaving of Program GraphsLet PGi = (Loci , Acti , Effecti , → i , Loc0,i , g0,i ), for i=1, 2 be two program graphs over thevariables Vari .

Program graph PG1 ||| PG2 over Var1 ∪ Var2 is defined byPG1 ||| PG2 = (Loc1 × Loc2 , Act1 Act2 , Effect, →, Loc0,1 × Loc0,2 , g0,1 ∧ g0,2 )where → is defined by the rules:g:α1 →1 1g:α1 , 2 → 1 , 2 g:αand2 →2 2g:α1 , 2 → 1 , 2 and Effect(α, η) = Effecti (α, η) if α ∈ Acti .The program graphs PG1 and PG2 have the variables Var1 ∩ Var2 in common. These arethe shared (sometimes also called “global”) variables. The variables in Var1 \ Var2 are thelocal variables of PG1 , and similarly, those in Var2 \ Var1 are the local variables of PG2 .Example 2.22.Interleaving of Program GraphsConsider the program graphs PG1 and PG2 that correspond to the assignments x := x+1and x := 2·x, respectively.

The program graph PG1 ||| PG2 is depicted in the bottomleft of Figure 2.5. Its underlying transition system TS(PG1 ||| PG2 ) is depicted in thebottom right of that figure where it is assumed that initially x equals 3. Note that thenondeterminism in the initial state of the transition system does not represent concurrencybut just the possible resolution of the contention between the statements x := 2·x andx := x+1 that both modify the shared variable x.The distinction between local and shared variables has also an impact on the actions of thecomposed program graph PG1 ||| PG2 .

Actions that access (i.e., inspect or modify) sharedParallelism and Communication41PG1 :PG2 :1x := 2 · x1PG1 ||| PG2 :2x := x + 12TS(PG1 ||| PG2 )1 2x=31 2x := 2 · xx := x + 11 21 2x := x + 11 2x := 2 · x1 2x=61 2x=41 2x=71 2x=8Figure 2.5: Interleaving of two example program graphs.42Modelling Concurrent Systemsvariables may be considered as “critical”; otherwise, they are viewed to be noncritical.(For the sake of simplicity, we are a bit conservative here and consider the inspection ofshared variables as critical.) The difference between the critical and noncritical actionsbecomes clear when interpreting the (possible) nondeterminism in the transition systemTS(PG1 ||| PG2 ).

nondeterminism in a state of this transition system may stand either for(i) an “internal” nondeterministic choice within program graph PG1 or PG2 ,(ii) the interleaving of noncritical actions of PG1 and PG2 , or(iii) the resolution of a contention between critical actions of PG1 and PG2 (concurrency).In particular, a noncritical action of PG1 can be executed in parallel with critical ornoncritical actions of PG2 as it will only affect its local variables.

By symmetry, the sameapplies to the noncritical actions of PG2 . Critical actions of PG1 and PG2 , however, cannotbe executed simultaneously as the value of the shared variables depends on the order ofexecuting these actions (see Example 2.20). Instead, any global state where critical actionsof PG1 and PG2 are enabled describe a concurrency situation that has to be resolved byan appropriate scheduling strategy.

(Simultaneous reading of shared variables could beallowed, however.)Remark 2.23.On AtomicityFor modeling a parallel system by means of the interleaving operator for program graphsit is decisive that the actions α ∈ Act are indivisible. The transition system representationonly expresses the effect of the completely executed action α. If there is, e.g., an action αwith its effect being described by the statement sequencex := x + 1; y := 2x + 1; if x < 12 then z := (x − z)2 ∗ y fi,then an implementation is assumed which does not interlock the basic substatements x :=x + 1, y := 2x + 1, the comparison “x < 12”, and, possibly, the assignment z := (x − z)2 ∗ ywith other concurrent processes. In this case,Effect(α, η)(x) = η(x) + 1Effect(α, η)(y) = 2(η(x) + 1) + 1(η(x) + 1 − η(z))2 ∗ 2(η(x) + 1) + 1Effect(α, η)(z) =η(z)if η(x) + 1 < 12otherwiseHence, statement sequences of a process can be declared atomic by program graphs whenput as a single label to an edge.

In program texts such multiple assignments are surroundedby brackets . . ..Parallelism and Communication43PG1 :PG2 :noncrit1y := y+1wait1noncrit2y := y + 1wait2y>0:y := y−1y>0:y := y − 1crit2crit1Figure 2.6: Individual program graphs for semaphore-based mutual exclusion.Example 2.24.Mutual Exclusion with SemaphoresConsider two simplified processes Pi , i=1, 2 of the form:Piloop forever...(* noncritical actions *)requestcritical sectionrelease...(* noncritical actions *)end loopProcesses P1 and P2 are represented by the program graphs PG1 and PG2 , respectively,that share the binary semaphore y.

y=0 indicates that the semaphore—the lock to getaccess to the critical section—is currently possessed by one of the processes. When y=1,the semaphore is free. The program graphs PG1 and PG2 are depicted in Figure 2.6.For the sake of simplicity, local variables and shared variables different from y are notconsidered. Also, the activities inside and outside the critical sections are omitted. Thelocations of PGi are noncriti (representing the noncritical actions), waiti (modeling thesituation in which Pi waits to enter its critical section), and criti (modeling the criticalsection).

The program graph PG1 ||| PG2 consists of nine locations, including the (undesired) location crit1 , crit2 that models the situation where both P1 and P2 are in theircritical section, see Figure 2.7.When unfolding PG1 ||| PG2 into the transition system TSSem = TS(PG1 ||| PG2 ) (seeFigure 2.8 on page 45), it can be easily checked that from the 18 global states in TSSem44Modelling Concurrent SystemsPG1 ||| PG2 :noncrit1 , noncrit2 y := y+1wait1 , noncrit2 y>0:y := y−1crit1 , noncrit2 crit1 , wait2 y := y+1noncrit1 , wait2 y := y+1wait1 , wait2 y>0:y := y−1y>0:y := y−1noncrit1 , crit2 wait1 , crit2 y := y+1y := y+1crit1 , crit2 Figure 2.7: PG1 ||| PG2 for semaphore-based mutual exclusion.only the following eight states are reachable:noncrit1 , noncrit2 , y = 1wait1 , noncrit2 , y = 1noncrit1 , crit2 , y = 0wait1 , crit2 , y = 0noncrit1 , wait2 , y = 1wait1 , wait2 , y = 1crit1 , noncrit2 , y = 0crit1 , wait2 , y = 0States noncrit1 , noncrit2 , y = 1, and noncrit1 , crit2 , y = 0 stand for examples of situations where both P1 and P2 are able to concurrently execute actions.

Note that inFigure 2.8 n stands for noncrit, w for wait, and c for crit. The nondeterminism in thesestates thus stand for interleaving of noncritical actions. State crit1 , wait2 , y = 0, e.g.,represents a situation where only PG1 is active, whereas PG2 is waiting.From the fact that the global state crit1 , crit2 , y = . . . is unreachable in TSSem , it followsthat processes P1 and P2 cannot be simultaneously in their critical section.

The parallelsystem thus satisfies the so-called mutual exclusion property.In the previous example, the nondeterministic choice in state wait1 , wait2 , y = 1 represents a contention between allowing either P1 or P2 to enter its critical section. Theresolution of this scheduling problem—which process is allowed to enter its critical sectionnext?—is left open, however. In fact, the parallel program of the previous example is“abstract” and does not provide any details on how to resolve this contention. At laterdesign stages, for example, when implementing the semaphore y by means of a queue ofwaiting processes (or the like), a decision has to be made on how to schedule the processesthat are enqueued for acquiring the semaphore. At that stage, a last-in first-out (LIFO),Parallelism and Communication45n1 , n2 , y=1w1 , n2 , y=1c1 , n2 , y=0n1 , w2 , y=1w1 , w2 , y=1c1 , w2 , y=0n1 , c2 , y=0w1 , c2 , y=0Figure 2.8: Mutual exclusion with semaphore (transition system representation).first-in first-out (FIFO), or some other scheduling discipline can be chosen.