On the Fairness of Schedulers

In appendix A.4, Tassarotti gives a definition of (weak) fairness in terms of diverging executions of thread pools. I will rephrase the definition here:

• A thread pool configuration is a list of expressions, denoting the evaluation state of each thread, and some shared state. A reduction step of a thread pool is indexed by the position \(i\) in the list of expressions: \[ (T, \sigma) \to_i (T', \sigma') \]
• A diverging execution is an infinite chain of reductions: \[ (T_0, \sigma_0) \to_{i_0} (T_1, \sigma_1) \to_{i_1} (T_2, \sigma_2) \to_{i_2} \to \dots \]
• A diverging execution is fair if for every thread \(i\), assuming there is a point \(t\) after which the thread pool configuration can always step, that there exists a \(t' > t\) in the diverging execution for which the evaluation steps: \[ (T_t', \sigma_t') \to_{t'} (T_{t'+1}, \sigma_{t'+1}) \]

Symbolically we express this as \[ \forall i \ldotp \underbrace{(\exists n\; \forall n' \geq n\; \exists (T', \sigma') \ldotp (T_n, \sigma_n) \to_i (T', \sigma'))}_{\text{Eventually always enabled}} \to \underbrace{(\forall n\; \exists n' \geq n \ldotp (T_n, \sigma_n) \to_i (T_{n+1}, \sigma_{n+1}))}_{\text{Eventually steps}} \]

Note that this definition is only interested in defining fairness of threads that do not terminate or get stuck. Furthermore, the implication does not say that if a thread can step in accordance to the fixed diverging execution that it will step. Instead the claim is more general, in that if from some point on a thread can make any kind of evaluation step, that the scheduler will select it to step.

The Rocq formalisation defines weak_fair in terms of a coinductive trace, much like the infinite chain of reductions given above. The definition is not given in terms of thread pool configurations, but a general relation.

Compared with the intuitive definition given above, this definition is weaker as we do not require every thread to always eventually step. This is sensible if dealing with stuck forms or in a normal form.

Quote section 4.1 (emphasis mine),

Moving to the case of a diverging program execution (denoted by ω), we crucially only consider fair infinite executions using the traditional definition of weak fairness [Lehmann et al. 1981]: an infinite execution of a thread pool is fair if every thread which is eventually always enabled does always eventually take a step. We consider a thread to be enabled when it can take a step […] Since Simuliris uses a non-blocking concurrency model, this notion off pairness is equivalent to saying: each thread will either terminate in a value or take infinitely many steps.

This definition ought to be equivalent to that used by Tassarotti, which does not come at a surprise as both reference Lehmann. The Rocq formalisation confirms this point:

Definition eventually_always_enabled {p T σ} i (f: div_exec p T σ)  :=
  ∃ m, ∀ n, m ≤ n → enabled p i ((f n).(pool)) ((f n).(state)).

Definition always_eventually_steps {p T σ} i (f: div_exec p T σ)  :=
  ∀ m, ∃ n, m ≤ n ∧ (f n).(id) = i.

Definition fair {p T σ} (f: div_exec p T σ) :=
  ∀ i, eventually_always_enabled i f → always_eventually_steps i f.

Lehmann et. al., approach fair execution in multiple steps:

1. A computation is finite if it reaches a point where no further transitions are possible.
2. A program is totally convergent if every computation is finite.
3. A program is impartial(ly convergent) if every impartial computation is finite.
   1. A computation is impartial if every thread is scheduled indefinitely often (or if is finite).
4. A program is just if every computation is just.
   1. A computation is just if every transition that is continuously enabled is taken indefinitely often (or is finite).

Lehmann's notion of "justice" matches Tassarotti and Gäher's notion of "(weak) fairness", as it is capable of dealing with expressions in formal form (continuously enabled).

Yet Tassarotti remarks (footnote 4):

This definition is simpler than the version found in Lehmann et al. [26], because there threads can be temporarily disabled, i.e., blocked and unable to take a step. In the languages we consider, threads can always take a step unless they have finished executing or have "gone wrong".

something bad cannot happen indefinitely without anything good occurring

where in the context of fairness properties, "something good" would be a scheduling event. Furthermore, scheduler fairness is described as

Scheduler fairness guarantees that every thread eventually gets scheduled infinitely often.

which is a consequence of the initial, intuitive definition.

Informally, Lee says a scheduler is fair if for any program, the set of concurrent behaviors are a subset of the behaviors of the same program executed by the non-deterministic, fair scheduler FairSch.

Fair Operational Semantics (FOS) defines the "fairness events" good and bad, where good must always occur after a finite number of bad steps. In the traces of observable behaviors, FAIR assertions ensure that execution paths where this condition does not hold are filtered out (or equivalently it backtracks to the previous non-deterministic choice-point).

Fairness events are used to define FairSch, which non-deterministically selects a thread \(n\) to execute and then asserts bad for all other threads \(n'\). As a consequence, every other thread has to be PICK'ed within a finite number of scheduler executions, to ensure that the trace doesn't contain an indefinite sequence of bad events for \(n'\).

It is noteworthy that Lee defines this notion of fairness within a new framework, but the consequence of the definition appears to coincide with the previous ones given above.

FOS is also the foundation of systems like Lilo, that therefore share the same definition of fairness.

It is also possible to define different kinds of fairness in terms of linear temporal logic. Based on Wahl's notes:

Absolute Fairness (Impartiality)

\(\forall t \ldotp \mathsf{G} \mathsf{F}\; \mathrm{execute}(t)\)

Strong Fairness

\(\forall t \ldotp (\mathsf{G}\mathsf{F}\; \mathrm{enabled}(t)) \implies (\mathsf{G}\mathsf{F}\; \mathrm{enabled}(t) \land \mathrm{execute}(t))\)

Weak Fairness

\(\forall t \ldotp (\mathsf{F}\mathsf{G}\; \mathrm{enabled}(t)) \implies (\mathsf{G}\mathsf{F}\; \mathrm{execute}(t))\)

Where recall, \(\mathsf{G} \phi\) means "globally \(\phi\) holds" (always) and \(\mathsf{F} \phi\) means "finally \(\phi\) holds" (eventually) and the predicates do not state anything regarding expressions or their reductions. A direct comparison to the previous definitions is therefore not possible, but intuitively the diverging execution from Tassarotti has now been embedded in the underlying Kripke structure.

In a general definition of liveness, of which fairness is an instance, Alpern and Schneider put forward a "most permissive" definition: For any set \(S\), \(S^\ast\) the finite sequences of \(S\) and \(S^\omega\) the infinite sequences of \(S\), \[ \forall \alpha \in S^\ast \exists \beta \in S^\omega \ldotp \alpha\beta \models P, \] where \(x \models P\) means that for some (possibly infinite) sequence \(x\) the property \(P\) holds — in our case fairness as defined above.