3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 72
Текст из файла (страница 72)
Under what assumption does PU2 terminate, then? This questionbrings us to the notion of strong fairness; it requires that every guardedcommand that is enabled infinitely often is also activated infinitely often.Under this assumption, a computation of PU2 cannot forever activate itsfirst command because the guard “full-page” of the second command is theninfinitely often enabled. Thus the assignment signal := true is eventuallyexecuted, causing termination of PU2.In this book, we understand by fairness the notion of strong fairness.
Weinvestigate fairness only for the class of nondeterministic programs that wecall one-level nondeterministic programs. These are programs of the formS0 ; do B1 → S1 ⊓⊔. . .⊓⊔Bn → Sn od,where S0 , S1 , . . ., Sn are while programs.Selections and RunsLet us now be more precise about fairness. Since it can be expressed exclusively in terms of enabled and activated components, we abstract from allother details in computations and introduce the notions of selection and run.This simplifies the definition and subsequent analysis of fairness, both hereand later for parallel programs.A selection (of n components) is a pair(E, i)consisting of a nonempty set E ⊆ {1, .
. . , n} of enabled components and anactivated component i ∈ E. A run (of n components) is a finite or infinitesequence(E0 , i0 ). . .(Ej , ij ). . .of selections.A run is called fair if it satisfies the following condition:∞∞∀(1 ≤ i ≤ n) : ( ∃ j ∈ N : i ∈ Ej → ∃ j ∈ N : i = ij ).∞The quantifier ∃ stands for “there exist infinitely many,” and N denotes theset {0, 1, 2, 3, . . .}. Thus, in a fair run, every component i which is enabledinfinitely often, is also activated infinitely often. In particular, every finiterun is fair.Next, we link runs to the computations of one-level nondeterministic programsS ≡ S0 ; do B1 → S1 ⊓⊔.
. .⊓⊔Bn → Sn od12.1 The Concept of Fairness411defined above. A transition< Tj , σ j > → < Tj+1 , σ j+1 >in a computation of S is called a loop transition ifTj ≡ do B1 → S1 ⊓⊔. . .⊓⊔Bn → Sn od and σ j |=n_Bi .i=1The selection (Ej , ij ) of a loop transition is given byEj = {i ∈ {1, . . . , n} | σ j |= Bi )}andTj+1 ≡ Sij ; Tj ,meaning that Ej is the set of indices i of enabled guards Bi and ij is theindex of the command activated in the transition.
Note that Ej 6= ∅.The run of a computation of Sξ :< S, σ >=< T0 , σ 0 > → . . . → < Tj , σ j > → . . .is defined as the run(Ej0 , ij0 ). . .(Ejk , ijk ). . .recording all selections of loop transitions in ξ. Here j0 < . . . < jk < . . . isthe subsequence of indices j ≥ 0 picking up all loop transitions< Tjk , σ jk > → < Tjk +1 , σ jk +1 >in ξ.
Thus computations that do not pass through any loop transition yieldthe empty run. A run of a program S is the run of one of its computations.A computation is fair if its run is fair. Thus for fairness only loop transitionsare relevant; transitions inside the deterministic parts S0 , S1 , . . ., Sn of S donot matter. Note that every finite computation is fair.Example 12.1. To practice with this definition, let us look at the programPU1 again. A computation of PU1 that exclusively activates the first component (the printer) yields the run({1, 2}, 1)({1, 2}, 1). . .({1, 2}, 1). .
. .Since the index 2 (representing the second component) is never activated, therun and hence the computation is not fair. Every fair computation of PU1 isfinite, yielding a run of the form({1, 2}, 1). . .({1, 2}, 1)({1, 2}, 2).41212 Fairness⊓⊔Fair Nondeterminism SemanticsThe fair nondeterminism semantics of one-level nondeterministic programsS is defined as follows where σ is a proper state:Mfair [[S]](σ) ={τ |< S, σ > →∗ < E, τ >}∪ {⊥ | S can diverge from σ in a fair computation}∪ {fail | S can fail from σ}.We see that Mfair [[S]] is like Mtot [[S]] except that only fair computations areconsidered.
Notice that this affects only the diverging computations yielding⊥.How does this restriction to fair computations affect the results of programs? The answer is given in the following example.Example 12.2. Consider a slight variation of the program PU1, namelyPU3 ≡ signal := false; count := 0;do ¬signal → “print next line”;count := count + 1⊓⊔ ¬signal → signal := trueod.The variable count counts the number of lines printed.
Let σ be a statewith σ(count) = 0 and σ(signal) = true. For i ≥ 0 let σ i be as σ but withσ i (count) = i. Ignoring the possible effect of the command “print next line”,we obtainMtot [[PU3]](σ) = {σ i | i ≥ 0} ∪ {⊥}butMfair [[PU3]](σ) = {σ i | i ≥ 0}.We see that under the assumption of fairness PU3 always terminates (⊥ isnot present) but still there are infinitely many final states possible: σ i withi ≥ 0.
This phenomenon differs from the bounded nondeterminism proved forMtot in the Bounded Nondeterminism Lemma 10.1; it is called unboundednondeterminism.⊓⊔12.3 Well-Founded Structures41312.2 Transformational SemanticsFair nondeterminism was introduced by restricting the set of allowed computations. This provides a clear definition but no insight on how to reasonabout or prove correctness of programs that assume fairness.We wish to provide such an insight by applying the principle of transformational semantics:Reduce the new concept (here fair nondeterminism semantics) to known concepts (here total correctness semantics) with the help of program transformations.In other words, we are looking for a transformation Tfair which transformseach one-level nondeterministic program S into another nondeterministic program Tfair (S) satisfying the semantic equationMfair [[S]] = Mtot [[Tfair (S)]].(12.1)The benefits of Tfair are twofold. First, it provides us with information on howto implement fairness.
Second, Tfair serves as a stepping stone for developing aproof system for fair nondeterminism. We start with the following conclusionof (12.1):|=fair {p} S {q} iff |=tot {p} Tfair (S) {q},(12.2)which states that a program S is correct in the sense of fair total correctness(explained in Section 12.7) if and only if its transformed version Tfair (S)is correct in the sense of usual total correctness.
Corollary (12.2) suggestsusing the transformation Tfair itself as a proof rule in a system for fair nondeterminism. This is a valid approach, but we can do slightly better here:by informally “absorbing” the parts added to S by Tfair into the pre- andpostconditions p and q we obtain a system for proving|=fair {p} S {q}directly without reference to Tfair . So, Tfair is used only to motivate andjustify the new proof rules.The subsequent sections explain this transformational semantics approachin detail.12.3 Well-Founded StructuresWe begin by introducing well-founded structures.
The reason is that to provetermination of programs involving unbounded nondeterminism (see Example 12.2), we need bound functions that take values in more general structuresthan integers.41412 FairnessDefinition 12.1. Let (P, <) be an irreflexive partial order; that is, let P be aset and < an irreflexive transitive relation on P . We say that < is well-foundedon a subset W ⊆ P if there is no infinite descending chain. .
. < w2 < w1 < w0of elements wi ∈ W . The pair (W, <) is then called a well-founded structure.If w < w′ for some w, w′ ∈ W we say that w is less than w′ or w′ is greaterthan w.⊓⊔Of course, the natural numbers form a well-founded structure (N, <) underthe usual relation <. But also the extension (N ∪ {ω}, <), with ω denotingan “unbounded value” satisfyingn<ωfor all n ∈ N, is well-founded.
We mention two important construction principles for building new well-founded structures from existing ones.Let (W1 , <1 ) and (W1 , <2 ) be two well-founded structures. Then thestructure (W1 × W2 , <com ) with <com denoting the componentwise orderon W1 × W2 defined by(m1 , m2 ) <com (n1 , n2 ) iff m1 <1 n1 or m2 <2 n2is well-founded, and the structure (W1 × W2 , <lex ) with <lex denoting thelexicographic order on W1 × W2 defined by(m1 , m2 ) <lex (n1 , n2 ) iff (m1 <1 n1 ) or(m1 = n1 and m2 <2 n2 )is also well-founded.Similarly, given well-founded structures (W1 , <1 ), .
. ., (Wn , <n ), we candefine the componentwise and the lexicographic orders on the products W1 ×. . . × Wn (n > 1). These also are well-founded.12.4 Random AssignmentNote that we cannot expect the transformed program Tfair (S) to be another nondeterministic program in the syntax of Section 10.1, because thesemantics Mtot yields bounded nondeterminism (Bounded NondeterminismLemma 10.1) for these programs whereas Mfair yields unbounded nondeterminism (Example 12.2).But we can find a transformation Tfair where the transformed programTfair (S) uses an additional language construct: the random assignment12.4 Random Assignment415x :=?.It assigns an arbitrary nonnegative integer to the integer variable x. Therandom assignment is an explicit form of unbounded nondeterminism.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
