Require Export prosa.model.priority.classes.
[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]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_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]
Require Export prosa.model.priority.gel.

(** * ELF Priority Policy  *)

(** We define the class of "EDF-Like-within-Fixed-priority (ELF)" scheduling
    policies. ELF scheduling is a (large) subset of the class of JLFP scheduling
    policies that can be structurally viewed as a combination of the fixed-priority
    and GEL scheduling policies. In ELF scheduling, we take an FP policy as an
    argument, and each task has a constant "priority-point offset". Each job's
    (absolute) "priority point" is given by its arrival time plus its task's
    priority-point offset.

    Given two jobs, their relative priority order is first determined by the fixed-
    priority policy, i.e., the priority order of their respective tasks. However,
    if their tasks have equal fixed priority, then it is determined by the jobs'
    priority points (GEL), with the interpretation that an earlier priority
    point implies higher priority. It can be viewed as an FP Policy with the GEL
    scheduling policy employed to resolve ties.

    The FP policy is a particular case of ELF if all the tasks are assigned distinct
    priorities. GEL (and hence, FIFO and EDF) are special cases of ELF if all tasks
    have equal priority according to the FP policy.  *)

(** In order to define the policy, we introduce the required context. *)
Section ELF.

  (** 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} .
  (** We parameterize the ELF priority policy based on a fixed-priority policy.
      Job [j1] is assigned a higher priority than job [j2] if either the task
      associated with [j1] has a strictly higher priority than the task
      associated with [j2], or if their tasks have equal priorities and the
      relative priority point of [j1] is less than or equal to the relative
      priority point of [j2], similar to the GEL policy.

      NB: The <<| 0>> at the end of the next line is a priority hint for
          type-class resolution, meaning this type class should be picked with
          highest priority in ambiguous contexts. *)
  #[export] Instance ELF (fp : FP_policy Task) : JLFP_policy Job | 0:=
  {
      hep_job (j1 j2 : Job) :=
        (** Recall the notion of a higher-priority job under the GEL policy as
            [gel_hep_job]. *)
        let gel_hep_job := @hep_job _ (GEL Job Task) in
        (** Under the ELF policy, job [j1] has higher-or-equal priority than job
            [j2] if (1) [j1]'s task has higher priority than [j2]'s task... *)
          hp_task (job_task j1) (job_task j2)
              (** ...or (2) if the two tasks have the same priority and [j1] has
                  higher priority than [j2] according to the GEL policy. *)
            || (hep_task (job_task j1) (job_task j2)
               && gel_hep_job j1 j2)
  }.

End ELF.