3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 50
Текст из файла (страница 50)
Tothis purpose four correctness formulas need to be verified. For example, theproof that the atomic region in (8.9) does not interfere with the postconditionof (8.10) is as follows:{(x = 0 ∨ x = 2) ∧ (¬done → x = 0) ∧ ¬done}{x = 0}hx := x + 2; done := truei{x = 2 ∧ done}{(x = 0 ∨ x = 2) ∧ (¬done → x = 0)}.The remaining three cases are in fact trivial. The parallelism with sharedvariables rule 27 applied to (8.9) and (8.10) and the consequence rule nowyield{¬done}[hx := x + 2; done := trueikx := 0]{x = 0 ∨ x = 2}.(8.11)8.4 Verification: Partial Correctness281On the other hand, the correctness formula{true} done := false {¬done}(8.12)obviously holds.
Thus, applying the composition rule to (8.11) and (8.12)yields (8.8) as desired.⊓⊔The above correctness proof is more complicated than expected. In particular, the introduction of the auxiliary variable done required some insightinto the execution of the given program. The use of done brings up twoquestions: how do we find appropriate auxiliary variables? Is there perhapsa systematic way of introducing them? The answer is affirmative. Followingthe lines of Lamport [1977], one can show that it is sufficient to introduce aseparate program counter for each component of a parallel program. A program counter is an auxiliary variable that has a different value in front ofevery substatement in a component.
It thus mirrors exactly the control flowin the component. In most applications, however, only partial informationabout the control flow is sufficient. This can be represented by a few suitableauxiliary variables such as the variable done above.It is interesting to note that the atomicity of hx := x + 2; done := trueiis decisive for the correctness proof in Example 8.3.
If the sequence of the twoassignments were interruptable, we would have to consider the proof outlines{¬done} x := x + 2; {¬done} done := true {true}and{true} x := 0 {(x = 0 ∨ x = 2) ∧ (¬done → x = 0)}which are not interference free. For example, the assignment x := x + 2interferes with the postcondition of x := 0. The introduction of the atomicregion hx := x + 2; done := truei is a typical example of virtual atomicitymentioned in Section 8.3: this atomic region is not a part of the originalprogram; it appears only in its correctness proof.Summarizing, to prove partial correctness of parallel programs with sharedvariables, we use the following proof system PSV :PROOF SYSTEM PSV :This system consists of the group of axiomsand rules 1–6, 25–27 and A2–A6.2828 Parallel Programs with Shared VariablesSoundnessWe now prove soundness of PSV for partial correctness.
Since we have alreadynoted the soundness of the atomic region rule 26, we concentrate here on thesoundness proofs of the auxiliary variables rule 25 and the parallelism withshared variables rule 27.Lemma 8.7. (Auxiliary Variables) The rule of auxiliary variables(rule 25) is sound for partial (and total) correctness of parallel programs.Proof. The proof of Lemma 7.10 stating soundness of rule 25 for disjointparallel programs does not depend on the assumption of disjoint parallelism.See also Exercise 8.3.⊓⊔To prove the soundness of the parallelism with shared variables rule 27for partial correctness we first show a stronger property: considering simultaneously the interference free standard proof outlines {p1 } S1∗ {q1 },.
. .,{pn } Sn∗ {qn } yields a valid annotation for the parallel program[S1 k. . .kSn ]. MoreVnprecisely, in a computation of [S1 k. . .kSn ] starting in astate satisfying i=1 pi , whenever the control in a component Si reachesa point annotated by an assertion, this assertion is true. This is the strongsoundness property for parallel programs.Lemma 8.8. (Strong Soundness for Parallel Programs) Let{pi } Si∗ {qi }, i ∈ {1, . . . , n}, be interference free standard proof outlines forpartial correctness for component programs Si .
Suppose that< [S1 k. . .kSn ], σ > →∗ < [R1 k. . .kRn ], τ >Vnfor some state σ satisfying i=1 pi , some component programs Ri with i ∈{1, . . . , n} and some state τ . Then for j ∈ {1, . . . , n}• if Rj ≡ at(T, Sj ) for a normal subprogram T of Sj , then τ |= pre(T );• if Rj ≡ E then τ |= qj .In particular, whenever< [S1 k. . .kSn ], σ > →∗ < E, τ >then τ |=Vni=1qi .Proof.
Fix j ∈ {1, . . . , n}. It is easy to show that either Rj ≡ at(T, Sj ) fora normal subprogram T of Sj or Rj ≡ E (see Exercise 8.4). In the first caselet r stand for pre(T ) and in the second case let r stand for qj . We need toshow τ |= r.The proof is by induction on the length ℓ of the transition sequence< [S1 k. . .kSn ], σ > →∗ < [R1 k. . .kRn ], τ > .8.4 Verification: Partial Correctness283Induction basis : ℓ = 0. Then pj → r and σ = τ ; thus σ |= pj and hence τ |= r.Induction step : ℓ −→ ℓ + 1. Then for some Rk′ and τ ′< [S1 k. . .kSn ], σ > →∗ < [R1 k.
. .kRk′ k. . .kRn ], τ ′ >→ < [R1 k. . .kRk k. . .kRn ], τ >;that is, the last step in the transition sequence was performed by the kthcomponent. Thus< Rk′ , τ ′ > → < Rk , τ > .Two cases naturally arise.Case 1 j = k.Then an argument analogous to the one given in the proof of the StrongSoundness Theorem 3.3 and the Strong Soundness for Component ProgramsLemma 8.5 shows that τ |= r.Case 2 j 6= k.By the induction hypothesis τ ′ |= r. If the last step in the computationconsists of an evaluation of a Boolean expression, then τ = τ ′ and consequently τ |= r.Otherwise the last step in the computation consists of an execution of anassignment A or an atomic region A.
Thus< A, τ ′ > → < E, τ > .By the induction hypothesis, τ ′ |= pre(A). Thus τ ′ |= r ∧ pre(A). By interference freedom and the Soundness Theorem 3.1,|= {r ∧ pre(A)} A {r}.Thus τ |= r.⊓⊔Corollary 8.1. (Parallelism with Shared Variables) The parallelismwith shared variables rule 27 is sound for partial correctness of parallel programs.Corollary 8.2.
(Soundness of PSV) The proof system PSV is sound forpartial correctness of parallel programs.Proof. Follows by the same argument as the one given in the proof of theSoundness Corollary 7.1.⊓⊔2848 Parallel Programs with Shared Variables8.5 Verification: Total CorrectnessComponent ProgramsTotal correctness of component programs can be proved by using the proofsystem T W for the total correctness of while programs together with theatomic region rule 26 for atomic regions introduced in Section 8.4. This ruleis clearly sound for total correctness.However, somewhat unexpectedly, this approach leads to a definition ofproof outlines for total correctness that is too weak for our purposes. Toensure that, as a next step, total correctness of parallel programs can beproved by using interference free proof outlines for total correctness of thecomponent programs, we must strengthen the premises of the formation rule(viii) of Chapter 3 defining the proof outlines for total correctness of a whileloop:{p ∧ B} S ∗ {p},{p ∧ B ∧ t = z} S ∗∗ {t < z},p→t≥0{inv : p}{bd : t} while B do {p ∧ B} S ∗ {p} od {p ∧ ¬B}where t is an integer expression and z is an integer variable not occurring inp, t, B or S ∗∗ .
We clarify this point at the end of this section.In the premises of this rule we separated proofs outlines involving S ∗ andS for the facts that the assertion p is kept invariant and that the boundfunction t decreases, but only the proof S ∗ for the invariant p is recordedin the proof outline of the while loop. In the context of parallel programsit is possible that components interfere with the termination proofs of othercomponents.
To eliminate this danger we now strengthen the definition of aproof outline for total correctness and require that in proof outlines of loopswhile B do S od the bound function t is such that∗∗(i) all normal assignments and atomic regions inside S decrease t or leaveit unchanged,(ii) on each syntactically possible path through S at least one normal assignment or atomic region decreases t.By a path we mean here a possibly empty finite sequence of normal assignments and atomic regions.
Intuitively, for a sequential component program S,path(S) stands for the set of all syntactically possible paths through the component program S, where each path is identified with the sequence of normalassignments and atomic regions lying on it. This intuition is not completelycorrect because for while-loops we assume that they immediately terminate.The idea is that if the bound function t is to decrease along every syntactically possible path while never being increased, then it suffices to assume that8.5 Verification: Total Correctness285every while loop is exited immediately. Indeed, if along such “shorter” pathsthe decrease of the bound function t is guaranteed, then it is also guaranteedalong the “longer” paths that do take into account the loop bodies.The formal definition of path(S) is as follows.Definition 8.2.
For a sequential component S, we define the set path(S) byinduction on S:• path(skip) = {ε},• path(u := t) = {u := t},• path(hSi) = {hSi},• path(S1 ; S2 ) = path(S1 ) ; path(S2 ),• path(if B then S1 else S2 fi) = path(S1 ) ∪ path(S2 ),• path(while B do S od) = {ε}.⊓⊔In the above definition ε denotes the empty sequence and sequential composition π1 ; π2 of paths π1 and π2 is lifted to sets Π1 , Π2 of paths by puttingΠ1 ; Π2 = {π1 ; π2 | π1 ∈ Π1 and π2 ∈ Π2 }.For any path π we have π; ε = ε; π = π.We can now formulate the revised definition of a proof outline.Definition 8.3. (Proof Outline: Total Correctness) Proof outlines andstandard proof outlines for the total correctness of component programs aregenerated by the same formation axioms and rules as those used for defining(standard) proof outlines for the partial correctness of component programs.The only exception is the formation rule (v) dealing with while loops whichis replaced by the following formation rule.(xi)(1) {p ∧ B} S ∗ {p} is standard,(2) {pre(R) ∧ t = z} R {t ≤ z} for every normalassignment and atomic region R within S,(3) for each path π ∈ path(S) there existsa normal assignment or atomic region R in πsuch that{pre(R) ∧ t = z} R {t < z},(4) p → t ≥ 0{inv : p}{bd : t} while B do {p ∧ B} S ∗ {p} od {p ∧ ¬B}where t is an integer expression and z is an integer variable not occurring inp, t, B or S ∗ , and where pre(R) stands for the assertion preceding R in thestandard proof outline {p ∧ B} S ∗ {p} for total correctness.⊓⊔2868 Parallel Programs with Shared VariablesNote that in premise (1) formation rule (xi) expects a standard proof outline for total correctness but in its conclusion it produces a “non-standard”proof outline for the while loop.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
