# Library prosa.analysis.definitions.workload.edf_athep_bound

Require Export prosa.analysis.definitions.request_bound_function.

# Bound on Higher-or-Equal Priority Workload under EDF 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 EDF scheduling.
Section EDFWorkloadBound.
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 `{TaskDeadline Task}.
Context `{MaxArrivals Task}.
Consider an arbitrary task set ts ...
Variable ts : seq Task.
... and a task tsk.
Variable tsk : Task.
For brevity, let's denote the relative deadline of a task as D ...
Let D tsk := task_deadline tsk.
... and let's use the abbreviation rbf for the task request-bound function.
Let rbf := task_request_bound_function.
Finally, we define an upper bound on workload received from jobs with higher-than-or-equal priority that come from other tasks.
Definition bound_on_athep_workload A Δ :=
\sum_(tsk_o <- ts | tsk_o != tsk)
rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
End EDFWorkloadBound.