3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 74
Текст из файла (страница 74)
.can be checked by SCH at every position in C if there exists a finite orinfinite sequenceσ 0 σ 1 . . .σ j , . . .of scheduler states, with σ 0 being an initial scheduler state, such thatfor all j ≥ 0(σ j , (Ej , ij ), σ j+1 ) ∈ schif j ∈ Cσ j = σ j+1otherwise.andWe say that a run can be checked by SCH if it can be checked by SCHat every position; that is, for the check set C = N.(ii) A scheduler SCH for n components is called fair (for a certain subsetof runs) if every run of n components which (is in this subset and) canbe checked by SCH is fair.(iii) A fair scheduler SCH for n components is called universal if every fairrun of n components can be checked by SCH.⊓⊔Thus for j ∈ C the scheduling relation sch checks the selection (Ej , ij )made in the run using and updating the current scheduler state; for j 6∈ Cthere is no interaction with the scheduler and hence the current schedulerstate remains unchanged (for technical convenience, however, this is treatedas an identical step with σ j = σ j+1 ).For example, with C = {2n + 1 | n ∈ N} every second selection in a run ischecked.
This can be pictured as follows:Run:Scheduler:(E0 , i0 ) (E1 ,i1 ) (E2 , i2 ) (E3 ,i3 ). . .↓ ↑↓ ↑σ 0 = σ 1 SCH σ 2 = σ 3 SCH σ 4 . . . .Note that the definition of checking applies also in the case of finite runs Hand infinite check sets C.The Scheduler FAIRUsing the programming syntax of this section, we now present a specificscheduler FAIR. For n components it is defined as follows:• The scheduler state is given by n integer variables z1 , . . ., zn ,42212 Fairness• this state is initialized nondeterministically by the random assignmentsINIT ≡ z1 :=?; . .
.; zn :=?,• the scheduling relation sch(σ, (E, i), σ ′ ) holds iff σ, E, i, σ ′ are as follows:(i) σ is given by the current values of z1 , . . ., zn ,(ii) E and i satisfy the conditionSCH i ≡ zi = min {zk | k ∈ E},(iii) σ ′ is obtained from σ by executingUPDATE i ≡ zi :=?;for all j ∈ {1, . . . , n} − {i} doif j ∈ E then zj := zj − 1 fiod,where we use the abbreviationfor all j ∈ {1, . .
. , n} − {i} do Sj od≡ S1 ; . . .; Si−1 ; Si+1 ; . . .; Sn .The scheduling variables z1 , . . ., zn represent priorities assigned to the ncomponents. A component i has higher priority than a component j if zi < zj .Initially, the components are assigned arbitrary priorities. If during a runFAIR is presented with a set E of enabled components, it selects a componenti ∈ E that has maximal priority; that is, withzi = min {zk | k ∈ E}.For any nonempty set E and any values of z1 , . . ., zn there exists some (butnot necessarily unique) i ∈ E with this property. Thus the scheduling relationsch of FAIR is total as required by Definition 12.2.The update of the scheduling variables guarantees that the priorities ofall enabled but not selected components j get increased.
The priority of theselected component i, however, gets reset arbitrarily. The idea is that bygradually increasing the priority of enabled components j their activationcannot be refused forever. The following theorem makes this idea precise.Theorem 12.2. (Fair Scheduling) For n components FAIR is a universalfair scheduler. In other words, a run of n components is fair iff it can bechecked by FAIR.Proof. “if ”: Consider a run(E0 , i0 ). .
.(Ej , ij ). . .that is checked at every position. Let(12.6)12.5 Schedulers423σ 0 . . .σ j . . .be a sequence of scheduler states of FAIR satisfying sch(σ j , (Ej , ij ), σ j+1 )for every j ∈ N. We claim that (12.6) is fair.Suppose the contrary. Then there exists some component i ∈ {1, . . . , n}which is infinitely often enabled, but from some moment j0 ≥ 0 on neveractivated. Formally,∞( ∃ j ∈ N : i ∈ Ej ) ∧ (∀j ≥ j0 : i 6= ij ).Since (12.6) is checked at every position, the variable zi of FAIR, which getsdecremented whenever the component i is enabled but not activated, becomesarbitrarily small, in particular, smaller than −n in some state σ j with j ≥ j0 .But this is impossible because the assertionINV ≡n^card {i ∈ {1, .
. . , n} | zi ≤ −k} ≤ n − kk=1holds in every scheduler state σ j of FAIR. INV states, in particular, for k = 1that at most n − 1 of the scheduling variables z1 , . . ., zn of FAIR can havevalues ≤ −1, and for k = n that none of the scheduling variables can havevalues ≤ −n.We prove this invariant by induction on j ≥ 0, the index of the state σ j .In σ 0 we have z1 , . . ., zn ≥ 0 so that INV is trivially satisfied. Assume nowthat INV holds in σ j .
We show that INV also holds in σ j+1 . Suppose INVis false in σ j+1 . Then there is some k ∈ {1, . . . , n} such that there are at leastn−k +1 indices i for which zi ≤ −k holds in σ j+1 . Let I be the set of all theseindices. Note that I is nonempty and card I ≥ n − k + 1. By the definitionof FAIR, zi ≤ −k + 1 holds for all i ∈ I in σ j . Thus card I ≤ n − k + 1 bythe induction hypothesis. So actually card I = n − k + 1 andI = {i ∈ {1, . . . , n} | σ j |= zi ≤ −k + 1}.Since FAIR checks the run (12.6) at position j, we have sch(σ j , (Ej , ij ), σ j+1 ).By the definition of FAIR, the activated component ij is in I. This is acontradiction because then zij ≥ 0 holds in σ j+1 due to the UPDATE ij partof FAIR.
Thus INV remains true in σ j+1 .“only if ”: Conversely, let the run(E0 , i0 ). . .(Ej , ij ). . .(12.7)be fair. We show that (12.7) can be checked at every position by constructinga sequenceσ 0 . . .σ j . . .42412 Fairnessof scheduler states of FAIR satisfying sch(σ j , (Ej , ij ), σ j+1 ) for every j ∈ N.The construction proceeds by assigning appropriate values to the sche-dulingvariables z1 , . . ., zn of FAIR. For i ∈ {1, .
. . , n} and j ∈ N we putσ j (zi ) = card {ℓ | j ≤ ℓ < mi,j ∧ i ∈ Eℓ },wheremi,j = min {m | j ≤ m ∧ (im = i ∨ ∀n ≥ m : i 6∈ En )}.Thus σ j (zi ) counts the number of times (ℓ) the ith component will be enabled(i ∈ Eℓ ) before its next activation (im = i) or before its final “retirement”(∀n ≥ m : i 6∈ En ).
Note that the minimum mi,j ∈ N exists because the run(12.7) is fair. In this construction the variables z1 , . . ., zn have values ≥ 0 inevery state σ j and exactly one variable zi with i ∈ Ej , has the value 0. Thisi is the index of the component activated next. It is easy to see that thisconstruction of values σ j (zi ) is possible with the assignments in FAIR.⊓⊔The universality of FAIR implies that every other fair scheduler can beobtained by implementing the nondeterministic choices in FAIR.
FollowingDijkstra [1976] and Park [1979], implementing nondeterminism means narrowing the set of nondeterministic choices. For example, a random assignmentz :=? can be implemented by any ordinary assignment z := t where t evaluates to a nonnegative value.The Scheduler ROROThe simplest scheduler is the round robin scheduler RORO.
For n componentsit selects the enabled components clockwise in the cyclic ordering1 → 2 → . . . → n → 1,thereby skipping over momentarily disabled components.Is RORO a fair scheduler? The answer is “no.” To see this, consider a runof three components 1, 2, 3 where 1 and 3 are always enabled but 2 is enabledonly at every second position in the run. Then RORO schedules the enabledcomponents as follows:({1, 2, 3}, 1)({1, 3}, 3)({1, 2, 3}, 1)({1, 3}, 3).
. . .Thus, component 2 is never selected by RORO, even though it is enabledinfinitely often. Hence, the run is unfair.However, it is easy to see that RORO is a fair scheduler for monotonicruns.12.5 Schedulers425Definition 12.4. A possibly infinite run(E0 , i0 )(E1 , i1 ). . .(Ej , ij ). . .is called monotonic ifE0 ⊇ E1 ⊇ . . . ⊇ Ej ⊇ . . ..⊓⊔Obviously, the run considered above is not monotonic. Note that one-levelnondeterministic programsS ≡ S0 ; do B → S1 ⊓⊔. .
.⊓⊔B → Sn odwith identical guards have only monotonic runs. Thus for these programsRORO can be used as a fair scheduler.How can we obtain RORO from FAIR? Consider the following implementation of the random assignments in FAIR for n components:INIT ≡ z1 := 1; . . .; zn := n,SCH i ≡ zi = min {zk | k ∈ E},UPDATE i ≡ zi := n;for all j ∈ {1, .
. . , n} − {i} doif j ∈ E then zj := zj − 1 fiod.By the Fair Scheduling Theorem 12.2, this is a fair scheduler for arbitraryruns. When applied to a monotonic run, it always schedules the next enabledcomponent in the cyclic ordering 1 → 2 → . . . → n → 1. Thus for monotonicruns the above is an implementation of the round robin scheduler RORO,systematically obtained from the general scheduler FAIR.Clearly, this implementation of RORO is too expensive in terms of storage requirements. Since we only need to remember which component wasselected as the last one, the variables z1 , . . ., zn of RORO can be condensedinto a single variable z ranging over {1, .
. . , n} and pointing to the indexof the last selected component. This idea leads to the following alternativeimplementation of RORO:INIT ≡ z := 1,SCH i ≡ i = succm (z) where m = min {k | succk (z) ∈ E},UPDATE i ≡ succm+1 (z).Here succ(·) is the successor function in the cyclic ordering 1 → 2 → . . . → n→ 1 and succk (·) is the kth iteration of this successor function.42612 FairnessThis implementation uses only n scheduler states. It follows from a resultof Fischer and Paterson [1983] that this number is optimal for fair schedulersfor monotonic runs of n components.The Scheduler QUEUEAs we have seen, for nonmonotonic runs fairness cannot be enforced by theinexpensive round robin scheduler.
Fischer and Paterson [1983] have shownthat any fair scheduler that is applicable for arbitrary runs of n componentsneeds at least n! = 1 · 2 · . . . · n scheduler states.One way of organizing such a scheduler is by keeping the componentsin a queue. In each check the scheduler activates that enabled componentwhich is earliest in the queue. This component is then placed at the endof the queue.
Fairness is guaranteed since every enabled but not activatedcomponent advances one position in the queue. Let us call this schedulerQUEUE.Consider once more a run of three components 1, 2, 3 where 1 and 3 arealways enabled but 2 is enabled only at every second position in the run.Then QUEUE schedules the enabled components as follows:Run:({ 1, 2, 3}, 1)({ 1, 3}, 3)({ 1, 2, 3}, 2)({ 1, 3}, 1)↓↑↓↑↓↑↓↑QUEUE:1.2.32.3.12.1.31.3.2Run:({ 1, 2, 3}, 3)({ 1, 3}, 1)({ 1, 2, 3}, 2)({ 1, 3}, 3)↓↑↓↑↓↑↓↑QUEUE:3.2.12.1.32.3.13.1.2Run:({ 1, 2, 3}, 1)↓↑QUEUE:1.2.3...... .Below each selection of the run we exhibit the value of the queue on whichthis selection is based.
We see that the ninth selection ({1, 2, 3},1) in the runis based on the same queue value 1.2.3 as the first selection ({1, 2, 3},1). Thusevery component gets activated infinitely often.The effect of QUEUE can be modeled by implementing the random assignments of the general scheduler FAIR as follows:12.6 Transformation427INIT ≡ z1 := 0; z2 := n; . .
.; zn := (n − 1) · n,SCH i ≡ zi := min {zk | k ∈ E},UPDATE i ≡ zi := n + max {z1 , . . ., zn };forall j ∈ {1, . . . , n} − {i} doif j ∈ E then zj := zj − 1 fiod.The idea is that in the QUEUE component i comes before component j iffzi < zj holds in the above implementation. Since FAIR leaves the variableszj of disabled components j unchanged and decrements those of enabledbut not activated ones, some care had to be taken in the implementationof the random assignment of FAIR in order to prevent any change of theorder of components within the queue. More precisely, the order “componenti before component j,” represented by zi < zj should be preserved as longas neither i nor j is activated. That is why initially and in every update wekeep a difference of n between the new value of zi and all previous values.This difference is sufficient because a component that is enabled n times isselected at least once.12.6 TransformationWe can now present the transformation Tfair reducing fair nondeterminismto the usual nondeterminism in the sense of transformational semantics ofSection 12.2:Mfair [[S]] = Mtot [[Tfair (S)]].Given a one-level nondeterministic programS ≡ S0 ; do ⊓⊔ni=1 Bi → Si od,the transformed program Tfair (S) is obtained by embedding the schedulerFAIR into S:Tfair (S) ≡ S0 ; INIT ;do ⊓⊔ni=1 Bi ∧ SCH i → UPDATE i ; Si od,where we interpret E as the set of indices k ∈ {1, .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
