3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 58
Текст из файла (страница 58)
Intuitively, a safety property is acondition that holds in every state in the computations of a program whereasa liveness property is a condition that for all computations is eventuallysatisfied. A formulation of condition (iii) in our proof theoretic framework ispossible but awkward (see Olderog and Apt [1988]).
Therefore its treatmentis omitted in this book.An appropriate framework for the treatment of liveness properties is temporal logic (see Manna and Pnueli [1991,1995]). To this end, however, temporal logic uses a more complex assertion language and more complex proofprinciples.To formalize conditions (i) and (ii) we assume that each process Si is aneternal loop of the following form:Si ≡ while true doN Ci ;ACQi ;CSi ;RELiod,where N Ci (abbreviation for noncritical section) denotes a part of the program in which process Si does not use the resource, ACQi (abbreviation foracquire protocol) denotes the part of the program that process Si executesto acquire the resource, CSi (abbreviation for critical section) denotes a loopfree part of the program in which process Si uses the resource and RELi (abbreviation for release protocol) denotes the part of the program that processSi executes to release the resource.
Additionally we assume that(var(N Ci ) ∪ var(CSi )) ∩ (var(ACQj ) ∪ var(RELj )) = ∅for i, j ∈ {1, . . . , n} such that i 6= j; that is, the acquire and release protocolsuse fresh variables. We also assume that no await statements are used insidethe sections N Ci and CSi .Then we consider a parallel program3269 Parallel Programs with SynchronizationS ≡ IN IT ; [S1 k. . .kSn ],where IN IT is a loop free while program in which the variables used in theacquire and release protocols are initialized.Assume first that S is a parallel program without synchronization, thatis, a program in the language studied in Chapter 8. Then we can formalizeconditions (i) and (ii) as follows:(a) mutual exclusion:no configuration in a computation of S is of the form< [R1 k. .
.kRn ], σ >,where for some i, j ∈ {1, . . . , n}, i 6= jRi ≡ at(CSi , Si ),Rj ≡ at(CSj , Sj );(b) absence of blocking:no computation of S ends in a deadlock.Note that in the case where S is a parallel program without synchronization, condition (ii) is actually automatically satisfied, and in the case whereS is a parallel program with synchronization it indeed reduces to (b) due tothe syntactic form of S.A trivial solution to the mutual exclusion problem would be to turn thecritical section CSi into an atomic region:Si ≡ while true doN Ci ;hCSi iod.Here we have chosen ACQi ≡ “h” and RELi ≡ “i”. Of course, this choiceguarantees mutual exclusion because in a computation of S the ith componentof S can never be of the form Ri ≡ at(CSi , Si ).However, we are interested here in more realistic solutions in which ACQiand RELi are implemented by more primitive programming constructs.VerificationConditions (a) and (b) refer to semantics.
To verify them we propose prooftheoretic conditions that imply them. These conditions can then be established by means of an axiomatic reasoning.9.5 Case Study: The Mutual Exclusion Problem327To reason about the mutual exclusion condition (a) we use the followinglemma.Lemma 9.6. (Mutual Exclusion)Vn Suppose that for some assertions pi withi ∈ {1, . . . , n}, {true} IN IT { i=1 pi } holds and {pi } Si∗ {false} for i ∈{1, .
. . , n} are interference free standard proof outlines for partial correctnessof the component programs Si such that¬(pre(CSi ) ∧ pre(CSj ))holds for i ∈ {1, . . . , n}, i 6= j. Then the mutual exclusion condition (a) issatisfied for the parallel program S.Proof. This is an immediate consequence of the Strong SoundnessLemma 9.3.⊓⊔To reason about the absence of blocking condition (b) we use the DeadlockFreedom Lemma 9.5. Also, we use auxiliary variables. The following lemmaallows us to do so.Lemma 9.7.
(Auxiliary Variables) Suppose that S ′ is a parallel programwith or without synchronization, A is a set of auxiliary variables of S ′ and Sis obtained from S ′ by deleting all assignments to the variables in A.(i) If S ′ satisfies the mutual exclusion condition (a), then so does S.(ii) If S ′ is deadlock free relative to some assertion p, then so is S.Proof. See Exercise 9.7.⊓⊔A Busy Wait SolutionFirst, let us consider the case of parallel programs without synchronization.When the acquire protocol for each process Si for i ∈ {1, .
. . , n} is of theformACQi ≡ Ti ; while ¬Bi do skip od,where Ti is loop free, we call such a solution to the mutual exclusion problema busy wait solution and the loop while ¬Bi do skip od a busy wait loop.We consider here the following simple busy wait solution to the mutualexclusion problem for two processes due to Peterson [1981]. LetMUTEX-B ≡ f lag1 := false; f lag2 := false; [S1 kS2 ],where3289 Parallel Programs with SynchronizationS1 ≡ while true doN C1 ;f lag1 := true; turn := 1;while ¬(f lag2 → turn = 2) do skip od;CS1 ;f lag1 := falseodandS2 ≡ while true doN C2 ;f lag2 := true; turn := 2;while ¬(f lag1 → turn = 1) do skip od;CS2 ;f lag2 := falseod.Intuitively, the Boolean variable f lagi indicates whether the component Siintends to enter its critical section, i ∈ {1, 2}.
The variable turn is used toresolve simultaneity conflicts: in case both components S1 and S2 intend toenter their critical sections, the component that set the variable turn firstis delayed in a busy wait loop until the other component alters the value ofturn. (Note that ¬(f lagi → turn = i) is equivalent to f lagi ∧ turn 6= i fori ∈ {1, 2}).To prove correctness of this solution we introduce two auxiliary variables,af ter1 and af ter2 , that serve to indicate whether in the acquire protocol ofSi (i ∈ {1, 2}) the control is after the assignment turn := i.
Thus we considernow the following extended programMUTEX-B ′ ≡ f lag1 := false; f lag2 := false; [S1′ kS2′ ],whereS1′ ≡ while true doN C1 ;hf lag1 := true; af ter1 := falsei;hturn := 1; af ter1 := truei;while ¬(f lag2 → turn = 2) do skip od;CS1 ;f lag1 := falseodandS2′ ≡ while true doN C2 ;hf lag2 := true; af ter2 := falsei;9.5 Case Study: The Mutual Exclusion Problem329hturn := 2; af ter2 := truei;while ¬(f lag1 → turn = 1) do skip od;CS2 ;f lag2 := falseod.With the help of the Mutual Exclusion Lemma 9.6 we prove now themutual exclusion condition (a) for the extended program MUTEX-B ′ .
To thisend we consider the following standard proof outlines for partial correctnessof the component programs S1′ and S2′ where we treat the parts N Ci andCSi as skip statements and use the abbreviationI ≡ turn = 1 ∨ turn = 2.{inv : ¬f lag1 }while true do{¬f lag1 }N C1 ;{¬f lag1 }hf lag1 := true; af ter1 := falsei;{f lag1 ∧ ¬af ter1 }hturn := 1; af ter1 := truei;{inv : f lag1 ∧ af ter1 ∧ I}while ¬(f lag2 → turn = 2) do{f lag1 ∧ af ter1 ∧ I}skipod{f lag1 ∧ af ter1 ∧ (f lag2 ∧ af ter2 → turn = 2)}CS1 ;{f lag1 }f lag1 := falseod{false}and{inv : ¬f lag2 }while true do{¬f lag2 }N C2 ;{¬f lag2 }hf lag2 := true; af ter2 := falsei;{f lag2 ∧ ¬af ter2 }hturn := 2; af ter2 := truei;{inv : f lag2 ∧ af ter2 ∧ I}while ¬(f lag1 → turn = 1) do{f lag2 ∧ af ter2 ∧ I}3309 Parallel Programs with Synchronizationskipod{f lag2 ∧ af ter2 ∧ (f lag1 ∧ af ter1 → turn = 1)}CS2 ;{f lag2 }f lag2 := falseod{false}.First, let us check that these are indeed proof outlines for partial correctness of S1′ and S2′ .
The only interesting parts are the busy wait loops. For thebusy wait loop in S1′{inv : f lag1 ∧ af ter1 ∧ I}while ¬(f lag2 → turn = 2) do{f lag1 ∧ af ter1 ∧ I}skipod{f lag1 ∧ af ter1 ∧ I ∧ (f lag2 → turn = 2)}is a correct proof outline and so is{inv : f lag1 ∧ af ter1 ∧ I}while ¬(f lag2 → turn = 2) do{f lag1 ∧ af ter1 ∧ I}skipod{f lag1 ∧ af ter1 ∧ (f lag2 ∧ af ter2 → turn = 2)},because I ∧ (f lag2 → turn = 2) trivially implies the conjunctf lag2 ∧ af ter2 → turn = 2.A similar argument can be used for the busy wait loop in S2′ .Next we show interference freedom of the above proof outlines.
In the proofoutline for S1′ only the assertionpre(CS1 ) ≡ f lag1 ∧ af ter1 ∧ (f lag2 ∧ af ter2 → turn = 2)can be invalidated by a statement from S2′ because all other assertions containonly variables that are local to S1′ or the obviously interference-free conjunctI. The only normal assignments or await statements of S2′ that can invalidateit are hf lag2 := true; af ter2 := falsei and hturn := 2; af ter2 := truei.Clearly both{pre(CS1 )} hf lag2 := true; af ter2 := falsei {pre(CS1 )}and9.5 Case Study: The Mutual Exclusion Problem331{pre(CS1 )} hturn := 2; af ter2 := truei {pre(CS1 )}hold.
Thus no normal assignment or await statement of S2′ interferes withthe proof outline for S1′ . By symmetry the same holds with S1′ and S2′ interchanged. This shows that the above proof outlines for S1′ and S2′ are interference free.By the implicationpre(CS1 ) ∧ pre(CS2 ) → turn = 1 ∧ turn = 2,we have¬(pre(CS1 ) ∧ pre(CS2 )).Thus the Mutual Exclusion Lemma 9.6 yields the mutual exclusion condition(a) for the extended parallel program MUTEX-B ′ and the Auxiliary VariablesLemma 9.7 (i) for the original program MUTEX-B .A Solution Using SemaphoresIn this subsection we consider a solution to the mutual exclusion problem forn processes due to Dijkstra [1968]. It uses the concept of a semaphore as asynchronization primitive. A semaphore is a shared integer variable, say sem,on which only the following operations are allowed:• initialization: sem := k where k ≥ 0,• P –operation: P (sem) ≡ await sem > 0 then sem := sem − 1 end,• V –operation: V (sem) ≡ sem := sem + 1.The letters P and V originate from the Dutch verbs “passeren” (to pass)and “vrijgeven” (to free).A binary semaphore is a semaphore that can take only two values: 0 and1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
