3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 66
Текст из файла (страница 66)
11.2 A transmission problem.RECEIVER ≡ j := 0; y := ‘ ’;do y 6= ‘∗’; output?y → c[j] := y; j := j + 1 od.The process FILTER can communicate with both other processes. Alongchannel input it is ready to receive characters from process SENDER until ‘∗’has been received. Along channel output it is ready to transmit all nonblankcharacters to the process RECEIVER. If the Boolean parts x 6= ‘∗’ and out 6=in of the generalized guards are both true, the choice whether to receive anew character along channel input or to transmit a processed character alongchannel output is nondeterministic. Thus the distributed program TRANScan pursue computations with different communication sequences among itsprocesses.What about termination? The process SENDER terminates once it hassent all its M characters to the FILTER.
The process FILTER terminateswhen it has received the character ‘∗’ and it has transmitted to RECEIVERall nonblank characters it has received. Finally, the process RECEIVER terminates once it has received from FILTER the character ‘∗’. Thus TRANSterminates if SENDER sends as the last of its M characters the ‘∗’.If SENDER did not send any ‘∗’, a deadlock would arise when the processesFILTER and RECEIVER waited in vain for some further input.
A deadlockwould also arise if SENDER sent the ‘∗’ too early, that is, before M charactershave been sent, because then FILTER would not accept any further charactersfrom the SENDER.⊓⊔38011 Distributed Programs11.2 SemanticsWe now provide a precise operational semantics of distributed programs byformalizing the above informal remarks. The following transition axiom formalizes the termination of a main loop within a process:(xxiv) < do ⊓⊔mj=1 gj → Sj od, σ > → < E, σ >Vmwhere for j ∈ {1, . .
., m} gj ≡ Bj ; αj and σ |= j=1 ¬Bj .Next, we consider the effect of a communication. We allow the followingtransition axiom:(xxv) < [S1 k. . .kSn ], σ > → < [S1′ k. . .kSn′ ], τ >where for some k, ℓ ∈ {1, . . ., n}, k 6= ℓ1Sk ≡ do ⊓⊔mj=1 gj → Rj od,2Sℓ ≡ do ⊓⊔mj=1 hj → Tj od,for some j1 ∈ {1, . . ., m1 } and j2 ∈ {1, . . ., m2 } the generalizedguards gj1 ≡ B1 ; α1 and hj2 ≡ B2 ; α2 match, and(1)(2)(3)(4)(5)σ |= B1 ∧ B2 ,M[[Eff (α1 , α2 )]](σ) = {τ },Si′ ≡ Si for i 6= k, ℓ,Sk′ ≡ Rj1 ; Sk ,Sℓ′ ≡ Tj2 ; Sℓ .Let us clarify the meaning of this transition by discussing its conditions.The form of the processes Sk and Sℓ indicates that each of them is about toexecute its main loop.
The generalized guards gj1 and hj2 match, so syntactically a communication between Sk and Sℓ can take place.Condition (1) states the semantic condition for this communication: theBoolean parts of gj1 and hj2 hold in the initial state σ. This enables gj1 andhj2 to pass jointly. The new state τ is obtained by executing the assignmentstatement representing the effect of the communication —see (2).
This communication involves only processes Sk and Sℓ ; hence (3). Finally, processesSk and Sℓ enter the respective branches of their main loops; hence (4) and(5).The above transition axiom explains how main loops are executed. It involves exactly two processes but is represented as a transition of a parallelcomposition of n processes. Other transitions of a parallel composition of processes are generated as in Chapter 7, by adopting the interleaving rule (xvii)from Section 7.2. The meaning of distributed programs is thus defined byexpanding the transition system for nondeterministic programs by transitionrule (xvii) and the above transition axioms (xxiv) and (xxv).11.2 Semantics381For distributed programs S we distinguish three variants of input/outputsemantics:• partial correctness semantics:M[[S]](σ) = {τ |< S, σ > →∗ < E, τ >},• weak total correctness semantics:Mwtot [[S]](σ) = M[[S]](σ) ∪ {⊥ | S can diverge from τ }∪ {fail | S can fail from τ },• total correctness semantics:Mtot [[S]](σ) = Mwtot [[S]](σ) ∪ {∆ | S can deadlock from σ}.Here we consider a proper state σ and three kinds of special states: ⊥ representing divergence, fail representing failure and ∆ representing deadlock.Divergence, failure and deadlock are defined as in Chapters 3, 10 and 9,respectively.
So, divergence arises when there is an infinite computation< S, σ > → . . .—it is possible due to the presence of the repetitive commands. Failure ariseswhen there exists a computation of the form< S, σ > → . . . → < S1 , fail >—it is possible due to the presence of the alternative commands. A deadlocktakes place when there exists a computation of the form< S, σ > → .
. . → < R, τ >,with R 6≡ E, such that the configuration of < R, τ > has no successor. Thisis possible due to the presence of i/o commands.Only the total correctness semantics takes all of these possibilities intoaccount. As in Chapter 9, weak total correctness results from total correctnessby ignoring deadlock. Note, however, that due to the presence of alternativestatements in the language of this chapter, weak total correctness now alsorecords failures. The semantics of weak total correctness is not interesting initself but helps us to modularize proofs of total correctness.We conclude this section by proving the bounded nondeterminism of distributed programs.Lemma 11.1. (Bounded Nondeterminism) Let S be a distributed program and σ a proper state.
Then Mtot [[S]](σ) is either finite or it contains⊥.38211 Distributed ProgramsProof. For distributed programs S every configuration < S, σ > has onlyfinitely many successors in the transition relation → , so the same argumentas in the proof of the Bounded Nondeterminism Lemma 8.2 based on theKönig’s Lemma 8.4 is applicable.⊓⊔11.3 Transformation into Nondeterministic ProgramsThe meaning of distributed programs can be better understood through atransformation into nondeterministic programs.
In contrast to the transformation of parallel programs into nondeterministic programs described in Section 10.6 we do not need here any additional control variables. This is dueto the simple form of the distributed programs considered here, where i/ocommands appear only in the main loop. In the next section we use thistransformation as a basis for the verification of distributed programs.Throughout this section we consider a distributed programS ≡ [S1 k. .
.kSn ],where each process Si for i ∈ {1, . . . , n} is of the formiSi ≡ Si,0 ; do ⊓⊔mj=1 Bi,j ; αi,j → Si,j od.As abbreviation we introduceΓ = {(i, j, k, ℓ) | αi,j and αk,ℓ match and i < k}.We transform S into the following nondeterministic program T (S):T (S) ≡ S1,0 ; . . .; Sn,0 ;do ⊓⊔(i,j,k,ℓ)∈Γ Bi,j ∧ Bk,ℓ → Eff (αi,j , αk,ℓ );Si,j ; Sk,ℓod,where the use of elements of Γ to “sum” all guards in the loop should beclear.
In particular, when Γ = ∅ we drop this loop from T (S).Semantic Relationship Between S and T (S)The semantics of S and T (S) are not identical because the termination behavior is different. Indeed, upon termination of S the assertion11.3 Transformation into Nondeterministic ProgramsTERM ≡min ^^383¬Bi,ji=1 j=1holds. On the other hand, upon termination of T (S) the assertion^BLOCK ≡¬(Bi,j ∧ Bk,ℓ )(i,j,k,ℓ)∈Γholds. ClearlyTERM → BLOCKbut not the other way round. States that satisfy BLOCK ∧ ¬TERM are deadlock states of S.The semantics of the programs S and T (S) are related in a simple way bymeans of the following theorem that is crucial for our considerations.Theorem 11.1.
(Sequentialization) For all proper states σ(i) M[[S]](σ) = M[[T (S)]](σ) ∩ [[TERM ]],(ii) {⊥, fail} ∩ Mwtot [[S]](σ) = ∅ iff {⊥, fail} ∩ Mtot [[T (S)]](σ) = ∅,(iii) ∆ 6∈ Mtot [[S]](σ) iff M[[T (S)]](σ) ⊆ [[TERM ]].The Sequentialization Theorem relates a distributed program to a nondeterministic program. In contrast to previous theorems concerning correctnessof program transformations (Sequentialization Lemma 7.7, Atomicity Theorem 8.1 and Initialization Theorem 8.2) we do not obtain here a precisematch between the semantics of S and the transformed program T (S).One of the reasons is that the termination conditions for S and T (S) aredifferent.
As noted above, upon termination of S, the condition TERM holds,whereas upon termination of T (S) only a weaker condition BLOCK holds.This explains why the condition TERM appears in (i).Next, the sequentialization of the executions of the subprograms Si,j can“trade” a failure for divergence, or vice versa. A trivial example for this is aprogram S of the formS ≡ [S1,0 ; skip || S2,0 ; skip].Then T (S) is of the formT (S) ≡ S1,0 ; S2,0 ; skip.Suppose now that S1,0 yields ⊥ and S2,0 yields fail. Then S can fail whereasT (S) diverges. If on the other hand S1,0 yields fail and S2,0 yields ⊥, thenS can diverge, whereas T (S) fails.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
