Library prosa.analysis.facts.transform.edf_wc

Require Import prosa.model.readiness.basic.
Require Export prosa.analysis.facts.transform.edf_opt.
Require Export prosa.analysis.facts.transform.wc_correctness.
Require Export prosa.analysis.facts.behavior.deadlines.
Require Export prosa.analysis.facts.readiness.backlogged.

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.

Section NonIdleSwapWorkConservationLemmas.

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

#[local] Existing Instance basic_ready_instance.

For any given type of jobs...

Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.

... and any valid job arrival sequence.

Variable arr_seq: arrival_sequence Job.
Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.

...consider an ideal uniprocessor schedule...

Variable sched: schedule (ideal.processor_state Job).

...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).

  Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
  Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
  Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.

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

Variables t1 t2 : instant.

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

Hypothesis H_well_ordered: t1 ≤ t2.

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

Variables j1 j2 : Job.

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

Hypothesis H_arrival_j2 : job_arrival j2 ≤ t1.

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

Hypothesis H_t1_not_idle : scheduled_at sched j1 t1.

...j2 is scheduled at time t2.

Hypothesis H_t2_not_idle : scheduled_at sched j2 t2.

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

Let swap_sched := swapped sched t1 t2.

Now consider an arbitrary job j...

Variable j : Job.

...and an arbitrary instant t...

Variable t : instant.

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

Hypothesis H_arrival_j : arrives_in arr_seq j.

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

Hypothesis H_backlogged_j_t : backlogged swap_sched j 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

  Lemma non_idle_swap_maintains_work_conservation_t1 :
    work_conserving arr_seq sched →
    t = t1 →
    ∃ j_other , scheduled_at swap_sched j_other t.

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

  Lemma non_idle_swap_maintains_work_conservation_t2 :
    work_conserving arr_seq sched →
    t = t2 →
    ∃ j_other , scheduled_at swap_sched j_other t.

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

  Lemma non_idle_swap_maintains_work_conservation_LEQ_t1 :
    work_conserving arr_seq sched →
    t ≤ t1 →
    ∃ j_other , scheduled_at swap_sched j_other t.

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

  Lemma non_idle_swap_maintains_work_conservation_GT_t2 :
    work_conserving arr_seq sched →
    t2 < t →
    ∃ j_other , scheduled_at swap_sched j_other t.

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

  Lemma non_idle_swap_maintains_work_conservation_BET_t1_t2 :
    work_conserving arr_seq sched →
    t1 < t ≤ t2 →
    ∃ j_other , scheduled_at swap_sched j_other t.

End NonIdleSwapWorkConservationLemmas.

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.

Section FSCWorkConservationLemmas.

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

#[local] Existing Instance basic_ready_instance.

For any given type of jobs...

Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.

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

Variable arr_seq: arrival_sequence Job.
Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.

...consider an ideal uniprocessor schedule...

Variable sched: schedule (ideal.processor_state Job).

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

Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

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

Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.

Suppose we are given a job j1...

Variable j1: Job.

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

Variable t1: instant.

...at which j1 is scheduled...

Hypothesis H_not_idle: scheduled_at sched j1 t1.

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

Hypothesis H_deadline_not_missed: t1 < job_deadline j1.

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.

  Corollary fsc_swap_maintains_work_conservation :
    work_conserving arr_seq sched →
    work_conserving arr_seq (swapped sched t1 (edf_trans.find_swap_candidate sched t1 j1)).

End FSCWorkConservationLemmas.

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.

Section MakeEDFWorkConservationLemmas.

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

#[local] Existing Instance basic_ready_instance.

For any given type of jobs...

Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.

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

Variable arr_seq: arrival_sequence Job.
Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.

... consider an ideal uniprocessor schedule ...

Variable sched: schedule (ideal.processor_state Job).

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

Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.

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

Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

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

Hypothesis H_no_deadline_misses: all_deadlines_met sched.

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

Variable t_edf: instant.

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

Let sched' := make_edf_at sched 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.

Lemma mea_maintains_work_conservation :
work_conserving arr_seq sched → work_conserving arr_seq sched'.

End MakeEDFWorkConservationLemmas.

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

Section EDFPrefixWorkConservationLemmas.

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

#[local] Existing Instance basic_ready_instance.

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

Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.

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

Variable arr_seq: arrival_sequence Job.
Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.

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

Variable sched: schedule (ideal.processor_state Job).

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

Variable horizon: instant.

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

Let sched_trans := edf_transform_prefix sched 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

  Definition scheduled_behavior_premises (sched : schedule (processor_state Job)) :=
    jobs_must_arrive_to_execute sched
    ∧ completed_jobs_dont_execute sched
    ∧ jobs_come_from_arrival_sequence sched arr_seq
    ∧ all_deadlines_met sched.

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

Let P (sched : schedule (processor_state Job)) :=
scheduled_behavior_premises sched ∧ work_conserving arr_seq sched.

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

Lemma edf_transform_prefix_maintains_work_conservation:
P sched → P sched_trans.

End EDFPrefixWorkConservationLemmas.

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.

Section EDFTransformWorkConservationLemmas.

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

#[local] Existing Instance basic_ready_instance.

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

Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.

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

Variable arr_seq: arrival_sequence Job.
Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.

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

Variable sched: schedule (ideal.processor_state Job).
Hypothesis H_sched_valid: valid_schedule sched arr_seq.

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

Hypothesis H_no_deadline_misses: all_deadlines_met sched.

We first note that sched satisfies scheduled_behavior_premises.

Lemma sched_satisfies_behavior_premises : scheduled_behavior_premises arr_seq sched.

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.

Lemma edf_transform_maintains_work_conservation :
work_conserving arr_seq sched → work_conserving arr_seq (edf_transform sched).

End EDFTransformWorkConservationLemmas.