3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 53
Текст из файла (страница 53)
. .,and if R2 is disjoint from Sj with j 6= i, then there is also an infinite transitionsequence of the formj1RRj2ξ3 :< U, σ > →1 < U0 , σ 0 > →2 < V0 , τ0 > → < V1 , τ1 > → . . . .We say that ξ2 is obtained from ξ1 by deletion of the initial R1 -transitionand ξ3 is obtained from ξ1 by insertion of an R2 -transition.
Replacing thesuffix ξ1 of ξ by ξ2 or ξ3 yields an almost good computation of T which is i/oequivalent to ξ.Claim 2 Every almost good computation of T is permutation equivalent toa good computation of T .Proof of Claim 2. Using the Change and Access Lemma 3.4 we establish thefollowing: if Rk with k ∈ {1, 2} is disjoint from Sj with j 6= i, then theRjrelations →k and → commute, orRkjjR→ ◦ → = → ◦ →k ,where ◦ denotes relational composition (see Section 2.1). Repeated application of this commutativity allows us to permute the transitions of everyalmost good fragment ξ1 of a computation of T of the formRjmj1Rξ1 :< U, σ > →1 ◦ → ◦ . . . ◦ → ◦ →2 < V, τ >with jk 6= i for k ∈ {1, .
. ., m} into a good order, that is, intojmj1RRξ2 :< U, σ > → ◦ . . . ◦ → ◦ →1 ◦ →2 < V, τ >orRRj1jmξ3 :< U, σ > →1 ◦ →2 ◦ → ◦ . . . ◦ → < V, τ >depending on whether R1 or R2 is disjoint from Sj with j 6= i.Consider now an almost good computation ξ of T . We construct from ξ apermutation equivalent good computation ξ ∗ of T by successively replacingevery almost good fragment of ξ of the form ξ1 by a good fragment of theform ξ2 or ξ3 .Claims 1 and 2 together imply the claim of Step 4.Step 5 By combining the results of Steps 3 and 5, we get the claim of thetheorem for the case when S has no initialization part S0 and T resultsfrom S by splitting hR1 ; R2 i into hR1 i; hR2 i. The cases when S has an2988 Parallel Programs with Shared Variablesinitialization part S0 and where T results from S by splitting the atomicregion hif B then R1 else R2 fii are left as Exercise 8.11.⊓⊔Corollary 8.5.
(Atomicity) Under the assumptions of the Atomicity Theorem, for all assertions p and q|= {p} S {q} iff |= {p} T {q}and analogously for |=tot .The second transformation moves initializations of a parallel program inside one of its components.Theorem 8.2. (Initialization) Consider a parallel program of the formS ≡ S0 ; R0 ; [S1 k. . .kSn ],where S0 and R0 are while programs. Suppose that for some i ∈ {1, . . . , n}the initialization part R0 is disjoint from all component programs Sj withj 6= i. Then the programT ≡ S0 ; [S1 k.
. .kR0 ; Si k. . .kSn ]has the same semantics as S; that is,M[[S]] = M[[T ]] and Mtot [[S]] = Mtot [[T ]].Proof. The proof can be structured similarly to the one of the AtomicityTheorem and is left as Exercise 8.12.⊓⊔Corollary 8.6. (Initialization) Under the assumptions of the InitializationTheorem, for all assertions p and q|= {p} S {q} iff |= {p} T {q}and analogously for |=tot .The program S considered in the Atomicity Corollary 8.5 and Initialization Corollary 8.6 admits fewer points for possible interference among itscomponents and thus fewer computations than the corresponding programT .
Therefore S is easier to prove correct. Thus in correctness proofs we applythe program transformations for atomicity and initialization “backwards”;that is, programs of the form T are replaced by programs of the form S andthen verified. Examples show that this approach often avoids the need forauxiliary variables in the sense of rule 25.We could have reformulated the Corollaries 8.5 and 8.6 also as proof rulesand integrated them in the proof systems PSV and TSV introduced in Sections 8.4 and 8.5. However, we prefer to keep them separate to stress theirstatus as additional program transformations.8.8 Case Study: Parallel Zero Search2998.8 Case Study: Parallel Zero SearchLet us consider Solution 3 to the zero search problem given in Section 1.1,that is, the parallel programZERO-3 ≡ f ound := false; [S1 kS2 ]withS1 ≡ x := 0;while ¬f ound dox := x + 1;if f (x) = 0 then f ound := true fiodandS2 ≡ y := 1;while ¬f ound doy := y − 1;if f (y) = 0 then f ound := true fiod.We wish to prove the partial correctness of this solution, that is, that in caseof termination ZERO-3 has indeed found a zero of the function f in one ofits variables x or y:|= {true} ZERO-3 {f (x) = 0 ∨ f (y) = 0}.(8.18)Termination cannot be proved here; it holds only under the assumption offairness (see Chapter 1).We proceed in two steps.Step 1.
Simplifying the programWe first use the Atomicity Corollary 8.5 and Initialization Corollary 8.6 andreduce the original problem (8.18) to the following claim|= {∃u : f (u) = 0} T {f (x) = 0 ∨ f (y) = 0},whereT ≡ f ound := false; x := 0; y := 1;[T1 kT2 ]with(8.19)3008 Parallel Programs with Shared VariablesT1 ≡ while ¬f ound doh x := x + 1;if f (x) = 0 then f ound := true fiiodandT2 ≡ while ¬f ound doh y := y − 1;if f (y) = 0 then f ound := true fii.od.Both corollaries are applicable here by virtue of the fact that x does notappear in S2 and y does not appear in S1 .
Recall that by assumption, assignments and the skip statement are considered to be atomic regions.Step 2. Proving partial correctnessWe prove (8.19) in the proof system PSV for partial correctness of parallelprograms with shared variables introduced in Section 8.4. To this end, we needto construct interference free standard proof outlines for partial correctnessof the sequential components T1 and T2 of T .For T1 we use the invariantp1 ≡x≥0∧ (f ound → (x > 0 ∧ f (x) = 0) ∨ (y ≤ 0 ∧ f (y) = 0))∧ (¬f ound ∧ x > 0 → f (x) 6= 0)(8.20)(8.21)(8.22)to construct the standard proof outline{inv : p1 }while ¬f ound do{x ≥ 0 ∧ (f ound → y ≤ 0 ∧ f (y) = 0)∧ (x > 0 → f (x) 6= 0)}h x := x + 1;if f (x) = 0 then f ound := true fiiod{p1 ∧ f ound}.(8.23)Similarly, for T2 we use the invariantp2 ≡y≤1∧ (f ound → (x > 0 ∧ f (x) = 0) ∨ (y ≤ 0 ∧ f (y) = 0))∧ (¬f ound ∧ y ≤ 0 → f (y) 6= 0)to construct the standard proof outline(8.24)(8.25)(8.26)8.8 Case Study: Parallel Zero Search301{inv : p2 }while ¬f ound do{y ≤ 1 ∧ (f ound → x > 0 ∧ f (x) = 0)∧ (y ≤ 0 → f (y) 6= 0)}h y := y − 1;if f (y) = 0 then f ound := true fiiod{p2 ∧ f ound}.The intuition behind the invariants p1 and p2 is as follows.
Conjuncts(8.20) and (8.24) state the range of values that the variables x and y mayassume during the execution of the loops T1 and T2 .Thanks to the initialization of x with 0 and y with 1 in T , the conditionx > 0 expresses the fact that the loop T1 has been traversed at least once,and the condition y ≤ 0 similarly expresses the fact that the loop T2 has beentraversed at least once. Thus the conjuncts (8.21) and (8.25) in the invariantsp1 and p2 state that if the variable f ound is true, then the loop T1 has beentraversed at least once and a zero x of f has been found, or that the loop T2has been traversed at least once and a zero y of f has been found.The conjunct (8.22) in p1 states that if the variable f ound is false andthe loop T1 has been traversed at least once, then x is not a zero of f .
Theconjunct (8.26) in p2 has an analogous meaning.Let us discuss now the proof outlines. In the first proof outline the mostcomplicated assertion is (8.23). Note thatp1 ∧ ¬f ound → (8.23)as required by the definition of a proof outline. (We cannot use, instead of(8.23), the assertion p1 ∧ ¬f ound because the latter assertion does not passthe interference freedom test with respect to the loop body in T2 .)Given (8.23) as a precondition, the loop body in T1 establishes the invariant p1 as a postcondition, as required. Notice that the conjunctf ound → y ≤ 0 ∧ f (y) = 0in the precondition (8.23) is necessary to establish the conjunct (8.21) in theinvariant p1 .
Indeed, without this conjunct in (8.23), the loop body in T1would fail to establish (8.21) since initiallyf ound ∧ x > 0 ∧ f (x) = 0 ∧ f (x + 1) 6= 0 ∧ y ≤ 0 ∧ f (y) 6= 0might hold.Next we deal with the interference freedom of the above proof outlines. Intotal six correctness formulas must be proved. The three for each componentare pairwise symmetric.3028 Parallel Programs with Shared VariablesThe most interesting case is the interference freedom of the assertion (8.23)in the proof outline for T1 with the loop body in T2 .
It is proved by thefollowing proof outline:{x ≥ 0 ∧ (f ound → y ≤ 0 ∧ f (y) = 0) ∧ (x > 0 → f (x) 6= 0)∧ y ≤ 1 ∧ (f ound → x > 0 ∧ f (x) = 0) ∧ (y ≤ 0 → f (y) 6= 0)}{x ≥ 0 ∧ y ≤ 1 ∧ ¬f ound ∧ (x > 0 → f (x) 6= 0)}h y := y − 1;if f (y) = 0 then f ound := true fii{x ≥ 0 ∧ (f ound → y ≤ 0 ∧ f (y) = 0) ∧ (x > 0 → f (x) 6= 0)}.Note that the first assertion in the above proof outline indeed implies¬f ound:(f ound → (x > 0 ∧ f (x) = 0)) ∧ (x > 0 → f (x) 6= 0)impliesf ound → (f (x) 6= 0 ∧ f (x) = 0)implies¬f ound.This information is recorded in the second assertion of the proof outline andused to establish the last assertion.The remaining cases in the interference freedom proof are straightforwardand left to the reader.We now apply the parallelism with shared variables rule 27 and get{p1 ∧ p2 } [T1 kT2 ] {p1 ∧ p2 ∧ f ound}.Since for the initialization part of T the correctness formula{true} f ound := false; x := 0 : y := 1 {p1 ∧ p2 }holds, a straightforward application of the rule for sequential compositionand the consequence rule yields the desired partial correctness result (8.18).Of course, we could have avoided applying the program transformations inStep 1 and proved the correctness formula (8.18) directly in the proof systemP SV .
But this would lead to a more complicated proof because ZERO-3contains more interference points than T and thus requires a more complextest of interference freedom. In fact, we need auxiliary variables in the senseof rule 25 to deal with the initialization x := 0 and y := 1 within the parallelcomposition in ZERO-3 (see Exercise 8.8).
This shows that the AtomicityTheorem 8.1 and the Initialization Theorem 8.2 simplify the task of provingparallel programs correct.8.9 Exercises3038.9 Exercises8.1. Prove the Input/Output Lemma 3.3 for parallel programs.8.2. Prove the Change and Access Lemma 3.4 for parallel programs.8.3. Prove the Stuttering Lemma 7.9 for parallel programs.8.4. Suppose that< [S1 k. . .kSn ], σ > →∗ < [R1 k. . .kRn ], τ > .Prove that for j ∈ {1, . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
