5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 29
Текст из файла (страница 29)
. and σ2 = B1 B2 . . .and n is the length of the longest common prefix. Moreover, we put d(σ, σ) = 0. Then,d is a metric on (2AP )ω , and hence induces a topology on (2AP )ω . Under this topology,126Linear-Time Propertiessafety and liveness property(2AP )ωsafety propertiesinvariantsliveness propertiesneither livenessnor safety propertiesFigure 3.11: Classification of linear-time properties.the safety properties are exactly the closed sets, while the liveness properties agree withthe dense sets.
In fact, closure(P ) is the topological closure of P , i.e., the smallest closedset that contains P . The result stated in Theorem 3.37 then follows from the well-knownfact that any subset of a topological space (of the kind described above) can be writtenas the intersection of its closure and a dense set.3.5FairnessAn important aspect of reactive systems is fairness.
Fairness assumptions rule out infinitebehaviors that are considered unrealistic, and are often necessary to establish livenessproperties. We illustrate the concept of fairness by means of a frequently encounteredproblem in concurrent systems.Example 3.40.Process FairnessConsider N processes P1 , .
. . , PN which require a certain service. There is one serverprocess Server that is expected to provide services to these processes. A possible strategythat Server can realize is the following. Check the processes starting with P1 , then P2 ,and so on, and serve the first thus encountered process that requires service. On finishingserving this process, repeat this selection procedure once again starting with checking P1 .Fairness127Now suppose that P1 is continuously requesting service. Then this strategy will resultin Server always serving P1 . Since in this way another process has to wait infinitelylong before being served, this is called an unfair strategy. In a fair serving strategy it isrequired that the server eventually responds to any request by any one of the processes.For instance, a round-robin scheduling strategy where each process is only served for alimited amount of time is a fair strategy: after having served one process, the next (in theround-robin order) is checked and, if needed, served.When verifying concurrent systems one is often only interested in paths in which enabledtransitions (statements) are executed in some “fair” manner.
Consider, for instance, amutual exclusion algorithm for two processes. In order to prove starvation freedom, thesituation in which a process that wants to enter its critical section has to wait infinitelylong, we want to exclude those paths in which the competitor process is always beingselected for execution. This type of fairness is also known as process fairness, since itconcerns the fair scheduling of the execution of processes. If we were to consider unfairpaths when proving starvation freedom, we would usually fail, since there always exists anunfair strategy according to which some process is always neglected, and thus can nevermake progress. One might argue that such unfair strategy is unrealistic and should beavoided.Example 3.41.Starvation FreedomConsider the transition systems TSSem and TSPet for the semaphore-based mutual exclusion algorithms (see Example 2.24 on page 43) and Peterson’s algorithm.
The starvationfreedom property“Once access is requested, a process does not have to wait infinitely long beforeacquiring access to its critical section”is violated by transition system TSSem while it permits only one of the processes to proceed, while the other process is starving (or only acquiring access to the critical sectionfinitely often). The transition system TSPet for Peterson’s algorithm, however, fulfills thisproperty.The property“Each of the processes is infinitely often in its critical section”is violated by both transition systems as none of them excludes the fact that a processwould never (or only finitely often) request to enter the critical section.128Linear-Time PropertiesProcess fairness is a particular form of fairness.
In general, fairness assumptions are neededto prove liveness or other properties stating that the system makes some progress (“something good will eventually happen”). This is of vital importance if the transition system tobe checked contains nondeterminism. Fairness is then concerned with resolving nondeterminism in such a way that it is not biased to consistently ignore a possible option. In theabove example, the scheduling of processes is nondeterministic: the choice of the next process to be executed (if there are at least two processes that can be potentially selected) isarbitrary. Another prominent example where fairness is used to “resolve” nondeterminismis in modeling concurrent processes by means of interleaving.
Interleaving is equivalent tomodeling the concurrent execution of two independent processes by enumerating all thepossible orders in which activities of the processes can be executed (see Chapter 2).Example 3.42.Independent Traffic LightsConsider the transition systemTS = TrLight1 ||| TrLight2for the two independent traffic lights described in Example 2.17 (page 36). The livenessproperty“Both traffic lights are infinitely often green”is not satisfied, since{ red1 , red2 } { green1 , red2 } { red1 , red2 } { green1 , red2 } .
. .is a trace of TS where only the first traffic light is infinitely often green.What is wrong with the above examples? In fact, nothing. Let us explain this. In thetraffic light example, the information whether each traffic light switches color infinitelyoften is lost by means of interleaving.
The trace in which only the first traffic light isacting while the second light seems to be completely stopped is formally a trace of thetransition system TrLight1 ||| TrLight2 . However, it does not represent a realistic behavioras in practice no traffic light is infinitely faster than another.For the semaphore-based mutual exclusion algorithm, the difficulty is the degree of abstraction. A semaphore is not a willful individual that arbitrarily chooses a process whichis authorized to enter its critical section.
Instead, the waiting processes are administeredin a queue (or another “fair” medium). The required liveness can be proven in one of thefollowing refinement steps, in which the specification of the behavior of the semaphore issufficiently detailed.Fairness3.5.1129Fairness ConstraintsThe above considerations show that we—to obtain a realistic picture of the behavior of aparallel system modeled by a transition system—need a more alleviated form of satisfactionrelation for LT properties, which implies an “adequate” resolution of the nondeterministicdecisions in a transition system. In order to rule out the unrealistic computations, fairnessconstraints are imposed.In general, a fair execution (or trace) is characterized by the fact that certain fairnessconstraints are fulfilled.
Fairness constraints are used to rule out computations that areconsidered to be unreasonable for the system under consideration. Fairness constraintscome in different flavors:• Unconditional fairness: e.g.,“Every process gets its turn infinitely often.”• Strong fairness: e.g., “Every process that is enabled infinitely often gets its turninfinitely often.”• Weak fairness: e.g., “Every process that is continuously enabled from a certain timeinstant on gets its turn infinitely often.”Here, the term “is enabled” has to be understood in the sense of “ready to execute (atransition)”.
Similarly, “gets its turn” stands for the execution of an arbitrary transition.This can, for example, be a noncritical action, acquiring a shared resource, an action inthe critical section, or a communication action.An execution fragment is unconditionally fair with respect to, e.g., “a process enters itscritical section” or “a process gets its turn”, if these properties hold infinitely often.
Thatis to say, a process enters its critical section infinitely often, or, in the second example,a process gets its turn infinitely often. Note that no condition (such as “a process isenabled”) is expressed that constrains the circumstances under which a process gets itsturn infinitely often. Unconditional fairness is sometimes referred to as impartiality.Strong fairness means that if an activity is infinitely often enabled—but not necessarilyalways, i.e., there may be finite periods during which the activity is not enabled—then itwill be executed infinitely often.
An execution fragment is strongly fair with respect toactivity α if it is not the case that α is infinitely often enabled without being taken beyonda certain point. Strong fairness is sometimes referred to as compassion.Weak fairness means that if an activity, e.g., a transition in a process or an entire process itself, is continuously enabled—no periods are allowed in which the activity is not130Linear-Time Propertiesenabled—then it has to be executed infinitely often. An execution fragment is weakly fairwith respect to some activity, α say, if it is not the case that α is always enabled beyondsome point without being taken beyond this point.
Weak fairness is sometimes referredto as justice.How to express these fairness constraints? There are different ways to formulate fairnessrequirements. In the sequel, we adopt the action-based view and define strong fairness for(sets of) actions. (In Chapter 5, also state-based notions of fairness will be introduced andthe relationship between action-based and state-based fairness is studied in detail.) Let Abe a set of actions. The execution fragment ρ is said to be strongly A-fair if the actions inA are not continuously ignored under the circumstance that they can be executed infinitelyoften.
ρ is unconditionally A-fair if some action in A is infinitely often executed in ρ. Weakfairness is defined in a similar way as strong fairness (see below).In order to formulate these fairness notions formally, the following auxiliary notion isconvenient. For state s, let Act(s) denote the set of actions that are executable in states, that is,α→ s }.Act(s) = {α ∈ Act | ∃s ∈ S. s −−Definition 3.43.Unconditional, Strong, and Weak FairnessFor transition system TS = (S, Act, →, I, AP, L) without terminal states, A ⊆ Act, andα0α1→ s1 −−→ . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
