3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 51
Текст из файла (страница 51)
To obtain a standard proof outline in theconclusion, it suffices to remove from it the assertions p ∧ B and p surrounding S ∗ .Convention In this and the next chapter we always refer to proof outlinesthat satisfy the stronger conditions of Definition 8.3.⊓⊔Parallel Composition: Interference FreedomThe total correctness of a parallel program is proved by considering interference free standard proof outlines for the total correctness of its componentprograms. In the definition of interference freedom both the assertions andthe bound functions appearing in the proof outlines must now be tested.
Thisis done as follows.Definition 8.4. (Interference Freedom: Total Correctness)(1) Let S be a component program. Consider a standard proof outline{p} S ∗ {q} for total correctness and a statement A with the precondition pre(A). We say that A does not interfere with {p} S ∗ {q} if thefollowing two conditions are satisfied:(i) for all assertions r in {p} S ∗ {q} the correctness formula{r ∧ pre(A)} A {r}holds in the sense of total correctness,(ii) for all bound functions t in {p} S ∗ {q} the correctness formula{pre(A) ∧ t = z} A {t ≤ z}holds in the sense of total correctness, where z is an integer variablenot occurring in A, t or pre(A).(2) Let [S1 k.
. .kSn ] be a parallel program. Standard proof outlines{pi } Si∗ {qi }, i ∈ {1, . . . , n}, for total correctness are called interferencefree if no normal assignment or atomic region A of a component programSi interferes with the proof outline {pj } Sj∗ {qj } of another componentprogram Sj where i 6= j.⊓⊔Thus interference freedom for total correctness means that the executionof atomic steps of one component program neither falsifies the assertions8.5 Verification: Total Correctness287(condition (i)) nor increases the bound functions (condition (ii)) used in theproof outline of any other component program.Note that the correctness formulas of condition (ii) have the same formas the ones considered in the second premise of formation rule (xi) for proofoutlines for total correctness of while loops.
In particular, the value of boundfunctions may drop during the execution of other components.As in the case of partial correctness, normal assignments and atomic regions need not be checked for interference freedom against assertions andbound functions from which they are disjoint.By referring to this extended notion of interference freedom, we may reusethe parallelism with shared variables rule 27 for proving total correctness ofparallel programs. Altogether we now use the following proof system TSV fortotal correctness of parallel programs with shared variables.PROOF SYSTEM TSV :This system consists of the group of axiomsand rules 1–5, 7, 25–27 and A3–A6.Example 8.4. As a first application of this proof system let us prove thatthe programS ≡ [while x > 2 do x := x − 2 odkx := x − 1]satisfies the correctness formula{x > 0 ∧ even(x)} S {x = 1}in the sense of total correctness. We use the following standard proof outlinesfor the components of S:{inv : x > 0}{bd : x}while x > 2 do{x > 2}x := x − 2od{x = 1 ∨ x = 2}and{even(x)} x := x − 1 {odd(x)}.Here even(x) and odd(x) express that x is an even or odd integer value,respectively.
These proof outlines satisfy the requirements of Definition 8.4:the only syntactic path in the loop body consists of the assignment x := x−2,and the bound function t ≡ x gets decreased by executing this assignment.Interference freedom of the proof outlines is easily shown. For example,{x > 2 ∧ even(x)} x := x − 1 {x > 2},2888 Parallel Programs with Shared Variablesholds because of x > 2 ∧ even(x) → x > 3. Thus the parallelism with sharedvariables rule 27 used now for total correctness is applicable and yields thedesired correctness result.⊓⊔SoundnessFinally, we prove soundness of the system TSV for total correctness. To thisend we first establish the following lemma.Lemma 8.9.
(Termination) Let {pi } Si∗ {qi }, i ∈ {1, . . . , n}, be interference free standard proof outlines for total correctness for component programsSi . Thenn^pi ]]).(8.13)⊥ 6∈ Mtot [[[S1 k. . .kSn ]]]([[i=1Proof. Suppose that the converse holds. ConsiderVan infinite computationnξ of [S1 k. . .kSn ] starting in a state σ satisfying i=1 pi . For some loopwhile B do S od within a component Si infinitely many configurations in ξare of the form< [T1 k. .
.kTn ], τ >(8.14)such that Ti ≡ at(while B do S od, Si ) and the ith component is activatedin the transition step from the configuration (8.14) to its successor configuration in ξ.Let p be the invariant and t the bound function associated with this loop.By the Strong Soundness for Parallel Programs Lemma 8.8, for each configuration of the form (8.14) we have τ |= p because p ≡ pre(while B do S od).But p → t ≥ 0 holds by virtue of the definition of the proof outline for totalcorrectness of component programs (Definition 8.3), so for each configurationof the form (8.14)τ (t) ≥ 0.(8.15)Consider now two consecutive configurations in ξ of the form (8.14), say< R1 , τ1 > and < R2 , τ2 >.
In the segment η of ξ starting at < R1 , τ1 > andending with < R2 , τ2 > a single iteration of the loop while B do S od tookplace. Let π ∈ path(S) be the path through S, in the sense of Definition 8.2,which was taken in this iteration.Let A be a normal assignment or an atomic region executed within thesegment η, say in the state σ 1 , and let σ 2 be the resulting state. Thus< A, σ 1 > → < E, σ 2 > .By Lemma 8.8, σ 1 |= pre(A). Suppose that A is a subprogram of Sj wherei 6= j. Then by the definition of interference freedom (Definition 8.4(1)(ii)),we have {pre(A) ∧ t = z} A {t < z} and thus σ 2 (t) ≤ σ 1 (t).8.5 Verification: Total Correctness289Suppose that A is a subprogram of Si .
Then A belongs to π. Thusby the definition of the proof outline for total correctness of loops{pre(A) ∧ t = z} A {t ≤ z} and thus σ 2 (t) ≤ σ 1 (t). Moreover, for some Abelonging to the path π we actually have {pre(A) ∧ t = z} A {t < z} andthus σ 2 (t) < σ 1 (t).This shows that the value of t during the execution of the segment ηdecreases; that is,τ2 (t) < τ1 (t).(8.16)Since this is true for any two consecutive configurations of the form (16) in theinfinite computation ξ, the statements (8.15) and (8.16) yield a contradiction.This proves (8.13).⊓⊔Corollary 8.3. (Parallelism with Shared Variables) The parallelismwith shared variables rule 27 is sound for total correctness of parallel programs.Proof. Consider interference free standard proof outlines for total correctness for component programs of a parallel program.
Then the TerminationLemma 8.9 applies. By removing from each of these proof outlines all annotations referring to the bound functions, we obtain interference free standardproof outlines for partial correctness. The desired conclusion now follows fromthe Parallelism with Shared Variables Corollary 8.1.⊓⊔Corollary 8.4. (Soundness of TSV) The proof system TSV is sound fortotal correctness of parallel programs.Proof. Follows by the same argument as the one given in the proof of theSoundness Corollary 7.1.⊓⊔DiscussionIt is useful to see why we could not retain in this section the original formationrule (formation rule (viii)) defining proof outlines for total correctness for awhile loop.Consider the following parallel programS ≡ [S1 kS2 ],where2908 Parallel Programs with Shared VariablesS1 ≡ while x > 0 doy := 0;if y = 0 then x := 0else y := 0 fiodandS2 ≡ while x > 0 doy := 1;if y = 1 then x := 0else y := 1 fiod.Individually, the while programs S1 and S2 satisfy the proof outlines fortotal correctness in which all assertions, including the loop invariants, equaltrue and the bound functions are in both cases max(x, 0).Indeed, in the case of S1 we have{x > 0 ∧ max(x, 0) = z}{z > 0}y := 0;if y = 0 then x := 0 else y := 0 fi{x = 0 ∧ z > 0}{max(x, 0) < z}and analogously for the case of S2 .Suppose now for a moment that we adopt the above proof outlines as proofoutlines for total correctness of the component programs S1 and S2 .
Since{max(x, 0) = z} x := 0 {max(x, 0) ≤ z}holds, we conclude that these proof outlines are interference free in the senseof Definition 8.4. By the parallelism with shared variables rule 27 we thenobtain the correctness formula{true} S {true}in the sense of total correctness.However, it is easy to see that the parallel program S can diverge.
Indeed,consider the following initial fragment of a computation of S starting in astate σ in which x is positive:8.6 Case Study: Find Positive Element More Quickly1→2→1→2→1→1→2→2→291< [S1 kS2 ], σ >< [y := 0; if . . . fi; S1 kS2 ], σ >< [y := 0; if . . . fi; S1 ky := 1; if . .
. fi; S2 ], σ >< [if . . . fi; S1 ky := 1; if . . . fi; S2 ], σ[y := 0] >< [if . . . fi; S1 kif . . . fi; S2 ], σ[y := 1] >< [y := 0; S1 kif . . . fi; S2 ], σ[y := 1] >< [S1 kif . . . fi; S2 ], σ[y := 0] >< [S1 ky := 1; S2 ], σ[y := 0] >< [S1 kS2 ], σ[y := 1] > .To enhance readability in each step we annotated the transition relation →with the index of the activated component. Iterating the above scheduling ofthe component programs we obtain an infinite computation of S.Thus with proof outlines for total correctness in the sense of Definition 3.8,the parallelism with shared variables rule 27 would become unsound. Thisexplains why we revised the definition of proof outlines for total correctness.It is easy to see why with the new definition of proof outlines for total correctness we can no longer justify the proof outlines suggested above.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
