Library prosa.analysis.abstract.IBF.task

In this section, we define a notion of task interference-bound function task_IBF. Function task_IBF bounds interference that excludes interference due to self-interference.

Consider any type of job associated with any type of tasks...

... with arrival times and costs.

Consider any kind of processor state model.

Consider any arrival sequence ...

... and any schedule of this arrival sequence.

Let tsk be any task that is to be analyzed.

Assume we are provided with abstract functions for interference and interfering workload.

Next we introduce the notion of task interference. Intuitively, task tsk incurs interference when some of the jobs of task tsk incur interference. As a result, tsk cannot make any progress. More formally, consider a job j of task tsk. The task experiences interference at time t if job j experiences interference (interference j t = true) and task tsk is not scheduled at time t. Let us define a predicate stating that the task of a job j is not scheduled at a time instant t.

We define task interference as conditional interference where nonself is used as the predicate. This way, task_interference j t is false if the interference experienced by a job j is caused by a job of the same task.

Next, we define the cumulative task interference.

Consider an interference bound function task_IBF.

We say that task interference is bounded by task_IBF iff for any job j of task tsk cumulative task interference within the interval [t1, t1 + R) is bounded by function task_IBF(tsk, A, R).

In the following section, we prove that, under certain assumptions defined next, the fact that a function task_IBF tsk A R satisfies hypothesis task_interference_is_bounded_by implies that a function (task_rbf (A + ε) - task_cost tsk) + task_IBF tsk A R satisfies job_interference_is_bounded_by. In other words, the self-interference can be bounded by the term (task_rbf (A + ε) - task_cost tsk), where A is the relative arrival time of a job under analysis.

Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Consider any kind of ideal uni-processor state model.

Consider any valid arrival sequence with consistent, non-duplicate arrivals...

... and any ideal schedule of this arrival sequence.

... where jobs do not execute before their arrival nor after completion.

Assume that the job costs are no larger than the task costs.

Consider an arbitrary task set.

Let tsk be any task in ts that is to be analyzed.

Let max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts, max_arrival tsk is (1) an arrival bound of tsk, and (2) it is a monotonic function that equals 0 for the empty interval delta = 0.

Assume we are provided with abstract functions for interference and interfering workload.

We assume that the schedule is work-conserving.

Let's define some local names for clarity.

When assuming sequential tasks, we need to introduce an additional hypothesis to ensure that the values of interference and workload remain consistent with the priority policy. To understand why, let us consider a case where the sequential task assumption does not hold, and then work backwards. Consider a fully preemptive policy that assigns the highest priority to the job that was released last. Then, if there is a pending job j of a task tsk, it is not a part of a busy interval of the next job j' of the same task. In this case, both the interference and the interfering workload of job j' will simply ignore job j. Thus, it is possible to have a quiet time (for j') even though j is pending. Now, assuming that our priority policy ensures that tasks are sequential, the situation described above is impossible (job j will always have a higher-or-equal priority than job j'). Hence, we need to rule our interference and interfering workload instantiations that do not conform to the sequential tasks assumption. We ensure the consistency by assuming that, when a busy interval of a job j of task tsk starts, both the cumulative task workload and the task service must be equal within the interval [0, t1). This implies that a busy interval for job j cannot start if there is another pending job of the same task tsk.

To prove the reduction from task_IBF to job_IBF, we need to ensure that the scheduling policy, interference, and interfering workload all respect the sequential tasks hypothesis. For this, we assume that (1) tasks are sequential and (2) functions interference and interfering_workload are consistent with the hypothesis of sequential tasks.

Next, we assume that task_IBF is a bound on interference incurred by the task.

Before proceed to the main proof, we first show a few simple lemmas about the completion of jobs from the task considering the busy interval of the job under consideration.

Consider any two jobs j1 j2 of tsk.

Consider the busy interval [t1, t2) of job j1.

We prove that if a job from task tsk arrived before the beginning of the busy interval, then it must be completed before the beginning of the busy interval

Next we prove that if a job is pending after the beginning of the busy interval [t1, t2) then it arrives after t1.

In this section we show that there exists a bound for cumulative interference for any job of task tsk.

Consider any job j of tsk.

Consider the busy interval [t1, t2) of job j.

Let's define A as a relative arrival time of job j (with respect to time t1).

Consider an arbitrary time x ...

... such that t1 + x is inside the busy interval ...

... and job j is not completed by time t1 + x.

In this section, we show that the cumulative interference of job j in the interval [t1, t1 + x) is bounded by the sum of the task workload in the interval [t1, t1 + A + ε) and the cumulative interference of j's task in the interval [t1, t1 + x). Note that the task workload is computed only on the interval [t1, t1 + A + ε). Thanks to the hypothesis about sequential tasks, jobs of task tsk that arrive after t1 + A + ε cannot interfere with j.

We start by proving a simpler analog of the lemma that states that at any time instant t ∈ [t1, t1 + x) the sum of interference j t and scheduled_at j t is no larger than the sum of the service received by jobs of task tsk at time t and task_iterference tsk t. Next we consider 4 cases.

Consider an arbitrary time instant t ∈ [t1, t1 + x).

Assume the processor is idle at time t.

In case when the processor is idle, one can show that interference j t = 1, service_at j t = 0. But since interference doesn't come from a job of task tsk task_interference tsk = 1. Which reduces to 1 ≤ 1.

Assume a job j' from another task is scheduled at time t.

If a job j' from another task is scheduled at time t, then interference j t = 1, served_at j t = 0. But since interference doesn't come from a job of task tsk task_interference tsk = 1. Which reduces to 1 ≤ 1.

Assume a job j' of task tsk is scheduled at time t but receives no service.

If a job j' of task tsk is scheduled at time t, then interference j t = 1, service_at j t = 0. Moreover, since interference comes from a job of the same task task_interference tsk = 0. However, in this case service_of_jobs of tsk = 1. Which reduces to 1 ≤ 1.

Before proceeding to the last case, let us note that the sum of interference and the service of j at t always equals to 1.

Assume that a job j' is scheduled at time t and receives service.

If job j' is served at time t, then service_of_jobs of tsk = 1. With the fact that interference + service_at = 1, we get the inequality to 1 ≤ 1.

We use the above case analysis to prove that any time instant t ∈ [t1, t1 + x) the sum of interference j t and scheduled_at j t is no larger than the sum of the service received by jobs of task tsk at time t and task_iterference tsk t.

Next we prove cumulative version of the lemma above.

As the next step, the service terms in the inequality above can be upper-bound by the workload terms.

Finally, we show that the cumulative interference of job j in the interval [t1, t1 + x) is bounded by the sum of the task workload in the interval t1, t1 + A + ε) and the cumulative interference of [j]'s task in the interval <<[t1, t1 + x)>>.

We use the lemmas above to obtain the bound on interference in terms of task_rbf and task_interference.

Finally, we show that one can construct a job IBF from the given task IBF.