3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 49
Текст из файла (страница 49)
Note that no additional clause dealing with atomicregions is needed in this definition.Lemma 8.5. (Strong Soundness for Component Programs) Considera component program S with a standard proof outline {p} S ∗ {q} for partialcorrectness. Suppose< S, σ > →∗ < R, τ >holds for a proper state σ satisfying p, a program R and a proper state τ .Then8.4 Verification: Partial Correctness275• either R ≡ at(T, S) for some normal subprogram T of S and τ |= pre(T )• or R ≡ E and τ |= q.Proof.
Removing all brackets h and i from S and the proof outline{p} S ∗ {q} yields a while program S1 with a proof outline {p} S1∗ {q} forpartial correctness. Inserting appropriate assertions in front of the subprograms of S1 that are nonnormal subprograms of S yields a standard proofoutline {p} S1∗∗ {q} for partial correctness.
By transition rule (xiv) definingthe semantics of atomic regions, for any program R< S, σ > →∗ < R, τ > iff < S1 , σ > →∗ < R1 , τ >,where R1 is obtained from R by removing from it all brackets h and i. Theclaim now follows by the Strong Soundness Theorem 3.3.⊓⊔This shows that the introduction of atomic regions leads to a straightforward extension of the proof theory from while programs to componentprograms.No Compositionality of Input/Output BehaviorMuch more complicated is the treatment of parallel composition. As alreadyshown in Example 8.1, the input/output behavior of a parallel program cannot be determined solely from the input/output behavior of its components.Let us make this observation more precise by examining correctness formulasfor the programs of Example 8.1.In isolation the component programs x := x + 2 and x := x + 1; x := x + 1exhibit the same input/output behavior.
Indeed, for all assertions p and q wehave|= {p} x := x + 2 {q} iff |= {p} x := x + 1; x := x + 1 {q}.However, the parallel composition with x := 0 leads to a different input/output behavior. On the one hand,|= {true} [x := x + 2kx := 0] {x = 0 ∨ x = 2}holds but6|= {true} [x := x + 1; x := x + 1kx := 0] {x = 0 ∨ x = 2}since here the final value of x might also be 1.We can summarize this observation as follows: the input/output behavior of parallel programs with shared variables is not compositional; that is,there is no proof rule that takes input/output specifications {pi } Si {qi } of2768 Parallel Programs with Shared Variablescomponentprograms Si asVnVnpremises and yields the input/output specification{ i=1 pi } [S1 k.
. .kSn ] { i=1 qi } for the parallel program as a conclusion under some nontrivial conditions. Recall that this is possible for disjoint parallelprograms —see the sequentialization rule 23.For parallel programs [S1 k. . .kSn ] with shared variables we have to investigate how the input/output behavior is affected by each action in thecomputations of the component programs Si .Parallel Composition: Interference FreedomTo reason about parallel programs with shared variables we follow the approach of Owicki and Gries [1976a] and consider proof outlines instead ofcorrectness formulas. By the Strong Soundness for Component ProgramsLemma 8.5, the intermediate assertions of proof outlines provide informationabout the course of the computation: whenever the control of a componentprogram in a given computation reaches a control point annotated by anassertion, this assertion is true.Unfortunately, this strong soundness property of proof outlines no longerholds when the component programs are executed in parallel.
Indeed, considerthe proof outlines{x = 0} x := x + 2 {x = 2}and{x = 0} x := 0 {true}and a computation of the parallel program [x := x + 2kx := 0] starting ina state satisfying x = 0. Then the postcondition x = 2 does not necessarilyhold after x := x + 2 has terminated because the assignment x := 0 couldhave reset the variable x to 0.The reason is that the above proof outlines do not take into account a possible interaction, or as we say, interference, among components. This bringsus to the following important notion of interference freedom due to Owickiand Gries [1976a].Definition 8.1. (Interference Freedom: Partial Correctness)(i) Let S be a component program. Consider a standard proof outline{p} S ∗ {q} for partial correctness and a statement R with the precondition pre(R).
We say that R does not interfere with {p} S ∗ {q} if• for all assertions r in {p} S ∗ {q} the correctness formula{r ∧ pre(R)} R {r}holds in the sense of partial correctness.8.4 Verification: Partial Correctness277(ii) Let [S1 k. . .kSn ] be a parallel program. Standard proof outlines{pi } Si∗ {qi }, i ∈ {1, . . . , n}, for partial correctness are called interference free if no normal assignment or atomic region of a program Siinterferes with the proof outline {pj } Sj∗ {qj } of another program Sjwhere i 6= j.⊓⊔Thus interference freedom means that the execution of atomic steps of onecomponent program never falsifies the assertions used in the proof outline ofany other component program.With these preparations we can state the following conjunction rule forgeneral parallel composition.RULE 27: PARALLELISM WITH SHARED VARIABLESThe standard proof outlines {pi } Si∗ {qi },i ∈ {1, .
. . , n}, are interference freeVnVn{ i=1 pi } [S1 k. . .kSn ] { i=1 qi }Note that the conclusion in this rule is the same as that in the disjointparallelism rule 24. However, its premises are now much more complicated.Instead of simply checking the correctness formulas {pi } Si {qi } for disjointness, their proofs as recorded in the standard proof outlines {pi } Si∗ {qi } mustbe tested for interference freedom. The restriction to standard proof outlinesreduces the amount of testing to a minimal number of assertions.The test of interference freedom makes correctness proofs for parallel programs more difficult than for sequential programs.
For example, in the caseof two component programs of length ℓ1 and ℓ2 , proving interference freedomrequires proving ℓ1 × ℓ2 additional correctness formulas. In practice, however,most of these formulas are trivially satisfied because they check an assignmentor atomic region R against an assertion that is disjoint from R.Example 8.2. As a first application of the parallelism with shared variablesrule let us prove partial correctness of the parallel programs considered inSection 8.1.(i) First we consider the program [x := x + 2kx := 0]. The standard proofoutlines{x = 0} x := x + 2 {x = 2}and{true} x := 0 {x = 0}are obviously correct, but they are not interference free. For instance, theassertion x = 0 is not preserved under the execution of x := x + 2.
Similarly,x = 2 is not preserved under the execution of x := 0.However, by weakening the postconditions, we obtain standard proof outlines2788 Parallel Programs with Shared Variables{x = 0} x := x + 2 {x = 0 ∨ x = 2}and{true} x := 0 {x = 0 ∨ x = 2}which are interference free. For example, the assignment x := x+2 of the firstproof outline does not interfere with the postcondition of the second proofoutline because{x = 0 ∧ (x = 0 ∨ x = 2)} x := x + 2 {x = 0 ∨ x = 2}holds. Thus the parallelism with shared variables rule yields{x = 0} [x := x + 2kx := 0] {x = 0 ∨ x = 2}.(ii) Next we study the program [x := x + 1; x := x + 1kx := 0].
Consider thefollowing proof outlines:{x = 0}x := x + 1;{x = 0 ∨ x = 1}x := x + 1{true}and{true} x := 0 {x = 0 ∨ x = 1 ∨ x = 2}.To establish their interference freedom seven interference freedom checks needto be made. All of them obviously hold. This yields by the parallelism withshared variables rule{x = 0} [x := x + 1; x := x + 1kx := 0] {x = 0 ∨ x = 1 ∨ x = 2}.(iii) Finally, we treat the first component in the parallel program from theprevious example as an atomic region. Then the proof outlines{x = 0} hx := x + 1; x := x + 1i {true}and{true} x := 0 {x = 0 ∨ x = 2}are clearly interference free.
This proves by the parallelism with shared variables rule the correctness formula{x = 0} [hx := x + 1; x := x + 1ikx := 0] {x = 0 ∨ x = 2}.Thus when executed in parallel with x := 0, the atomic region hx := x + 1;x := x + 1i behaves exactly like the single assignment x := x + 2.⊓⊔8.4 Verification: Partial Correctness279Auxiliary Variables NeededHowever, once a slightly stronger claim about the program from Example 8.2(i) is considered, the parallelism with shared variables rule 27 becomestoo weak to reason about partial correctness.Lemma 8.6.
(Incompleteness) The correctness formula{true} [x := x + 2kx := 0] {x = 0 ∨ x = 2}(8.1)is not a theorem in the proof system P W + rule 27.Proof. Suppose by contradiction that this correctness formula can be provedin the system P W + rule 27. Then, for some interference free proof outlines{p1 } x := x + 2 {q1 },and{p2 } x := 0 {q2 },the implicationstrue → p1 ∧ p2(8.2)q1 ∧ q2 → x = 0 ∨ x = 2(8.3)andhold. Then by (8.2) both p1 and p2 are true.Thus {true} x := x + 2 {q1 } holds, so by the Soundness Theorem 3.1 theassertion q1 [x := x + 2] is true. Since x ranges over all integers,q1(8.4)itself is true. Also, {true} x := 0 {q2 } implies by the Soundness Theorem 3.1q2 [x := 0].(8.5)Moreover, by interference freedom {true ∧ q2 } x := x + 2 {q2 } which givesq2 → q2 [x := x + 2].(8.6)By induction (8.5) and (8.6) imply∀x : (x ≥ 0 ∧ even(x) → q2 ).(8.7)Now by (8.3) and (8.4) we obtain from (8.7)∀x : (x ≥ 0 ∧ even(x) → x = 0 ∨ x = 2)which gives a contradiction.⊓⊔2808 Parallel Programs with Shared VariablesSummarizing, in any interference free proof outline of the above form, thepostcondition q2 of x := 0 would hold for every even x ≥ 0, whereas it shouldhold only for x = 0 or x = 2.
The reason for this mismatch is that we cannotexpress in terms of the variable x the fact that the first component x := x + 2should still be executed.What is needed here is the rule of auxiliary variables (rule 25) introducedin Chapter 7.Example 8.3. We now prove the correctness formula (8.1) using additionallythe rule of auxiliary variables. The proof makes use of an auxiliary Booleanvariable “done” indicating whether the assignment x := x + 2 has been executed. This leads us to consider the correctness formula{true}done := false;[hx := x + 2; done := trueikx := 0]{x = 0 ∨ x = 2}.(8.8)Since {done} is indeed a set of auxiliary variables of the extended program,the rule of auxiliary variables allows us to deduce (8.1) whenever (8.8) hasbeen proved.To prove (8.8), we consider the following standard proof outlines for thecomponents of the parallel composition:{¬done} hx := x + 2; done := truei {true}(8.9)and{true} x := 0 {(x = 0 ∨ x = 2) ∧ (¬done → x = 0)}.(8.10)Note that the atomic region rule 26 is used in the proof of (8.9).It is straightforward to check that (8.9) and (8.10) are interference free.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
