Abstract Response-Time Analysis for Restricted-Supply Processors with Sequential Tasks

In this section we propose a general framework for response-time analysis (RTA) for real-time tasks with arbitrary arrival models and sequential _tasks under uni-processor scheduling subject to supply restrictions, characterized by a given SBF. In this section, we assume tasks to be sequential. This allows us to establish a more precise response-time bound, since jobs of the same task will be executed strictly in the order they arrive.

Consider any type of tasks ...

... 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 that the job costs are no larger than the task costs.

Consider a task set ts ...

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

Consider a valid preemption model ...

... with valid task run-to-completion thresholds. 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.

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 functions characterizing interference and interfering workload.

Let's define a local name for clarity.

We assume that the scheduler is work-conserving.

Unlike the more general, underlying theorem uniprocessor_response_time_bound_restricted_supply, we assume that tasks are sequential.

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

Consider a unit SBF valid in busy intervals (w.r.t. task tsk). That is, (1) SBF 0 = 0, (2) for any duration Δ, the supply produced during a busy-interval prefix of length Δ is at least SBF Δ, and (3) SBF makes steps of at most one.

Next, we assume that task_intra_IBF is a bound on intra-supply interference incurred by task tsk. That is, task_intra_IBF bounds interference ignoring interference due to lack of supply and due to self-interference.

We use the function task_intra_IBF, which satisfies the hypothesis task_intra_interference_is_bounded_by, to construct a new function intra_IBF := (task_rbf (A + ε) - task_cost tsk) + task_intra_IBF A Δ that satisfies the hypothesis intra_interference_is_bounded_by. This is needed to later apply the lemma uniprocessor_response_time_bound_restricted_supply from file restricted_supply/abstract_rta (recall that it requires intra_IBF, not task_intra_IBF). The logic behind intra_IBF is quite simple. Consider a job j of task tsk that arrives exactly A units after the beginning of the busy interval. Then the bound on the total interference incurred by j within an interval of length Δ is no greater than task_rbf (A + ε) - task_cost tsk + task_intra_IBF A Δ. Note that, for sequential tasks, the bound consists of two parts: (1) the part that bounds the interference received from other jobs of task tsk -- task_rbf (A + ε) - task_cost tsk and (2) any other interference that is bounded by task_intra_IBF(tsk, A, Δ).

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_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + task_intra_IBF A F ≤ SBF F, (3) and SBF F + (task_cost tsk - task_rtct tsk) ≤ SBF (A + R).

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

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

To rule out pathological cases with the H_R_is_maximum_seq_rs equation (such as task_cost tsk being greater than task_rbf (A + ε)), we assume that the arrival curve is non-pathological.

To later apply the theorem uniprocessor_response_time_bound_restricted_supply, we need to provide the IBF, which bounds the total interference.

Next we prove that H_R_is_maximum_seq_rs implies H_R_is_maximum_rs from file (.../restricted_supply/abstract_rta.v). In other words, a solution to the response-time recurrence for restricted-supply processor models with sequential tasks can be translated to a solution for the same processor model with non-necessarily sequential tasks.

Finally, we apply the uniprocessor_response_time_bound_restricted_supply theorem, and using the lemmas above, prove that all its requirements are satisfied. Hence, R is a response-time bound for task tsk.