Library prosa.analysis.definitions.busy_interval.edf_pi_bound
Require Export prosa.model.task.preemption.parameters.
Require Export prosa.analysis.definitions.sbf.sbf.
Require Export prosa.analysis.definitions.request_bound_function.
Require Export prosa.analysis.definitions.sbf.sbf.
Require Export prosa.analysis.definitions.request_bound_function.
Bound for a Busy-Interval Starting with Priority Inversion under EDF Scheduling
Consider any type of tasks.
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskDeadline Task}.
Context `{TaskMaxNonpreemptiveSegment Task}.
Context `{TaskCost Task}.
Context `{TaskDeadline Task}.
Context `{TaskMaxNonpreemptiveSegment Task}.
Consider an arrival curve max_arrivals.
For brevity, let's denote the relative deadline of a task as D.
Consider an arbitrary task set ts ...
... and let tsk be any task to be analyzed.
Assume that there is a job j of task tsk and that job j's
busy interval starts with priority inversion. Then, the busy
interval can be bounded by a constant
longest_busy_interval_with_pi.
Intuitively, such a bound holds because of the following two
observations. (1) The presence of priority inversion implies an
upper bound on the job arrival offset A < D tsk_o - D tsk,
where A is the time elapsed between the arrival of j and the
beginning of the corresponding busy interval. (2) An upper bound
on the offset implies an upper bound on the
higher-or-equal-priority workload of each task.
Let lp_interference tsk_lp denote the maximum service
inversion caused by task tsk_lp.
Let hep_interference tsk_lp denote the maximum higher-or-equal
priority workload released within D tsk_lp.
let hep_interference tsk_lp :=
\sum_(tsk_hp <- ts | D tsk_hp ≤ D tsk_lp)
task_request_bound_function tsk_hp (D tsk_lp - D tsk_hp) in
\sum_(tsk_hp <- ts | D tsk_hp ≤ D tsk_lp)
task_request_bound_function tsk_hp (D tsk_lp - D tsk_hp) in