Connecting the General Result to the Model in the Paper

In the following, we instantiate the general transfer schedulability result for a system model that more closely resembles the system model defined in the paper by Willemsen et al. (EMSOFT 2025, DOI: 10.1145/3763236). In particular, we explicitly introduce the notion of system evolutions, which are usually left implicit in Prosa.

Elements of the EMSOFT'25 System Model

We first define the key notions that refine the model in the paper relative to the more abstract one in the main proof of transfer schedulability:

• job precedence and delay constraints,
• system evolutions, and
• a notion of schedulers.

Precedence and Delay

We introduce a readiness model that matches the model assumed in the paper: jobs have predecessors and may be scheduled (i.e., become ready) only after a predecessor-dependent delay has passed.

Job Parameters

We introduce two new job parameters that model, for each job, the set of predecessors and the associated delays. The list of a job j's predecessors is given by job_predecessors j.

The delay that must pass between when a job j is first scheduled and the completion of a predecessor j' is given by job_delay j j'.

Definition of Job Readiness

Based on the above two job parameters, we can precisely define the assumed precedence constraints in terms of a readiness model, which is a standard Prosa interface.

Consider any kind of jobs...

... and any kind of processor state.

Suppose jobs have an arrival time, a cost, a set of predecessors, and predecessor-specific release delays.

For a given predecessor j_pred of a job j, we say the delay has passed at time t if j_pred completed at least job_delay j j_pred time units earlier.

We say that a job j is released at a time t after its arrival if the delay has passed w.r.t. each predecessor.

A job j is hence ready to be scheduled at time t if and only if it is released and not yet complete.

System Evolutions

Next, we introduce the notion of system evolutions that determine each job's cost and delay parameters. Given an arbitrary type of evolutions Omega, ...

... the job costs in an evolution omega : Omega are given by evo_costs omega and ...

... the delays are given by evo_delays omega.

Scheduler Interface

Finally, we introduce the notion of a scheduling algorithm.

Allowing for any type of system evolutions Omega, ...

... any kind of jobs, ...

... and any kind of processor model, ...

... a scheduler is a function that, given each job's arrival time, predecessors, and an evolution omega, yields a schedule of the jobs.

Instantiation of the EMSOFT'25 System Model

With all basic elements defined, we can state the transfer schedulability results in terms of the system model assumed in the paper.

The Set of Jobs

We consider jobs described by evolution-independent arrival times and predecessor sets, ...

... which arrive according to the arrival sequence arr_seq.

Ideal Uniprocessor Assumption

We consider ideal uniprocessor schedules.

System Evolutions

Let Omega denote the set of all system evolutions.

For clarity, we introduce the following abbreviations:

• job_cost omega j denotes the cost of job j in evolution omega.

• job_delay omega j j' denotes the delay between jobs j and its predecessor j' in evolution omega.

• job_ready omega denotes the readiness model resulting from job_delay omega and the evolution-invariant predecessor sets.

Worst-Case Reference Evolution Let omega_0 denote the system evolution with maximal parameters, ...

... that is, the job costs in omega_0 upper-bound the costs in any other evolution, ...

... and the delays in omega_0 similarly upper-bound the delays in any other evolution.

The Schedulers

Suppose we are given two scheduling algorithms algA and algB.

As discussed in the paper, we restrict our attention to schedulers that always produce well-formed schedules.

For brevity, recall the notion of schedulability_transferred. We specialize the definition such that algA omega_0 is the reference schedule and algB omega the online schedule.

Clairvoyant Results

We are now ready to state the results pertaining to clairvoyant scheduling algorithms. First, recall the transfer_schedulability_criterion as applied to clairvoyant schedulers.

For any evolution omega, the criterion is assumed to hold ...

... for the reference schedule algA omega_0 and the online schedule algB omega ...

... w.r.t. the respective job costs ...

... for the given, fixed job arrival times ...

with regard to online job costs. This last parameter is the "clairvoyant" part.

The above clairvoyant criterion ensures that schedulability is transferred in every evolution.

Conversely, the fact that schedulability is transferred in every evolution implies that the above criterion holds.

Non-Clairvoyant Result

Finally, we state the sufficiency result for non-clairvoyant schedulers. As above, we recall the transfer schedulability criterion, this time instantiated for reference costs job_cost omega_0 (again, note the last parameter).

Assuming the above criterion holds, schedulability is transferred in all evolutions.

Results w.r.t. Finish Times

The results stated above are stated w.r.t. Prosa's standard completed_by predicate, which tests whether or not a job is finished at a given time (and in a given schedule) by comparing the total amount of service received so far with the job's cost. The advantage of Prosa's completed_by predicate is that it is always applicable, even if some jobs never finish (i.e., are starved). It does not, however, yield the job's finish time, which is the earliest time at which the completed_by predicate holds, and which consequently is defined only in starvation-free schedules. In the following, we re-state the above theorems in terms of finish times under the strengthened assumption that we are indeed looking at starvation-free schedules. We begin with the two sufficiency theorems.

Non-Starvation Assumption

For convenience, to match Prosa's existing definitions, we state the non-starvation assumption in terms of the existence of some finite response-time bound for every job in the arrival sequence. First, we assume non-starvation only for the reference schedule algA omega_0. The following notation means that there exists a bound R for each job j in the arrival sequence such that j completes within R time units of its arrival (in the reference schedule).

Definition of Finish Times

With the non-starvation assumption in place, we can start reasoning about finish times. Let us recall the relevant definitions from Prosa.

In the context of a given evolution omega ...

... and for a given, certainly finishing job jf that is part of the arrival sequence arr_seq, ...

... we exploit the non-starvation assumption ...

... to define jf's finish time in the reference schedule algA omega_0.

To define the finish time in the online schedule, we need to put in a little more legwork, since the non-starvation assumption above applies only to the reference schedule, but not to the online schedule. To this end, assume that schedulability is transferred from algA omega_0 to algB omega.

Under this assumption, R is of course also a response-time bound w.r.t. the online schedule.

Having established that the online schedule is starvation-free, too, we can recall the finish time in algB omega, too.

With the finish times in place for both schedules, we can state the property that we're after: the finish time in the online schedule is no later than in the reference schedule.

Clairvoyant Sufficiency Result for Finish Times

With the above setup in place, we can easily re-state the clairvoyant_sufficiency theorem in terms of finish times.

Under the assumption that the schedulability transfer criterion holds w.r.t. online job costs, ...

... the finish time of any job (that is part of the arrival sequence) in any online schedule is no later than in the reference schedule.

Before moving on to the necessity argument for the clairvoyant case, which will require further assumptions and legwork, we first quickly dispatch the sufficiency argument in the case of non-clairvoyant schedulers.

Non-Clairvoyant Sufficiency Result for Finish Times

The sufficiency claim for non-clairvoyant schedulers follows virtually identically to the above theorem since the underlying argument is the same.

Under the assumption that the schedulability transfer criterion holds w.r.t. reference job costs, ...

... the finish time of any job (that is part of the arrival sequence) in any online schedule is no later than in the reference schedule.

Clairvoyant Necessity Result for Finish Times

For the necessity case, we need to strengthen our non-starvation assumption to also cover any online schedule. We again express this assumption in terms of the existence of a finite response-time bound for every job in all online schedules.

Online Finish Times, Revisited

Based on the above non-starvation assumption, we can refer to the completion time in the online schedule directly.

In the context of a given evolution omega ...

... and for a given, certainly finishing job jf that is part of the arrival sequence arr_seq, ...

... we exploit the non-starvation assumption ...

... to define j's finish time in the online schedule algB omega.

Using this notion of j's online finish time, we can re-state that it finishes no later in the online schedule than in the reference schedule.

Clairvoyant Necessity Theorem

Finally, we are in a position to state the necessity result w.r.t. finish times.

Under the assumption that, for any job that arrives in the arrival sequence, the finish time in any online schedule is no later than in the reference schedule, ...

... we can show that the transfer schedulability criterion w.r.t. online job costs holds.