# Library prosa.model.priority.deadline_monotonic

# Deadline-Monotonic Fixed-Priority Policy

#[export] Instance DM (Task : TaskType) `{TaskDeadline Task} : FP_policy Task :=

{

hep_task (tsk1 tsk2 : Task) := task_deadline tsk1 ≤ task_deadline tsk2

}.

{

hep_task (tsk1 tsk2 : Task) := task_deadline tsk1 ≤ task_deadline tsk2

}.

In this section, we prove a few basic properties of the DM policy.

Consider any kind of tasks with relative deadlines...

...and jobs stemming from these tasks.

DM is reflexive.

Lemma DM_is_reflexive : reflexive_priorities.

Proof. by move⇒ ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /DM. Qed.

Proof. by move⇒ ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /DM. Qed.

DM is transitive.

DM is total.

Lemma DM_is_total : total_priorities.

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

End Properties.

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

End Properties.

We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically.

Global Hint Resolve

DM_is_reflexive

DM_is_transitive

DM_is_total

: basic_rt_facts.

DM_is_reflexive

DM_is_transitive

DM_is_total

: basic_rt_facts.