3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 56
Текст из файла (страница 56)
, n}, Ri is an await statement in Si .(ii) Given interference free standard proof outlines {pi } Si∗ {qi } for weaktotal correctness, i ∈ {1, . . . , n}, we associate with every potential deadlock of S a corresponding tuple (r1 , . . ., rn ) of assertions by put-ting fori ∈ {1, . . . , n}:• ri ≡ pre(Ri ) ∧ ¬B if Ri ≡ await B then S end,• ri ≡ qi if Ri ≡ E.⊓⊔VnIf we can show ¬ i=1 ri for every such tuple (r1 , .
. ., rn ) of assertions,none of the potential deadlocks can actually arise. This is how deadlock freedom is established in the second premise of the following proof rule for totalcorrectness of parallel programs.RULE 29: PARALLELISM WITH DEADLOCK FREEDOM(1) The standard proof outlines {pi } Si∗ {qi }, i ∈ {1, . . . , n}for weak total correctness are interference free,(2) For every potential deadlock (R1 , . . ., Rn ) of[S1 k. . .kSn ] the corresponding tupleVn ofassertions (r1 , . .
., rn ) satisfies ¬ i=1 ri .VnVn{ i=1 pi } [S1 k. . .kSn ] { i=1 qi }To prove total correctness of parallel programs with synchronization, we usethe following proof system TSY :PROOF SYSTEM TSY :This system consists of the group of axiomsand rules 1–5, 7, 25, 28, 29 and A2–A6.Proof outlines for parallel programs with synchronization are defined in astraightforward manner (cf. Chapter 7).The following example illustrates the use of rule 29 and demonstrates thatfor the components of parallel programs we cannot prove in isolation morethan weak total correctness.Example 9.2.
We now wish to prove the correctness formula{x = 0} [await x = 1 then skip endkx := 1] {x = 1}(9.1)of Example 9.1 in the proof system TSY. For the component programs weuse the following interference free standard proof outlines for weak total cor-3169 Parallel Programs with Synchronizationrectness:{x = 0 ∨ x = 1} await x = 1 then skip end {x = 1}(9.2)and{x = 0} x := 1 {x = 1}.Formula (9.2) is proved using the synchronization rule 28; it is true only in thesense of weak total correctness because the execution of the await statementgets blocked when started in a state satisfying x = 0.Deadlock freedom is proved as follows. The only potential deadlock is(await x = 1 then skip end, E).(9.3)The corresponding pair of assertions is((x = 0 ∨ x = 1) ∧ x 6= 1, x = 1),the conjunction of which is clearly false.
This shows that deadlock cannotarise. Rule 29 is now applicable and yields (9.1) as desired.⊓⊔SoundnessWe now prove the soundness of PSY. Since we noted already the soundnessof the synchronization rule 28, we concentrate here on the soundness proofsof the auxiliary variables rule 25 and the parallelism with shared variablesrule 27.Lemma 9.2. (Auxiliary Variables) The auxiliary variables rule 25 issound for partial (and total) correctness of parallel programs with synchronization.Proof.
See Exercise 9.6.⊓⊔To prove the soundness of the parallelism with shared variables rule 27 forpartial correctness of parallel programs with synchronization, we proceed asin the case of parallel programs with shared variables in Chapter 8. Namely,we first prove the following lemma analogous to the Strong Soundness forParallel Programs Lemma 8.8.Lemma 9.3. (Strong Soundness for Parallel Programs with Synchronization) Let {pi } Si∗ {qi }, i ∈ {1, . .
. , n}, be interference free standardproof outlines for partial correctness for component programs Si . Suppose that< [S1 k. . .kSn ], σ > →∗ < [R1 k. . .kRn ], τ >9.3 Verification317Vnfor 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 .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 9.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 considered in the formulation of the lemma, and proceeds analogously to theproof of the Strong Soundness for Parallel Programs Lemma 8.8. We needonly to consider one more case in the induction step: the last transition ofthe considered transition sequence is due to a step< Rk′ , τ ′ > → < Rk , τ >(9.4)of the kth component executing an await statement, say await B then Send.
ThenRk′ ≡ at(await B then S end, Sk ).By the induction hypothesis τ ′ |= pre(await B then S end). Also by thesemantics of await statements τ ′ |= B. Two cases now arise.Case 1 j = k.By the definition of a proof outline, in particular formation rule (xii) forthe await statements, there exist assertions p and q and an annotated versionS ∗ of S such that the following three properties hold:pre(await B then S end) → p,(9.5){p ∧ B} S ∗ {q} is a proof outline for partial correctness,(9.6)q → r.(9.7)Here r is the assertion associated with Rj and defined in the proof of theStrong Soundness for Parallel Programs Lemma 8.8, so r ≡ pre(T ) if Rj ≡at(T, Sj ) for a normal subprogram T of Sj and r ≡ qj if Rj ≡ E.Since τ ′ |= pre(await B then S end) ∧ B, by (9.5)τ ′ |= p ∧ B.(9.8)By (9.4)< await B then S end, τ ′ > → < E, τ >,so by the definition of semantics< S ′ , τ ′ > →∗ < E, τ > .(9.9)3189 Parallel Programs with SynchronizationNow by (9.6), (9.8) and (9.9), and by virtue of the Strong Soundness Theorem 3.3 we get τ |= q.
By (9.7) we conclude τ |= r.Case 2 j 6= k.The argument is the same as in the proof of the Strong Soundness forParallel Programs Lemma 8.8.⊓⊔Corollary 9.1. (Parallelism) The parallelism with shared variables rule 27is sound for partial correctness of parallel programs with synchronization.Corollary 9.2. (Soundness of PSY) The proof system PSY is sound forpartial correctness of parallel programs with synchronization.Proof.
We use the same argument as in the proof of the Soundness Corollary 7.1.⊓⊔Next, we prove soundness of the proof system TSY for total correctness ofparallel programs with synchronization. We concentrate here on the soundness proof of the new parallelism rule 29. To this end we establish the following two lemmata. The first one is an analogue of Termination Lemma 8.9.Lemma 9.4.
(Divergence Freedom) Let {pi } Si∗ {qi }, i ∈ {1, . . . , n}, beinterference free standard proof outlines for weak total correctness for component programs Si . ThenVn⊥ 6∈ Mtot [[[S1 k. . .kSn ]]]([[ i=1 pi ]]).Proof. The proof is analogous to the proof of the Termination Lemma 8.9.It relies now on the definition of proof outlines for weak total correctnessand the Strong Soundness for Component Programs Lemma 9.1 instead ofDefinition 8.3 and the Strong Soundness for Parallel Programs Lemma 8.8.Lemma 9.5.
(Deadlock Freedom) Let {pi } Si∗ {qi }, i ∈ {1, . . . , n}, beinterference free standard proof outlines for partial correctness for component programs Si . Suppose that for every potential deadlock (R1 , . . ., Rn )ofV[S1 k. . .kSn ] the corresponding tuple of assertions (r1 , . . ., rn ) satisfiesn¬ i=1 ri . ThenVn∆ 6∈ Mtot [[[S1 k. . .kSn ]]]([[ i=1 pi ]]).Proof. Suppose that the converse holds. Then for some states σ and τ andcomponent programs T1 , . . ., Tn< [S1 k.
. .kSn ], σ > →∗ < [T1 k. . .kTn ], τ >,where < [T1 k. . .kTn ], τ > is a deadlock.By the definition of deadlock,(9.10)9.4 Case Study: Producer/Consumer Problem319(i) for every i ∈ {1, . . . , n} eitherTi ≡ at(Ri , Si )(9.11)for some await statement Ri in the component program Si , orTi ≡ E,(9.12)(ii) for some i ∈ {1, . . . , n} case (9.11) holds.By collecting the await statements Ri satisfying (9.11) and by definingRi ≡ E in case of (9.12), we obtain a potential deadlock (R1 , .
. ., Rn ) of[S1 k. . .kSn ]. Consider now the corresponding tuple of assertions (r1 , . . ., rn )and fix some i ∈ {1, . . . , n}.If Ri ≡ await B then S end for some B and S, then ri ≡ pre(Ri ) ∧ ¬B.By the Strong Soundness for Component Programs Lemma 9.1, (9.10) and(9.11) we have τ |= pre(Ri ). Moreover, since < [T1 k. . .kTn ], τ > is a deadlock,τ |= ¬B also. Thus τ |= ri .If Ri ≡ E, then ri ≡ qi . By the Strong Soundness for Component ProgramsLemma 9.1, (9.10)Vnwe have τ |= ri , as well.Vn and (9.11)⊔Thus τ |= i=1 ri ; so ¬ i=1 ri is not true. This is a contradiction.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
