3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 60
Текст из файла (страница 60)
In totalwe have to check 64 correctness formulas. However, a careful inspection ofthe proof outlines shows that only a few parts of the assertions and boundfunctions of each proof outline contain variables that can be modified by theother component.
For the proof outline of U1 there are the conjunctsturn = 1 ∨ turn = 2,¬f ound → x < u,f ound ∧ af ter2 → turn = 1.(9.32)(9.33)(9.36)Conjunct (9.32) is obviously preserved under the execution of the statementsin U2 . Conjunct (9.33) is preserved because the only way U2 can modify thevariable f ound is by changing its value from false to true.
With f ound evaluating to true, conjunct (9.33) is trivially satisfied. Finally, conjunct (9.36) ispreserved because, by the proof outline of U2 , whenever the variable af ter2is set to true, the variable turn is simultaneously set to 1.For the proof outline of U2 , only the conjunctsturn = 1 ∨ turn = 2,f ound ∧ af ter1 → turn = 2and the bound functiont2 ≡ turn + int(¬af ter1 ) + u − x(9.32)(9.39)9.7 Case Study: Synchronized Zero Search341contain variables that can be modified by U1 .
Conjuncts (9.32) and (9.39)are dealt with analogously to the conjuncts (9.32) and (9.36) from the proofoutline of U1 . Thus it remains to show that none of the atomic regions inU1 can increase the value of t2 . This amounts to checking the following twocorrectness formulas:{(turn = 1 ∨ turn = 2) ∧ ¬af ter1 ∧ t2 = z}hturn := 2; af ter1 := truei{t2 ≤ z}and{af ter1 ∧ t2 = z}h x := x + 1;if f (x) = 0 then f ound := true fi;af ter1 := falsei{t2 ≤ z}.Both correctness formulas are clearly true. This completes the proof of interference freedom.Next, we show deadlock freedom. The potential deadlocks are(wait turn = 1,wait turn = 2),(wait turn = 1,E),(E,wait turn = 2),and logical consequences of the corresponding pairs of assertions from theabove proof outlines are((turn = 1 ∨ turn = 2) ∧ turn 6= 1, turn 6= 2),((f ound ∧ af ter2 → turn = 1) ∧ turn 6= 1, f ound ∧ af ter2 ),(f ound ∧ af ter1 , (f ound ∧ af ter1 → turn = 2) ∧ turn 6= 2).Obviously, the conjunction of the corresponding two assertions is false in allthree cases.
This proves deadlock freedom.Thus we can apply rule 29 for the parallel composition of U1 and U2 andobtain{p1 ∧ p2 } [U1 kU2 ] {f ound ∧ af ter1 ∧ af ter2 }.Since{f (u) = 0 ∧ u > 0}turn := 1; f ound := false;x := 0; y := 1;af ter1 := false; af ter2 := false;{p1 ∧ p2 }andf ound ∧ af ter1 ∧ af ter2 → true,3429 Parallel Programs with Synchronizationwe obtain the statement (9.30) about U by virtue of the soundness of thecomposition rule and of the consequence rule.For the case in which f has a zero u ≤ 0 we must prove|=tot {f (u) = 0 ∧ u ≤ 0} U {true}.(9.40)Instead of the component U1 , now the component U2 of U is responsiblefor finding a zero. Hence the proof of (9.40) in the system TSY is entirelysymmetric to that of (9.30) and is therefore omitted.Finally, we combine the results (9.30) and (9.40).
By the soundness of thedisjunction rule (rule A3) and of the consequence rule, we obtain|=tot {f (u) = 0} U {true}.Final application of the ∃-introduction rule (rule A5) yields the desired termination result (9.29) for U .Step 4. Proving Partial CorrectnessFinally, we prove (9.28) in the proof system PSY for partial correctness introduced in Section 9.3.
We have isolated this step because we can reuse herethe argument given in Step 4 of the Case Study of Section 8.8. Indeed, toconstruct interference free proof outlines for partial correctness of the component programs T1 and T2 of T , we reuse the invariants p1 and p2 giventhere:p1 ≡x≥0∧ (f ound → (x > 0 ∧ f (x) = 0) ∨ (y ≤ 0 ∧ f (y) = 0))∧ (¬f ound ∧ x > 0 → f (x) 6= 0)p2 ≡y≤1∧ (f ound → (x > 0 ∧ f (x) = 0) ∨ (y ≤ 0 ∧ f (y) = 0))∧ (¬f ound ∧ y ≤ 0 → f (y) 6= 0).andThe intuition behind these invariants was explained in Step 4 of Section 8.8.For convenience let us introduce names for two other assertions appearing inthe proof outlines of Section 8.8:r1 ≡ x ≥ 0 ∧ (f ound → y ≤ 0 ∧ f (y) = 0)∧ (x > 0 → f (x) 6= 0)andr2 ≡ y ≤ 1 ∧ (f ound → x > 0 ∧ f (x) = 0)∧ (y ≤ 0 → f (y) 6= 0).9.7 Case Study: Synchronized Zero Search343From Section 8.8 we now “lift” the standard proof outlines to the presentprograms T1 and T2 .
Since the variable turn does not occur in the assertions used in the proof outlines in Section 8.8, any statement accessing turnpreserves these assertions.Thus for T1 we consider now the standard proof outline{inv : p1 }while ¬f ound do{r1 }wait turn = 1;{r1 }turn := 2;{r1 }h x := x + 1;if f (x) = 0 then f ound := true fiiod;{p1 ∧ f ound}turn := 2{p1 ∧ f ound}and similarly for T2 the standard proof outline{inv : p2 }while ¬f ound do{r2 }wait turn = 2;{r2 }turn := 1;{r2 }h y := y − 1;if f (y) = 0 then f ound := true fiiod;{p2 ∧ f ound}turn := 1{p2 ∧ f ound}.From Section 8.8 we can also lift the test of interference freedom to thepresent proof outlines. Indeed, consider any of the correctness formulas to bechecked for this test. Either it has already been checked in Section 8.8, forexample,{r1 ∧ r2 }h y := y − 1;if f (y) = 0 then f ound := true fii{r1 },or it trivially holds because only the variable turn, which does not occur inany of the assertions, is modified.3449 Parallel Programs with SynchronizationThus we can apply rule 27 to the parallel composition of T1 and T2 andobtain{p1 ∧ p2 } [T1 kT2 ] {p1 ∧ p2 ∧ f ound}.From this correctness formula proving the desired partial correctness result(9.28) is straightforward.This concludes the proof of (9.25).9.8 Exercises9.1.
Prove the Input/Output Lemma 3.3 for parallel programs with synchronization.9.2. Prove the Change and Access Lemma 3.4 for parallel programs withsynchronization.9.3. Prove the Stuttering Lemma 7.9 for parallel programs with synchronization.9.4. Suppose that< [S1 k. .
.kSn ], σ > →∗ < [R1 k. . .kRn ], τ > .Prove that for j ∈ {1, . . . , n} either Rj ≡ E or Rj ≡ at(T, Sj ) for a normalsubprogram T of Sj .Hint. See Exercise 3.13.9.5. Prove the Strong Soundness for Component Programs Lemma 9.1.Hint. See the proof of the Strong Soundness for Component ProgramsLemma 8.5.9.6. Prove the Auxiliary Variables Lemma 9.2.Hint. Use Exercise 9.3.9.7. Prove the Auxiliary Variables Lemma 9.7.Hint. See the proof of the Auxiliary Variables Lemma 7.10.9.8.
Consider the following solution to the producer/consumer problem inwhich the synchronization is achieved by means of semaphores:P C ′ ≡ f ull := 0; empty := N ; i := 0; j := 0; [P ROD′ kCON S ′ ],whereP ROD′ ≡ while i < M dox := a[i];P (empty);9.9 Bibliographic Remarks345buffer[i mod N ] := x;V (f ull);i := i + 1odandCON S ′ ≡ while j < M doP (f ull);y := buffer[j mod N ];V (empty);b[j] := y;j := j + 1od.Prove that|=tot {true} P C ′ {∀k : (0 ≤ k < M → a[k] = b[k])}.9.9. Prove the Atomicity Theorem 9.1.Hint. Modify the proof of the Atomicity Theorem 8.1.9.10.
Prove the Initialization Theorem 9.2.9.11. Consider the programs ZERO-5 and ZERO-6 of Section 1.1. Showthat the total correctness of ZERO-6 as proven in Case Study 9.7 impliestotal correctness of ZERO-5.9.9 Bibliographic RemarksAs already mentioned, this chapter owes much to Owicki and Gries [1976a]:the idea of modeling synchronization by await statements, the approach toproving deadlock freedom and the solution to the producer/consumer problem presented in Section 9.4 are from this source.
The intermediate notionof weak total correctness is new, introduced here for a clean formulation ofthe proof rule for parallelism with deadlock freedom. Schneider and Andrews[1986] provide an introduction to the verification of parallel programs usingthe method of Owicki and Gries.Nipkow and Nieto [1999] formalized the method of Owicki and Gries inthe interactive theorem prover Isabelle/HOL introduced by Nipkow, Paulsonand Wenzel [2002], which is based on higher-order logic.
More precisely, theyformalize syntax, semantics, and proof rules for partial correctness of parallelprograms as discussed in this chapter (essentially the proof system PSY ).They proved soundness of the proof rules and verified a number of examples including the producer/consumer case study in Isabelle/HOL, using thetactics of that theorem prover.3469 Parallel Programs with SynchronizationBalser [2006] formalized parallel programs with synchronization and theirverification on the basis of dynamic logic in the KIV system, see Balser et al.[2000].
His approach combines symbolic execution of the operational semantics of the programs with induction.The await statement is a more flexible and structured synchronizationconstruct than the classical semaphore introduced in Dijkstra [1968]. However, the price is its inefficiency when implemented directly —during its execution by one component of a parallel program all other components needto be suspended.In Hoare [1972] a more efficient synchronization construct called conditional critical region is introduced. In Owicki and Gries [1976b] a proof theoryto verify parallel programs using conditional regions is proposed.Several other solutions to the producer/consumer problem and the mutual exclusion problem are analyzed in Ben-Ari [1990]. More solutions to themutual exclusion problem are discussed in Raynal [1986].The Atomicity and the Initialization Theorems stated in Section 9.6 are—as are their counterparts in Chapter 8— inspired by Lipton [1975].Part IVNondeterministic and DistributedPrograms10 Nondeterministic Programs10.110.210.310.410.510.610.710.8ISyntax .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Why Are Nondeterministic Programs Useful? . . . . . . . .
.Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Case Study: The Welfare Crook Problem . . . . . . . . . . . . .Transformation of Parallel Programs . . . . . . . . . . . . . . . . . .Exercises . . . . . . . . . . . . . . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
