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.
For any given type of jobs...
... and any valid job arrival sequence.
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.
(∃ 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.
For any given type of jobs,...
...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.
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.
∃ 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.