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]
(** * EDF Priority Policy *) (** We introduce the classic EDF priority policy, under which jobs are scheduled in order of their urgency, i.e., jobs are ordered according to their absolute deadlines. The EDF policy belongs to the class of JLFP policies. *) #[export] Instance EDF (Job : JobType) `{JobDeadline Job} : JLFP_policy Job := { hep_job (j1 j2 : Job) := job_deadline j1 <= job_deadline j2 }. (** In this section, we prove a few properties about EDF policy. *) Section PropertiesOfEDF. (** Consider any type of jobs with deadlines. *) Context {Job : JobType}. Context `{JobDeadline Job}. (** Consider any arrival sequence. *) Variable arr_seq : arrival_sequence Job. (** EDF is reflexive. *)
Job: JobType
H: JobDeadline Job
arr_seq: arrival_sequence Job

reflexive_priorities
Job: JobType
H: JobDeadline Job
arr_seq: arrival_sequence Job

reflexive_priorities
by intros t j; unfold hep_job_at, JLFP_to_JLDP, hep_job, EDF. Qed. (** EDF is transitive. *)
Job: JobType
H: JobDeadline Job
arr_seq: arrival_sequence Job

transitive_priorities
Job: JobType
H: JobDeadline Job
arr_seq: arrival_sequence Job

transitive_priorities
by intros t y x z; apply leq_trans. Qed. (** EDF is total. *)
Job: JobType
H: JobDeadline Job
arr_seq: arrival_sequence Job

total_priorities
Job: JobType
H: JobDeadline Job
arr_seq: arrival_sequence Job

total_priorities
by move=> t j1 j2; apply leq_total. Qed. End PropertiesOfEDF. (** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *) Global Hint Resolve EDF_is_reflexive EDF_is_transitive EDF_is_total : basic_rt_facts.