5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 31
Текст из файла (страница 31)
The strong-fairness assumption{ { enter1 }, { enter2 } }indeed realizes the above requirement. This assumption should be viewed as a requirementon how to resolve the contention when both processes are awaiting to get access to thecritical section.Fairness assumptions can be verifiable properties whenever all infinite execution fragmentsare fair. For example, it can be verified that the transition system for Peterson’s algorithmFairness135satisfies the strong-fairness assumptionFstrong = { { enter1 }, { enter2 } }.But in many cases it is necessary to assume the validity of the fairness conditions to verifyliveness properties.A transition system TS satisfies the LT property P under fairness assumption F if allF-fair paths fulfill the property P .
However, no requirements whatsoever are imposed onthe unfair paths. This is formalized as follows.Definition 3.48.Fair Satisfaction Relation for LT PropertiesLet P be an LT property over AP and F a fairness assumption over Act. Transitionsystem TS = (S, Act, →, I, AP, L) fairly satisfies P , notation TS |=F P , if and only ifFairTracesF (TS) ⊆ P .For a transition system that satisfies the fairness assumption F (i.e., all paths are F-fair),the satisfaction relation |= without fairness assumptions (see Definition 3.11, page 100)corresponds with the fair satisfaction relation |=F . In this case, the fairness assumptiondoes not rule out any trace.
However, in case a transition system has traces that are notF-fair, then in general we are confronted with a situationTS |=F PwhereasTS |= P.By restricting the validity of a property to the set of fair paths, the verification can berestricted to “realistic” executions.Before turning to some examples, a few words on the relationship between unconditional,strong, and weak fairness are (again) in order.
As indicated before, we have that the setof unconditional A-fair executions is a subset of all strong A-fair executions. In a similarway, the latter set of executions is a subset of all weak A-fair executions. Stated differently, unconditional fairness rules out more behaviors than strong fairness, and strongexcludes more behaviors than weak fairness.
For F = { A1 , . . . , Ak }, let fairness assumption Fucond = (F, ∅, ∅), Fstrong = (∅, F, ∅), and Fweak = (∅, ∅, F). Then for anytransition system TS and LT property P it follows that:TS |=Fweak P ⇒ TS |=Fstrong P ⇒ TS |=Fucond P.136Linear-Time PropertiesExample 3.49.Independent Traffic LightsConsider again the independent traffic lights. Let action switch2green denote the switchingto green. Similarly switch2red denotes the switching to red. The fairness assumptionF = { { switch2green 1 , switch2red1 }, { switch2green 2 , switch2red2 } }expresses that both traffic lights infinitely often switch color.
In this case, it is irrelevantwhether strong, weak, or unconditional fairness is required.Note that in this example F is not a verifiable system property (as it is not guaranteedto hold), but a natural property which is satisfied for a practical implementation of thesystem (with two independent processors). Obviously,TrLight1 ||| TrLight2 |=F “each traffic light is green infinitely often”while the corresponding proposition for the nonfair relation |= is refuted.Example 3.50.Fairness for Mutual Exclusion AlgorithmsConsider again the semaphore-based mutual exclusion algorithm, and assume the fairnessassumption F consists ofFweak = {{ req1 }, { req2 }}andFstrong = {{ enter1 }, { enter 2 }}and Fucond = ∅.
The strong fairness constraint requires each process to enter its criticalsection infinitely often when it infinitely often gets the opportunity to do so. This does notforbid a process to never leave its noncritical section. To avoid this unrealistic scenario,the weak fairness constraint requires that any process infinitely often requests to enterthe critical section.
In order to do so, each process has to leave the noncritical sectioninfinitely often. It follows that TSSem |=F P where P stands for the property “everyprocess enters its critical section infinitely often”.Weak fairness is sufficient for request actions, as such actions are not critical: if reqi isexecutable in (global) state s, then it is executable in all direct successor states of s thatare reached by an action that differs from reqi .Peterson’s algorithm satisfies the strong fairness property“Every process that requests access to the critical sectionwill eventually be able to do so”.We can, however, not ensure that a process will ever leave its noncritical section andrequest the critical section.
That is, the property P is refuted. This can be “repaired”by imposing the weak fairness constraint Fweak = { { req1 }, { req2 } }. We now haveTSPet |=Fweak P .Fairness3.5.2137Fairness StrategiesThe examples in the previous section indicate that fairness assumptions may be necessaryto verify liveness properties of transition system TS. In order to rule out the “unrealistic”computations, fairness assumptions are imposed on the traces of TS, and it is checkedwhether TS |=F P as opposed to checking TS |= P (without fairness).
Which fairness assumptions are appropriate to check P ? Many model-checking tools provide the possibilityto work with built-in fairness assumptions. Roughly speaking, the intention is to rule outexecutions that cannot occur in a realistic implementation. But what does that exactlymean? In order to give some insight into this, we consider several fairness assumptions forsynchronizing concurrent systems. The aim is to establish a fair communication mechanism between the various processes involved. A rule of thumb is: Strong fairness is neededto obtain an adequate resolution of contentions (between processes), while weak fairnesssuffices for sets of actions that represent the concurrent execution of independent actions(i.e., interleaving).For modeling asynchronous concurrency by means of transition systems, the following ruleof thumb can be adopted:concurrency =Example 3.51.interleaving (i.e., nondeterminism) + fairnessFair Concurrency with SynchronizationConsider the concurrent transition system:TS = TS1 TS2 .
. . TSn,where TSi = (Si , Acti , →i , Ii , APi , Li ), for 1 i n, is a transition system withoutterminal states. Recall that each pair of processes TSi and TSj (for i=j) has to synchronizeon their common sets of actions, i.e., Syni,j = Acti ∩ Actj . It is assumed that Syni,j ∩Actk = ∅ for any k = i, j.
For simplicity, it is assumed that TS has no terminal states.(In case there are terminal states, each finite execution is considered to be fair.)We consider several fairness assumptions on the transition system TS. First, consider thestrong fairness assumption{Act1 , Act2 , . . . , Actn }which ensures that each transition system TSi executes an action infinitely often, providedthe composite system TS is infinitely often in a (global) state with a transition beingexecutable in which TSi participates. This fairness assumption, however, cannot ensurethat a communication will ever occur—it is possible for each TSi to only execute localactions ad infinitum.138Linear-Time PropertiesIn order to force a synchronization to take place every now and then, the strong fairnessassumption{ { α } | α ∈ Syni,j , 0 < i < j n }(3.1)could be imposed.
It forces every synchronization action to happen infinitely often. Alternatively, a somewhat weaker fairness assumption can be imposed by requiring every pair ofprocesses to synchronize—regardless of the synchronization action—infinitely often. Thecorresponding strong fairness assumption is{ Syni,j | 0 < i < j n }.(3.2)Whereas (3.2) allows processes to always synchronize on the same action, (3.1) does notpermit this. The strong fairness assumption:Syni,j }{0<i<jngoes even one step further as it only requires a synchronization to take place infinitelyoften, regardless of the process involved. This fairness assumption does not rule outexecutions in which always the same synchronization takes place or in which always thesame pair of processes synchronizes.Note that all fairness assumptions in this example so far are strong.
This requires thatinfinitely often a synchronization is enabled. As the constituting transition systems TSimay execute internal actions, synchronizations are not continuously enabled, and henceweak fairness is in general inappropriate.If the internal actions should be fairly considered, too, then we may use, e.g., the strongfairness assumption{ Act1 \ Syn1 , .
. . , Actn \ Synn } ∪ { { α } | α ∈ Syn },=where Synij=i Syni,j denotes the set of all synchronization actions of TSi andSyn = i Syni .Under the assumption that in every (local) state either only internal actions or onlysynchronization actions are executable, it suffices to impose the weak fairness constraint{ Act1 \ Syn1 , . . . , Actn \ Synn }.Weak fairness is appropriate for the internal actions α ∈ Acti \ Syni , as the ability toperform an internal action is preserved until it will be executed.Fairness139As an example of another form of fairness we consider the following sequential hardwarecircuit.Example 3.52.Circuit FairnessFor sequential circuits we have modeled the environmental behavior, which provides theinput bits, by means of nondeterminism.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
