3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 78
Текст из файла (страница 78)
The correctness of this program depends on the fairness assumption.For pedagogical reasons we first study an example where the main idea forthe termination argument is exercised.Example 12.7. Consider a programS ≡ do B1 → S1 ⊓⊔. . .⊓⊔Bn → Sn odwith the following property: the index set {1, . . . , n} is partitioned into setsK and L with L 6= ∅, such that executing any subprogram Sk with k ∈ Kdoes not change the program state, whereas executing any subprogram Sℓwith ℓ ∈ L yields a new program state which is closer to a terminal state ofS.More specifically, we takeB ≡ x 6= 0, Sk ≡ skip for k ∈ K and Sℓ ≡ x := x − 1 for ℓ ∈ L,where x is an integer variable.
For any choice of K and L we wish to prove|=fair {x ≥ 0} S {x = 0}with the help of the fair repetition rule 39′ of system FN. As invariant wetakep ≡ x ≥ 0.This choice obviously satisfies premise (1) of rule 39′ .To find an appropriate bound function, let us first consider the case whereK = {1, .
. ., n − 1} and L = {n}; that is, whereS ≡ do x 6= 0 → skip ⊓⊔. . .⊓⊔ x 6= 0 → skip ⊓⊔ x 6= 0 → x := x − 1 od.|{z}n − 1 timesAs in Example 12.6, we observe a hierarchy of changes:• executing one of the n − 1 subprograms skip; the assumption of fairnessimplies that the subprogram Sn ≡ x := x − 1 cannot be neglected forever,• executing Sn decrements x, thus bringing us closer to the termination ofS.12.9 Case Study: Asynchronous Fixed Point Computation447Since the number of rounds through the loop during which Sn is neglectedis counted by the scheduling variable zn referring to Sn , we arrive at thebound functiont ≡ (x, zn )ranging over the well-founded structure W = N × N ordered lexicographicallyby <lex .Clearly, p and t satisfy premise (3) of rule 39′ .
By the simple form of thesubprograms of S, checking premise (2) of rule 39′ boils down to checkingthe following implications:• for Sk ≡ skip where k ∈ {1, . . ., n − 1}:x > 0 ∧ zn ≥ 0 ∧ (x, zn + 1) = α → (x, zn ) <lex α,• for Sn ≡ x := x − 1:x > 0 ∧ zn ≥ 0 ∧ ∃zn ≥ 0 : (x, zn ) = α → (x − 1, zn ) <lex α.These implications are obviously true.Thus the fair repetition rule 39′ and the rule of consequence yield|=fair {x ≥ 0} S {x = 0}as claimed.Let us now turn to the general case of sets K and L where it is not onlysubprogram Sn that is responsible for decrementing x, but any subprogramSℓ with ℓ ∈ L will do. Then the number of rounds neglecting any of these subprograms is given by min {zℓ | ℓ ∈ L} with zℓ being the scheduling variablereferring to Sℓ .
This leads tot ≡ (x, min {zℓ | ℓ ∈ L})as a suitable bound function for the general case.⊓⊔Before we formulate the problem we wish to solve, we need to introducesome auxiliary notions first. A partial order is a pair (A, ⊑ ) consisting of aset A and a reflexive, antisymmetric and transitive relation ⊑ on A.Consider now a partial order (A, ⊑ ). Let a ∈ A and X ⊑ A. Then a iscalled the least element of X if a ∈ X and a ⊑ x for all x ∈ X. The element ais called an upper bound of X if x ⊑ a for all x ∈ X. Note that upper boundsof X need not be elements of X. Let U be the set of all upper bounds of X.Then a is called the least upper bound of X if a is the least element of U .A partial order (A, ⊑ ) is called complete if A contains a least elementand if for every ascending chaina0 ⊑ a1 ⊑ a2 .
. .44812 Fairnessof elements from A the set{a0 , a1 , a2 , . . .}has a least upper bound.Now we turn to the problem of computing fixed points. Let (L, ⊑ ) be acomplete partial order. For x, y ∈ L we write x ⊏ y if x ⊑ y and x 6= y. Let⊐ denote the inverse of ⊏ ; so x ⊐ y if y ⊏ x holds. Assume that (L, ⊑ )has the finite chain property, that is, every ascending chainx1 ⊑ x2 ⊑ x3 ⊑ .
. .of elements xi ∈ L stabilizes. In other words, there is no infinite increasingchainx1 ⊏ x2 ⊏ x3 ⊏ . . .in L, or equivalently, the inverse relation ⊐ is well-founded on L.We consider here the n-fold Cartesian product Ln of L for some n ≥ 2.The relation ⊑ is extended componentwise from L to Ln :(x1 , . . ., xn ) ⊑ (y1 , . . ., yn ) iff ∀(1 ≤ i ≤ n) : xi ⊑ yi .We also extend the relation ⊏ and its inverse ⊐ :(x1 , . .
., xn ) ⊏ (y1 , . . ., yn ) iff (x1 , . . ., xn ) ⊑ (y1 , . . ., yn )and (x1 , . . ., xn ) 6= (y1 , . . ., yn ),(x1 , . . ., xn ) ⊐ (y1 , . . ., yn ) iff(y1 , . . ., yn ) ⊏ (x1 , . . ., xn ).Then also the pair (Ln , ⊑ ) is a complete partial order with the finite chainproperty. Let ∅ denote the least element in Ln .Consider now a functionF : Ln → Lnwhich is monotonic under ⊑ ; that is, whenever (x1 , . .
., xn ) ⊑ (y1 , . . ., yn )then F (x1 , . . ., xn ) ⊑ F (y1 , . . ., yn ).By Fi we denote the ith component functionFi : Ln → Lof F . Thus we define Fi as follows:Fi (x1 , . . ., xn ) = yi iff F (x1 , . . ., xn ) = (y1 , . . ., yn ).Since ⊑ is defined componentwise and F is monotonic, the functions Fi arealso monotonic under ⊑ .By a general theorem due to Knaster and Tarski (see Tarski [1955]), F hasa least fixed point µF ∈ Ln ; that is,F (µF ) = µF12.9 Case Study: Asynchronous Fixed Point Computation449andF (x1 , . .
., xn ) = (x1 , . . ., xn ) implies µF ⊑ (x1 , . . ., xn ).Usually µF is computed as follows. Starting with the least element ∅ in Lnthe operator F is applied iteratively:∅ ⊑ F (∅) ⊑ F (F (∅)) ⊑ F (F (F (∅))) ⊑ . . . .By the finite chain property of Ln , this iteration process will surely stabilizeby the least fixed point µF . Since an application of F requires a simultaneousupdate of all n components of its arguments, this method of computing µFis called a synchronous fixed point computation.Following Cousot and Cousot [1977b] we are interested here in a moreflexible method. We wish to compute µF asynchronously by employing nsubprograms Si , for i ∈ {1, . .
. , n}, where each of them is allowed to apply only the ith component function Fi . These subprograms are activatednondeterministically by the following program:AFIX ≡ do B → x1 := F1 (x̄)⊓⊔. . .⊓⊔B → xn := Fn (x̄) od,where x̄ ≡ (x1 , . . ., xn ) and B ≡ x̄ 6= F (x̄). In general AFIX will not computeµF , but the claim is that it will do so under the assumption of fairness:|=fair {x̄ = ∅} AFIX {x̄ = µF }.(12.29)This correctness result is a special case of a more general theorem proved inCousot and Cousot [1977b].We would like to prove (12.29) in the system FN. To this end, we proceedin two steps.Step 1 We start with an informal analysis of AFIX. Consider a computationξ :< AFIX, σ >=< S1 , σ 1 > → . . . → < Sj , σ j > → . .
.of AFIX and the abbreviations σ j (x̄) = (σ j (x1 ), . . ., σ j (xn )) for j ≥ 1 andFi [x̄] = (x1 , . . ., xi−1 , Fi (x̄), xi+1 , . . ., xn )for i ∈ {1, . . . , n}. Since σ 1 (x̄) = ∅ holds and the component functions Fi aremonotonic, the assertion∅ ⊑ x̄ ⊑ Fi [x̄] ⊑ µF(12.30)is true for i ∈ {1, . . . , n} in every state σ j of ξ. Thus, by the least fixed pointproperty, x̄ = µF holds as soon as AFIX has terminated with x̄ = F (x̄).But why does AFIX terminate? Note that by (12.30) AFIX produces anascending chainσ 1 (x̄) ⊑ . . .
⊑ σ j (x̄) ⊑ . . .45012 Fairnessof values in the variable x̄. That there exists a state σ j in which x̄ = F (x̄)relies on the following two facts.(i) By the finite chain property of L and hence Ln , the values σ j (x̄) ∈ Lncannot be increased infinitely often.(ii) By the assumption of fairness, the values σ j (x̄) cannot be constantarbitrarily long without increasing.(i) is clear, but (ii) needs a proof. Consider some nonterminal state σ jin ξ (thus satisfying B ≡ x̄ 6= F (x̄)) for which either σ j (x̄) = σ 1 (x̄) (start)or σ j−1 (x̄) ⊏ σ j (x̄) (increase just happened) holds. Then we can find twoindex sets K and L, both depending on σ j , which partition the subprogramsS1 , .
. ., Sn of AFIX into subsets {Sk | k ∈ K} and {Sℓ | ℓ ∈ L} such that theSk stabilize the values of x̄, so for k ∈ K, x̄ = Fk [x̄] holds in σ j , whereas theSℓ increase the values of x̄, so for ℓ ∈ L, x̄ ⊏ Fℓ [x̄] holds in σ j . Note thatL 6= ∅ holds because σ j is nonterminal.Thus, as long as subprograms Sk with k ∈ K are executed, the programAFIX generates states σ j+1 , σ j+2 , .
. . satisfyingσ j (x̄) = σ j+1 (x̄) = σ j+2 (x̄) = . . . .But as soon as a subprogram Sℓ with ℓ ∈ L is executed in some state σ mwith j ≤ m, we get the desired next increaseσ m (x̄) ⊏ σ m+1 (x̄)after σ j . Fairness guarantees that such an increase will indeed happen.The situation is close to that investigated in Example 12.7, except for thefollowing changes:• instead of decrementing an integer variable x, here x̄ = (x1 , . .
., xn ) isincreased in the ordering ⊏ on Ln ,• the number of possible increases of x̄ is unknown but finite,• the index sets K and L depend on the state σ j .Step 2 With this informal discussion in mind, we are now prepared for theformal correctness proof. The essential step is the application of the fairrepetition rule 39′ . A suitable invariant isp≡n^(∅ ⊑ x̄ ⊑ Fi [x̄] ⊑ µF ).i=1Clearly, p satisfies premise (1′ ) of rule 39′ .By analogy to Example 12.7, we take as the well-founded structure the setW = Ln × Nordered lexicographically as follows:12.9 Case Study: Asynchronous Fixed Point Computation451(x̄, u) <lex (ȳ, v) iff x̄ ⊐ ȳ or (x̄ = ȳ and u < v),with the inverse relation ⊐ in the first component because increasing x̄means getting closer to the desired fixed point, hence termination.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
