3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 55
Текст из файла (страница 55)
If B ≡ true, weobtain the same effect as with an unconditional atomic region of Chapter 8.Hence we identifyawait true then S end ≡ hSi.As an abbreviation we also introducewait B ≡ await B then skip end.For the extended syntax of this chapter, a subprogram of a program S iscalled normal if it does not occur within an await statement of S.3109 Parallel Programs with Synchronization9.2 SemanticsThe transition system for parallel programs with synchronization consistsof the axioms and rules (i)–(vii) introduced in Section 3.2, the interleavingrule xvii introduced in Section 7.2 and the following transition rule:(xix)< S, σ > →∗ < E, τ >< await B then S end, σ > → < E, τ >where σ |= B.This transition rule formalizes the intuitive meaning of conditional atomic regions.
If B evaluates to true, the statement await B then S end isexecuted like an atomic region hSi, with each terminating computation ofS reducing to an uninterruptible one-step computation of await B then Send.If B evaluates to false, the rule does not allow us to derive any transitionfor await B then S end. In that case transitions of other components canbe executed. A deadlock arises if the program has not yet terminated, butall nonterminated components are blocked. Formally, this amounts to sayingthat no transition is possible.Definition 9.1. Consider a parallel program S, a proper state σ and anassertion p.(i) A configuration < S, σ > is called deadlock if S 6≡ E and there is nosuccessor configuration of < S, σ > in the transition relation → .(ii) The program S can deadlock from σ if there exists a computation of Sstarting in σ and ending in a deadlock.(iii) The program S is deadlock free (relative to p) if there is no state σ(satisfying p) from which S can deadlock.⊓⊔Thus, for parallel programs with synchronization, there is no analogue tothe Absence of Blocking Lemma 8.1.
Consequently, when started in a properstate σ, a parallel program S can now terminate, diverge or deadlock. Depending on which of these outcomes is recorded, we distinguish three variantsof semantics:• partial correctness semantics:M[[S]](σ) = {τ |< S, σ > →∗ < E, τ >},• weak total correctness semantics:Mwtot [[S]](σ) = M[[S]](σ) ∪ {⊥ | S can diverge from σ},9.3 Verification311• total correctness semantics:Mtot [[S]](σ) = Mwtot [[S]](σ) ∪ {∆ | S can deadlock from σ}.As mentioned in Section 2.6, ∆ is one of the special states, in addition to ⊥and fail, which can appear in the semantics of a program but which will neversatisfy an assertion.
The new intermediate semantics Mwtot is not interestingin itself, but it is useful when justifying proof rules for total correctness.9.3 VerificationEach of the above three variants of semantics induces in the standard waya corresponding notion of program correctness. For example, weak total correctness is defined as follows:|=wtot {p} S {q} iff Mwtot [[S]]([[p]]) ⊆ [[q]].First we deal with partial correctness.Partial CorrectnessFor component programs, we use the proof rules of the system P W forwhile programs plus the following proof rule given in Owicki and Gries[1976a]:RULE 28: SYNCHRONIZATION{p ∧ B} S {q}{p} await B then S end {q}The soundness of the synchronization rule is an immediate consequenceof the transition rule (xix) defining the semantics of await statements.
Notethat with B ≡ true we get the atomic region rule 26 as a special case.Proof outlines for partial correctness of component programs are generatedby the same formation rules as those used for while programs together withthe following one:(xii){p ∧ B} S ∗ {q}{p} await B then {p ∧ B} S ∗ {q} end {q}where S ∗ stands for an annotated version of S.3129 Parallel Programs with SynchronizationThe definition of a standard proof outline is stated as in the previouschapter, but it refers now to the extended notion of a normal subprogramgiven in Section 9.1. Thus there are no assertions within await statements.The connection between standard proof outlines and computations of component programs can be stated analogously to the Strong Soundness for Component Programs Lemma 8.5 and the Strong Soundness Theorem 3.3.
We usethe notation at(T, S) introduced in Definition 3.7 but with the understanding that T is a normal subprogram of a component program S. Note that noadditional clause dealing with await statements is needed in this definition.Lemma 9.1. (Strong Soundness for Component Programs) Considera component program S with a standard proof outline {p} S ∗ {q} for partialcorrectness. Suppose that< S, σ > →∗ < R, τ >for a proper state σ satisfying p, a program R and a proper state τ .
Then• either R ≡ at(T, S) for some normal subprogram T of S and τ |= pre(T )• or R ≡ E and τ |= q.Proof. See Exercise 9.5.⊓⊔Interference freedom refers now to await statements instead of atomicregions. Thus standard proof outlines {pi } Si∗ {qi }, i ∈ {1, . . .
, n}, forpartial correctness are called interference free if no normal assignment orawait statement of a component program Si interferes (in the sense of theprevious chapter) with the proof outline of another component program Sj ,i 6= j.For parallel composition we use the parallelism with shared variablesrule 27 from the previous chapter but refer to the above notions of a standardproof outline and interference freedom.Summarizing, we use the following proof system PSY for partial correctness of parallel programs with synchronization:PROOF SYSTEM PSY :This system consists of the group of axiomsand rules 1–6, 25, 27, 28 and A2–A6.Example 9.1. We wish to prove the correctness formula{x = 0} [await x = 1 then skip endkx := 1] {x = 1}in the proof system PSY. For its components we consider the following proofoutlines for partial correctness:{x = 0 ∨ x = 1} await x = 1 then skip end {x = 1}9.3 Verification313and{x = 0} x := 1 {x = 1}.Interference freedom of the assertions in the first proof outline under theexecution of the assignment x := 1 is easy to check.
In detail let us test theassertions of the second proof outline. For the precondition x = 0 we have{x = 0 ∧ (x = 0 ∨ x = 1)} await x = 1 then skip end {x = 0}because by the synchronization rule 28 it suffices to show{x = 0 ∧ (x = 0 ∨ x = 1) ∧ x = 1} skip {x = 0},which holds trivially since its precondition is equivalent to false.For the postcondition x = 1 we have{x = 1 ∧ (x = 0 ∨ x = 1)} await x = 1 then skip end {x = 1},because by the synchronization rule 28 it suffices to show{x = 1 ∧ (x = 0 ∨ x = 1) ∧ x = 1} skip {x = 1},which is obviously true. Thus the parallelism with shared variables rule 27 isapplicable and yields the desired result.⊓⊔Weak Total CorrectnessThe notion of a weak total correctness combines partial correctness with divergence freedom.
It is introduced only for component programs, and used asa stepping stone towards total correctness of parallel programs. By definition,a correctness formula {p} S {q} is true in the sense of weak total correctnessifMwtot [[S]]([[p]]) ⊆ [[q]]holds. Since ⊥ 6∈ [[q]], every execution of S starting in a state satisfying p isfinite and thus either terminates in a state satisfying q or gets blocked.Proving weak total correctness of component programs is simple.
We usethe proof rules of the system T W for while programs and the synchronizationrule 28 when dealing with await statements. Note that the synchronizationrule is sound for weak total correctness but not for total correctness becausethe execution of await B then S end does not terminate when started ina state satisfying ¬B. Instead it gets blocked. This blocking can only beresolved with the help of other components executed in parallel.To prove total correctness of parallel programs with await statements weneed to consider interference free proof outlines for weak total correctness3149 Parallel Programs with Synchronizationof component programs. To define the proof outlines we proceed as in thecase of total correctness in Chapter 8 (see Definitions 8.2 and 8.3 and theconvention that follows the latter definition).First we must ensure that await statements decrease or leave unchangedthe bound functions of while loops.
To this end, we adapt Definition 8.2 of theset path(S) for a component program S by replacing the clause path(hSi) ={hSi} with• path(await B then S end) = {await B then S end}.With this change, (standard) proof outlines for weak total correctness of component programs are defined by the same rules as those used for (standard)proof outlines for total correctness in Definition 8.3 together with rule (xii)dealing with await statements.Standard proof outlines {pi } Si∗ {qi }, i ∈ {1, . . . , n}, for weak total correctness are called interference free if no normal assignment or await statement of a component program Si interferes with the proof outline of anothercomponent program Sj , i 6= j.Total CorrectnessProving total correctness is now more complicated than in Chapter 8 becausein the presence of await statements program termination not only requiresdivergence freedom (absence of infinite computations), but also deadlock freedom (absence of infinite blocking).
Deadlock freedom is a global propertythat can be proved only by examining all components of a parallel programtogether. Thus none of the components of a terminating program need toterminate when considered in isolation; each of them may get blocked (seeExample 9.2 below).To prove total correctness of a parallel program, we first prove weak totalcorrectness of its components, and then establish deadlock freedom.To prove deadlock freedom of a parallel program, we examine interference free standard proof outlines for weak total correctness of its componentprograms and use the following method of Owicki and Gries [1976a]:1. Enumerate all potential deadlock situations.2. Show that none of them can actually occur.This method is sound because in the proof of the Deadlock FreedomLemma 9.5 below we show that every deadlock in the sense of Definition 9.1is also a potential deadlock.Definition 9.2.
Consider a parallel program S ≡ [S1 k. . .kSn ].(i) A tuple (R1 , . . ., Rn ) of statements is called a potential deadlock of S ifthe following two conditions hold:9.3 Verification315• For every i ∈ {1, . . . , n}, Ri is either an await statement in the component Si or the symbol E which stands for the empty statement andrepresents termination of Si ,• for some i ∈ {1, . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
