Require Export prosa.model.task.preemption.parameters.
[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.task.arrival.curves.
Require Import prosa.model.priority.elf.
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]

(** * Blocking Bound for ELF *)
(** In this section, we define a bound on the length of a
    non-preemptive segment of a lower-priority job (w.r.t. a task
    [tsk]) under ELF scheduling. *)
Section MaxNPSegmentBlockingBound.

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

  (** ... with relative priority points. *)
  Context `{PriorityPoint Task}.

  (** Consider an arbitrary task set [ts]. *)
  Variable ts : list Task.

  (** Let [max_arrivals] be a family of arrival curves. *)
  Context `{MaxArrivals Task}.

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

  (** Only other tasks that potentially release non-zero-cost jobs are
      relevant, so we define a predicate to exclude pathological
      cases. *)
  Let blocking_relevant (tsk_o : Task) :=
    (max_arrivals tsk_o ε > 0) && (task_cost tsk_o > 0).

  (** Now we define a predicate to only include [blocking_relevant] tasks
      that have a lower priority than [tsk]. *)
  Let lp_tsk_blocking_relevant (tsk : Task) (tsk_o : Task) :=
    (hp_task tsk tsk_o) && (blocking_relevant tsk_o).

  (** Next we define a predicate for filtering [blocking_relevant] tasks
      that have the same priority as [tsk]. *)
  Let ep_tsk_blocking_relevant (tsk : Task) (tsk_o : Task) (A : duration) :=
    let ep_tsk_j_blocking_relevant :=  (task_priority_point tsk_o > A%:R +  task_priority_point tsk)%R in
      (ep_task tsk tsk_o) && ep_tsk_j_blocking_relevant && (blocking_relevant tsk_o).

  (** For a job of a given task [tsk], given the relative arrival offset [A]
      within its busy window, we define the following blocking
      bound. This bound assumes that task are independent (i.e., it
      does not account for possible blocking due to locking
      protocols). *)
  Definition blocking_bound (tsk : Task) (A : duration)  :=
    \max_(tsk_o <- ts | lp_tsk_blocking_relevant tsk tsk_o || ep_tsk_blocking_relevant tsk tsk_o A)
      (task_max_nonpreemptive_segment tsk_o - ε).

End MaxNPSegmentBlockingBound.