# Library prosa.model.priority.edf

# EDF Priority Policy

#[export] Instance EDF (Job : JobType) `{JobDeadline Job} : JLFP_policy Job :=

{

hep_job (j1 j2 : Job) := job_deadline j1 ≤ job_deadline j2

}.

{

hep_job (j1 j2 : Job) := job_deadline j1 ≤ job_deadline j2

}.

In this section, we prove a few properties about EDF policy.

Consider any type of jobs with deadlines.

Consider any arrival sequence.

EDF is reflexive.

Lemma EDF_is_reflexive : reflexive_priorities.

Proof. by intros t j; unfold hep_job_at, JLFP_to_JLDP, hep_job, EDF. Qed.

Proof. by intros t j; unfold hep_job_at, JLFP_to_JLDP, hep_job, EDF. Qed.

EDF is transitive.

EDF is total.

Lemma EDF_is_total : total_priorities.

Proof. by move⇒ t j1 j2; apply leq_total. Qed.

End PropertiesOfEDF.

Proof. 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.

EDF_is_reflexive

EDF_is_transitive

EDF_is_total

: basic_rt_facts.