Library rt.restructuring.analysis.edf.optimality
From rt.restructuring.model Require Export schedule.edf.
From rt.restructuring.analysis Require Import schedulability transform.facts.edf_opt.
From rt.restructuring.analysis Require Import schedulability transform.facts.edf_opt.
This file contains the theorem that states the famous EDF
optimality result: if there is any way to meet all deadlines
(assuming an ideal uniprocessor), then there is also an EDF
schedule in which all deadlines are met.
Section Optimality.
(* 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.
(* We observe that EDF is optimal in the sense that, if there exists
any schedule in which all jobs of arr_seq meet their deadline,
then there also exists an EDF schedule in which all deadlines are
met. *)
Theorem EDF_optimality:
(∃ any_sched : schedule (ideal.processor_state Job),
valid_schedule any_sched arr_seq ∧
all_deadlines_of_arrivals_met arr_seq any_sched) →
∃ edf_sched : schedule (ideal.processor_state Job),
valid_schedule edf_sched arr_seq ∧
all_deadlines_of_arrivals_met arr_seq edf_sched ∧
is_EDF_schedule edf_sched.
Proof.
move⇒ [sched [[COME [ARR COMP]] DL_ARR_MET]].
move: (all_deadlines_met_in_valid_schedule _ _ COME DL_ARR_MET) ⇒ DL_MET.
set sched' := edf_transform sched.
∃ sched'. split; last split.
- by apply edf_schedule_is_valid.
- by apply edf_schedule_meets_all_deadlines_wrt_arrivals.
- by apply edf_transform_ensures_edf.
Qed.
End Optimality.
We further state a weaker notion of the above optimality claim
that avoids a dependency on a given arrival sequence.
Section WeakOptimality.
(* For any given type of jobs,... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ...if we have a well-behaved schedule in which no deadlines are missed,... *)
Variable any_sched: schedule (ideal.processor_state Job).
Hypothesis H_must_arrive: jobs_must_arrive_to_execute any_sched.
Hypothesis H_completed_dont_execute: completed_jobs_dont_execute any_sched.
Hypothesis H_all_deadlines_met: all_deadlines_met any_sched.
(* ...then there also exists a corresponding EDF schedule in which
no deadlines are missed (and in which exactly the same set of
jobs is scheduled, as ensured by the last clause). *)
Theorem weak_EDF_optimality:
∃ edf_sched : schedule (ideal.processor_state Job),
jobs_must_arrive_to_execute edf_sched ∧
completed_jobs_dont_execute edf_sched ∧
all_deadlines_met edf_sched ∧
is_EDF_schedule edf_sched ∧
∀ j,
(∃ t, scheduled_at any_sched j t) ↔
(∃ t', scheduled_at edf_sched j t').
Proof.
set sched' := edf_transform any_sched.
∃ sched'. repeat split.
- by apply edf_transform_jobs_must_arrive.
- by apply edf_transform_completed_jobs_dont_execute.
- by apply edf_transform_deadlines_met.
- by apply edf_transform_ensures_edf.
- by move⇒ [t SCHED_j]; apply edf_transform_job_scheduled' with (t0 := t).
- by move⇒ [t SCHED_j]; apply edf_transform_job_scheduled with (t0 := t).
Qed.
End WeakOptimality.
(* For any given type of jobs,... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ...if we have a well-behaved schedule in which no deadlines are missed,... *)
Variable any_sched: schedule (ideal.processor_state Job).
Hypothesis H_must_arrive: jobs_must_arrive_to_execute any_sched.
Hypothesis H_completed_dont_execute: completed_jobs_dont_execute any_sched.
Hypothesis H_all_deadlines_met: all_deadlines_met any_sched.
(* ...then there also exists a corresponding EDF schedule in which
no deadlines are missed (and in which exactly the same set of
jobs is scheduled, as ensured by the last clause). *)
Theorem weak_EDF_optimality:
∃ edf_sched : schedule (ideal.processor_state Job),
jobs_must_arrive_to_execute edf_sched ∧
completed_jobs_dont_execute edf_sched ∧
all_deadlines_met edf_sched ∧
is_EDF_schedule edf_sched ∧
∀ j,
(∃ t, scheduled_at any_sched j t) ↔
(∃ t', scheduled_at edf_sched j t').
Proof.
set sched' := edf_transform any_sched.
∃ sched'. repeat split.
- by apply edf_transform_jobs_must_arrive.
- by apply edf_transform_completed_jobs_dont_execute.
- by apply edf_transform_deadlines_met.
- by apply edf_transform_ensures_edf.
- by move⇒ [t SCHED_j]; apply edf_transform_job_scheduled' with (t0 := t).
- by move⇒ [t SCHED_j]; apply edf_transform_job_scheduled with (t0 := t).
Qed.
End WeakOptimality.