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.

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 consider two possible interpretations. In the first interpretation, a lower numeric value indicates lower priority, while in the other interpretation, a lower numeric value indicates higher priority. Both interpretations can be found in practice and in the literature. For example, Linux uses "higher numeric value <-> higher priority", whereas many papers in the academic literature assume "lower numeric value <-> higher priority".

Section NumericFPInterpretations.

Consider tasks with numeric priorities.

Context {Task : TaskType} `{TaskPriority Task}.

A fixed-priority policy is ascending numeric FP if it assigns higher priority to tasks with higher numeric task_priority values.

  Definition policy_is_numeric_FP_ascending (FP : FP_policy Task) :=
    ∀ tsk1 tsk2,
      hep_task tsk1 tsk2 = (task_priority tsk1 ≥ task_priority tsk2 ).

A fixed-priority policy is descending numeric FP if it assigns higher priority to tasks with lower numeric task_priority values.

  Definition policy_is_numeric_FP_descending (FP : FP_policy Task) :=
    ∀ tsk1 tsk2,
      hep_task tsk1 tsk2 = (task_priority tsk1 ≤ task_priority tsk2 ).

End NumericFPInterpretations.