Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Import prosa.model.readiness.basic.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Import prosa.model.preemption.fully_preemptive.
Require Export prosa.analysis.facts.transform.edf_opt.
Require Export prosa.analysis.facts.transform.edf_wc.
Require Export prosa.analysis.facts.edf_definitions.
Require prosa.model.priority.edf.
(** * Optimality of EDF on Ideal Uniprocessors *)
(** This module provides the famous EDF optimality theorem: if there
is any way to meet all deadlines (assuming an ideal uniprocessor
schedule), then there is also an (ideal) EDF schedule in which all
deadlines are met. *)
(** ** Optimality Theorem *)
Section Optimality .
(** Consider 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 arrival sequence of such jobs. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arr_seq_valid : valid_arrival_sequence arr_seq.
(** 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 .
(** We assume that jobs are fully preemptive. *)
#[local] Existing Instance fully_preemptive_job_model .
(** Under these assumptions, 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 :
(exists any_sched : schedule (ideal.processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists edf_sched : schedule (ideal.processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\
EDF_schedule edf_sched.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq
(exists any_sched : schedule (processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\
EDF_schedule edf_sched
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq
(exists any_sched : schedule (processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\
EDF_schedule edf_sched
move => [sched [[COME READY] DL_ARR_MET]].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\
EDF_schedule edf_sched
have ARR := jobs_must_arrive_to_be_ready sched READY.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched ARR : jobs_must_arrive_to_execute sched
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\
EDF_schedule edf_sched
have COMP := completed_jobs_are_not_ready sched READY.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\
EDF_schedule edf_sched
move : (all_deadlines_met_in_valid_schedule _ _ COME DL_ARR_MET) => DL_MET.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched DL_MET : all_deadlines_met sched
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\
EDF_schedule edf_sched
set sched' := edf_transform sched.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched DL_MET : all_deadlines_met sched sched' := edf_transform sched : instant -> processor_state Job
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\
EDF_schedule edf_sched
exists sched' .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched DL_MET : all_deadlines_met sched sched' := edf_transform sched : instant -> processor_state Job
valid_schedule sched' arr_seq /\
all_deadlines_of_arrivals_met arr_seq sched' /\
EDF_schedule sched'
split ; last split .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched DL_MET : all_deadlines_met sched sched' := edf_transform sched : instant -> processor_state Job
valid_schedule sched' arr_seq
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched DL_MET : all_deadlines_met sched sched' := edf_transform sched : instant -> processor_state Job
valid_schedule sched' arr_seq
by apply edf_schedule_is_valid.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched DL_MET : all_deadlines_met sched sched' := edf_transform sched : instant -> processor_state Job
all_deadlines_of_arrivals_met arr_seq sched'
by apply edf_schedule_meets_all_deadlines_wrt_arrivals.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched DL_MET : all_deadlines_met sched sched' := edf_transform sched : instant -> processor_state Job
EDF_schedule sched'
by apply edf_transform_ensures_edf.
Qed .
(** Moreover, we note that, since EDF maintains work conservation, if there
exists a schedule in which all jobs of [arr_seq] meet their deadline,
then there also exists a work-conserving EDF in which all deadlines are
met. *)
Theorem EDF_WC_optimality :
(exists any_sched : schedule (ideal.processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists edf_wc_sched : schedule (ideal.processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq
(exists any_sched : schedule (processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists edf_wc_sched : schedule (processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq
(exists any_sched : schedule (processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists edf_wc_sched : schedule (processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched
move => [sched [[COME READY] DL_ARR_MET]].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched
exists edf_wc_sched : schedule (processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched
move : (all_deadlines_met_in_valid_schedule _ _ COME DL_ARR_MET) => DL_MET.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched
exists edf_wc_sched : schedule (processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched
set wc_sched := wc_transform arr_seq sched.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job
exists edf_wc_sched : schedule (processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched
have wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
by apply wc_jobs_come_from_arrival_sequence.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq
exists edf_wc_sched : schedule (processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched
have wc_READY : jobs_must_be_ready_to_execute wc_sched
by apply wc_jobs_must_be_ready_to_execute.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq wc_READY : jobs_must_be_ready_to_execute wc_sched
exists edf_wc_sched : schedule (processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched
have wc_ARR := jobs_must_arrive_to_be_ready wc_sched wc_READY.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq wc_READY : jobs_must_be_ready_to_execute wc_sched wc_ARR : jobs_must_arrive_to_execute wc_sched
exists edf_wc_sched : schedule (processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched
have wc_COMP := completed_jobs_are_not_ready wc_sched wc_READY.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq wc_READY : jobs_must_be_ready_to_execute wc_sched wc_ARR : jobs_must_arrive_to_execute wc_sched wc_COMP : completed_jobs_dont_execute wc_sched
exists edf_wc_sched : schedule (processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched
have wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
by apply wc_all_deadlines_of_arrivals_met; apply DL_ARR_MET.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq wc_READY : jobs_must_be_ready_to_execute wc_sched wc_ARR : jobs_must_arrive_to_execute wc_sched wc_COMP : completed_jobs_dont_execute wc_sched wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
wc_sched
exists edf_wc_sched : schedule (processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched
move : (all_deadlines_met_in_valid_schedule _ _ wc_COME wc_DL_ARR_MET) => wc_DL_MET.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq wc_READY : jobs_must_be_ready_to_execute wc_sched wc_ARR : jobs_must_arrive_to_execute wc_sched wc_COMP : completed_jobs_dont_execute wc_sched wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
wc_sched wc_DL_MET : all_deadlines_met wc_sched
exists edf_wc_sched : schedule (processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched
set sched' := edf_transform wc_sched.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq wc_READY : jobs_must_be_ready_to_execute wc_sched wc_ARR : jobs_must_arrive_to_execute wc_sched wc_COMP : completed_jobs_dont_execute wc_sched wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
wc_sched wc_DL_MET : all_deadlines_met wc_sched sched' := edf_transform wc_sched : instant -> processor_state Job
exists edf_wc_sched : schedule (processor_state Job),
valid_schedule edf_wc_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
work_conserving arr_seq edf_wc_sched /\
EDF_schedule edf_wc_sched
exists sched' .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq wc_READY : jobs_must_be_ready_to_execute wc_sched wc_ARR : jobs_must_arrive_to_execute wc_sched wc_COMP : completed_jobs_dont_execute wc_sched wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
wc_sched wc_DL_MET : all_deadlines_met wc_sched sched' := edf_transform wc_sched : instant -> processor_state Job
valid_schedule sched' arr_seq /\
all_deadlines_of_arrivals_met arr_seq sched' /\
work_conserving arr_seq sched' /\ EDF_schedule sched'
split ; last split ; last split .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq wc_READY : jobs_must_be_ready_to_execute wc_sched wc_ARR : jobs_must_arrive_to_execute wc_sched wc_COMP : completed_jobs_dont_execute wc_sched wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
wc_sched wc_DL_MET : all_deadlines_met wc_sched sched' := edf_transform wc_sched : instant -> processor_state Job
valid_schedule sched' arr_seq
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq wc_READY : jobs_must_be_ready_to_execute wc_sched wc_ARR : jobs_must_arrive_to_execute wc_sched wc_COMP : completed_jobs_dont_execute wc_sched wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
wc_sched wc_DL_MET : all_deadlines_met wc_sched sched' := edf_transform wc_sched : instant -> processor_state Job
valid_schedule sched' arr_seq
by apply edf_schedule_is_valid.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq wc_READY : jobs_must_be_ready_to_execute wc_sched wc_ARR : jobs_must_arrive_to_execute wc_sched wc_COMP : completed_jobs_dont_execute wc_sched wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
wc_sched wc_DL_MET : all_deadlines_met wc_sched sched' := edf_transform wc_sched : instant -> processor_state Job
all_deadlines_of_arrivals_met arr_seq sched'
by apply edf_schedule_meets_all_deadlines_wrt_arrivals.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq wc_READY : jobs_must_be_ready_to_execute wc_sched wc_ARR : jobs_must_arrive_to_execute wc_sched wc_COMP : completed_jobs_dont_execute wc_sched wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
wc_sched wc_DL_MET : all_deadlines_met wc_sched sched' := edf_transform wc_sched : instant -> processor_state Job
work_conserving arr_seq sched'
apply edf_transform_maintains_work_conservation; by [ | apply wc_is_work_conserving ].
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
sched DL_MET : all_deadlines_met sched wc_sched := wc_transform arr_seq sched : nat -> processor_state Job wc_COME : jobs_come_from_arrival_sequence wc_sched
arr_seq wc_READY : jobs_must_be_ready_to_execute wc_sched wc_ARR : jobs_must_arrive_to_execute wc_sched wc_COMP : completed_jobs_dont_execute wc_sched wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq
wc_sched wc_DL_MET : all_deadlines_met wc_sched sched' := edf_transform wc_sched : instant -> processor_state Job
EDF_schedule sched'
by apply edf_transform_ensures_edf.
Qed .
(** Remark: [EDF_optimality] is of course an immediate corollary of
[EDF_WC_optimality]. We nonetheless have two separate proofs for historic
reasons as [EDF_optimality] predates [EDF_WC_optimality] (in Prosa). *)
(** Finally, we state the optimality theorem also in terms of a
policy-compliant schedule, which a more generic notion used in Prosa for
scheduling policies (rather than the simpler, but ad-hoc
[EDF_schedule] predicate used above).
Given that we're considering the EDF priority policy and a fully
preemptive job model, satisfying the [EDF_schedule] predicate is
equivalent to satisfying the [respects_policy_at_preemption_point]
w.r.t. to the EDF policy predicate. The optimality of priority-compliant
schedules that are work-conserving follows hence directly from the above
[EDF_WC_optimality] theorem. *)
Corollary EDF_priority_compliant_WC_optimality :
(exists any_sched : schedule (ideal.processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists priority_compliant_sched : schedule (ideal.processor_state Job),
valid_schedule priority_compliant_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq priority_compliant_sched /\
work_conserving arr_seq priority_compliant_sched /\
respects_JLFP_policy_at_preemption_point arr_seq priority_compliant_sched (EDF Job).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq
(exists any_sched : schedule (processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists
priority_compliant_sched : schedule
(processor_state Job),
valid_schedule priority_compliant_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq
priority_compliant_sched /\
work_conserving arr_seq priority_compliant_sched /\
respects_JLFP_policy_at_preemption_point arr_seq
priority_compliant_sched (EDF Job)
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq
(exists any_sched : schedule (processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists
priority_compliant_sched : schedule
(processor_state Job),
valid_schedule priority_compliant_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq
priority_compliant_sched /\
work_conserving arr_seq priority_compliant_sched /\
respects_JLFP_policy_at_preemption_point arr_seq
priority_compliant_sched (EDF Job)
move /EDF_WC_optimality => [edf_sched [[ARR READY] [DL_MET [WC EDF]]]].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq edf_sched : schedule (processor_state Job) ARR : jobs_come_from_arrival_sequence edf_sched
arr_seq READY : jobs_must_be_ready_to_execute edf_sched DL_MET : all_deadlines_of_arrivals_met arr_seq
edf_sched WC : work_conserving arr_seq edf_sched EDF : EDF_schedule edf_sched
exists
priority_compliant_sched : schedule
(processor_state Job),
valid_schedule priority_compliant_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq
priority_compliant_sched /\
work_conserving arr_seq priority_compliant_sched /\
respects_JLFP_policy_at_preemption_point arr_seq
priority_compliant_sched (edf.EDF Job)
exists edf_sched .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq edf_sched : schedule (processor_state Job) ARR : jobs_come_from_arrival_sequence edf_sched
arr_seq READY : jobs_must_be_ready_to_execute edf_sched DL_MET : all_deadlines_of_arrivals_met arr_seq
edf_sched WC : work_conserving arr_seq edf_sched EDF : EDF_schedule edf_sched
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\
work_conserving arr_seq edf_sched /\
respects_JLFP_policy_at_preemption_point arr_seq
edf_sched (edf.EDF Job)
apply (EDF_schedule_equiv arr_seq) in EDF => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq edf_sched : schedule (processor_state Job) ARR : jobs_come_from_arrival_sequence edf_sched
arr_seq READY : jobs_must_be_ready_to_execute edf_sched DL_MET : all_deadlines_of_arrivals_met arr_seq
edf_sched WC : work_conserving arr_seq edf_sched EDF : EDF_schedule edf_sched H2 : valid_arrival_sequence arr_seq ->
forall 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_of_arrivals_met arr_seq sched ->
EDF_schedule sched ->
respects_JLFP_policy_at_preemption_point arr_seq
sched (edf.EDF Job)
completed_jobs_dont_execute edf_sched
exact : (completed_jobs_are_not_ready edf_sched READY).
Qed .
End Optimality .
(** ** Weak Optimality Theorem *)
(** We further state a weaker notion of the above optimality result
that avoids a dependency on a given arrival
sequence. Specifically, it establishes that, given a reference
schedule without deadline misses, there exists an EDF schedule of
the same jobs in which no deadlines are missed. *)
Section WeakOptimality .
(** 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}.
(** ... if we have a well-behaved reference schedule ... *)
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.
(** ... in which no deadlines are missed, ... *)
Hypothesis H_all_deadlines_met : all_deadlines_met any_sched.
(** ...then there also exists an 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 :
exists 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 /\
EDF_schedule edf_sched /\
forall j ,
(exists t , scheduled_at any_sched j t) <->
(exists t' , scheduled_at edf_sched j t').Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job any_sched : schedule (processor_state Job) H_must_arrive : jobs_must_arrive_to_execute any_sched H_completed_dont_execute : completed_jobs_dont_execute
any_sched H_all_deadlines_met : all_deadlines_met any_sched
exists edf_sched : schedule (processor_state Job),
jobs_must_arrive_to_execute edf_sched /\
completed_jobs_dont_execute edf_sched /\
all_deadlines_met edf_sched /\
EDF_schedule edf_sched /\
(forall j : Job,
(exists t : instant, scheduled_at any_sched j t) <->
(exists t' : instant, scheduled_at edf_sched j t'))
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job any_sched : schedule (processor_state Job) H_must_arrive : jobs_must_arrive_to_execute any_sched H_completed_dont_execute : completed_jobs_dont_execute
any_sched H_all_deadlines_met : all_deadlines_met any_sched
exists edf_sched : schedule (processor_state Job),
jobs_must_arrive_to_execute edf_sched /\
completed_jobs_dont_execute edf_sched /\
all_deadlines_met edf_sched /\
EDF_schedule edf_sched /\
(forall j : Job,
(exists t : instant, scheduled_at any_sched j t) <->
(exists t' : instant, scheduled_at edf_sched j t'))
set sched' := edf_transform any_sched.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job any_sched : schedule (processor_state Job) H_must_arrive : jobs_must_arrive_to_execute any_sched H_completed_dont_execute : completed_jobs_dont_execute
any_sched H_all_deadlines_met : all_deadlines_met any_sched sched' := edf_transform any_sched : instant -> processor_state Job
exists edf_sched : schedule (processor_state Job),
jobs_must_arrive_to_execute edf_sched /\
completed_jobs_dont_execute edf_sched /\
all_deadlines_met edf_sched /\
EDF_schedule edf_sched /\
(forall j : Job,
(exists t : instant, scheduled_at any_sched j t) <->
(exists t' : instant, scheduled_at edf_sched j t'))
exists sched' .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job any_sched : schedule (processor_state Job) H_must_arrive : jobs_must_arrive_to_execute any_sched H_completed_dont_execute : completed_jobs_dont_execute
any_sched H_all_deadlines_met : all_deadlines_met any_sched sched' := edf_transform any_sched : instant -> processor_state Job
jobs_must_arrive_to_execute sched' /\
completed_jobs_dont_execute sched' /\
all_deadlines_met sched' /\
EDF_schedule sched' /\
(forall j : Job,
(exists t : instant, scheduled_at any_sched j t) <->
(exists t' : instant, scheduled_at sched' j t'))
repeat split .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job any_sched : schedule (processor_state Job) H_must_arrive : jobs_must_arrive_to_execute any_sched H_completed_dont_execute : completed_jobs_dont_execute
any_sched H_all_deadlines_met : all_deadlines_met any_sched sched' := edf_transform any_sched : instant -> processor_state Job
jobs_must_arrive_to_execute sched'
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job any_sched : schedule (processor_state Job) H_must_arrive : jobs_must_arrive_to_execute any_sched H_completed_dont_execute : completed_jobs_dont_execute
any_sched H_all_deadlines_met : all_deadlines_met any_sched sched' := edf_transform any_sched : instant -> processor_state Job
jobs_must_arrive_to_execute sched'
by apply edf_transform_jobs_must_arrive.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job any_sched : schedule (processor_state Job) H_must_arrive : jobs_must_arrive_to_execute any_sched H_completed_dont_execute : completed_jobs_dont_execute
any_sched H_all_deadlines_met : all_deadlines_met any_sched sched' := edf_transform any_sched : instant -> processor_state Job
completed_jobs_dont_execute sched'
by apply edf_transform_completed_jobs_dont_execute.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job any_sched : schedule (processor_state Job) H_must_arrive : jobs_must_arrive_to_execute any_sched H_completed_dont_execute : completed_jobs_dont_execute
any_sched H_all_deadlines_met : all_deadlines_met any_sched sched' := edf_transform any_sched : instant -> processor_state Job
all_deadlines_met sched'
by apply edf_transform_deadlines_met.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job any_sched : schedule (processor_state Job) H_must_arrive : jobs_must_arrive_to_execute any_sched H_completed_dont_execute : completed_jobs_dont_execute
any_sched H_all_deadlines_met : all_deadlines_met any_sched sched' := edf_transform any_sched : instant -> processor_state Job
EDF_schedule sched'
by apply edf_transform_ensures_edf.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job any_sched : schedule (processor_state Job) H_must_arrive : jobs_must_arrive_to_execute any_sched H_completed_dont_execute : completed_jobs_dont_execute
any_sched H_all_deadlines_met : all_deadlines_met any_sched sched' := edf_transform any_sched : instant -> processor_state Job j : Job
(exists t : instant, scheduled_at any_sched j t) ->
exists t' : instant, scheduled_at sched' j t'
by move => [t SCHED_j]; apply edf_transform_job_scheduled' with (t := t).
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job any_sched : schedule (processor_state Job) H_must_arrive : jobs_must_arrive_to_execute any_sched H_completed_dont_execute : completed_jobs_dont_execute
any_sched H_all_deadlines_met : all_deadlines_met any_sched sched' := edf_transform any_sched : instant -> processor_state Job j : Job
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
by move => [t SCHED_j]; apply edf_transform_job_scheduled with (t := t).
Qed .
End WeakOptimality .