Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[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.util.rel.
Require Export prosa.util.list.

(** * The FP, JLFP, and JLDP Priority Classes *)

(** In this module, we define the three well-known classes of priority
    relations: (1) fixed-priority (FP) policies, (2) job-level fixed-priority
    (JLFP) polices, and (3) job-level dynamic-priority (JLDP) policies, where
    (2) is a subset of (3), and (1) a subset of (2). *)

(** As a convention, we use "hep" to mean "higher or equal priority." *)

(** We define an FP policy as a relation among tasks, ... *)
Class FP_policy (Task: TaskType) := hep_task : rel Task.

(** ... a JLFP policy as a relation among jobs, and ... *)
Class JLFP_policy (Job: JobType) := hep_job : rel Job.

(** ... a JLDP policy as a relation among jobs that may vary over time. *)
Class JLDP_policy (Job: JobType) := hep_job_at : instant -> rel Job.

(** 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.  *)


(** ** Properties of Priority Policies *)

(** In the following section, we define key properties of common priority
    policies that proofs often depend on. *)

Section Priorities.

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

  (**  ... and any type of jobs associated with these tasks, ... *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.

  (** .. and assume that jobs have a cost and an arrival time. *)
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

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

    (** Consider any JLDP policy. *)
    Context (JLDP : JLDP_policy Job).

    (** We define what it means for a JLDP policy to be reflexive, transitive,
        and total. *)

    (** A JLDP policy is reflexive if the relation among "jobs" is reflexive at
        "every point in time." *)
    Definition reflexive_priorities := forall t, reflexive (hep_job_at t).

     (** A JLDP policy is transitive if the relation among "jobs" is transitive at
        "every point in time." *)
    Definition transitive_priorities := forall t, transitive (hep_job_at t).

    (** A JLDP policy is total if the relation among "jobs" is total at
        "every point in time." *)
    Definition total_priorities := forall t, total (hep_job_at t).

  End JLDP.

  (** Next, we define properties of JLFP policies. *)
  Section JLFP.

    (** Consider any JLFP policy. *)
    Context (JLFP : JLFP_policy Job).

    (** We define what it means for a JLFP policy to be reflexive, transitive,
        and total. *)

    (** A JLFP policy is reflexive if the relation among "jobs" is reflexive. *)
    Definition reflexive_job_priorities := reflexive hep_job.

    (** A JLFP policy is transitive if the relation among "jobs" is transitive. *)
    Definition transitive_job_priorities := transitive hep_job.

    (** A JLFP policy is total if the relation among "jobs" is total. *)
    Definition total_job_priorities := total hep_job.

    (** 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 :=
      forall j1 j2,
        job_task j1 == job_task j2 ->
        job_arrival j1 <= job_arrival j2 ->
        hep_job j1 j2.

  End JLFP.

  (** Finally, we define properties of FP policies. *)
  Section FP.

    (** Consider any FP policy. *)
    Context (FP : FP_policy Task).

    (** We define what it means for an FP policy to be reflexive, transitive,
        and total. *)

    (** An FP policy is reflexive if the relation among "tasks" is reflexive. *)
    Definition reflexive_task_priorities := reflexive hep_task.

    (** An FP policy is transitive if the relation among "tasks" is transitive. *)
    Definition transitive_task_priorities := transitive hep_task.

    (** An FP policy is total if the relation among "tasks" is total. *)
    Definition total_task_priorities := total hep_task.

    (** To express the common assumption that task priorities are unique, we
        define whether the given FP policy is antisymmetric over a task set
        [ts]. *)
    Definition antisymmetric_over_taskset (ts : seq Task) :=
      antisymmetric_over_list hep_task ts.

  End FP.

End Priorities.

(** ** Derived Priority Relations *)

(** In the following section, we derive two auxiliary priority
    relations for JLFP policies. *)
Section JLFPDerivedPriorityRelations.

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}.

  (**  ... and any type of jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.

  (** Consider a JLFP-policy that indicates a higher-or-equal priority relation. *)
  Context `{JLFP_policy Job}.

  (** First, we introduce a relation that defines whether job [j1] has
      a priority no less than job [j2] and [j1] is not
      equal to [j2]. *)
  Definition another_hep_job j1 j2 := hep_job j1 j2 && (j1 != j2).

  (** Next, we introduce a relation that defines whether a job [j1]
      has priority no less than job [j2] and the task of
      [j1] is not equal to task of [j2]. *)
  Definition another_task_hep_job j1 j2 :=
    hep_job j1 j2 && (job_task j1 != job_task j2).

  (** Finally, we introduce a relation that defines whether a job [j1]
      has priority no less than another job [j2] from the
      same task. *)
  Definition another_hep_job_of_same_task j1 j2 :=
    another_hep_job j1 j2 && (job_task j1 == job_task j2).

End JLFPDerivedPriorityRelations.

(** In the following section, we derive two more auxiliary priority relations
    for FP policies to incorporate the notions of higher and equal priority of tasks. *)
Section FPDerivedPriorityRelations.

  (** Consider any type of tasks and an FP policy that indicates a higher-or-equal
      priority relation on the tasks. *)
  Context {Task : TaskType} {FP_policy : FP_policy Task}.

  (** First, we introduce a relation that defines whether task [tsk1] has higher
      priority than task [tsk2] ,i.e., [tsk1] has higher-or-equal priority than
      [tsk2] but [tsk2] does not have higher-or-equal priority than [tsk1].*)
  Definition hp_task (tsk1 tsk2 : Task) :=
    hep_task tsk1 tsk2 && ~~ hep_task tsk2 tsk1.

  (** Next, we introduce a relation that defines whether task [tsk1] has equal
      priority as task [tsk2] ,i.e., [tsk1] has higher-or-equal priority than [tsk2]
      and [tsk2] has higher-or-equal priority than [tsk1]. *)
  Definition ep_task (tsk1 tsk2 : Task) :=
    hep_task tsk1 tsk2 && hep_task tsk2 tsk1.

End FPDerivedPriorityRelations.