Project Page Index Table of Contents

# Library prosa.model.priority.numeric_fixed_priority

Require Export prosa.model.priority.classes.

# Numeric Fixed Task Priorities

We define the notion of arbitrary numeric fixed task priorities, i.e., tasks are prioritized in order of user-provided numeric priority values, where numerically smaller values indicate lower priorities (as for instance it is the case in Linux).
First, we define a new task parameter task_priority that maps each task to a numeric priority value.
Class TaskPriority (Task : TaskType) := { task_priority : Task → nat }.
Based on this parameter, we define two corresponding FP policies. In one instance, a lower numeric value indicates lower priority, while in the other instance, a lower numeric value indicates higher priority. Both these interpretations can be found in practice and in the literature. For example, Linux uses "higher numeric value <-> higher priority", whereas many papers assume "lower numeric value <-> higher priority".
In this section, we define ascending numeric fixed priorities, where a larger numeric value indicates higher priority, and note some trivial facts about this interpretation of priority values.
Section PropertiesNFPA.
The instance numeric_fp_ascending assigns higher priority to tasks with higher numeric task_priority value.
#[local] Instance numeric_fp_ascending (Task : TaskType) `{TaskPriority Task} : FP_policy Task :=
{
hep_task (tsk1 tsk2 : Task) := task_priority tsk1 ≥ task_priority tsk2
}.
Consider any kind of tasks with specified priorities...
Context {Task : TaskType}.
Context `{TaskPriority Task}.
...and jobs stemming from these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
The resulting priority policy is reflexive.
Lemma NFPA_is_reflexive : reflexive_task_priorities (numeric_fp_ascending Task).
Proof. by move⇒ ?; rewrite /hep_task /numeric_fp_ascending. Qed.
The resulting priority policy is transitive.
Lemma NFPA_is_transitive : transitive_task_priorities (numeric_fp_ascending Task).
Proof.
move⇒ y x z.
by rewrite /hep_task /numeric_fp_ascending ⇒ PRIO_yx PRIO_xy; lia.
Qed.
The resulting priority policy is total.
Lemma NFPA_is_total : total_task_priorities (numeric_fp_ascending Task).
Proof. by move⇒ j1 j2; apply: leq_total. Qed.
End PropertiesNFPA.
Next, we define descending numeric fixed priorities, where a larger numeric value indicates lower priority, and again note some trivial facts about this alternate interpretation of priority values.
Section PropertiesNFPD.
The instance numeric_fp_descending assigns lower priority to tasks with higher numeric task_priority value.
#[local] Instance numeric_fp_descending (Task : TaskType) `{TaskPriority Task} : FP_policy Task :=
{
hep_task (tsk1 tsk2 : Task) := task_priority tsk1 ≤ task_priority tsk2
}.
Consider any kind of tasks with specified priorities...
Context {Task : TaskType}.
Context `{TaskPriority Task}.
...and jobs stemming from these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
The resulting priority policy is reflexive.
Lemma NFPD_is_reflexive : reflexive_task_priorities (numeric_fp_descending Task).
Proof. by move⇒ ?; rewrite /hep_task /numeric_fp_descending. Qed.
The resulting priority policy is transitive.
Lemma NFPD_is_transitive : transitive_task_priorities (numeric_fp_descending Task).
Proof.
move⇒ y x z.
by rewrite /hep_task /numeric_fp_descending ⇒ PRIO_yx PRIO_xy; lia.
Qed.
The resulting priority policy is total.
Lemma NFPD_is_total : total_task_priorities (numeric_fp_descending Task).
Proof. by move⇒ j1 j2; apply: leq_total. Qed.
End PropertiesNFPD.
We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically.
Global Hint Resolve
NFPA_is_reflexive
NFPA_is_transitive
NFPA_is_total
NFPD_is_reflexive
NFPD_is_transitive
NFPD_is_total
: basic_rt_facts.