*Rajeev Alur and
Thomas A. Henzinger*

Fairness is a mathematical abstraction:
in a multiprogramming environment, fairness abstracts the details of
admissible ("fair") schedulers;
in a distributed environment, fairness abstracts the relative speeds of
processors.
We argue that the standard definition of fairness often is unnecessarily weak
and can be replaced by the stronger, yet still abstract, notion of finitary
fairness.
While standard weak fairness requires that no enabled transition is postponed
forever, finitary weak fairness requires that for every run of a system there
is an unknown bound *k* such that no enabled transition is postponed
more than *k* consecutive times.
In general, the *finitary restriction fin(F)* of any given fairness
assumption *F* is the union of all omega-regular safety properties that
are contained in *F*.

The adequacy of the proposed abstraction is shown in two ways. Suppose that we prove a program property under the assumption of finitary fairness. In a multiprogramming environment, the program then satisfies the property for all fair finite-state schedulers. In a distributed environment, the program then satisfies the property for all choices of lower and upper bounds on the speeds (or timings) of processors.

The benefits of finitary fairness are twofold. First, the proof rules for verifying liveness properties of concurrent programs are simplified: well-founded induction over the natural numbers is adequate for proving termination under finitary fairness. Second, the fundamental problem of consensus in a faulty asynchronous distributed environment can be solved assuming finitary fairness.

*ACM Transactions on Programming Languages and Systems*
20:1171-1194, 1998.
A preliminary version appeared in the
*Proceedings of the
Ninth Annual IEEE Symposium on Logic in Computer Science*
(LICS), IEEE Computer Society Press, 1994, pp. 52-61.

Download inofficial, sometimes updated PostScript / PDF document. © 1994 IEEE, 1998 ACM.