On the Impossibility of Maximal Scheduling for Strong Fairness with Interleaving

A strongly fair schedule is one in which tasks that are enabled infinitely often are also executed infinitely often. When tasks execute atomically, a strongly fair scheduler can be implemented in a maximal manner. That is, an algorithm exists that, for any valid schedule, is capable of generating that schedule. We show that this assumption of atomicity is necessary. That is, when task execution can be interleaved with other tasks, no algorithm is capable of generating all valid schedules. In other words, any algorithm that correctly generates some strongly fair schedules must also be incapable of generating some other valid schedules. This impossibility result is the first example of an implementable UNITY specification for which no maximal solution exists.