Project Page Index Table of Contents

# Library prosa.analysis.abstract.IBF.supply_task

Require Export prosa.analysis.abstract.abstract_rta.
Require Export prosa.analysis.abstract.IBF.supply.
Require Export prosa.analysis.abstract.IBF.task.
In this module, we define a task-intra-supply-interference-bound function (task_intra_IBF). Function task_intra_IBF bounds interference ignoring interference due to lack of supply and due to self-interference.
Section TaskIntraInterferenceBound.
Consider any type of job associated with any type of tasks ...
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
... with arrival times and costs.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any kind of processor state model.
Context {PState : ProcessorState Job}.
Consider any arrival sequence ...
Variable arr_seq : arrival_sequence Job.
... and any schedule of this arrival sequence.
Variable sched : schedule PState.
Let tsk be any task that is to be analyzed.
Variable tsk : Task.
Assume we are provided with abstract functions characterizing interference and interfering workload.
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
Next, we introduce the notions of "task intra-supply interference" and "task intra-supply IBF". Using these notions, one can separate the interference due to the lack of supply or due to self-interference from all the other sources of interference.
Let us define a predicate stating that (1) there is supply at time t and (2) the task of a job j is not scheduled at a time instant t.
Definition nonself_intra (j : Job) (t : instant) :=
(nonself arr_seq sched j t) && has_supply sched t.
We define task intra-supply interference as interference conditioned on the fact that there is supply and there is no self-interference.
Definition task_intra_interference (j : Job) (t : instant) :=
cond_interference nonself_intra j t.
Consider an interference bound function task_intra_IBF.
Variable task_intra_IBF : duration → duration → work.
We say that task intra-supply interference is bounded by task_intra_IBF iff, for any job j of task tsk, the cumulative task intra-supply interference within the interval `[t1, t1 + R)` is bounded by task_intra_IBF(A, R).
Definition task_intra_interference_is_bounded_by :=
cond_interference_is_bounded_by
arr_seq sched tsk task_intra_IBF
(relative_arrival_time_of_job_is_A sched) nonself_intra.
End TaskIntraInterferenceBound.