3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 70
Текст из файла (страница 70)
The corresponding premise of the distributed programs rule 34refers to the second part of the do loop in T (TRANS):{I ∧ out 6= in ∧ y 6= ‘∗’}y := b[out]; out := out + 1;c[j] := y; j := j + 1{I}.First we consider the last two conjuncts of I. We have{b[0 : out − 1] = c[0 : j − 1] ∧ out ≤ in ∧ out 6= in}y := b[out]; out := out + 1;c[j] := y; j := j + 1{b[0 : out − 1] = c[0 : j − 1] ∧ out ≤ in}.Since the first conjunct of I is disjoint from the above program part, theinvariance rule rule A6 yields that the invariant I is preserved altogether.Thus we have shown that I is indeed a global invariant relative to p.Applying the distributed programs rule 34 we now get|= {p} TRANS {I ∧ TERM },whereTERM ≡ i = M ∧ x = ‘∗’ ∧ out = in ∧ y = ‘∗’.By the consequence rule, the correctness formula (11.4) holds in the sense ofpartial correctness.Step 3.
Proving Absence of Failures and of DivergenceWe now prove (11.4) in the sense of weak total correctness; that is,40011 Distributed Programs|=wtot {p} TRANS {q}.Since in TRANS the only alternative command consists of a complete casedistinction, no failure can occur. Thus it remains to show the absence ofdivergence.
To this end we use the following bound function:t ≡ 2 · (M − i) + in − out.Here M − i is the number of characters that remain to be transmitted andin − out is the number of characters buffered in the process FILTER. Thefactor 2 for M − i guarantees that the value of t decreases if a communicationalong the channel input with i := i + 1; in := in + 1 as part of the jointtransition occurs. A communication along the channel output executes out :=out + 1 without modifying i and in and thus it obviously decrements t.However, to apply the distributed programs rule 35 we need to use aninvariant which guarantees that t remains nonnegative. The invariant I ofStep 2 is not sufficient for this purpose since the values of M and i are notrelated.
Let us considerI1 ≡ i ≤ M ∧ out ≤ in.It is straightforward to prove that I1 is a global invariant relative to p withI1 → t ≥ 0. Thus rule 35 is applicable and yields|=wtot {p} TRANS {I1 ∧ T ERM }.Applying rule A9 to this result and the previous invariant I we now get|=wtot {p} TRANS {I ∧ I1 ∧ TERM },which implies (11.4) in the sense of weak total correctness.Step 4. Proving Deadlock FreedomFinally, we prove deadlock freedom.
By the Deadlock Freedom Lemma 11.4,it suffices to find a global invariant I ′ relative to p for whichI ′ ∧ BLOCK → TERMholds. For the program TRANS we haveBLOCK ≡ (i = M ∨ x = ‘∗’) ∧ (out = in ∨ y = ‘∗’)and, as noted before,(11.5)11.5 Case Study: A Transmission Problem401TERM ≡ i = M ∧ x = ‘∗’ ∧ out = in ∧ y = ‘∗’.We exhibit I ′ “in stages” by first introducing global invariants I2 , I3 and I4relative to p withI2 → (i = M ↔ x = ‘∗’),I3 ∧ i = M ∧ x = ‘∗’ ∧ out = in → y = ‘∗’,(11.6)(11.7)I4 ∧ i = M ∧ x = ‘∗’ ∧ y = ‘∗’ → out = in.(11.8)Then we putI ′ ≡ I2 ∧ I3 ∧ I4 .By rule A8 I ′ is also a global invariant relative to p. Note that each of theequalities used in (11.6), (11.7) and (11.8) is a conjunct of TERM ; (11.6),(11.7) and (11.8) express certain implications between these conjuncts whichguarantee that I ′ indeed satisfies (11.5).It remains to determine I2 , I3 and I4 . We putI2 ≡ p ∧ (i > 0 ∨ x = ‘∗’ → x = a[i − 1]).I2 relates variables of the processes SENDER and FILTER.
It is easy to checkthat I2 is indeed a global invariant relative to p. Note that (11.6) holds.Next, we considerI3 ≡ I ∧ p ∧ (j > 0 → y = c[j − 1]).The last conjunct of I3 states a simple property of the variables of the process RECEIVER. Again I3 is a global invariant relative to p. The followingsequence of implications proves (11.7):I3 ∧ i = M ∧ x = ‘∗’ ∧ out = in→{definition of I}I3 ∧ c[0 : j − 1] = delete(a[0 : M − 1])→{p implies a[0 : M − 1] = ‘∗’}I3 ∧ c[j − 1] = ‘∗’ ∧ j > 0→{definition of I3 }y = ‘∗’.Finally, we putI4 ≡ I ∧ p ∧ (y = ‘∗’ → c[j − 1] = ‘∗’).Here as well, the last conjunct describes a simple property of the variablesof the process RECEIVER.
It is easy to show that I4 is a global invariant40211 Distributed Programsrelative to p. We prove the property (11.8):I4 ∧ i = M ∧ x = ‘∗’ ∧ y = ‘∗’→{definition of I4 }I4 ∧ c[j − 1] = ‘∗’→{definition of I and p}I4 ∧ b[out − 1] = a[M − 1]→{there is only one ‘∗’ in a[0 : M − 1],namely a[M − 1], so the first conjunctof I implies b[in − 1] = a[M − 1]}out = in.We have thus proved (11.5), that is, the deadlock freedom of the programTRANS. Together with the result from Step 3 we have established the desiredcorrectness formula (11.4) in the sense of total correctness.11.6 Exercises11.1. Let S be a distributed program. Prove that if < S, σ > → < S1 , τ >,then S1 is also a distributed program.11.2. Let S ≡ [S1 k.
. .kSn ] be a distributed program.(i) Prove the Commutativity Lemma 11.2.(ii) Prove that for distinct i, j, k, ℓ ∈ {1, . . . , n} with i < j and k < ℓ, the(i,j)(k,ℓ)relations −→ and −→ commute.(iii) Prove the Failure Lemma 11.3.Hint. Use the Change and Access Lemma 10.4.11.3. Consider Step 4 of the proof of the Sequentialization Theorem 11.1.Prove that the result of inserting a step of a process in a computation of Sis indeed a computation of S.Hint.
Use the Change and Access Lemma 10.4.11.4. Prove Claim 2 in the proof of the Sequentialization Theorem 11.1 whenξ is terminating or ends in a deadlock or ends in a failure.11.5. Prove the Change and Access Lemma 3.4 for distributed programs andthe partial correctness, weak total correctness and total correctness semantics.Hint. Use the Sequentialization Theorem 11.1.11.6. Prove the Soundness of PDP, WDP and TDP Theorem 11.5.11.6 Exercises40311.7. Given a section a[1 : n] of an array a of type integer → integerthe processCENTER should compute in an integer variable x the weightedPnsum i=1 wi · a[i].
We assume that the weights wi are stored in a distributedfashion in separate processes Pi , and that the multiplications are carried outby the processes Pi while the addition is carried out by the process CENTER.Thus CENTER has to communicate in an appropriate way with theseprocesses Pi . We stipulate that for this purpose communication channelslinki are available and consider the following distributed program:WSUM ≡ [CENTER k P1 k ...
k Pn ],whereCENTER ≡ x := 0; to[1] := true; ... ; to[n] := true;f rom[1] := true; ... ; f rom[n] := true;do to[1]; link!a[1] → to[1] := false;................................................to[n]; link!a[n] → to[n] := false;f rom[1]; link?y → x := x + y; f rom[1] := false;............................................................................f rom[n]; link?y → x := x + y; f rom[n] := false;odandPi≡ reci := false; senti := false;do ¬reci ; link?zi → reci := truereci ∧ ¬senti ; link!wi · zi → senti := trueodfor i ∈ {1, ..., n}. The process CENTER uses Boolean control variables to[i]and f rom[i] of two arrays to and f rom of type integer → Boolean.
Additionally, each process Pi uses two Boolean control variables reci und senti .Prove the total correctness of WSUM :Pn|=tot {true} WSUM {x = i=1 wi · a[i]}.11.8. Let X0 and Y0 be two disjoint, nonempty finite sets of integers. Weconsider the following problem of set partition due to Dijkstra [1977] (see alsoApt, Francez and de Roever [1980]): the union X0 ∪Y0 should be partitionedin two sets X and Y such that X has the same number of elements as X0 ,Y has the same number of elements as Y0 and all elements of X are smallerthan those of Y .To solve this problem we consider a distributed program SETPART consisting of two processes SMALL and BIG which manipulate local variablesX and Y for finite sets of integers and communicate with each other alongchannels big and small:SETPART ≡ [SMALL k BIG].40411 Distributed ProgramsInitially, the sets X0 and Y0 are stored in X and Y .
Then the process SMALLrepeatedly sends the maximum of the set stored in X along the channnel bigto the process BIG. This process sends back the minimum of the updated setY along the channel small to the process SMALL. This exchange of valuesterminates as soon as the process SMALL gets back the maximum just sentto BIG.Altogether the processes of SETPART are defined as follows:SMALL ≡ more := true; send := true;mx := max(X);do more ∧ send; big ! mx → send := false⊓⊔ more ∧ ¬send; small ? x →if mx = x → more := false⊓⊔ mx 6= x → X := X − {mx} ∪ {x};mx := max(X);send := truefiod,BIG ≡ go := true;do go; big ? y → Y := Y ∪ {y};mn := min(Y );Y := Y − {mn}⊓⊔ go; small ! mn → go := (mn 6= y)od.The Boolean variables more, send and go are used to coordinate the behaviorof SMALL and BIG.
In particular, thanks to the variable send the processesSMALL and BIG communicate in an alternating fashion along the channelsbig and small. The integer variables mx, x, mn, y are used to store valuesfrom the sets X and Y .Prove the total correctness of the program SETPART for the preconditionp ≡ X ∩ Y = ∅ ∧ X 6= ∅ ∧ Y 6= ∅ ∧ X = X0 ∧ Y = Y0and the postconditionq≡X ∪ Y = X0 ∪ Y0∧ card X = card X0 ∧ card Y = card Y0∧ max(X) < min(Y ).Recall from Section 2.1 that for a finite set A, card A denotes the number ofits elements.11.9. Extend the syntax of distributed programs by allowing the clausesdefining nondeterministic programs in Chapter 10 in addition to the clausefor parallel composition.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
