## Finitary Fairness

*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 speeds of independent
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 demonstrated 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.

*Proceedings of the
Ninth Annual IEEE Symposium on Logic in Computer Science*
(LICS 1994), pp. 52-61.