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

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

## Non-Idle Swaps

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

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

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.

Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.

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

Now consider an arbitrary job j...

...and an arbitrary instant t...

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

Lemma non_idle_swap_maintains_work_conservation_t1 :

work_conserving arr_seq sched →

t = t1 →

∃ j_other, scheduled_at swap_sched j_other t.

work_conserving arr_seq sched →

t = t1 →

∃ j_other, scheduled_at swap_sched j_other t.

Lemma non_idle_swap_maintains_work_conservation_t2 :

work_conserving arr_seq sched →

t = t2 →

∃ j_other, scheduled_at swap_sched j_other t.

work_conserving arr_seq sched →

t = t2 →

∃ j_other, scheduled_at swap_sched j_other t.

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.

work_conserving arr_seq sched →

t ≤ t1 →

∃ j_other, scheduled_at swap_sched j_other t.

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.

work_conserving arr_seq sched →

t2 < t →

∃ j_other, scheduled_at swap_sched j_other t.

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 arr_seq sched →

t1 < t ≤ t2 →

∃ j_other, scheduled_at swap_sched j_other t.

End NonIdleSwapWorkConservationLemmas.

## Work-Conserving Swap Candidates

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

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

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_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

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

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_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

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

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

... consider an ideal uniprocessor schedule ...

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

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

Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

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

Lemma mea_maintains_work_conservation :

work_conserving arr_seq sched → work_conserving arr_seq sched'.

End MakeEDFWorkConservationLemmas.

work_conserving arr_seq sched → work_conserving arr_seq sched'.

End MakeEDFWorkConservationLemmas.

## Work-Conserving EDF Prefix

#[local] Existing Instance basic_ready_instance.

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

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

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.

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.

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.

P sched → P sched_trans.

End EDFPrefixWorkConservationLemmas.

## Work-Conservation of the EDF Transformation

#[local] Existing Instance basic_ready_instance.

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

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

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

Variable sched: schedule (ideal.processor_state Job).

Hypothesis H_sched_valid: valid_schedule sched arr_seq.

Hypothesis H_sched_valid: valid_schedule sched arr_seq.

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