Library prosa.analysis.definitions.workload.elf_athep_bound

Require Export prosa.analysis.definitions.request_bound_function.
Require Import prosa.model.priority.elf.

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.