Library rt.restructuring.analysis.edf.optimality
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.
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').
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').
End WeakOptimality.