# 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 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 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, 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.