# 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.
Proof.
move⇒ _ EQ; rewrite EQ; by ∃ j2; rewrite swap_job_scheduled_t1.
Qed.
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.
Proof.
move⇒ _ EQ; rewrite EQ; by ∃ j1; rewrite swap_job_scheduled_t2.
Qed.
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.
Proof.
move⇒ WC_sched LEQ.
case: (boolP(t == t1)) ⇒ [/eqP EQ| /eqP NEQ]; first by apply non_idle_swap_maintains_work_conservation_t1.
case: (boolP(t == t2)) ⇒ [/eqP EQ'| /eqP NEQ']; first by apply non_idle_swap_maintains_work_conservation_t2.
have [j_other j_other_scheduled] : ∃ j_other, scheduled_at sched j_other t.
{ rewrite /work_conserving in WC_sched. apply (WC_sched j) ⇒ //; move :H_backlogged_j_t.
rewrite /backlogged/job_ready/basic_ready_instance/pending/completed_by.
move /andP ⇒ [ARR_INCOMP scheduled]; move :ARR_INCOMP; move /andP ⇒ [arrive not_comp].
apply /andP; split; first (apply /andP; split) ⇒ //.
+ by rewrite (service_before_swap_invariant sched t1 t2 _ t).
+ by rewrite -(swap_job_scheduled_other_times _ t1 t2 j t) //; (apply /neqP; eauto).
}
∃ j_other; by rewrite (swap_job_scheduled_other_times) //; do 2! (apply /neqP; eauto).
Qed.
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.
Proof.
move⇒ WC_sched GT.
case: (boolP(t == t1)) ⇒ [/eqP EQ| /eqP NEQ]; first by apply non_idle_swap_maintains_work_conservation_t1.
case: (boolP(t == t2)) ⇒ [/eqP EQ'| /eqP NEQ']; first by apply non_idle_swap_maintains_work_conservation_t2.
have [j_other j_other_scheduled] : ∃ j_other, scheduled_at sched j_other t.
{ rewrite /work_conserving in WC_sched. apply (WC_sched j) ⇒ //; move :H_backlogged_j_t.
rewrite /backlogged/job_ready/basic_ready_instance/pending/completed_by.
move /andP ⇒ [ARR_INCOMP scheduled]; move :ARR_INCOMP; move /andP ⇒ [arrive not_comp].
apply /andP; split; first (apply /andP; split) ⇒ //.
+ by rewrite (service_after_swap_invariant sched t1 t2 _ t) // /t2; apply fsc_range1.
+ by rewrite -(swap_job_scheduled_other_times _ t1 t2 j t) //; (apply /neqP; eauto).
}
∃ j_other; by rewrite (swap_job_scheduled_other_times) //; do 2! (apply /neqP; eauto).
Qed.
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.
Proof.
move⇒ WC_sched H_range.
case: (boolP(t == t1)) ⇒ [/eqP EQ| /eqP NEQ]; first by apply non_idle_swap_maintains_work_conservation_t1.
case: (boolP(t == t2)) ⇒ [/eqP EQ'| /eqP NEQ']; first by apply non_idle_swap_maintains_work_conservation_t2.
move: H_range. move /andP ⇒ [LT GE].
case: (boolP(scheduled_at sched j2 t)) ⇒ Hj'.
- ∃ j2; by rewrite (swap_job_scheduled_other_times _ t1 t2 j2 t) //; (apply /neqP; eauto).
- have [j_other j_other_scheduled] : ∃ j_other, scheduled_at sched j_other t.
{ rewrite /work_conserving in WC_sched. apply (WC_sched j2).
- by unfold jobs_come_from_arrival_sequence in H_from_arr_seq; apply (H_from_arr_seq _ t2) ⇒ //.
- rewrite/backlogged/job_ready/basic_ready_instance/pending/completed_by.
apply /andP; split⇒ [|//]; apply /andP; split⇒ //.
+ by rewrite /has_arrived; apply (leq_trans H_arrival_j2); apply ltnW.
+ rewrite -ltnNge. apply (leq_ltn_trans) with (service sched j2 t2).
× exact: service_monotonic.
× exact: H_completed_jobs_dont_execute. }
by ∃ j_other; rewrite swap_job_scheduled_other_times//; apply /neqP.
Qed.
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)).
Proof.
set t2 := edf_trans.find_swap_candidate sched t1 j1.
have [j2 [t2_not_idle t2_arrival]] : ∃ j2, scheduled_at sched j2 t2 ∧ job_arrival j2 ≤ t1
by apply fsc_not_idle.
have H_range : t1 ≤ t2 by apply fsc_range1.
move⇒ WC_sched j t ARR BL.
case: (boolP(t == t1)) ⇒ [/eqP EQ| /eqP NEQ].
- by apply (non_idle_swap_maintains_work_conservation_t1 arr_seq _ _ _ j2).
- case: (boolP(t == t2)) ⇒ [/eqP EQ'| /eqP NEQ'].
+ by apply (non_idle_swap_maintains_work_conservation_t2 arr_seq _ _ _ j1).
+ case: (boolP((t ≤ t1) || (t2 < t))) ⇒ [NOT_BET | BET]. (* t <> t2 *)
× move: NOT_BET; move/orP ⇒ [] ⇒ NOT_BET.
{ by apply (non_idle_swap_maintains_work_conservation_LEQ_t1 arr_seq _ _ _ H_range _ _ H_not_idle t2_not_idle j). }
{ by apply (non_idle_swap_maintains_work_conservation_GT_t2 arr_seq _ _ _ H_range _ _ H_not_idle t2_not_idle j). }
× move: BET; rewrite negb_or. move /andP. case; rewrite <- ltnNge ⇒ range1; rewrite <- leqNgt ⇒ range2.
have BET: (t1 < t) && (t ≤ t2) by apply /andP.
now apply (non_idle_swap_maintains_work_conservation_BET_t1_t2 arr_seq _ H_completed_jobs_dont_execute H_from_arr_seq _ _ _ _ t2_arrival H_not_idle t2_not_idle ).
Qed.
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'.
Proof.
rewrite /sched'/make_edf_at ⇒ WC_sched. destruct (sched t_edf) as [s|] eqn:E ⇒ //.
apply fsc_swap_maintains_work_conservation ⇒ //.
- by rewrite scheduled_at_def; apply /eqP ⇒ //.
- apply (scheduled_at_implies_later_deadline sched) ⇒ //.
+ rewrite /all_deadlines_met in (H_no_deadline_misses).
now apply (H_no_deadline_misses s t_edf); rewrite scheduled_at_def; apply /eqP.
+ by rewrite scheduled_at_def; apply/eqP ⇒ //.
Qed.
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.
Proof.
rewrite/sched_trans/edf_transform_prefix. apply (prefix_map_property_invariance ). rewrite /P.
move⇒ sched' t [[H_ARR [H_COMPLETED [H_COME H_all_deadlines_met]]] H_wc_sched].
rewrite/scheduled_behavior_premises/valid_schedule; split; first split.
- by apply mea_jobs_must_arrive.
- split; last split.
+ by apply mea_completed_jobs.
+ by apply mea_jobs_come_from_arrival_sequence.
+ by apply mea_no_deadline_misses.
- by apply mea_maintains_work_conservation.
Qed.
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.
Proof.
split; [ apply (jobs_must_arrive_to_be_ready sched) | split; [ apply (completed_jobs_are_not_ready sched) | split]].
all: by try apply H_sched_valid.
Qed.
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).
Proof.
move⇒ WC_sched j t ARR.
set sched_edf := edf_transform sched.
have IDENT: identical_prefix sched_edf (edf_transform_prefix sched t.+1) t.+1
by rewrite /sched_edf/edf_transform ⇒ t' LE_t; apply (edf_prefix_inclusion) ⇒ //; apply sched_satisfies_behavior_premises.
rewrite (backlogged_prefix_invariance _ _ (edf_transform_prefix sched t.+1) t.+1) // ⇒ BL;
last by apply basic_readiness_nonclairvoyance.
have WC_trans: work_conserving arr_seq (edf_transform_prefix sched (succn t))
by apply edf_transform_prefix_maintains_work_conservation; split ⇒ //; apply sched_satisfies_behavior_premises.
move: (WC_trans _ _ ARR BL) ⇒ [j_other SCHED_AT].
∃ j_other.
now rewrite (identical_prefix_scheduled_at _ (edf_transform_prefix sched t.+1) t.+1) //.
Qed.
End EDFTransformWorkConservationLemmas.