Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.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.
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]


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 "[ 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]


(** * Cumulative Priority Inversion for JLFP-models *)
(** In this module we define the notion of cumulative priority inversion for uni-processor for JLFP schedulers. *)
Section CumulativePriorityInversion.
  
  (** 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}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.    

  (** Consider any arrival sequence with consistent arrivals. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
  
  (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
  Variable sched : schedule (ideal.processor_state Job).

  (** Assume a given JLFP policy. *)
  Context `{JLFP_policy Job}. 

  (** In this section, we define a notion of bounded priority inversion experienced by a job. *)
  Section JobPriorityInversionBound.

    (** Consider an arbitrary task [tsk]. *)
    Variable tsk : Task.

    (** Consider any job j of [tsk]. *)
    Variable j : Job.
    Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
    Hypothesis H_job_task : job_of_task tsk j. 

    (** We say that the job incurs priority inversion if it has higher
        priority than the scheduled job. Note that this definition
        implicitly assumes that the scheduler is
        work-conserving. Therefore, it cannot be applied to models
        with jitter or self-suspensions. *)
    Definition is_priority_inversion (t : instant) :=
      if sched t is Some jlp then
        ~~ hep_job jlp j
      else false.

    (** Then we compute the cumulative priority inversion incurred by
         a job within some time interval <<[t1, t2)>>. *)
    Definition cumulative_priority_inversion (t1 t2 : instant) :=
      \sum_(t1 <= t < t2) is_priority_inversion t.

    (** We say that the priority inversion experienced by a job [j] is bounded
        by a constant [B] if the cumulative priority inversion within any busy
        interval prefix is bounded by [B]. *)
    Definition priority_inversion_of_job_is_bounded_by_constant (B : duration) :=
      forall (t1 t2 : instant),
        busy_interval_prefix arr_seq sched j t1 t2 ->
        cumulative_priority_inversion t1 t2 <= B.

    (** More generally, if the priority inversion experienced by a job [j]
        depends on its relative arrival time w.r.t. the beginning of its busy
        interval at a time [t1], we say that the priority inversion of job [j]
        is bounded by a function [B : duration -> duration] if the cumulative
        priority inversion within any busy interval prefix is bounded by [B
        (job_arrival j - t1)] *)
    Definition priority_inversion_of_job_is_bounded_by (B : duration -> duration) :=
      forall (t1 t2 : instant),
        busy_interval_prefix arr_seq sched j t1 t2 ->
        cumulative_priority_inversion t1 t2 <= B (job_arrival j - t1).

  End JobPriorityInversionBound.

  (** In this section, we define a notion of the bounded priority inversion for task. *)
  Section TaskPriorityInversionBound.

    (** Consider an arbitrary task [tsk]. *)
    Variable tsk : Task.

    (** We say that priority inversion of task [tsk] is bounded by a constant
        [B] if all jobs released by the task have cumulative priority inversion
        bounded by [B] *)
    Definition priority_inversion_is_bounded_by_constant (B : duration) :=
      forall (j : Job),
        arrives_in arr_seq j ->
        job_of_task tsk j ->
        job_cost j > 0 ->
        priority_inversion_of_job_is_bounded_by_constant j B.

    (** We say that task [tsk] has bounded priority inversion if all its jobs
        have bounded cumulative priority inversion that depends on its relative
        arrival time w.r.t.  the beginning of the busy interval. *)
    Definition priority_inversion_is_bounded_by (B : duration -> duration) :=
      forall (j : Job),
        arrives_in arr_seq j ->
        job_of_task tsk j ->
        job_cost j > 0 ->
        priority_inversion_of_job_is_bounded_by j B.

  End TaskPriorityInversionBound.

End CumulativePriorityInversion.