Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.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 Export prosa.analysis.facts.model.ideal.schedule.[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 ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_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 Export prosa.analysis.facts.behavior.deadlines.
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.model.priority.edf.
Require Export prosa.model.schedule.edf.
Require Export prosa.model.schedule.priority_driven.
Require Import prosa.model.readiness.basic.
Require Import prosa.model.preemption.fully_preemptive.
(** * Equivalence of EDF Definitions *)
(** Recall that we have defined "EDF schedules" in two ways.
The generic way to define an EDF schedule is by using the EDF priority
policy defined in [model.priority.edf] and the general notion of
priority-compliant schedules defined in [model.schedule.priority_driven].
Another, more straight-forward way to define an EDF schedule is the standalone
definition given in [model.schedule.edf], which is less general but simpler
and used in the EDF optimality proof.
In this file, we show that both definitions are equivalent assuming:
(1) ideal uniprocessor schedules,
(2) the classic Liu & Layland model of readiness without jitter and
without self-suspensions, where pending jobs are always ready, and
(3) that jobs are fully preemptive. *)
Section Equivalence .
(** We assume the basic (i.e., Liu & Layland)
readiness model under which any pending job is ready. *)
#[local] Existing Instance basic_ready_instance .
(** We assume that jobs are fully preemptive. *)
#[local] Existing Instance fully_preemptive_job_model .
(** For any given type of jobs, each characterized by an arrival time,
an execution cost, and an absolute deadline, ... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(** ...consider a given valid job arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arr_seq_valid : valid_arrival_sequence arr_seq.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** ...and a corresponding ideal uniprocessor schedule. *)
Variable sched : schedule (ideal.processor_state Job).
(** Suppose jobs don't execute before their arrival nor after their
completion, ... *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** ...all jobs come from the arrival sequence [arr_seq], ...*)
Hypothesis H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq.
(** ...and jobs from [arr_seq] don't miss their deadlines. *)
Hypothesis H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched.
(** We first show that a schedule that satisfies the standalone
[EDF_schedule] predicate is also compliant with the generic notion of EDF
policy defined in Prosa, namely the [respects_policy_at_preemption_point]
predicate. *)
Lemma EDF_schedule_implies_respects_policy_at_preemption_point :
EDF_schedule sched ->
respects_JLFP_policy_at_preemption_point arr_seq 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched
EDF_schedule sched ->
respects_JLFP_policy_at_preemption_point arr_seq 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched
EDF_schedule sched ->
respects_JLFP_policy_at_preemption_point arr_seq sched
(EDF Job)
move => EDF j' j t ARR PREEMPTION BL 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched EDF : EDF_schedule sched j', j : Job t : instant ARR : arrives_in arr_seq j' PREEMPTION : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
hep_job_at t j j'
have suff : exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t'.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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched EDF : EDF_schedule sched j', j : Job t : instant ARR : arrives_in arr_seq j' PREEMPTION : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
(exists t' : nat,
t <= t' < job_deadline j' /\
scheduled_at sched j' t') -> hep_job_at t j j'
{ 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched EDF : EDF_schedule sched j', j : Job t : instant ARR : arrives_in arr_seq j' PREEMPTION : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
(exists t' : nat,
t <= t' < job_deadline j' /\
scheduled_at sched j' t') -> hep_job_at t j j'
move => [t' [/andP [LE _] 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched EDF : EDF_schedule sched j', j : Job t : instant ARR : arrives_in arr_seq j' PREEMPTION : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t t' : nat LE : t <= t' SCHED' : scheduled_at sched j' t'
hep_job_at t j j'
apply : (EDF t); [by [] | exact : LE | exact : 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched EDF : EDF_schedule sched j', j : Job t : instant ARR : arrives_in arr_seq j' PREEMPTION : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t t' : nat LE : t <= t' SCHED' : scheduled_at sched j' t'
job_arrival j' <= t
by apply : (backlogged_implies_arrived sched j' t). } 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched EDF : EDF_schedule sched j', j : Job t : instant ARR : arrives_in arr_seq j' PREEMPTION : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
((exists t' : nat,
t <= t' < job_deadline j' /\
scheduled_at sched j' t') -> hep_job_at t j j') ->
hep_job_at t j j'
apply ; apply : incomplete_implies_scheduled_later.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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched EDF : EDF_schedule sched j', j : Job t : instant ARR : arrives_in arr_seq j' PREEMPTION : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
job_meets_deadline sched j'
- 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched EDF : EDF_schedule sched j', j : Job t : instant ARR : arrives_in arr_seq j' PREEMPTION : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
job_meets_deadline sched j'
exact : H_no_deadline_misses.
- 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched EDF : EDF_schedule sched j', j : Job t : instant ARR : arrives_in arr_seq j' PREEMPTION : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
~~ completed_by sched j' t
exact : (backlogged_implies_incomplete sched j' t).
Qed .
(** Conversely, the reverse direction also holds: a schedule that satisfies
the [respects_policy_at_preemption_point] predicate is also an EDF
schedule in the sense of [EDF_schedule]. *)
Lemma respects_policy_at_preemption_point_implies_EDF_schedule :
respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job) ->
EDF_schedule 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched
respects_JLFP_policy_at_preemption_point arr_seq sched
(EDF Job) -> EDF_schedule 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched
respects_JLFP_policy_at_preemption_point arr_seq sched
(EDF Job) -> EDF_schedule sched
move => H_priority_driven t j_hp SCHED t' j LEQ SCHED' EARLIER_ARR.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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t
job_deadline j_hp <= job_deadline j
case (boolP (j == j_hp)); first by move /eqP => EQ; subst .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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t
j != j_hp -> job_deadline j_hp <= job_deadline j
move /neqP => NEQ.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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t NEQ : j <> j_hp
job_deadline j_hp <= job_deadline j
exploit (H_priority_driven j j_hp t) => //. 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t NEQ : j <> j_hp
preemption_time arr_seq sched t
{ 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t NEQ : j <> j_hp
preemption_time arr_seq sched t
by rewrite /preemption_time scheduled_job_at_def //; destruct (sched t). } 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t NEQ : j <> j_hp
backlogged sched j t
{ 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t NEQ : j <> j_hp
backlogged sched j t
apply /andP; 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t NEQ : j <> j_hp
job_ready sched j t
- 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t NEQ : j <> j_hp
job_ready sched j t
apply /andP; 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t NEQ : j <> j_hp
~~ completed_by sched j t
apply (incompletion_monotonic _ j _ _ LEQ).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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t NEQ : j <> j_hp
~~ completed_by sched j t'
by apply scheduled_implies_not_completed.
- 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t NEQ : j <> j_hp
~~ scheduled_at sched j t
apply /negP; move => 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched H_priority_driven : respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) t : instant j_hp : Job SCHED : scheduled_at sched j_hp t t' : instant j : Job LEQ : t <= t' SCHED' : scheduled_at sched j t' EARLIER_ARR : job_arrival j <= t NEQ : j <> j_hp SCHED'' : scheduled_at sched j t
False
by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t). }
Qed .
(** From the two preceding lemmas, it follows immediately that the two EDF
definitions are indeed equivalent, which we note with the following
corollary. *)
Corollary EDF_schedule_equiv :
EDF_schedule sched <-> respects_JLFP_policy_at_preemption_point arr_seq 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched
EDF_schedule sched <->
respects_JLFP_policy_at_preemption_point arr_seq 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched
EDF_schedule sched <->
respects_JLFP_policy_at_preemption_point arr_seq sched
(EDF Job)
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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched
EDF_schedule sched ->
respects_JLFP_policy_at_preemption_point arr_seq 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched
EDF_schedule sched ->
respects_JLFP_policy_at_preemption_point arr_seq sched
(EDF Job)
exact : EDF_schedule_implies_respects_policy_at_preemption_point.
- 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 H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (ideal.processor_state Job) H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq H_no_deadline_misses : all_deadlines_of_arrivals_met
arr_seq sched
respects_JLFP_policy_at_preemption_point arr_seq sched
(EDF Job) -> EDF_schedule sched
exact : respects_policy_at_preemption_point_implies_EDF_schedule.
Qed .
End Equivalence .