3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 57
Текст из файла (страница 57)
⊓Corollary 9.3. (Parallelism) Rule 29 is sound for total correctness of parallel programs with synchronization.Proof. Consider interference free standard proof outlines for weak total correctness for component programs. Then Lemma 9.4 applies. By removingfrom each of these proof outlines all annotations referring to the bound functions, we obtain interference free proof outlines for partial correctness. Theclaim now follows from the Parallelism Corollary 9.1 and the Deadlock Freedom Lemma 9.5.⊓⊔Corollary 9.4. (Soundness of TSY) The proof system TSY is sound fortotal correctness of parallel programs with synchronization.Proof.
We use the same argument as that in the proof of the SoundnessCorollary 7.1.⊓⊔9.4 Case Study: Producer/Consumer ProblemA recurring task in the area of parallel programming is the coordination ofproducers and consumers. A producer generates a stream of M ≥ 1 valuesfor a consumer. We assume that the producer and consumer work in paralleland proceed at a variable but roughly equal pace.3209 Parallel Programs with SynchronizationThe problem is to coordinate their work so that all values produced arriveat the consumer and in the order of production.
Moreover, the producershould not have to wait with the production of a new value if the consumeris momentarily slow with its consumption. Conversely, the consumer shouldnot have to wait if the producer is momentarily slow with its production.The general idea of solving this producer/consumer problem is to interposea buffer between producer and consumer.
Thus the producer adds values tothe buffer and the consumer removes values from the buffer. This way smallvariations in the pace of producers are not noticeable to the consumer andvice versa. However, since in reality the storage capacity of a buffer is limited,say to N ≥ 1 values, we must synchronize producer and consumer in such away that the producer never attempts to add a value into the full buffer andthat the consumer never attempts to remove a value from the empty buffer.Following Owicki and Gries [1976a], we express the producer/consumerproblem as a parallel program PC with shared variables and await statements. The producer and consumer are modeled as two components P RODand CON S of a parallel program.
Production of a value is modeled as readingan integer value from a finite sectiona[0 : M − 1]of an array a of type integer → integer and consumption of a value aswriting an integer value into a corresponding sectionb[0 : M − 1]of an array b of type integer → integer. The buffer is modeled as a sectionbuffer[0 : N − 1]of a shared array buffer of type integer → integer. M and N are integer constants M, N ≥ 1. For a correct access of the buffer the componentsP ROD and CON S share an integer variable in counting the number of values added to the buffer and an integer variable out counting the number ofvalues removed from the buffer. Thus at each moment the buffer containsin − out values; it is full if in − out = N and it is empty if in − out = 0.Adding and removing values to and from the buffer is performed in a cyclicorderbuffer[0], .
. ., buffer[N − 1], buffer[0], . . ., buffer[N − 1], buffer[0], . . . .Thus the expressions in mod N and out mod N determine the subscript ofthe buffer element where the next value is to be added or removed. Thisexplains why we start numbering the buffer elements from 0 onwards.With these preparations we can express the producer/consumer problemby the following parallel program:9.4 Case Study: Producer/Consumer Problem321PC ≡ in := 0; out := 0; i := 0; j := 0; [P RODkCON S],whereP ROD ≡ while i < M dox := a[i];ADD(x);i := i + 1odandCON S ≡ while j < M doREM (y);b[j] := y;j := j + 1od.Here i, j, x, y are integer variables and ADD(x) and REM (y) abbreviatethe following synchronized statements for adding and removing values fromthe shared buffer:ADD(x) ≡ wait in − out < N ;buffer[in mod N ] := x;in := in + 1andREM (y) ≡ wait in − out > 0;y := buffer[out mod N ];out := out + 1.Recall that for a Boolean expression B the statement wait B abbreviatesawait B then skip end.We claim the following total correctness property:|=tot {true} PC {∀k : (0 ≤ k < M → a[k] = b[k])},(9.13)stating that the program PC is deadlock free and terminates with all valuesfrom a[0 : M − 1] copied in that order into b[0 : M − 1].
The verification of(9.13) follows closely the presentation in Owicki and Gries [1976a].First consider the component program P ROD. As a loop invariant we takep1 ≡∀k : (out ≤ k < in → a[k] = buffer[k mod N ])∧ 0 ≤ in − out ≤ N∧ 0≤i≤M∧ i = in(9.14)(9.15)(9.16)(9.17)3229 Parallel Programs with Synchronizationand as a bound functiont1 ≡ M − i.Further, we introduce the following abbreviation for the conjunction of someof the lines in p1 :I ≡ (9.14) ∧ (9.15)andI1 ≡ (9.14) ∧ (9.15) ∧ (9.16).As a standard proof outline we consider{inv : p1 }{bd : t1 }while i < M do{p1 ∧ i < M }x := a[i];{p1 ∧ i < M ∧ x = a[i]}wait in − out < N ;{p1 ∧ i < M ∧ x = a[i] ∧ in − out < N }buffer[in mod N ] := x;{p1 ∧ i < M ∧ a[i] = buffer[in mod N ] ∧ in − out < N }in := in + 1;{I1 ∧ i + 1 = in ∧ i < M }i := i + 1od{p1 ∧ i = M }.(9.18)(9.19)Clearly, this is indeed a proof outline for weak total correctness of P ROD.In particular, note that (9.18) implies∀k : (out ≤ k < in + 1 → a[k] = buffer[k mod N ]),which justifies the conjunct (9.14) of the postcondition (9.19) of the assignment in := in + 1.
Note also that the bound function t1 clearly satisfies theconditions required by the definition of proof outline.Now consider the component program CON S. As a loop invariant we takep2 ≡I∧ ∀k : (0 ≤ k < j → a[k] = b[k])∧ 0≤j≤M∧ j = out,(9.20)(9.21)(9.22)(9.23)letting the I-part of p1 reappear here, and as a bound function we taket2 ≡ M − j.Let us abbreviateI2 ≡ (9.20) ∧ (9.21) ∧ (9.22),and consider the following standard proof outline:9.4 Case Study: Producer/Consumer Problem{inv : p2 }{bd : t2 }while j < M do{p2 ∧ j < M }wait in − out > 0;{p2 ∧ j < M ∧ in − out > 0}y := buffer[out mod N ];{p2 ∧ j < M ∧ in − out > 0 ∧ y = a[j]}out := out + 1;{I2 ∧ j + 1 = out ∧ j < M ∧ y = a[j]}b[j] := y;{I2 ∧ j + 1 = out ∧ j < M ∧ a[j] = b[j]}j := j + 1od{p2 ∧ j = M }.323(9.24)Clearly, this is a correct proof outline for weak total correctness.
In particular, the conjunct y = a[j] in the assertion (9.24) is obtained by noting that y = buffer[out mod N ] is a postcondition for the assignmenty := buffer[out mod N ] and by calculating==buffer[out mod N ]{(14) ∧ in − out > 0}a[out]{(23)}a[j].Also the bound function t2 satisfies the conditions required by the definitionof proof outline.Let us now turn to the test of interference freedom of the two proofoutlines. Naive calculations suggest that 80 correctness formulas must bechecked! However, most of these checks can be dealt with by a single argument, that the I-part of p1 and p2 is kept invariant in both proof outlines. Inother words, all assignments T in the proof outlines for P ROD and CON Ssatisfy{I ∧ pre(T )} T {I}.It thus remains to check the assertions outside the I-part against possible interference.
Consider first the proof outline for P ROD. Examine all conjunctsoccurring in the assertions used in this proof outline. Among them, apartfrom I, only the conjunct in − out < N contains a variable that is changedin the component CON S. But this change is done only by the assignmentout := out + 1. Obviously, we have here interference freedom:{in − out < N } out := out + 1 {in − out < N }.3249 Parallel Programs with SynchronizationNow consider the proof outline for CON S. Examine all conjuncts occurringin the assertions used in this proof outline. Among them, apart from I, onlythe conjunct in − out > 0 contains a variable that is changed in the component P ROD.
But this change is done only by the assignment in := in + 1.Obviously, we again have interference freedom:{in − out > 0} in := in + 1 {in − out > 0}.Next, we show deadlock freedom. The potential deadlocks are(wait in − out < N , wait in − out > 0),(wait in − out < N , E),(E, wait in − out > 0),and logical consequences of the corresponding pairs of assertions from theabove proof outlines are(in − out ≥ N, in − out ≤ 0),(in < M ∧ in − out ≥ N, out = M ),(in = M, out < M ∧ in − out ≤ 0).Since N ≥ 1, the conjunction of the corresponding two assertions is false inall three cases. This proves deadlock freedom.We can now apply rule 29 for the parallel composition of P ROD andCON S and obtain{p1 ∧ p2 } [P RODkCON S] {p1 ∧ p2 ∧ in = M ∧ j = M }.Since{true} in := 0; out := 0; i := 0; j := 0 {p1 ∧ p2 }andp1 ∧ p2 ∧ i = M ∧ j = M → ∀k : (0 ≤ k < M → a[k] = b[k]),we obtain the desired correctness formula (9.13) about PC by straightforwardapplications of the composition rule and the consequence rule.9.5 Case Study: The Mutual Exclusion ProblemProblem FormulationAnother classical problem in parallel programming is mutual exclusion, firstinvestigated in Dijkstra [1968].
Consider n processes, n ≥ 2, running indefinitely that share a resource, say a printer. The mutual exclusion problem is9.5 Case Study: The Mutual Exclusion Problem325the task of synchronizing these processes in such a way that the followingtwo conditions are satisfied:(i) mutual exclusion:at any point of time at most one process uses the resource,(ii) absence of blocking:the imposed synchronization discipline does not prevent the processesfrom running indefinitely,(iii) individual accessibility:if a process is trying to acquire the resource, eventually it will succeed.Conditions (i) and (ii) are instances of a safety property whereas condition(iii) is an instance of a liveness property.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
