# Library prosa.analysis.definitions.workload.bounded

Require Export prosa.model.aggregate.workload.
Require Export prosa.analysis.definitions.busy_interval.classical.

# Workload Bound in an Interval Starting with Quiet Time

In this section, we define the notion of a bound on the total workload from higher-or-equal-priority tasks in an interval that starts with a quiet time.
Section WorkloadBound.
Consider any type of tasks ...
Context {Task : TaskType}.
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobCost Job}.
Context `{JobArrival Job}.
Context `{JobTask Job Task}.
Consider any kind of processor model.
Context `{PState : ProcessorState Job}.
Consider a JLFP policy that indicates a higher-or-equal-priority relation.
Context {JLFP : JLFP_policy Job}.
Consider an arrival sequence ...
Variable arr_seq : arrival_sequence Job.
... and a schedule of this arrival sequence.
Variable sched : schedule PState.
Let tsk be any task.
Variable tsk : Task.
We say that B : duration → duration → work is a bound on the higher-or-equal-priority workload of tasks different from tsk iff, for any job j ∈ tsk and any interval `[t1, t1 + Δ)` that starts with a quiet time (w.r.t. job j), the total workload of higher-or-equal-priority tasks distinct from tsk in the interval `[t1, t1 + Δ)` is bounded by B (job_arrival j - t1) Δ.
Definition athep_workload_is_bounded (B : duration → duration → work) :=
∀ (j : Job) (t1 : instant) (Δ : duration),
job_cost_positive j →
job_of_task tsk j →
quiet_time arr_seq sched j t1 →
workload_of_jobs (another_task_hep_job^~ j) (arrivals_between arr_seq t1 (t1 + Δ))
≤ B (job_arrival j - t1) Δ.
End WorkloadBound.