Optimality of Work-Conserving EDF on Ideal Uniprocessors

In this file, we establish the foundation needed to connect the EDF and work-conservation optimality theorems: if there is any work-conserving way to meet all deadlines (assuming an ideal uniprocessor schedule), then there is also an (ideal) EDF schedule that is work-conserving in which all deadlines are met.

Non-Idle Swaps

We start by showing that swapped, a function used in the inner-most level of edf_transform, maintains work conservation if the two instants being swapped are not idle.

For any given type of jobs...

... following the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready, ...

... and any valid job arrival sequence, ...

...consider an ideal uniprocessor schedule...

...that is well-behaved (i.e., in which jobs execute only after having arrived and only if they are not yet complete, and in which all jobs come from the arrival sequence).

Suppose we are given two specific times t1 and t2,...

...which we assume to be ordered (to avoid dealing with symmetric cases),...

...and two jobs j1 and j2...

...such that j2 arrives before time t1,...

...j1 is scheduled at time t1, and...

...j2 is scheduled at time t2.

We let swap_sched denote the schedule in which the allocations at t1 and t2 have been swapped.

Now consider an arbitrary job j...

...and an arbitrary instant t...

...such that j arrives in arr_seq...

...and is backlogged in swap_sched at instant t.

We proceed by case analysis. We first show that, if t equals t1, then swap_sched maintains work conservation. That is, there exists some job that's scheduled in swap_sched at instant t

Similarly, if t equals t2, then swap_sched maintains work conservation.

If t is less than or equal to t1, then swap_sched maintains work conservation.

Similarly, if t is greater than t2, swap_sched maintains work conservation.

Lastly, we show that if t lies between t1 and t2 then work conservation is still maintained.

Work-Conserving Swap Candidates

Now, we show that work conservation is maintained by the inner-most level of edf_transform, which is find_swap_candidate.

For any given type of jobs...

... following the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready, ...

...and any valid job arrival sequence,...

...consider an ideal uniprocessor schedule...

...that is well-behaved (i.e., in which jobs execute only after having arrived and only if they are not yet complete)...

...and in which all jobs come from the arrival sequence.

Suppose we are given a job j1...

...and a point in time t1...

...at which j1 is scheduled...

...and that is before j1's deadline.

We now show that, if t2 is a swap candidate returned by find_swap_candidate for t1, then swapping the processor allocations at the two instants maintains work conservation.

Work-Conservation of the Point-Wise EDF Transformation

In the following section, we show that work conservation is maintained by the next level of edf_transform, which is make_edf_at.

For any given type of jobs...

... following the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready, ...

... and any valid job arrival sequence, ...

... consider an ideal uniprocessor schedule ...

... in which all jobs come from the arrival sequence, ...

...that is well-behaved,...

...and in which no scheduled job misses a deadline.

We analyze make_edf_at applied to an arbitrary point in time, which we denote t_edf in the following.

For brevity, let sched' denote the schedule obtained from make_edf_at applied to sched at time t_edf.

We show that, if a schedule is work-conserving, then applying make_edf_at to it at an arbitrary instant t_edf maintains work conservation.

Work-Conserving EDF Prefix

On to the next layer, we prove that the transform_prefix function at the core of the EDF transformation maintains work conservation

For any given type of jobs, each characterized by execution costs, an arrival time, and an absolute deadline,...

... following the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready, ...

... and any valid job arrival sequence, ...

... consider an ideal uniprocessor schedule,...

... an arbitrary finite horizon, and ...

...let sched_trans denote the schedule obtained by transforming sched up to the horizon.

Let schedule_behavior_premises define the premise that a schedule is: 1) well-behaved, 2) has all jobs coming from the arrival sequence arr_seq, and 3) in which no scheduled job misses its deadline

For brevity, let P denote the predicate that a schedule satisfies scheduled_behavior_premises and is work-conserving.

We show that if sched is work-conserving, then so is sched_trans.

Work-Conservation of the EDF Transformation

Finally, having established that edf_transform_prefix maintains work conservation, we go ahead and prove that edf_transform maintains work conservation, too.

For any given type of jobs, each characterized by execution costs, an arrival time, and an absolute deadline,...

... following the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready, ...

... and any valid job arrival sequence, ...

... consider a valid ideal uniprocessor schedule ...

...and in which no scheduled job misses a deadline.

We first note that sched satisfies scheduled_behavior_premises.

We prove that, if the given schedule sched is work-conserving, then the schedule that results from transforming it into an EDF schedule is also work-conserving.