Abstract Response-Time Analysis with sequential tasks

In this section we propose the general framework for response-time analysis (RTA) of uni-processor scheduling of real-time tasks with arbitrary arrival models and sequential tasks. We prove that the maximum among the solutions of the response-time bound recurrence for some set of parameters 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 function, 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 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.

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, (2) for any job of task tsk job_rtct is bounded by task_rtct.

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.

Unlike the previous theorem uniprocessor_response_time_bound_ideal, we assume that (1) tasks are sequential, moreover (2) functions interference and interfering_workload are consistent with the hypothesis of sequential tasks.

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

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

Let's define some local names for clarity.

Given any job j of task tsk that arrives exactly A units after the beginning of the busy interval, 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's IBF Δ. Note that in case of 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_IBF(tsk, A, Δ).

Note that since we consider the modified interference bound function, the search space has also changed. One can see that the new search space is guaranteed to include any A for which task_rbf (A) ≠ task_rbf (A + ε), since this implies the fact that total_interference_bound (A, Δ) ≠ total_interference_bound (A + ε, Δ).

Consider any value R, and assume that for any relative arrival time A from the search space there is a solution F of the response-time recurrence that is bounded by R. In contrast to the formula in "non-sequential" Abstract RTA, assuming that tasks are sequential leads to a more precise response-time bound. Now we can explicitly express the interference caused by other jobs of the task under consideration. To understand the right part of the fix-point in the equation, it is helpful to note that the bound on the total interference (bound_of_total_interference) is equal to task_rbf (A + ε) - task_cost tsk + task_IBF tsk A Δ. Besides, a job must receive enough service to become non-preemptive task_lock_in_service tsk. The sum of these two quantities is exactly the right-hand side of the equation.

Since we are going to use the uniprocessor_response_time_bound_ideal theorem to prove the theorem of this section, we have to show that all the hypotheses are satisfied. Namely, we need to show that H_R_is_maximum_seq implies H_R_is_maximum. Note that the fact that hypotheses H_sequential_tasks, H_i_w_are_task_consistent and H_task_interference_is_bounded_by imply H_job_interference_is_bounded is proven in the file analysis/abstract/IBF/task. In this section, we prove that H_R_is_maximum_seq implies H_R_is_maximum.

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

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

We prove that H_R_is_maximum holds.

We apply the uniprocessor_response_time_bound_ideal theorem, and using the lemmas proven earlier, we prove that all the requirements are satisfied. So, R is a response-time bound.