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]


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]


(** * Bound on Higher-or-Equal Priority Workload under ELF Scheduling  *)

(** In this file, we define an upper bound on workload incurred by a
    job from jobs with higher-or-equal priority that come from other
    tasks under ELF scheduling. *)
Section ELFWorkloadBound.

  (** Consider any type of tasks, each characterized by a WCET
      [task_cost], and an arrival curve [max_arrivals]. *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{MaxArrivals Task}.

  (** Suppose the tasks have relative priority points. *)
  Context `{PriorityPoint Task}.

  (** Now consider any task set [ts]. *)
  Variable ts : seq Task.

  (** Consider any FP Policy. *)
  Context {FP : FP_policy Task}.

  (** Now we define, given the arrival offset [A], the length of the interval in which
     a higher or equal priority job from a task [tsk_o] in the same priority band as [tsk]
     may arrive. *)
  Definition ep_task_interfering_interval_length (tsk tsk_o : Task) (A : duration) :=
    ((A + ε)%:R + task_priority_point tsk - task_priority_point tsk_o)%R.

  (** Using the above definition, we now define a bound on the higher-or-equal priority workload
      from tasks in the same priority band as [tsk]. *)
  Definition bound_on_ep_task_workload (tsk : Task) (A : duration) (delta : duration) :=
    let rbf_duration (tsk_o : Task) := minn `|Num.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| delta in
      \sum_(tsk_o <- ts | ep_task tsk tsk_o && (tsk_o != tsk))
        task_request_bound_function tsk_o (rbf_duration tsk_o).

  (** Next we define a bound on the higher-priority workload from tasks in
      higher priority bands than [tsk]. *)
  Definition bound_on_hp_task_workload (tsk : Task) (delta : duration) :=
    total_hp_request_bound_function_FP ts tsk delta.

  (** Finally, we define an upper bound on the workload received from jobs
      with higher-than-or-equal priority that come from other
      tasks. *)
  Definition bound_on_athep_workload tsk A delta :=
    bound_on_hp_task_workload tsk delta + bound_on_ep_task_workload tsk A delta.

End ELFWorkloadBound.