Project Page Index Table of Contents

# Library prosa.model.priority.deadline_monotonic

Require Export prosa.model.priority.classes.

# Deadline-Monotonic Fixed-Priority Policy

We define what it means for an abstract fixed-priority policy to behave as deadline-monotonic.
Section DMPolicy.
Consider tasks with relative deadlines.
Context {Task : TaskType} `{TaskDeadline Task}.
A fixed-priority policy is deadline-monotonic if it assigns higher priority to tasks with shorter relative deadlines.
Definition policy_is_DM (FP : FP_policy Task) :=
∀ tsk1 tsk2,
hep_task tsk1 tsk2 = (task_deadline tsk1 ≤ task_deadline tsk2).
End DMPolicy.