3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 46
Текст из файла (страница 46)
In the next chapterwe explain, in the setting of general parallelism, how auxiliary variables canbe introduced in a systematic way.⊓⊔Summarizing, for proofs of partial correctness of disjoint parallel programswe use the following proof system PP.PROOF SYSTEM PP :This system consists of the group of axiomsand rules 1–6, 24, 25 and A2–A6.For proofs of total correctness of disjoint parallel programs we use thefollowing proof system TP.PROOF SYSTEM TP :This system consists of the group of axiomsand rules 1–5, 7, 24, 25 and A3–A6.Proof outlines for partial and total correctness of parallel programs aregenerated in a straightforward manner by the formation axioms and rulesgiven for while programs together with the following formation rule:(ix){pi } Si∗ {qi }, i ∈ {1, .
. . , n}VnVn{ i=1 pi } [{p1 } S1∗ {q1 }k. . .k{pn } Sn∗ {qn }] { i=1 qi }.Whether some variables are used as auxiliary variables is not visible fromproof outlines; it has to be stated separately.Example 7.4. The following proof outline records the proof of the correctness formula (7.1) in the proof systems PP and TP:{x = y}z := x;{x = z ∧ y = z}[ {x = z} x := x + 1 {x = z + 1}k {y = z} y := y + 1 {y = z + 1}]{x = z + 1 ∧ y = z + 1}{x = y}.Here z is just a normal program variable.
If one wants to use it as anauxiliary variable, the corresponding application of Rule 17 has to be statedseparately as in Example 7.3.⊓⊔7.3 Verification259SoundnessWe finish this section by proving soundness of the systems PP and TP. Tothis end we prove soundness of the new proof rules 24 and 25.Lemma 7.8. (Disjoint Parallelism) The disjoint parallelism rule (rule 24)is sound for partial and total correctness of disjoint parallel programs.Proof.
Suppose the premises of the disjoint parallelism rule are true in thesense of partial correctness for some pi s, qi s and Si s, i ∈ {1, . . . , n} such thatf ree(pi , qi ) ∩ change(Sj ) = ∅ for i 6= j.By the truth of the invariance axiom (Axiom A2 —see Theorem 3.7)|= {pi } Sj {pi }(7.2)|= {qi } Sj {qi }(7.3)andfor i, j ∈ {1, . . . , n} such that i 6= j. By the soundness of the conjunctionrule (Rule A4 —see Theorem 3.7), (7.2), (7.3) and the assumed truth of thepremises of the disjoint parallelism rule,VnVn|= { i=1 Vpi } S1 {q1 ∧ i=2 pi }, Vnn|= {q1 ∧ i=2 pi } S2 {q1 ∧ q2 ∧ i=3 pi },...Vn−1Vn|= { i=1 qi ∧ pn } Sn { i=1 qi }.By the soundness of the composition ruleVnVn|= { i=1 pi } S1 ; .
. .; Sn { i=1 qi };so by the soundness of the sequentialization rule 23VnVn|= { i=1 pi } [S1 k. . .kSn ] { i=1 qi }.An analogous proof using the invariance rule A6 instead of the invarianceaxiom takes care of total correctness.⊓⊔To prove soundness of the rule of auxiliary variables, we use the followinglemma which allows us to insert skip statements into any disjoint parallelprogram without changing its semantics.Lemma 7.9.
(Stuttering) Consider a disjoint parallel program S. Let S ∗result from S by replacing an occurrence of a substatement T in S by“skip; T ” or “T ; skip”. ThenM[[S]] = M[[S ∗ ]]and2607 Disjoint Parallel ProgramsMtot [[S]] = Mtot [[S ∗ ]].Proof. See Exercise 7.4.⊓⊔The name of this lemma is motivated by the fact that after inserting someskip statement into a disjoint parallel program we obtain a program in whosecomputations certain states are repeated.Lemma 7.10.
(Auxiliary Variables) The auxiliary variables rule (rule 25)is sound for partial and total correctness of disjoint parallel programs.Proof. Let A be a set of simple variables and S a disjoint parallel program.If A ∩ var(S) is a set of auxiliary variables of S, then we say that A agreeswith S. We then denote the program obtained from S by deleting from itall the assignments to the variables of A by SA , and the program obtainedfrom S by replacing by skip all the assignments to the variables of A byS[A := skip].Suppose now that A agrees with S. Then the Boolean expressions withinS and the assignments within S to the variables outside A do not containany variables from A.
Thus, if< S[A := skip], σ > → < S1′ , σ ′1 > → . . . → < Si′ , σ ′i > → . . .(7.4)is a computation of S[A := skip] starting in σ, then the corresponding computation of S starting in σ< S, σ > → < S1 , σ 1 > → . . . → < Si , σ i > → . . .(7.5)is such that for all iA agrees with Si , Si′ ≡ Si [A := skip], σ ′i [V ar − A] = σ i [V ar − A].(7.6)Conversely, if (7.5) is a computation of S starting in σ, then the correspondingcomputation of S[A := skip] starting in σ is of the form (7.4) where (7.6)holds.Thus, using the mod notation introduced in Section 2.3,M[[S]](σ) = M[[S[A := skip]]](σ) mod AandMtot [[S]](σ) = Mtot [[S[A := skip]]](σ) mod A.Note that S[A := skip] can be obtained from SA by inserting some skipstatements.
Thus, by the Stuttering Lemma 7.9,M[[SA ]](σ) = M[[S[A := skip]]](σ)andMtot [[SA ]](σ) = Mtot [[S[A := skip]]](σ).7.4 Case Study: Find Positive Element261Consequently,M[[S]](σ) = M[[SA ]](σ) mod A(7.7)Mtot [[S]](σ) = Mtot [[SA ]](σ) mod A.(7.8)andBy (7.7) for any assertion pM[[S]]([[p]]) = M[[SA ]]([[p]]) mod A.Thus, by Lemma 2.3(ii), for any assertion q such that f ree(q) ∩ A = ∅M[[S]]([[p]]) ⊆ [[q]] iff M[[SA ]]([[p]]) ⊆ [[q]].This proves the soundness of the auxiliary variables rule for partial correctness. The case of total correctness is handled analogously using (7.8) insteadof (7.7).⊓⊔Corollary 7.1. (Soundness of PP and TP)(i) The proof system PP is sound for partial correctness of disjoint parallelprograms.(ii) The proof system TP is sound for total correctness of disjoint parallelprograms.Proof.
The proofs of truth and soundness of the other axioms and proof rulesof PP and TP remain valid for disjoint parallel programs. These proofs relyon the Input/Output Lemma 3.3 and the Change and Access Lemma 3.4,which also hold for disjoint parallel programs (see Exercises 7.1 and 7.2). ⊓⊔7.4 Case Study: Find Positive ElementWe study here a problem treated in Owicki and Gries [1976a]. Consider aninteger array a and a constant N ≥ 1. The task is to write a program FINDthat finds the smallest index k ∈ {1, . .
., N } witha[k] > 0if such an element of a exists; otherwise the dummy value k = N + 1 shouldbe returned.Formally, the program FIND should satisfy the input/output specification{true}FIND{1 ≤ k ≤ N + 1 ∧ ∀(1 ≤ l < k) : a[l] ≤ 0 ∧ (k ≤ N → a[k] > 0)}(7.9)2627 Disjoint Parallel Programsin the sense of total correctness. Clearly, we require a 6∈ change(FIND).To speed up the computation, FIND is split into two components whichare executed in parallel: the first component S1 searches for an odd indexk and the second component S2 for an even one. The component S1 uses avariable i for the (odd) index currently being checked and a variable oddtopto mark the end of the search:S1 ≡ while i < oddtop doif a[i] > 0 then oddtop := ielse i := i + 2 fiod.The component S2 uses variables j and eventop for analogous purposes:S2 ≡ while j < eventop doif a[j] > 0 then eventop := jelse j := j + 2 fiod.The parallel program FIND is then given byFIND ≡ i := 1; j := 2; oddtop := N + 1; eventop := N + 1;[S1 kS2 ];k := min(oddtop, eventop).This is a version of the program FINDPOS studied in Owicki and Gries[1976a] where the loop conditions have been simplified to achieve disjointparallelism.
The original, more efficient, program FINDPOS is discussed inSection 8.6.To prove that FIND satisfies its input/output specification (7.9), we firstdeal with its components. The first component S1 searching for an odd indexstores its result in the variable oddtop. Thus it should satisfy{i = 1 ∧ oddtop = N + 1} S1 {q1 }(7.10)in the sense of total correctness where q1 is the following adaptation of thepostcondition of (7.9):q1 ≡1 ≤ oddtop ≤ N + 1∧ ∀l : (odd(l) ∧ 1 ≤ l < oddtop → a[l] ≤ 0)∧ (oddtop ≤ N → a[oddtop] > 0).Similarly, the second component S2 should satisfy{j = 2 ∧ eventop = N + 1} S2 {q2 },where(7.11)7.4 Case Study: Find Positive Elementq2 ≡2632 ≤ eventop ≤ N + 1∧ ∀l : (even(l) ∧ 1 ≤ l < eventop → a[l] ≤ 0)∧ (eventop ≤ N → a[eventop] > 0).The notation odd(l) and even(l) expresses that l is odd or even, respectively.We prove (7.10) and (7.11) using the proof system TW for total correctnessof while programs.
We start with (7.10). As usual, the main task is to findan appropriate invariant p1 and a bound function t1 for the loop in S1 .As a loop invariant p1 we choose a slight generalization of the postconditionq1 which takes into account the loop variable i of S1 :p1 ≡1 ≤ oddtop ≤ N + 1 ∧ odd(i) ∧ 1 ≤ i ≤ oddtop + 1∧ ∀l : (odd(l) ∧ 1 ≤ l < i → a[l] ≤ 0)∧ (oddtop ≤ N → a[oddtop] > 0).As a bound function t1 , we chooset1 ≡ oddtop + 1 − i.Note that the invariant p1 ensures that t1 ≥ 0 holds.We verify our choices by exhibiting a proof outline for the total correctnessof S1 :{inv : p1 }{bd : t1 }while i < oddtop do{p1 ∧ i < oddtop}if a[i] > 0 then {p1 ∧ i < oddtop ∧ a[i] > 0}{1 ≤ i ≤ N + 1 ∧ odd(i) ∧ 1 ≤ i ≤ i + 1∧ ∀l : (odd(l) ∧ 1 ≤ l < i → a[l] ≤ 0)∧ (i ≤ N → a[i] > 0)}oddtop := i{p1 }else {p1 ∧ i < oddtop ∧ a[i] ≤ 0}{1 ≤ oddtop ≤ N + 1 ∧ odd(i + 2)∧ 1 ≤ i + 2 ≤ oddtop + 1∧ ∀l : (odd(l) ∧ 1 ≤ l < i + 2 → a[l] ≤ 0)∧ (oddtop ≤ N → a[oddtop] > 0)}i := i + 2{p1 }fi{p1 }od{p1 ∧ oddtop ≤ i}{q1 }.It is easy to see that in this outline all pairs of subsequent assertions form validimplications as required by the consequence rule.
Also, the bound functiont1 decreases with each iteration through the loop.2647 Disjoint Parallel ProgramsFor the second component S2 we choose of course a similar invariant p2and bound function t2 :p2 ≡2 ≤ eventop ≤ N + 1 ∧ even(j) ∧ j ≤ eventop + 1∧ ∀l : (even(l) ∧ 1 ≤ l < j → a[l] ≤ 0)∧ (eventop ≤ N → a[eventop] > 0),andt2 ≡ eventop + 1 − j.The verification of (7.11) with p2 and t2 is symmetric to (7.10) and is omitted.We can now apply the rule of disjoint parallelism to (7.10) and (7.11)because the corresponding disjointness conditions are satisfied. We obtain{p1 ∧ p2 }[S1 kS2 ]{q1 ∧ q2 }.(7.12)To complete the correctness proof, we look at the following proof outlines{true}i := 1; j := 2; oddtop := N + 1; eventop := N + 1;{p1 ∧ p2 }(7.13)and{q1 ∧ q2 }(7.14){1 ≤ min(oddtop, eventop) ≤ N + 1∧ ∀(1 ≤ l < min(oddtop, eventop)) : a[l] ≤ 0∧ (min(oddtop, eventop) ≤ N → a[min(oddtop, eventop)] > 0)}k := min(oddtop, eventop){1 ≤ k ≤ N + 1 ∧ ∀(1 ≤ l < k) : a[l] ≤ 0 ∧ (k ≤ N → a[k] > 0)}.Applying the composition rule to (7.12), (7.13) and (7.14) yields the desiredformula (7.9) about FIND.7.5 Exercises7.1.
Prove the Input/Output Lemma 3.3 for disjoint parallel programs.7.2. Prove the Change and Access Lemma 3.4 for disjoint parallel programs.7.3. Let x and y be two distinct integer variables and let s and t be integerexpressions containing some free variables. State a condition on s and t suchthatM[[x := s; y := t]] = M[[y := t; x := s]]holds.7.5 Exercises2657.4.
Prove the Stuttering Lemma 7.9.7.5. Consider a computation ξ of a disjoint parallel program S ≡ [S1 k. . .kSn ].Every program occurring in a configuration of ξ is the parallel composition ofn components. To distinguish among the transitions of different components,we attach labels to the transition arrow → and writei< U, σ > → < V, τ >if i ∈ {1, .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
