# Library prosa.model.priority.classes

From mathcomp Require Export seq.

Require Export prosa.model.task.concept.

Require Export prosa.util.rel.

Require Export prosa.util.list.

Require Export prosa.model.task.concept.

Require Export prosa.util.rel.

Require Export prosa.util.list.

# The FP, JLFP, and JLDP Priority Classes

... a JLFP policy as a relation among jobs, and ...

... a JLDP policy as a relation among jobs that may vary over time.

NB: The preceding definitions currently make it difficult to express
priority policies in which the priority of a job at a given time varies
depending on the preceding schedule prefix (e.g., least-laxity
first). That is, there is room for an even more general notion of a
schedule-dependent JLDP policy, where the priority relation among jobs
may vary depending both on time and the schedule prefix prior to a
given time. This is left to future work.
Since there are natural interpretations of FP and JLFP policies as JLFP and
JLDP policies, respectively, we define conversions that express these
generalizations. In practice, this means that Coq will be able to
automatically satisfy a JLDP assumption if a JLFP or FP policy is in
scope.
First, any FP policy can be interpreted as an JLFP policy by comparing jobs
according to the priorities of their respective tasks.

## Automatic FP ➔ JLFP ➔ JLDP Conversion

#[global]

Instance FP_to_JLFP (Job: JobType) (Task: TaskType)

`{JobTask Job Task} `{FP_policy Task} : JLFP_policy Job :=

fun j1 j2 ⇒ hep_task (job_task j1) (job_task j2).

Instance FP_to_JLFP (Job: JobType) (Task: TaskType)

`{JobTask Job Task} `{FP_policy Task} : JLFP_policy Job :=

fun j1 j2 ⇒ hep_task (job_task j1) (job_task j2).

Second, any JLFP policy implies a JLDP policy that simply ignores the time
parameter.

#[global]

Instance JLFP_to_JLDP (Job: JobType) `{JLFP_policy Job} : JLDP_policy Job :=

fun _ j1 j2 ⇒ hep_job j1 j2.

Instance JLFP_to_JLDP (Job: JobType) `{JLFP_policy Job} : JLDP_policy Job :=

fun _ j1 j2 ⇒ hep_job j1 j2.

## Properties of Priority Policies

Consider any type of tasks ...

... and any type of jobs associated with these tasks, ...

.. and assume that jobs have a cost and an arrival time.

In the following section, we define properties of JLDP policies, and by
extension also properties of FP and JLFP policies.

Consider any JLDP policy.

We define what it means for a JLDP policy to be reflexive, transitive,
and total. Note that these definitions, although phrased in terms of a
given JLDP policy, can also be used for JLFP and FP policies due to the
above-defined conversion instances.
A JLDP policy is reflexive if the relation among jobs is reflexive at
every point in time.

A JLDP policy is transitive if the relation among jobs is transitive at
every point in time.

A JLDP policy is total if the relation among jobs is total at
every point in time.

Next, we define a property of JLFP policies.

Consider any JLFP policy.

Recall that jobs of a sequential task are necessarily executed in the
order that they arrive.
An arbitrary JLFP policy, however, can violate the sequential tasks
hypothesis. For example, consider two jobs j1, j2 of the same task
such that job_arrival j1 < job_arrival j2. It is possible that a JLFP
priority policy π will assign a higher priority to the second job π
j2 j1 = true. But such a situation would contradict the natural
execution order of sequential tasks. It is therefore sometimes
necessary to restrict the space of JLFP policies to those that assign
priorities in a way that is consistent with sequential tasks.
To this end, we say that a policy respects sequential tasks if, for any
two jobs j1, j2 of the same task, job_arrival j1 ≤ job_arrival j2
implies π j1 j2 = true.

Definition policy_respects_sequential_tasks :=

∀ j1 j2,

job_task j1 == job_task j2 →

job_arrival j1 ≤ job_arrival j2 →

hep_job j1 j2.

End JLFP.

∀ j1 j2,

job_task j1 == job_task j2 →

job_arrival j1 ≤ job_arrival j2 →

hep_job j1 j2.

End JLFP.

Finally, we we define and observe two properties of FP policies.

Consider any FP policy.

To express the common assumption that task priorities are unique, we
define whether the given FP policy is antisymmetric over a task set
ts.

Further, we observe that any FP_policy respects the sequential tasks
hypothesis, meaning that later-arrived jobs of a task don't have higher
priority than earlier-arrived jobs of the same task (assuming that task
priorities are reflexive).

Remark respects_sequential_tasks :

reflexive_priorities → policy_respects_sequential_tasks.

Proof.

move ⇒ REFL j1 j2 /eqP EQ LT.

rewrite /hep_job /FP_to_JLFP EQ.

by eapply (REFL 0).

Qed.

End FP.

End Priorities.

reflexive_priorities → policy_respects_sequential_tasks.

Proof.

move ⇒ REFL j1 j2 /eqP EQ LT.

rewrite /hep_job /FP_to_JLFP EQ.

by eapply (REFL 0).

Qed.

End FP.

End Priorities.

Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Consider a JLFP-policy that indicates a higher-or-equal priority relation.

First, we introduce a relation that defines whether job j1 has
a higher-than-or-equal-priority than job j2 and j1 is not
equal to j2.

Next, we introduce a relation that defines whether a job j1
has a higher-or-equal-priority than job j2 and the task of
j1 is not equal to task of j2.

Definition another_task_hep_job :=

fun j1 j2 ⇒ hep_job j1 j2 && (job_task j1 != job_task j2).

End DerivedPriorityRleations.

fun j1 j2 ⇒ hep_job j1 j2 && (job_task j1 != job_task j2).

End DerivedPriorityRleations.

We add the above observation into the "Hint Database" basic_rt_facts, so Coq
will be able to apply it automatically.

Global Hint Resolve respects_sequential_tasks : basic_rt_facts.