Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.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.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** * 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. (** ...and a corresponding schedule. *) Variable sched : schedule (ideal.processor_state Job). (** Suppose jobs don't execute after their completion, ... *) 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. *)
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 (ideal.processor_state Job)
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
sched: schedule (ideal.processor_state Job)
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
sched: schedule (ideal.processor_state Job)
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 sched t
BL: backlogged sched j' t
SCHED: 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
sched: schedule (ideal.processor_state Job)
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 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
sched: schedule (ideal.processor_state Job)
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 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'
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 (ideal.processor_state Job)
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 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
sched: schedule (ideal.processor_state Job)
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 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'
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 (ideal.processor_state Job)
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 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
sched: schedule (ideal.processor_state Job)
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 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'
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 (ideal.processor_state Job)
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 sched t
BL: backlogged sched j' t
SCHED: scheduled_at sched j t

~~ completed_by sched j' t
by apply: (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]. *)
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 (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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

arrives_in arr_seq 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
sched: schedule (ideal.processor_state Job)
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 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
sched: schedule (ideal.processor_state Job)
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
sched: schedule (ideal.processor_state Job)
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

arrives_in arr_seq j
by apply (H_from_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 (ideal.processor_state Job)
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 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
sched: schedule (ideal.processor_state Job)
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
sched: schedule (ideal.processor_state Job)
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 sched t
by rewrite /preemption_time; 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
sched: schedule (ideal.processor_state Job)
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
sched: schedule (ideal.processor_state Job)
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
sched: schedule (ideal.processor_state Job)
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
sched: schedule (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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
sched: schedule (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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'
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 (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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. *)
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 (ideal.processor_state Job)
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
sched: schedule (ideal.processor_state Job)
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
sched: schedule (ideal.processor_state Job)
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
sched: schedule (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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
sched: schedule (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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
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 (ideal.processor_state Job)
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
by apply respects_policy_at_preemption_point_implies_EDF_schedule. Qed. End Equivalence.