Require Import prosa.util.int.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
New coercion path [GRing.subring_closedM;
                   GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.sdivr_closed_div;
                   GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subalg_closedBM;
                   GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.divring_closed_div;
                   GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.divalg_closedBdiv;
                   GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,coercions,default]
Notation "_ - _" was already used in scope
distn_scope. [notation-overridden,parsing,default]
Require Export prosa.model.priority.classes.
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]

(** * GEL Priority Policy  *)

(** We define the class of "Global-EDF-like" (GEL) priority policies,
    as first introduced by Leontyev et al. ("Multiprocessor Extensions
    to Real-Time Calculus", Real-Time Systems, 2011).

    GEL scheduling is a (large) subset of the class of JLFP policies,
    which structurally resembles EDF scheduling, hence the name. Under
    GEL scheduling, each task has a constant "priority point offset."
    Each job's priority point is given by its arrival time plus its
    task's offset, with the interpretation that an earlier priority
    point implies higher priority.

    EDF and FIFO are both special cases of GEL with the offset
    respectively being the relative deadline and zero. *)

(** To begin, we define the offset type. Note that an offset may be negative. *)
Definition offset := int.

(** We define a task-model parameter to express each task's relative priority point. *)
Class PriorityPoint (Task : TaskType) := task_priority_point : Task -> offset.

(** Based on the task-level relative priority-point parameter, we
    define a job's absolute priority point in a straightforward manner.
    To this end, we need to introduce some context first. *)
Section AbsolutePriorityPoint.
  (** For any type of tasks with relative priority points, ... *)
  Context {Job : JobType} {Task : TaskType} `{JobTask Job Task} `{PriorityPoint Task} `{JobArrival Job}.

  (** ... a job's absolute priority point is given by its arrival time
          plus its task's relative priority point. *)
  Definition job_priority_point (j : Job) :=
    ((job_arrival j)%:R + task_priority_point (job_task j))%R.
End AbsolutePriorityPoint.

(** The resulting definition of GEL is straightforward: a job [j1]'s
    priority is higher than or equal to a job [j2]'s priority iff
    [j1]'s absolute priority point is no later than [j2]'s absolute
    priority point.  *)
#[export] Instance GEL (Job : JobType) (Task : TaskType)
          `{PriorityPoint Task} `{JobArrival Job} `{JobTask Job Task} : JLFP_policy Job :=
{
  hep_job (j1 j2 : Job) := (job_priority_point j1 <= job_priority_point j2)%R
}.

(** In this section, we note three basic properties of the GEL policy:
    the priority relation is reflexive, transitive, and total.  *)
Section PropertiesOfGEL.

  (** Consider any type of tasks with relative priority points...*)
  Context {Task : TaskType} `{PriorityPoint Task}.

  (** ...and jobs of these tasks. *)
  Context {Job : JobType} `{JobArrival Job} `{JobTask Job Task}.

  (** GEL is reflexive. *)
  Fact GEL_is_reflexive : reflexive_job_priorities (GEL Job Task).
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
reflexive_job_priorities (GEL Job Task)
  Proof.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
reflexive_job_priorities (GEL Job Task) move=> j; exact: lexx. Qed.

  (** GEL is transitive. *)
  Fact GEL_is_transitive : transitive_job_priorities (GEL Job Task).
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
transitive_job_priorities (GEL Job Task)
  Proof.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
transitive_job_priorities (GEL Job Task) move=> x y z; exact: le_trans. Qed.

  (** GEL is total. *)
  Fact GEL_is_total : total_job_priorities (GEL Job Task).
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
total_job_priorities (GEL Job Task)
  Proof.
Task: TaskType
H: PriorityPoint Task
Job: JobType
H0: JobArrival Job
H1: JobTask Job Task
total_job_priorities (GEL Job Task) move=> j1 j2; exact: le_total. Qed.

End PropertiesOfGEL.

(** We add the above facts into a "Hint Database" basic_rt_facts, so Coq
    will be able to apply them automatically where needed. *)
Global Hint Resolve
     GEL_is_reflexive
     GEL_is_transitive
     GEL_is_total
  : basic_rt_facts.