Require Export prosa.model.priority.classes.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

(** * 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 the corresponding FP policy. *)
Instance NumericFP (Task : TaskType) `{TaskPriority Task} : FP_policy Task :=
{
  hep_task (tsk1 tsk2 : Task) := task_priority tsk1 >= task_priority tsk2
}.
The default value for instance locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding instances outside of sections without
specifying an explicit locality attribute is therefore
deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example:
"#[export] Instance Foo : Bar := baz."
[deprecated-instance-without-locality,deprecated]

(** In this section, we prove a few basic properties of numeric fixed priorities. *)
Section Properties.

  (**  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 NFP_is_reflexive : reflexive_priorities.
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task
reflexive_priorities
  Proof.
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task
reflexive_priorities by move=> ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFP. Qed.

  (** The resulting priority policy is transitive. *)
  Lemma NFP_is_transitive : transitive_priorities.
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task
transitive_priorities
  Proof.
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task
transitive_priorities
    move=> t y x z.
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task
t: instant
y, x, z: Job
hep_job_at t x y ->
hep_job_at t y z -> hep_job_at t x z
    rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFP.
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task
t: instant
y, x, z: Job
task_priority (job_task y) <=
task_priority (job_task x) ->
task_priority (job_task z) <=
task_priority (job_task y) ->
task_priority (job_task z) <=
task_priority (job_task x)
    by move=> PRIO_yx PRIO_zy; apply leq_trans with (n := task_priority (job_task y)).
  Qed.

  (** The resulting priority policy is total. *)
  Lemma NFP_is_total : total_priorities.
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task
total_priorities
  Proof.
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task
total_priorities by move=> t j1 j2; apply leq_total. Qed.

End Properties.

(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
    will be able to apply them automatically. *)
Global Hint Resolve
     NFP_is_reflexive
     NFP_is_transitive
     NFP_is_total
  : basic_facts.