3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 68

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

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

To establish the claim formulated at the beginning of this step we provetwo simpler claims.Claim 1 Every computation ξ of S is 2-equivalent to an almost good computation of S.Proof of Claim 1. Suppose ξ is a terminating computation or ends in a deadlock. Then no process is abandoned in it, so it is almost good.Suppose ξ is a computation that ends in a failure or is infinite. Assume ξ isnot almost good.

Let P1 , . . ., Pk ∈ {S1 , . . ., Sn }, where k ≥ 1, be the list of allprocesses abandoned in ξ, ordered in such a way that each Pj is abandonedin ξ before Pj+1 .Repeat for as long as possible the following steps, where initially γ = ξand j = 1:(i) insert in γ for as long as possible a step of Pj consisting of a privateaction,(ii) rename γ to the resulting computation and increment j.Suppose that for any γ and j step (i) does not insert any failure in γ andterminates.

Then after executing steps (i) and (ii) j times, Pj+1 , . . ., Pk isthe list of all processes abandoned in the resulting computation. Thus afterk repetitions of steps (i) and (ii) the resulting computation γ is almost goodand either ends in a failure or is infinite.Otherwise for some j step (i) inserts a failure in γ or does not terminate.Then the resulting computation is also almost good and either ends in afailure or is infinite.In both cases by definition the resulting computation is 2-equivalent to ξ.⊓⊔Claim 2 Every almost good computation ξ of S is 2-equivalent to a goodcomputation of S.11.3 Transformation into Nondeterministic Programs389Proof of Claim 2. We distinguish three cases.Case 1 ξ is properly terminating or ends in a deadlock.Then repeatedly using the Commutativity Lemma 11.2 we can transformξ to a 2-equivalent good computation (see Exercise 11.4).Case 2 ξ ends in a failure.Then repeatedly using the Commutativity Lemma 11.2 and the FailingLemma 11.3 we can transform ξ to a 2-equivalent failing computation (seeExercise 11.4).Case 3 ξ is infinite.Suppose that ξ starts in a state σ.

We first construct a series ξ1 , ξ2 , . . . ofgood transition sequences starting in < S, σ > such that for every k > 0• ξk+1 extends ξk ,• ξk+1 can be extended to an infinite almost good computation of S.We proceed by induction. Define ξ1 to be < S, σ >.Suppose that ξk has been defined (k > 0) and let γ be an extension of ξkto an infinite almost good computation of S.Let C be the last configuration of ξk . Suppose that there exists a transitioniC → D in which the process Si executes a private action. Choose the leastAsuch i.

Let F → G with A = i be the first transition in γ after C in whichthe process Si is activated. Such a transition exists, since in γ no process isabandoned.iIf such a transition C → D does not exist, then in C only the main loops’Aexits or communications can be performed. Let F → G with A = (i, j) be thefirst transition in γ after C in which a communication is performed. Such atransition exists since γ is infinite.By repeatedly applying the Commutativity Lemma 11.2, we obtain anAinfinite almost good computation with a transition C → D′ . Define now ξk+1Aas ξk followed by C → D′ .Now using the series ξ1 , ξ2 , .

. ., we can construct an infinite good computation of S starting in σ by defining its kth configuration to be the kthconfiguration of ξk .⊓⊔Claims 1 and 2 imply the claim formulated at the beginning of this stepbecause 2-equivalence is an equivalence relation.Step 5 Combining the claims of Steps 2 and 4 we obtain by virtue of theintroduced notions of 1- and 2-equivalence the proof of the claims (i)–(iii) ofthe theorem.⊓⊔39011 Distributed Programs11.4 VerificationThe three variants of semantics of distributed programs yield in the by nowstandard way three notions of program correctness: partial correctness, weaktotal correctness and total correctness.For the verification of these correctness properties we follow Apt [1986]and introduce particularly simple proof rules which we obtain from the Sequentialization Theorem 11.1.

Throughout this section we adopt the notationof the previous section. In particular, S stands for a distributed program ofthe form [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.Partial CorrectnessConsider first partial correctness.

We augment the proof system PN for partialcorrectness of nondeterministic programs by the following rule:RULE 34: DISTRIBUTED PROGRAMS{p} S1,0 ; . . .; Sn,0 {I},{I ∧ Bi,j ∧ Bk,ℓ } Eff (αi,j , αk,ℓ ); Si,j ; Sk,ℓ {I}for all (i, j, k, ℓ) ∈ Γ{p} S {I ∧ TERM }We call an assertion I that satisfies the premises of the above rule aglobal invariant relative to p. Also, we refer to a statement of the formEff (αi,j , αk,ℓ ); Si,j ; Sk,ℓ as a joint transition (within S) and to Bi,j ∧ Bk,ℓas the Boolean condition of this transition.

An execution of a joint transitioncorresponds to a joint execution of a pair of branches of the main loops withmatching generalized guards.Informally the above rule can be phrased as follows. If I is establishedupon execution of all the Si,0 sections and is preserved by each joint transition started in a state satisfying its Boolean condition, then I holds upontermination. This formulation explains why we call I a global invariant. Theword “global” relates to the fact that we reason here about all processessimultaneously and consequently adopt a “global” view.When proving that an assertion is a global invariant we usually argueinformally, but with arguments that can easily be formalized in the underlyingproof system PN.11.4 Verification391Weak Total CorrectnessHere we consider weak total correctness, which combines partial correctnesswith absence of failures and divergence freedom.

Consequently, we augmentthe proof system TN for total correctness of nondeterministic programs bythe following strengthening of the distributed programs rule 34:RULE 35: DISTRIBUTED PROGRAMS II(1) {p} S1,0 ; . . .; Sn,0 {I},(2) {I ∧ Bi,j ∧ Bk,ℓ } Eff (αi,j , αk,ℓ ); Si,j ; Sk,ℓ {I}for all (i, j, k, ℓ) ∈ Γ,(3) {I ∧ Bi,j ∧ Bk,ℓ ∧ t = z} Eff (αi,j , αk,ℓ ); Si,j ; Sk,ℓ {t < z}for all (i, j, k, ℓ) ∈ Γ,(4) I → t ≥ 0{p} S {I ∧ TERM }where t is an integer expression and z is an integer variable not appearing inp, t, I or S.Total CorrectnessFinally, consider total correctness. We must take care of deadlock freedom.We now augment the proof system TN for total correctness of nondeterministic programs by a strengthened version of the distributed programs II rule 35.It has the following form:RULE 36: DISTRIBUTED PROGRAMS III(1) {p} S1,0 ; . .

.; Sn,0 {I},(2) {I ∧ Bi,j ∧ Bk,ℓ } Eff (αi,j , αk,ℓ ); Si,j ; Sk,ℓ {I}for all (i, j, k, ℓ) ∈ Γ,(3) {I ∧ Bi,j ∧ Bk,ℓ ∧ t = z} Eff (αi,j , αk,ℓ ); Si,j ; Sk,ℓ {t < z}for all (i, j, k, ℓ) ∈ Γ,(4) I → t ≥ 0,(5) I ∧ BLOCK → TERM{p} S {I ∧ TERM }where t is an integer expression and z is an integer variable not appearing inp, t, I or S.39211 Distributed ProgramsThe new premise (5) allows us to deduce additionally that S is deadlockfree relative to p, and consequently to infer the conclusion in the sense oftotal correctness.Proof SystemsAlso, we use the following auxiliary rules which allow us to present the proofsin a more convenient way.RULE A8:RULE A9:I1 and I2 are global invariant relative to pI1 ∧ I2 is a global invariant relative to pI is a global invariant relative to p,{p} S {q}{p} S {I ∧ q}We use rule A8 in the proofs of partial correctness and rule A9 in theproofs of partial, weak total and total correctness.

Note that rule A8 hasseveral conclusions; so it is actually a convenient shorthand for a number ofclosely related rules.We thus use three proof systems: a proof system PDP for partial correctness of d istributed programs, a proof system WDP for w eak total correctness of d istributed programs and a proof system TDP for total correctnessof d istributed programs. These systems consist of the following axioms andproof rules.PROOF SYSTEM PDP :This system consists of the proof system PN augmentedby the group of axioms and rules 34, A8 and A9.PROOF SYSTEM WDP :This system consists of the proof system TN augmentedby the group of axioms and rules 35 and A9.PROOF SYSTEM TDP :This system consists of the proof system TN augmentedby the group of axioms and rules 36 and A9.11.4 Verification393Example 11.3.

As a first application of the above proof systems we provethe correctness of the program SR from Example 11.1. More precisely, weprove{M ≥ 1} SR {a[0 : M − 1] = b[0 : M − 1]}in the sense of total correctness. As a global invariant relative to M ≥ 1 wechooseI ≡ a[0 : i − 1] = b[0 : j − 1] ∧ 0 ≤ i ≤ M,where a[0 : j − 1] = b[0 : j − 1] is an abbreviation for the assertion∀(0 ≤ k < j) : a[k] = b[k] ∧ i = j.As a termination function we choose t ≡ M − i.In the program SR there is only one joint transition to consider, namely,b[j] := a[i]; i := i + 1; j := j + 1with the Boolean condition i 6= M ∧ j 6= M . Thus the premises of thedistributed programs III rule 36 amount to the following:(1) {M ≥ 1} i := 0; j := 0 {I},(2) {I ∧ i 6= M ∧ j 6= M } b[j] := a[i]; i := i + 1; j := j + 1 {I},(3) {I ∧ i =6 M ∧ j 6= M ∧ t = z}b[j] := a[i]; i := i + 1; j := j + 1{t < z},(4) I → t ≥ 0,(5) (I ∧ ¬(i 6= M ∧ j 6= M )) → i = M ∧ j = M .All these premises can be easily verified.

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

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