3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 45
Текст из файла (страница 45)
.. Consider a sequenceb0 → b1 → . . . → bk where b0 = a and bk = b. Then k > 0. Let b0 → . . . → bℓbe the longest prefix of b0 → . . . → bk which is an initial fragment of an infinite sequence a → c1 → c2 → . . .. Then ℓ is well defined, bℓ = cℓ and ℓ < k,since bk is → -maximal. Thus bℓ → bℓ+1 and bℓ → cℓ+1 . By the definition ofℓ, bℓ+1 6= cℓ+1 . By the Infinity Lemma 7.3 there exists an infinite sequencebℓ → bℓ+1 → . . .. This contradicts the choice of ℓ.⊓⊔To apply the Yield Lemma 7.4 to the case of disjoint parallel programs,we need the following lemma.Lemma 7.5. (Diamond) Let S be a disjoint parallel program and σ a properstate. Whenever< S, σ >ւ ց< S1 , σ 1 >6=< S2 , σ 2 >,then for some configuration < T, τ >< S1 , σ 1 > < S2 , σ 2 >ց ւ< T, τ >.Proof.
By the Determinism Lemma 3.1 and the interleaving transition rule(viii), the program S is of the form [T1 k. . .kTn ] where T1 , . . ., Tn are pairwisedisjoint while programs, and S1 and S2 result from S by transitions of twoof these while programs, some Ti and Tj , with i 6= j. More precisely, forsome while programs Ti′ and Tj′2527 Disjoint Parallel ProgramsS1 = [T1 k. . .kTi′ k. . .kTn ],S2 = [T1 k. .
.kTj′ k. . .kTn ],< Ti , σ > → < Ti′ , σ 1 >,< Tj , σ > → < Tj′ , σ 2 > .Define T and τ as follows:T = [T1′ k. . .kTn′ ],where for k ∈ {1, . . . , n} with k 6= i and k 6= jTk′ = Tkand for any variable uu ∈ change(Ti ), σ 1 (u) ifu ∈ change(Tj ),τ (u) = σ 2 (u) ifσ(u) otherwise.By disjointness of Ti and Tj , the state τ is well defined. Using the Changeand Access Lemma 3.4 it is easy to check that both < S1 , σ 1 > → < T, τ >and < S2 , σ 2 > → < T, τ >.⊓⊔As an immediate corollary we obtain the desired result.Lemma 7.6.
(Determinism) For every disjoint parallel program S andproper state σ, Mtot [[S]](σ) has exactly one element.Proof. By Lemmata 7.4 and 7.5 and observing that for every proper stateσ, Mtot [[S]](σ) = yield(< S, σ >).⊓⊔SequentializationThe Determinism Lemma helps us provide a quick proof that disjoint parallelism reduces to sequential composition. In Section 7.3 this reduction enablesus to state a first, very simple proof rule for disjoint parallelism.
To relatethe computations of sequential and parallel programs, we use the followinggeneral notion of equivalence.Definition 7.4. Two computations are input/output equivalent, or simplyi/o equivalent, if they start in the same state and are either both infiniteor both finite and then yield the same final state. In later chapters we alsoconsider error states such as fail or ∆ among the final states.⊓⊔7.3 Verification253Lemma 7.7. (Sequentialization) Let S1 , . .
., Sn be pairwise disjoint whileprograms. ThenM[[[S1 k. . .kSn ]]] = M[[S1 ; . . .; Sn ]],andMtot [[[S1 k. . .kSn ]]] = Mtot [[S1 ; . . .; Sn ]].Proof. We call a computation of [S1 k. . .kSn ] sequentialized if the componentsS1 , . . ., Sn are activated in a sequential order: first execute exclusively S1 ,then, in case of termination of S1 , execute exclusively S2 , and so forth.We claim that every computation of S1 ; .
. .; Sn is i/o equivalent to asequentialized computation of [S1 k. . .kSn ].This claim follows immediately from the observation that the computations of S1 ; . . .; Sn are in a one-to-one correspondence with the sequentialized computations of [S1 k. . .kSn ]. Indeed, by replacing in a computation ofS1 ; . . .; Sn each configuration of the form< T ; Sk+1 ; . .
.; Sn , τ >by< [Ek. . .kEkT kSk+1 k. . .kSn ], τ >we obtain a sequentialized computation of [S1 k. . .kSn ]. Conversely, in a sequentialized computation of [S1 k. . .kSn ] each configuration is of the latterform, so by applying to such a computation the above replacement operationin the reverse direction, we obtain a computation of S1 ; . .
.; Sn .This claim implies that for every state σMtot [[S1 ; . . .; Sn ]](σ) ⊆ Mtot [[[S1 k. . .kSn ]]](σ).By the Determinism Lemmata 3.1 and 7.6, both sides of the above inclusionhave exactly one element. Thus in fact equality holds. This also impliesM[[S1 ; . . .; Sn ]](σ) = M[[[S1 k. . .kSn ]]](σ)and completes the proof of the lemma.⊓⊔7.3 VerificationPartial and total correctness of disjoint parallel programs S ≡ [S1 k. . .kSn ]are defined as for while programs. Thus for partial correctness we have|= {p} S {q} iff M[[S]]([[p]]) ⊆ [[q]]and for total correctness2547 Disjoint Parallel Programs|=tot {p} S {q} iff Mtot [[S]]([[p]]) ⊆ [[q]].Parallel CompositionThe Sequentialization Lemma 7.7 suggests the following proof rule for disjointparallel programs.RULE 23: SEQUENTIALIZATION{p} S1 ; .
. .; Sn {q}{p} [S1 k. . .kSn ] {q}By the Sequentialization Lemma 7.7 this rule is sound for both partialand total correctness. Thus when added to the previous proof systems PWor TW for partial or total correctness of while programs, it yields a soundproof system for partial or total correctness of disjoint parallel programs. Fora very simple application let us look at the following example.Example 7.2. We wish to show|=tot {x = y} [x := x + 1ky := y + 1] {x = y};that is, if x and y have identical values initially, the same is true upon termination of the parallel program.
By the sequentialization rule it suffices toshow|=tot {x = y} x := x + 1; y := y + 1 {x = y},which is an easy exercise in the proof system TW of Chapter 3.⊓⊔Though simple, the sequentialization rule has an important methodological drawback. Proving its premise amounts —by the composition rule— toproving{p} S1 {r1 }, . . ., {ri−1 } Si {ri }, . . ., {rn−1 } Sn {q}for appropriate assertions r1 , .
. ., rn−1 . Thus the pre- and post-assertions ofdifferent components of [S1 k. . .kSn ] must fit exactly. This does not reflect theidea of disjoint parallelism that S1 , . . ., Sn are independent programs.What we would like is a proof rule where the input/output specificationof [S1 k. . .kSn ] is simply the conjunction of the input/output specifications ofits components S1 , . . ., Sn . This aim is achieved by the following proof rulefor disjoint parallel programs proposed in Hoare [1972].7.3 Verification255RULE 24: DISJOINT PARALLELISM{pi } Si {qi }, i ∈ {1, . .
. , n}VnVn{ i=1 pi } [S1 k. . .kSn ] { i=1 qi }where f ree(pi , qi ) ∩ change(Sj ) = ∅ for i 6= j.The premises of this rule are to be proven in the proof systems PW orTW for while programs. Depending on whether we choose PW or TW, theconclusion of the rule holds in the sense of partial or total correctness, respectively.This proof rule links parallel composition of programs with logical conjunction of the corresponding pre- and postconditions and also sets the basicpattern for the more complicated proof rules needed to deal with shared variables and synchronization in Chapters 8 and 9. In the present case of disjointparallel programs the proof rule allows us to reason compositionally aboutthe input/output behavior of disjoint parallel programs: once we know thepre- and postconditions of the component programs we can deduce that thelogical conjunction of these conditions yields the pre- and postcondition ofthe parallel program.Requiring disjointness of the pre- and postconditions and the componentprograms in the disjoint parallelism rule is necessary.Without it we could, for example, derive from the true formulas{y = 1} x := 0 {y = 1} and {true} y := 0 {true}the conclusion{y = 1} [x := 0ky := 0] {y = 1},which is of course wrong.However, due to this restriction the disjoint parallelism rule is weaker thanthe sequentialization rule.
For example, one can show that the correctnessformula{x = y} [x := x + 1ky := y + 1] {x = y}of Example 7.2 cannot be proved using the disjoint parallelism rule (see Exercise 7.9). Intuitively, we cannot express in a single assertion pi or qi anyrelationship between variables changed in different components, such as therelationship x = y. But let us see in more detail where a possible proof breaksdown.Clearly, we can use a fresh variable z to prove{x = z} x := x + 1 {x = z + 1}and{y = z} y := y + 1 {y = z + 1}.2567 Disjoint Parallel ProgramsThus by the disjoint parallelism rule we obtain{x = z ∧ y = z} [x := x + 1ky := y + 1] {x = z + 1 ∧ y = z + 1}.Now the consequence rule yields{x = z ∧ y = z} [x := x + 1ky := y + 1] {x = y}.But we cannot simply replace the preassertion x = z ∧ y = z by x = ybecause the implicationx=y→x=z ∧ y =zdoes not hold.
On the other hand, we have{x = y} z := x {x = z ∧ y = z};so by the composition rule{x = y} z := x; [x := x + 1ky := y + 1] {x = y}.(7.1)To complete the proof we would like to drop the assignment z := x. But howmight we justify this step?Auxiliary VariablesWhat is needed here is a new proof rule allowing us to delete assignments toso-called auxiliary variables.The general approach thus consists of extending the program by the assignments to auxiliary variables, proving the correctness of the extended programand then deleting the added assignments. Auxiliary variables should neitherinfluence the control flow nor the data flow of the program, but only recordsome additional information about the program execution. The following definition identifies sets of auxiliary variables in an extended program.Definition 7.5. Let A be a set of simple variables in a program S. We callA a set of auxiliary variables of S if each variable from A occurs in S only inassignments of the form z := t with z ∈ A.⊓⊔Since auxiliary variables do not appear in Boolean expressions, they cannotinfluence the control flow in S, and since they are not used in assignments tovariables outside of A, auxiliary variables cannot influence the data flow inS.
As an example, consider the programS ≡ z := x; [x := x + 1ky := y + 1].7.3 Verification257Then∅, {y}, {z}, {x, z}, {y, z}, {x, y, z}are all sets of auxiliary variables of S.Now we can state the announced proof rule which was first introduced inOwicki and Gries [1976a].RULE 25: AUXILIARY VARIABLES{p} S {q}{p} S0 {q}where for some set of auxiliary variables A of S with f ree(q) ∩ A = ∅, theprogram S0 results from S by deleting all assignments to variables in A.This deletion process can result in incomplete programs. For example,taking A = {y} andS ≡ z := x; [x := x + 1ky := y + 1],the literal deletion of the assignment y := y + 1 would yieldz := x; [x := x + 1k • ]with a “hole” • in the second component. By convention, we fill in such“holes” by skip.
Thus in the above example we obtainS ′ ≡ z := x; [x := x + 1kskip].Like the disjoint parallelism rule, the auxiliary variables rule is appropriatefor both partial and total correctness.Example 7.3. As an application of the auxiliary variables rule we can nowcomplete the proof of our running example. We have already proved thecorrectness formula (7.1); that is,{x = y} z := x; [x := x + 1ky := y + 1] {x = y}with the rule of disjoint parallelism. Using the auxiliary variables rule we candelete the assignment to z and obtain{x = y} [x := x + 1ky := y + 1] {x = y},the desired correctness formula.In this proof the auxiliary variable z served to link the values of the program variables x and y. In general, auxiliary variables serve to record additional information about the course of computation in a program that isnot directly expressible in terms of the program variables. This additional2587 Disjoint Parallel Programsinformation then makes possible the correctness proof.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
