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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 18)

Forstatements stmt ∈ {skip, x := expr, c?x, c!expr} the set of substatements is sub(stmt) ={stmt, exit}. For sequential composition letsub(stmt1 ; stmt2 ) ={ stmt ; stmt2 | stmt ∈ sub(stmt1 ) \ {exit} } ∪ sub(stmt2 ).For conditional commands, the set of substatements is defined as the set consisting of theif–fi-statement itself and substatements of its guarded commands.

That is, for cond cmd70Modelling Concurrent Systemsbeing if :: g1 ⇒ stmt1 . . . :: gn ⇒ stmtn fi we havesub(cond cmd) = { cond cmd } ∪1insub(stmti ).The substatements of a loop loop given by do :: g1 ⇒ stmt1 . . . :: gn ⇒ stmtn od aredefined similarly, but taking into account that control moves back to loop when guardedcommands terminate. That is:sub(loop) ={ loop, exit } ∪1in{ stmt ; loop | stmt ∈ sub(stmti ) \ {exit} }.For atomic regions let sub(atomic{stmt}) = { atomic{stmt}, exit }.The definition of sub(loop) relies on the observation that the effect of a loop with a singleguarded command, say “do :: g ⇒ stmt od”, corresponds to the effect ofif g then stmt ; do :: g ⇒ stmt od else skip fiAn analogous characterization applies to loops with two or more guarded commands.Thus, the definition of the substatements of loop relies on combining the definitions of thesets of substatements for sequential composition and conditional commands.The formal semantics of nanoPromela program P = [P1 | .

. . |Pn ] where the behavior of theprocess Pi is specified by a nanoPromela statement is a channel system [PG1 | . . . |PGn ]over (Var, Chan) where Var is the set of variables and Chan the set of channels thatare declared in P. As mentioned before, a formal syntax for the variable and channeldeclarations will not be provided, and global and local variables will not be distinguished.We assume that the set Var of typed variables and the set Chan of channels (togetherwith a classification of the channels into synchronous and FIFO-channels of some capacitycap(·)) are given.

Hence, local variable and channel declarations for the processes Pi arenot considered. It is assumed that they are given by a nanoPromela-statement over somefixed tuple (Var, Chan).We now provide inference rules for the nanoPromela constructs. The inference rules for theatomic commands (skip, assignment, communication actions) and sequential composition,conditional and repetitive commands give rise to the edges of a “large” program graphwhere the set of locations agrees with the set of nanoPromela-statements. Thus, the edgeshave the formg:commg:α→ stmtstmt → stmt or stmt where stmt is a nanoPromela statement, stmt a substatement of stmt, and g a guard, αan action, and comm a communication action c?x or c!expr.

The subgraph consisting ofParallelism and Communication71the substatements of Pi then yields the program graph PGi of process Pi as a componentof the program P.The semantics of the atomic statement skip is given by a single axiom formalizing thatthe execution of skip terminates in one step without affecting the variablestrue: idskip → exitwhere id denotes an action that does not change the values of the variables, i.e., Effect(id, η)= η for all variable evaluations η.

Similarly, the execution of a statement consisting of anassignment x := expr has the trivial guard and terminates in one step:true : assign(x, expr)x := expr → exitwhere assign(x, expr) denotes the action that changes the value of x according to theassignment x := expr and does not affect the other variables, i.e., if η ∈ Eval(Var) andy ∈ Var then Effect(assign(x, expr), η)(y) = η(y) if y = x and Effect(assign(x, expr), η)(x)is the value of expr when evaluated over η. For the communication actions c!expr and c?xthe following axioms apply:c!exprc?xc!expr → exitc?x → exitThe effect of an atomic region atomic{x1 := expr1 ; . .

. ; xm := exprm } is the cumulativeeffect of the assignments xi := expri . It can be defined by the rule:true : αmatomic{x1 := expr1 ; . . . ; xm := exprm } → exitwhere α0 = id, αi = Effect(assign(xi , expri ), Effect(αi−1 , η)) for 1 i m.Sequential composition stmt1 ; stmt2 is defined by two rules that distinguish whether ornot stmt1 terminates in one step. If the first step of stmt1 leads to a location (statement)different from exit, then the following rule applies:g:αstmt1 → stmt1 = exitg:αstmt1 ; stmt2 → stmt1 ; stmt2If the computation of stmt1 terminates in one step by executing action α, then control ofstmt1 ; stmt2 moves to stmt2 after executing α:g:αstmt1 → exitg:αstmt1 ; stmt2 → stmt272Modelling Concurrent SystemsThe effect of a conditional command cond cmd = if :: g1 ⇒ stmt1 .

. . :: gn ⇒ stmtn fi isformalized by means of the following rule:h:αstmti → stmtigi ∧h:αcond cmd → stmtiThis rule relies on the test-and-set semantics where choosing one of the enabled guardedcommands and performing its first action are treated as an atomic step. The blocking ofcond cmd when none of its guards is enabled needs no special treatment.

The reason isthat cond cmd has no other edges than the ones specified by the rule above. Thus, in aglobal state s = 1 , . . . , n , η, ξ where the location i of the ith process is i = cond cmdand all guards g1 , . . . , gn evaluate to false, then there is no action of the ith process that isenabled in s. However, actions of other processes might be enabled. Thus, the ith processhas to wait until the other processes modify the variables appearing in g1 , . . . , gn such thatone or more of the guarded commands gi ⇒ stmti become enabled.For loops, say loop = do :: g1 ⇒ stmt1 . .

. :: gn ⇒ stmtn od, we deal with three rules. Thefirst two rules are similar to the rule for conditional commands, but taking into accountthat control moves back to loop after the execution of the selected guarded command hasbeen completed. This corresponds to the following rules:h:αh:αstmti → stmti = exitstmti → exitgi ∧h:αloop → stmti ; loopgi ∧h:αloop → loopIf none of the guards g1 , . . . , gn holds in the current state then the do–od-loop will beaborted. This is formalized by the following axiom:¬g1 ∧...∧¬gnloop → exitRemark 2.39.Test-and-Set Semantics vs. Two-Step SemanticsThe rules for if–fi- and do–od-statements formalize the so-called test-and-set semantics ofguarded commands. This means that evaluating guard gi and performing the first step ofthe selected enabled guarded command gi ⇒ stmti are performed atomically.

In contrast,SPIN’s interpretation of Promela relies on a two-step-semantics where the selection of anenabled guarded command and the execution of its first action are split into two steps.The rule for a conditional command is formalized by the axiomgi : idif :: g1 ⇒ stmt1 . . . :: gn ⇒ stmtn fi → stmtiParallelism and Communication73where id is an action symbol for an action that does not affect the variables. Similarly,the first two rules for loops have to be replaced for the two-step semantics by the followingrule:gi : idloop → stmti ; loopThe rule for terminating the loop remains unchanged.As long as we consider the statements in isolation, the test-and-set semantics and thetwo-step semantics are equal.

However, when running several processes in parallel, theinterleaving might cause undesired side effects. For example, consider the semaphore-basedsolution of the mutual exclusion problem, modeled by a nanoPromela program where thebehavior of Pi is given by the following nanoPromela-statement:do :: true ⇒ skip;if :: y > 0 ⇒ y := y − 1;criti := truefi;y := y + 1odThe initial value of the semaphore y is zero. Under the two-step semantics the mutualexclusion property is not guaranteed as it allows the processes to verify that the guardy > 0 of the if–fi-statement holds, without decreasing the value of y, and moving controlto the assignment y := y − 1.

But from there the processes can enter their critical sections.However, the protocol works correctly for the test-and-set semantics since then checkingy > 0 and decreasing y is an atomic step that cannot be interleaved by the actions of theother process.Remark 2.40.Generalized GuardsSo far we required that the guards in conditional or repetitive commands consist of Booleanconditions on the program variables. However, it is also often useful to ask for interactionfacilities in the guards, e.g., to specify that a process has to wait for a certain input alonga FIFO-channel by means of a conditional command if :: c?x ⇒ stmt fi.

Характеристики

Список файлов книги