Abstract Response-Time Analysis for Restricted-Supply Processors (aRSA)

In this section we propose a general framework for response-time analysis (RTA) for real-time tasks with arbitrary arrival models under uni-processor scheduling subject to supply restrictions, characterized by a given SBF. We prove that the maximum (with respect to the set of offsets) among the solutions of the response-time bound recurrence is a response-time bound for tsk. Note that in this section we add additional restrictions on the processor state. These assumptions allow us to eliminate the second equation from aRTA+'s recurrence since jobs experience delays only due to the lack of supply while executing non-preemptively.

Consider any type of tasks with a run-to-completion threshold ...

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

Consider any kind of fully supply-consuming unit-supply processor state model.

Consider any valid arrival sequence.

Consider any restricted supply uniprocessor schedule of this arrival sequence ...

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

Assume we are given valid WCETs for all tasks.

Consider a task set ts...

... and a task tsk of ts that is to be analyzed.

Consider a valid preemption model ...

...and a valid task run-to-completion threshold function. That is, task_rtc tsk is (1) no bigger than tsk's cost and (2) for any job j of task tsk job_rtct j is bounded by task_rtct tsk.

Assume we are provided with abstract functions for Interference and Interfering Workload.

We assume that the scheduler is work-conserving.

Let L be a constant that bounds any busy interval of task tsk.

Consider a valid, unit supply-bound function SBF. That is, (1) SBF 0 = 0, (2) for any duration Δ, the supply produced during a busy interval of length Δ is at least SBF Δ, and (3) SBF makes steps of at most one.

Next, we assume that intra_IBF is a bound on the intra-supply interference incurred by task tsk.

Given any job j of task tsk that arrives exactly A units after the beginning of the busy interval, the bound on the interference incurred by j within an interval of length Δ is no greater than (Δ - SBF Δ) + intra_IBF A Δ.

Next, we instantiate function IBF_NP, which is a function that bounds interference in a non-preemptive stage of execution. We prove that this function can be instantiated as λ tsk F Δ ⟹ (F - task_rtct tsk) + (Δ - SBF Δ - (F - SBF F)). Let us reiterate on the intuitive interpretation of this function. Since F is a solution to the first equation task_rtct tsk + IBF_P A F ≤ F, we know that by time instant t1 + F a job receives task_rtct tsk units of service and, hence, it becomes non-preemptive. Knowing this information, how can we bound the job's interference in an interval [t1, t1 + Δ)>>? Note that this interval starts with the beginning of the busy interval. We know that the job receives F - task_rtct tsk units of interference. In the non-preemptive mode, a job under analysis can still experience some interference due to a lack of supply. This interference is bounded by (Δ - SBF Δ) - (F - SBF F) since part of this interference has already been accounted for in the preemptive part of the execution (F - SBF F).

In the next section, we prove a few helper lemmas.

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 Δ ...

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

... the job j is not completed by time (t1 + Δ).

First, we show that blackout is counted as interference.

Next, we show that interference is equal to a sum of two functions: is_blackout and intra_interference.

As a corollary, cumulative interference during a time interval [t1, t1 + Δ) can be split into a sum of total blackouts in [t1, t1 + Δ) and cumulative intra-supply interference during [t1, t1 + Δ).

Moreover, since the total blackout duration in an interval of length Δ is bounded by Δ - SBF Δ, the cumulative interference during the time interval [t1, t1 + Δ) is bounded by the sum of Δ - SBF Δ and cumulative intra-supply interference during [t1, t1 + Δ).

Next, consider a duration F such that F ≤ Δ and job j has enough service to become non-preemptive by time instant t1 + F.

Then, we show that job j does not experience any intra-supply interference in the time interval [t1 + F, t1 + Δ)>>.

For clarity, let's define a local name for the search space.

We use the following equation to bound the response-time of a job of task tsk. Consider any value R that upper-bounds the solution of each response-time recurrence, i.e., for any relative arrival time A in the search space, there exists a corresponding solution F such that (1) F ≤ A + R, (2) task_rtct tsk + intra_IBF tsk A F ≤ SBF F and SBF F + (task_cost tsk - task_rtct tsk) ≤ SBF (A + R). Note that, compared to "ideal RTA," there is an additional requirement F ≤ A + R. Intuitively, it is needed to rule out a nonsensical situation when the non-preemptive stage completes earlier than the preemptive stage.

In the following section we prove that all the premises of abstract RTA are satisfied.

First, we show that IBF_P correctly upper-bounds interference in the preemptive stage of execution.

Next, we prove that IBF_NP correctly bounds interference in the non-preemptive stage given a solution to the preemptive stage F.

Next, we prove that F is bounded by task_cost tsk + IBF_NP F Δ for any F and Δ. As explained in file analysis/abstract/abstract_rta, this shows that the second stage indeed takes into account service received in the first stage.

Next we prove that H_R_is_maximum_rs implies H_R_is_maximum.

Finally, we apply the uniprocessor_response_time_bound theorem, and using the lemmas above, we prove that all the requirements are satisfied. So, R is a response time bound.