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.