5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 30
Текст из файла (страница 30)
. of TS:infinite execution fragment ρ = s0 −−∞1. ρ is unconditionally A-fair whenever ∃ j. αj ∈ A.2. ρ is strongly A-fair whenever∞∞=⇒∃ j. Act(sj ) ∩ A = ∅∃ j. αj ∈ A .3. ρ is weakly A-fair whenever∞∞j.Act(sj.α)∩A=∅=⇒∈A.∀∃jj∞∞Here, ∃ j stands for “there are infinitely many j” and ∀ j for “for nearly all j” in thesense of “for all, except for finitely many j”. The variable j, of course, ranges over thenatural numbers.Fairness131To check whether a run is unconditionally A-fair it suffices to consider the actions thatoccur along the execution, i.e., it is not necessary to check which actions in A are enabledin visited states.
However, in order to decide whether a given execution is strongly orweakly A-fair, it does not suffice to only consider the actions actually occurring in theexecution. Instead, also the enabled actions in all visited states need to be considered.These enabled actions are possible in the visited states, but do not necessarily have to betaken along the considered execution.Example 3.44.A Simple Shared-Variable Concurrent ProgramConsider the following two processes that run in parallel and share an integer variable xthat initially has value 0:proc Inc = while x 0 do x := x + 1 odproc Reset = x := −1The pair of brackets . .
. embraces an atomic section, i.e., process Inc performs the checkwhether x is positive and the increment of x (if the guard holds) as one atomic step. Doesthis parallel program terminate? When no fairness constraints are imposed, it is possiblethat process Inc is permanently executing, i.e., process Reset never gets its turn, and theassignment x = −1 is not executed.
In this case, termination is thus not guaranteed, andthe property is refuted. If, however, we require unconditional process fairness, then everyprocess gets its turn, and termination is guaranteed.An important question now is: given a verification problem, which fairness notion touse? Unfortunately, there is no clear answer to this question. Different forms of fairnessdo exist—the above is just a small, though important, fragment of all possible fairnessnotions—and there is no single favorite notion. For verification purposes, fairness constraints are crucial, though. Recall that the purpose of fairness constraints is to rule outcertain “unreasonable” computations.
If the fairness constraint is too strong, relevantcomputations may not be considered. In case a property is satisfied (for a transition system), it might well be the case that some reasonable computation that is not considered(as it is ruled out by the fairness constraint) refutes this property. On the other hand,if the fairness constraint is too weak, we may fail to prove a certain property as someunreasonable computations (that are not ruled out) refute it.The relationship between the different fairness notions is as follows.
Each unconditionallyA-fair execution fragment is strongly A-fair, and each strongly A-fair execution fragmentis weakly A-fair. In general, the reverse direction does not hold. For instance, an executionfragment that solely visits states in which no A-actions are possible is strongly A-fair (asthe premise of strong A-fairness does not hold), but not unconditionally A-fair. Besides,132Linear-Time Propertiesan execution fragment that only visits finitely many states in which some A-actions areenabled but never executes an A-action is weakly A-fair (as the premise of weak A-fairnessdoes not hold), but not strongly A-fair. Summarizing, we haveunconditional A-fairness =⇒ strong A-fairness =⇒ weak A-fairnesswhere the reverse implication in general does not hold.Example 3.45.Fair Execution FragmentsConsider the transition system TSSem for the semaphore-based mutual exclusion solution.We label the transitions with the actions reqi , enteri (for i=1, 2), and rel in the obviousway, see Figure 3.12.In the execution fragmentreq1req1enterrel1n1 , n2 , y = 1 −−−−→w1 , n2 , y = 1 −−−−−→c1 , n2 , y = 0 −−−→ n1 , n2 , y = 1 −−−−→...only the first process gets its turn.
This execution fragment is indicated by the dashedarrows in Figure 3.12. It is not unconditionally fair for the set of actionsA = { enter2 }.It is, however, strongly A-fair, since no state is visited in which the action enter2 isexecutable, and hence the premise of strong fairness is vacuously false. In the alternativeexecution fragmentreq2req1enter1n1 , n2 , y = 1 −−−−→n1 , w2 , y = 1 −−−−→w1 , w2 , y = 1 −−−−−→req1rel−→ n1 , w2 , y = 1 −−−−→...c1 , w2 , y = 0 −−the second process requests to enter its critical section but is ignored forever. This execution fragment is indicated by the dotted arrows in Figure 3.12. It is not stronglyA-fair: although the action enter2 is infinitely often enabled (viz.
every time when visitingthe state w1 , w2 , y = 1 or n1 , w2 , y = 1), it is never taken. It is, however, weaklyA-fair, since the action enter2 is not continuously enabled—it is not enabled in the statec1 , w2 , y = 0.A fairness constraint imposes a requirement on all actions in a set A. In order to enabledifferent fairness constraints to be imposed on different, possibly nondisjoint, sets of actions, fairness assumptions are used.
A fairness assumption for a transition system mayrequire different notions of fairness with respect to several sets of actions.Fairness133n1 , n2 , y=1req2relreq1relw1 , n2 , y=1n1 , w2 , y=1req2enter2req1enter1c1 , n2 , y=0req2relw1 , w2 , y=1reln1 , c2 , y=0enter2req1enter1c1 , w2 , y=0w1 , c2 , y=0Figure 3.12: Two examples of fair execution fragments of the semaphore-based mutualexclusion algorithm.Definition 3.46.Fairness AssumptionA fairness assumption for Act is a tripleF = (Fucond , Fstrong , Fweak )with Fucond , Fstrong , Fweak ⊆ 2Act . Execution ρ is F-fair if• it is unconditionally A-fair for all A ∈ Fucond ,• it is strongly A-fair for all A ∈ Fstrong , and• it is weakly A-fair for all A ∈ Fweak .If the set F is clear from the context, we use the term fair instead of F-fair.Intuitively speaking, a fairness assumption is a triple of sets of (typically different) actionsets, one such set of action sets is treated in a strongly fair manner, one in a weakly fairmanner, and one in an unconditionally fair way.
This is a rather general definition thatallows imposing different fairness constraints on different sets of actions. Quite often, onlya single type of fairness constraint suffices. In the sequel, we use the casual notationsfor these fairness assumptions. For F ⊆ 2Act , a strong fairness assumption denotes thefairness assumption (∅, F, ∅). Weak, and unconditional fairness assumptions are used ina similar way.134Linear-Time PropertiesThe notion of F-fairness as defined on execution fragments is lifted to traces and pathsin the obvious way. An infinite trace σ is F-fair if there is an F-fair execution ρ withtrace(ρ) = σ. F-fair (infinite) path fragments and F-fair paths are defined analogously.Let FairPathsF (s) denote the set of F-paths of s (i.e., infinite F-fair path fragments thatstart in state s), and FairPathsF (TS) the set of F-fair paths that start in some initialstate of TS.
Let FairTracesF (s) denote the set of F-fair traces of s, and FairTracesF (TS)the set of F-fair traces of the initial states of transition system TS:FairTracesF (s) = trace(FairPathsF (s))FairTracesF (s).FairTracesF (TS) =ands∈INote that it does not make much sense to define these notions for finite traces as any finitetrace is fair by default.Example 3.47.Mutual Exclusion AgainConsider the following fairness requirement for two-process mutual exclusion algorithms:“process Pi acquires access to its critical section infinitely often”for any i ∈ { 1, 2 }.
What kind of fairness assumption is appropriate to achieve this?Assume each process Pi has three states ni (noncritical), wi (waiting), and ci (critical).As before, the actions reqi , enteri , and rel are used to model the request to enter thecritical section, the entering itself, and the release of the critical section. The strongfairness assumption{ {enter1 , enter2 } }ensures that one of the actions enter1 or enter2 , is executed infinitely often. A behaviorin which one of the processes gets access to the critical section infinitely often while theother gets access only finitely many times is strongly fair with respect to this assumption.This is, however, not intended.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
