Abstract Response-Time Analysis with Sequential Tasks

In this file, we propose a general framework for response-time analysis (RTA) of uni-processor scheduling of real-time tasks with arbitrary arrival models and sequential tasks, valid for any processor state satisfying the uniprocessor and unit-service assumptions. We prove that the maximum among the solutions of the response-time bound inequalities is a response-time bound for tsk. Note that in this section we do rely on the hypothesis about task sequentiality. This allows us to provide a more precise response-time bound, since jobs of the same task will be executed strictly in the order they arrive. Unlike uniprocessor_response_time_bound_seq in analysis.abstract.ideal.abstract_seq_rta, this theorem does not assume an ideal processor. The non-preemptive interference bound IBF_NP is therefore kept as an explicit parameter.

Consider any type of tasks ...

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

Consider any kind of uniprocessor state model with unit service. Note that unlike the ideal version of this theorem, we do not require ideal_progress_proc_model.

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

Next, consider any 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.

Consider a valid preemption model ...

... and a valid task run-to-completion threshold function. That is, task_rtct 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_arrivals tsk is (1) an arrival bound of tsk and (2) 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.

Unlike uniprocessor_response_time_bound, we assume that (1) tasks are sequential and (2) the interference and interfering workload functions are consistent with the sequential-tasks hypothesis.

Assume we have a constant L that bounds the busy interval of any of tsk's jobs.

Let us abbreviate task tsk's RBF for clarity.

Next, we assume that task_IBF is a bound on the non-self interference incurred by jobs of task tsk (i.e., interference due to sources other than other jobs of tsk).

We define the first-phase IBF IBF_P as the sum of the self-interference bound task_rbf (A + ε) - task_cost tsk and the non-self interference bound task_IBF A Δ. Note that the self-interference term is computed via the task's request-bound function, following the standard sequential-tasks argument.

Next, we assume that IBF_NP is a bound on interference incurred by a job of task tsk during the non-preemptive execution stage. The parameter semantics for IBF_NP is relative_time_to_reach_rtct: IBF_NP F Δ bounds interference in an interval of length Δ given that the job reaches its run-to-completion threshold by time t1 + F. Unlike in analysis.abstract.ideal.abstract_seq_rta, IBF_NP is not derived from the processor model here; it is kept as an explicit parameter to support non-ideal processor models.

We also assume that IBF_NP respects its own parameter, i.e., task_cost tsk + IBF_NP F Δ ≥ F for all F and Δ. Intuitively, this ensures the second-phase bound is at least as large as the first-phase solution.

For clarity, define the search space in terms of IBF_P.

Consider any value R that upper-bounds the solutions of the two-inequality response-time recurrence. That is, for any relative arrival time A from the search space there exists a solution F such that (1) task_rtct tsk + (task_rbf (A + ε) - task_cost tsk) + task_IBF A Δ A F ≤ F, and (2) task_cost tsk + IBF_NP F (A + R) ≤ A + R.

Using task_IBF_implies_job_IBF, we lift the task-level bound task_IBF to the job level, obtaining a valid IBF_P. We then apply uniprocessor_response_time_bound to conclude that R is a response-time bound for tsk.