3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 73
Текст из файла (страница 73)
In thetransformation Tfair it will localize the unbounded nondeterminism implicitlyinduced by the assumption of fairness. Thus; random assignments will enableus to reason about programs under fairness assumptions. In this section wepresent a semantics and proof theory of random assignments as an extensionof ordinary nondeterministic programs.SemanticsThe random assignment x :=? terminates for any initial state σ, but thereare infinitely many possibilities for the final state —one for each non-negativevalue that might be assigned to x. This idea is captured in the followingtransition axiom where σ is a proper state:(xxvi) < x :=?, σ > → < E, σ[x := d] > for every natural number d ≥ 0.The semantics of nondeterministic programs with random assignments is defined just as in Section 10.2, but with the transition relation → referring tothis additional transition axiom.
In particular, we haveN [[x :=?]](σ) = {σ[x := d] | d ≥ 0}for a proper state σ and N = M or N = Mtot .VerificationThe proof theory of random assignments in isolation is simple. We just needthe following axiom.AXIOM 37: RANDOM ASSIGNMENT{∀x ≥ 0 : p} x :=? {p}Thus, to establish an assertion p after the random assignment x :=?, p musthold before x :=? for all possible values of x generated by this assignment;that is, for all integers x ≥ 0. Thus, as with the assignment axiom 2 for ordinary assignments, this axiom formalizes backward reasoning about randomassignments. By the above semantics, the random assignment axiom is soundfor partial and total correctness.41612 FairnessBut does it suffice when added to the previous proof systems for nondeterministic programs? For partial correctness the answer is “yes.” Thusfor proofs of partial correctness of nondeterministic programs with randomassignments we consider the following proof system PNR.PROOF SYSTEM PNR :This system consists of the proof systemPN augmented with axiom 37.Proving termination, however, gets more complicated: the repetitive command II rule 33 of Section 10.4, using an integer-valued bound function t,is no longer sufficient.
The reason is that in the presence of random assignments some repetitive commands always terminate but the actual number ofrepetitions does not depend on the initial state and is unbounded.To illustrate this point, consider the programSω ≡ do b ∧ x > 0 → x := x − 1⊓⊔ b ∧ x < 0 → x := x + 1⊓⊔ ¬b→ x :=?; b := trueod.Activated in a state where b is true, this program terminates after |x| repetitions. Thus t = |x| is an appropriate bound function for showing{b} Sω {true}with the rule of repetitive commands II.Sω also terminates when activated in a state σ where b is false, but wecannot predict the number of repetitions from σ. This number is known onlyafter the random assignment x :=? has been executed; then it is |x| again.Thus any bound function t on the number of repetitions has to satisfyt ≥ |x|for all x ≥ 0.
Clearly, this is impossible for any integer valued t. Consequently,the rule of repetitive commands II is not sufficient to show{¬b} Sω {true}.The following, more general proof rule for repetitive commands assumes awell-founded structure (W, <) to be a part of the underlying semantic domain D (cf. Section 2.3). Variables ranging over W can appear only in assertions and not in programs. As before, program variables range only over thestandard parts of the domain D like the integers or the Booleans.12.4 Random Assignment417RULE 38: REPETITIVE COMMAND IIIwhere{p ∧ Bi } Si {p}, i ∈ {1, . . . , n},{p ∧ Bi ∧ t = α} Si {t < α}, i ∈ {1, .
. . , n},p→t∈WVn{p} do ⊓⊔ni=1 Bi → Si od {p ∧ i=1 ¬Bi }(i) t is an expression which takes values in an irreflexive partial order (P, <)that is well-founded on the subset W ⊆ P ,(ii) α is a simple variable ranging over P that does not occur in p, t, Bi orSi for i ∈ {1, .
. . , n}.The expression t is the bound function of the repetitive command. Sinceit takes values in W that are decreased by every execution of a commandSi , the well-foundedness of < on W guarantees the termination of the wholerepetitive command do ⊓⊔ni=1 Bi → Si od. Note that with P = Z, the set ofintegers, and W = N, the set of natural numbers, the rule reduces to theprevious repetitive command II rule 33. Often P itself is well-founded. Thenwe take W = P .For proofs of total correctness of nondeterministic programs with randomassignments we use the following proof system TNR.PROOF SYSTEM TNR :This system is obtained from the proof system TNby adding axiom 37 and replacing rule 33 by rule 38.Example 12.3.
As a simple application of the system TNR let us prove thetermination of the program Sω considered above; that is,⊢TNR {true} Sω {true}.As a loop invariant we can simply take the assertion true. To find an appropriate bound function, we recall our informal analysis of Sω . Activated in astate where b is true, Sω terminates after |x| repetitions. But activated ina state where b is false, we cannot predict the number of repetitions of Sω .Only after executing the random assignment x :=? in the first round of Sωdo we know the remaining number of repetitions.This suggests using the well-founded structure(N ∪ {ω}, <)discussed earlier.
Recall that ω represents an unknown number which willbecome precise as soon as ω is decreased to some α < ω that must be in N.With this intuition the number of repetitions can be expressed by the boundfunction41812 Fairnesst ≡ if b then |x| else ω fi.Of course, we have to check whether the premises of the repetitive commandIII rule 38 are really satisfied. We take hereP = W = N ∪ {ω}so that rule 38 is applied with both t and α ranging over N ∪ {ω}. Thepremises dealing with the loop invariant are trivially satisfied.
Of the premisesdealing with the decrease of the bound function,⊢TNR {b ∧ x > 0 ∧ t = α} x := x − 1 {t < α}(12.3)⊢TNR {b ∧ x < 0 ∧ t = α} x := x + 1 {t < α}(12.4)andare easy to establish because t ranges over N when b evaluates to true.Slightly more involved is the derivation of⊢TNR {¬b ∧ t = α} x :=?; b := true {t < α}.(12.5)By the axiom of random assignment we have{∀x ≥ 0 : |x| < α} x :=? {|x| < α}.Since x is an integer variable, the quantifier ∀x ≥ 0 ranges over all naturalnumbers.
Since on the other hand α ranges over N ∪ {ω} and by definitionn < ω for all n ∈ N, the rule of consequence yields{ω = α} x :=? {|x| < α}.Using the (ordinary) axiom of assignment and the rule of sequential composition, we have{ω = α} x :=?; b := true {b ∧ |x| < α}.Thus, by the rule of consequence,{¬b ∧ ω = α} x :=?; b := true {b ∧ |x| < α}.Finally, using the definition of t in another application of the rule of consequence yields{¬b ∧ t = α} x :=?; b := true {t < α}.Since we applied only proof rules of the system TNR, we have indeed established (12.5).Thus an application of the repetitive command III rule 38 yields the desiredtermination result:⊢TNR {true} Sω {true}.12.5 Schedulers419As before, we can represent proofs by proof outlines. The above proof of totalcorrectness is represented as follows:{inv : true}{bd : if b then |x| else ω fi}do b ∧ x > 0 → {b ∧ x > 0}x := x − 1⊓⊔ b ∧ x < 0 → {b ∧ x < 0}x := x + 1⊓⊔ ¬b →{¬b}x :=?; b := trueod{true}.This concludes the example.⊓⊔The following theorem can be proved by a simple modification of the argument used to prove the Soundness of PW and TW Theorem 3.1.Theorem 12.1.
(Soundness of PNR and TNR)(i) The proof system PNR is sound for partial correctness of nondeterministic programs with random assignments.(ii) The proof system TNR is sound for total correctness of nondeterministicprograms with random assignments.Proof. See Exercise 12.3.⊓⊔12.5 SchedulersUsing random assignments we wish to develop a transformation Tfair whichreduces fair nondeterminism to ordinary nondeterminism.
We divide this taskinto two subtasks:• the development of a scheduler that enforces fairness in abstract runs,• the embedding of the schedulers into nondeterministic programs.In this section we deal with schedulers so that later, when considering parallelprograms, we can reuse all results obtained here. In addition, schedulers areinteresting in their own right because they explain how to implement fairness.In general, a scheduler is an automaton that enforces a certain disciplineon the computations of a nondeterministic or parallel program. To this end,the scheduler keeps in its local state sufficient information about the run ofa computation, and engages in the following interaction with the program:42012 FairnessAt certain moments during a computation, the program pre-sents the set E ofcurrently enabled components to the scheduler (provided E 6= ∅).
By consultingits local state, the scheduler returns to the program a nonempty subset I ofE. The idea is that whatever component i ∈ I is activated next, the resultingcomputation will still satisfy the intended discipline. So the program selectsone component i ∈ I for activation, and the scheduler updates its local stateaccordingly.We call a pair (E, i), where E ∪ {i} ⊆ {1, .
. . , n}, a selection (of n components). From a more abstract point of view, we may ignore the actualinteraction between the program and scheduler and just record the result ofthis interaction, the selection (E, i) checked by the scheduler. Summarizing,we arrive at the following definition.Definition 12.2. A scheduler (for n components) is given by• a set of local scheduler states σ, which are disjoint from the program states,• a subset of initial scheduler states, and• a ternary scheduling relationsch ⊆{scheduler states} × {selections of n components} × {scheduler states}which is total in the following sense:∀σ∀E 6= ∅ ∃i ∈ E ∃σ ′ : (σ, (E, i), σ ′ ) ∈ sch.Thus for every scheduler state σ and every nonempty set E of enabledcomponents there exists a component i ∈ E such that the selection (E, i)of n components together with the updated local state σ ′ satisfies thescheduling relation.⊓⊔Thus, given the local state σ of the scheduler,I = {i | ∃σ ′ : (σ, (E, i), σ ′ ) ∈ sch}is the subset returned by the scheduler to the program.
Totality of thescheduling relation ensures that this set I is nonempty. Consequently a scheduler can never block the computation of a program but only influence itsdirection. Consider now a finite or infinite run(E0 , i0 )(E1 , i1 ). . .(Ej , ij ). . .and a scheduler SCH. We wish to ensure that sufficiently many, but notnecessarily all, selections (Ej , ij ) are checked by SCH. To this end, we takea so-called check setC ⊆Nrepresenting the positions of selections to be checked.12.5 SchedulersDefinition 12.3.421(i) A run(E0 , i0 )(E1 , i1 ). . .(Ej , ij ). .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
