3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 59
Текст из файла (страница 59)
To model a binary semaphore it is convenient to use a Boolean variable,say out, and redefine the semaphore operations as follows:• initialization: out := true,• P –operation: P (out) ≡ await out then out := false end,• V –operation: V (out) ≡ out := true.The solution to the mutual exclusion problem using binary semaphoreshas the following simple form:MUTEX-S ≡ out := true; [S1 k. . .kSn ]where for i ∈ {1, . . . , n}3329 Parallel Programs with SynchronizationSi ≡ while true doN Ci ;P (out);CSi ;V (out)od.Intuitively, the binary semaphore out indicates whether all processes are outof their critical sections.To prove correctness of this solution, we have to prove the properties (a)and (b). To this end, we introduce an auxiliary variable who that indicateswhich component, if any, is inside the critical section. Thus we consider nowthe following extended programMUTEX-S ′ ≡ out := true; who := 0; [S1′ k.
. .kSn′ ],where for i ∈ {1, . . . , n}Si′ ≡ while true doN Ci ;await out then out := false; who := i end;CSi ;hout := true; who := 0iod.Note that the binary P - and V -operations have been extended to atomicactions embracing assignment to the auxiliary variable who.For the component programs Si′ for i ∈ {1, . . . , n} we use the assertionI≡(n_who = j) ∧ (who = 0 ↔ out)j=0in the following standard proof outlines for partial correctness:{inv : who 6= i ∧ I}while true do{who 6= i ∧ I}N Ci ;{who 6= i ∧ I}await out then out := false; who := i end;{¬out ∧ who = i}CSi ;{¬out ∧ who = i}hout := true; who := 0iod{false}.9.5 Case Study: The Mutual Exclusion Problem333Considered in isolation these are correct proof outlines. We now prove theirinterference freedom.
First we consider the assertion who 6= i ∧ I occurringthree times in the proof outline of Si′ . This assertion is kept invariant underboth the extended P -operationawait out then out := false; who := i endand the V -operationhout := true; who := 0ifrom any Sj′ with i 6= j. Next we consider the assertion ¬out ∧ who = ioccurring twice in Si′ . To show that this assertion is kept invariant underthe extended P -operation, we consider the body of this await statement. Wehave{¬out ∧ who = i ∧ out}{false}out := false; who := j{false}{¬out ∧ who = i};so by the synchronization rule 28{¬out ∧ who = i ∧ true}await out then out := false; who := j end{¬out ∧ who = i}.For the extended V -operation hout := true; who := 0i from Sj′ with i 6= jthe atomic region rule 26 (as a special case of the synchronization rule 28)yields{¬out ∧ who = i ∧ ¬out ∧ who = j}{false}out := true; who := 0{false}{¬out ∧ who = i}.This finishes the proof of interference freedom.To prove the mutual exclusion condition (a) note that for i, j ∈ {1, .
. . , n}such that i 6= jpre(CSi ) ∧ pre(CSj ) → who = i ∧ who = j;so¬(pre(CSi ) ∧ pre(CSj ))holds. It suffices now to apply the Mutual Exclusion Lemma 9.6 and theAuxiliary Variables Lemma 9.7(i).3349 Parallel Programs with SynchronizationFinally, we prove the absence of blocking condition (b), thus showing thatMUTEX-S is deadlock free. To this end, we investigate the potential deadlocks of MUTEX-S ′ andVthe corresponding tuple of assertions (r1 , . . ., rn ).nWe need to show that ¬ i=1 ri holds. Because of the form of the postconditions of Si′′ for i ∈ {1, .
. . , n} it suffices to consider the case where each ri isassociated with the precondition of the await statement of Si′ , that is, wherefor i ∈ {1, . . . , n}ri ≡ who 6= i ∧ I ∧ ¬out.By the form of I,(n^ri ) → who = 0 ∧ (who = 0 ↔ out) ∧ ¬out,i=1so¬n^rii=1indeed holds. By virtue of the Deadlock Freedom Lemma 9.5 this provesdeadlock freedom of MUTEX-S ′ and the deadlock freedom of MUTEX-Snow follows by the Auxiliary Variables Lemma 9.7(ii).9.6 Allowing More Points of InterferenceAs in Chapter 8 we can apply program transformations to parallel programswith synchronization. These transformations are the same as in Section 8.7and as before can be used in two ways.
First, they allow us to derive from aparallel program another parallel program with more points of interference.Second, they can be used to simplify a correctness proof of a parallel programby applying them in a reverse direction. In the next section we illustrate thesecond use of them.Theorem 9.1. (Atomicity) Consider a parallel program with synchronization of the form S ≡ S0 ; [S1 k. . .kSn ] where S0 is a while program.
Let Tresult from S by replacing in one of its components, say Si with i > 0, either• an atomic region hR1 ; R2 i where one of the Rl s is disjoint from all components Sj with j 6= i byhR1 i; hR2 ior• an atomic region hif B then R1 else R2 fii where B is disjoint from allcomponents Sj with j 6= i byif B then hR1 i else hR2 i fi.9.7 Case Study: Synchronized Zero Search335Then the semantics of S and T agree; that is,M[[S]] = M[[T ]] and Mtot [[S]] = Mtot [[T ]].Proof.
See Exercise 9.9.⊓⊔Corollary 9.5. (Atomicity) Under the assumptions of the Atomicity Theorem 9.1, for all assertions p and q|= {p} S {q} iff |= {p} T {q}and analogously for |=tot .Theorem 9.2. (Initialization) Consider a parallel program with synchronization of the formS ≡ S0 ; R0 ; [S1 k. . .kSn ],where S0 and R0 are while programs. Suppose that for some i ∈ {1, .
. . , n}the initialization part R0 is disjoint from all component programs Sj withj 6= i. Then the programT ≡ S0 ; [S1 k. . .kR0 ; Si k. . .kSn ]has the same semantics as S; that is,M[[S]] = M[[T ]] and Mtot [[S]] = Mtot [[T ]].Proof. See Exercise 9.10.⊓⊔Corollary 9.6. (Initialization) Under the assumptions of the InitializationTheorem 9.2, for all assertions p and q|= {p} S {q} iff |= {p} T {q}and analogously for |=tot .9.7 Case Study: Synchronized Zero SearchWe wish to prove the correctness of Solution 6 to the zero search problemgiven in Section 1.1. That is, we wish to prove that due to the incorporatedsynchronization constructs the parallel programZERO-6 ≡ turn := 1; f ound := false; [S1 kS2 ]with3369 Parallel Programs with SynchronizationS1 ≡ x := 0;while ¬f ound dowait turn = 1;turn := 2;x := x + 1;if f (x) = 0 then f ound := true fiod;turn := 2andS2 ≡ y := 1;while ¬f ound dowait turn = 2;turn := 1;y := y − 1;if f (y) = 0 then f ound := true fiod;turn := 1finds a zero of the function f provided such a zero exists:|=tot {∃u : f (u) = 0} ZERO-6 {f (x) = 0 ∨ f (y) = 0}.(9.25)As in the Case Study of Section 8.8 we proceed in four steps.Step 1.
Simplifying the ProgramWe apply the Atomicity Corollary 9.5 and Initialization Corollary 9.6 toreduce the original problem (9.25) to the following claim|=tot {∃u : f (u) = 0} T {f (x) = 0 ∨ f (y) = 0},whereT ≡ turn := 1; f ound := false;x := 0; y := 1;[T1 kT2 ]withT1 ≡ while ¬f ound dowait turn = 1;turn := 2;h x := x + 1;if f (x) = 0 then f ound := true fii(9.26)9.7 Case Study: Synchronized Zero Search337od;turn := 2andT2 ≡ while ¬f ound dowait turn = 2;turn := 1;h y := y − 1;if f (y) = 0 then f ound := true fiiod;turn := 1.Both corollaries are applicable here because x does not appear in S2 and ydoes not appear in S1 .Step 2.
Decomposing Total CorrectnessTo prove (9.26) we use the fact that total correctness can be decomposedinto termination and partial correctness. More precisely we use the followingobservation.Lemma 9.8. (Decomposition) For all programs R and all assertions p andq|=tot {p} R {q} iff |=tot {p} R {true} and |= {p} R {q}.Proof. By the definition of total and partial correctness.⊓⊔Thus to prove (9.26) it suffices to prove|=tot {∃u : f (u) = 0} T {true}(9.27)|= {∃u : f (u) = 0} T {f (x) = 0 ∨ f (y) = 0}.(9.28)andStep 3. Proving TerminationWe prove (9.27) in the proof system TSY for total correctness introduced inSection 9.3.
To prove deadlock freedom we need two Boolean auxiliary variables af ter1 and af ter2 to indicate whether the execution of the componentprograms T1 and T2 is just after one of the assignments to the variable turn.Thus instead of T we consider the augmented program3389 Parallel Programs with SynchronizationU ≡ turn := 1; f ound := false;x := 0; y := 1;af ter1 := false; af ter2 := false;[U1 kU2 ]withU1 ≡ while ¬f ound dowait turn = 1;hturn := 2; af ter1 := truei;h x := x + 1;if f (x) = 0 then f ound := true fi;af ter1 := falseiod;hturn := 2; af ter1 := trueiandU2 ≡ while ¬f ound dowait turn = 2;hturn := 1; af ter2 := truei;h y := y − 1;if f (y) = 0 then f ound := true fi;af ter2 := falseiod;hturn := 1; af ter2 := truei.The rule of auxiliary variables (rule 25) is sound for total correctness of parallel programs with synchronization (see the Auxiliary Variables Lemma 9.2);so to prove (9.27) it suffices to prove|=tot {∃u : f (u) = 0} U {true}.(9.29)To prove (9.29) we first deal with the case of a positive zero u of f :|=tot {f (u) = 0 ∧ u > 0} U {true}.(9.30)In this case the component U1 of U is responsible for finding the zero.
Thisobservation is made precise in the proof outlines for weak total correctnessof the component programs U1 and U2 . For U1 we take as a loop invariantp1 ≡f (u) = 0 ∧ u > 0 ∧ x ≤ u∧ (turn = 1 ∨ turn = 2)∧ (¬f ound → x < u)∧ ¬af ter1and as a bound functiont1 ≡ u − x.(9.31)(9.32)(9.33)(9.34)9.7 Case Study: Synchronized Zero Search339Let us abbreviate the first two lines in p1 :I1 ≡ (9.31) ∧ (9.32).Then we consider the following standard proof outline for U1 :{inv : p1 }{bd : t1 }while ¬f ound do{I1 ∧ (f ound ∧ af ter2 → turn = 1)∧ x < u ∧ ¬af ter1}wait turn = 1;{I1 ∧ x < u ∧ ¬af ter1 }hturn := 2; af ter1 := truei{I1 ∧ x < u ∧ af ter1 }h x := x + 1;if f (x) = 0 then f ound := true fi;af ter1 := falseiod;{f ound ∧ (turn = 1 ∨ turn = 2) ∧ ¬af ter1 }hturn := 2; af ter1 := truei{f ound ∧ af ter1 }.(9.35)It is easy to check that this is indeed a proof outline for weak total correctness of U1 .
In particular, note that p1 ∧ ¬f ound trivially implies theconjunctf ound ∧ af ter2 → turn = 1(9.36)in assertion (9.35). This conjunct is crucial for showing deadlock freedombelow. Note also that the bound function t1 clearly satisfies the conditionsrequired by the definition of proof outline.Now consider the component program U2 . As a loop invariant we simplytakep2 ≡x≤u∧ (turn = 1 ∨ turn = 2)∧ ¬af ter2 ,(9.37)(9.32)(9.38)but as a bound function we need to taket2 ≡ turn + int(¬af ter1 ) + u − x.For U2 considered in isolation, the variable turn would suffice as a boundfunction, but when U2 is considered in parallel with U1 the remaining summands of t2 are needed to achieve interference freedom.
Let us abbreviateI2 ≡ (9.37) ∧ (9.32)and consider the following standard proof outline for U2 :3409 Parallel Programs with Synchronization{inv : p2 }{bd : t2 }while ¬f ound do{I2 ∧ (f ound ∧ af ter1 → turn = 2) ∧ ¬af ter2 }wait turn = 2;{I2 ∧ ¬af ter2 }hturn := 1; af ter2 := truei{I2 ∧ af ter2 }h y := y − 1;if f (y) = 0 then f ound := true fi;af ter2 := falseiod;{f ound}hturn := 1; af ter2 := truei{f ound ∧ af ter2 }.Clearly, this is indeed a proof outline for weak total correctness of U2 . Inparticular, note that the bound function t2 satisfiesp2 → t 2 ≥ 0and that it is decreased along every syntactically possible path through theloop in U2 because the variable turn drops from 2 to 1.Let us now check the two proof outlines for interference freedom.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
