Abstract Response-Time Analysis

In this module, we propose the general framework for response-time analysis (RTA) of uni-processor scheduling of real-time tasks with arbitrary arrival models. 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 the task under analysis.

Consider any type of tasks ...

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

Consider any kind of processor state model.

Consider any arrival and any schedule of this arrival sequence.

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.

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 the length of any busy interval of task tsk.

Note that response-time analyses are static analyses and by definition have no access to dynamic information of an individual execution of a system. However, oftentimes some dynamic information can improve the tightness of a response-time bound. For example, in case of a model with sequential tasks, information about relative arrival time of a job can be used to bound the maximum self-interference. To gain access to some dynamic information for a response-time recurrence, one can assume that an execution of a system satisfies a statically defined predicate. Then a response-time bound can be calculated by considering a family of inputs to the predicate that covers all the relevant dynamic scenarios. To give a concrete example, one can (1) assume that any job j of a task tsk arrives exactly A time units after the beginning of j's busy interval, (2) calculate the response-time bound of tsk as if the assumption of step (1) was satisfied, and (3) try all the possible As. That results in a "relative-arrival"-aware analysis. The idea we will employ in this file is that one can use more sophisticated dynamic information in a response-time recurrence. In the following, we consider a case when information about (1) relative arrival time of a job and (2) relative time when any job of task tsk receives at least task_rtc tsk units of service is used in the response-time recurrence. Next, the response-time analysis will proceed in a sequence of stages. A stage defines the set of sources of interference that can postpone the execution of a job. Note that this separation is mostly a design question. And for different models there might be a varying number of stages with different meanings. For our purposes, we consider two stages. First stage: A job j can be (1) preempted because of the presence of higher-or-equal priority workload and (2) make no progress due to some other reason (spinning, lack of supply, and so on). To bound all this interference we introduce an interference bound function IBF_P. Note that IBF_P (1) counts any job with higher-or-equal priority as interference and (2) depends on the relative arrival time of a job. To bound time that j spends in the first stage, we need to find a fixpoint of equation F : task_rtc tsk + IBF_P tsk A F ≤ F. To formalize the dependency of IBF_P on the relative arrival time in Coq, we introduce a predicate that tests whether a job j arrives exactly A time units after the beginning of its busy interval, which is unique (if it exists).

Next, consider a valid interference bound function IBF_P that can use information about relative time arrival of a job of task tsk. Recall that an interference bound function gives a bound on the cumulative interference incurred by jobs of task tsk.

Second stage: Job j reaches its run-to-completion threshold. After this point the job cannot be preempted by a high-or-equal priority job (so we can forget about any task-generated workload). At this stage, the only reason why the job cannot make progress is due to lack of supply or similar. To bound time that j spends in the second stage we use IBF_NP. Note that the amount of interference may depend on the relative time when job j receives task_rtc tsk units of service; hence, IBF_NP depends on this parameter. Also, notice that IBF_NP still bounds interference starting from the beginning of the busy window, even though it can use the solution of the first fixpoint equation. To formalize the dependency of IBF_NP on the relative time when job j receives task_rtc tsk units of service in Coq, we introduce a predicate that tests whether a job j has more than task_rtc tsk units of service at a time instant t1 + F, where t1 is the beginning of j's busy interval. The first conjunct of the proposition is needed to derive a fact that by time t1 + F job j does not receive any interference from higher-or-equal priority jobs.

Next, consider a valid interference bound function IBF_NP that can use information about the relative time when any given job of task tsk receives at least task_rtc tsk units of service.

In addition, we assume that IBF_NP indeed takes into account information received in the first stage. Specifically, we assume that the sum of tsk's cost and IBF_NP tsk F Δ is never smaller than F. This intuitively means that the second stage cannot have a solution that is smaller than the solution to the first stage.

Given IBF_P and IBF_NP we construct a response-time recurrence. 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 task_rtc tsk + IBF_P tsk A F ≤ F and task_cost tsk + IBF_NP tsk F (A + R) ≤ A + R.

Proof of the Theorem

In the next section we show a detailed proof of the main theorem that establishes that R is indeed a response-time bound of task tsk.

Consider any job j of tsk with a positive cost. Note that the assumption about positive job cost is needed to apply hypothesis H_bounded_busy_interval_exists. Later, we consider the case when job_cost j = 0 as well. This way, we ensure that this assumption does not propagate further.

Assume we have a busy interval [t1, t2) of job j.

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

First, note that job_arrival j is equal to t1 + A.

Since the length of the busy interval is bounded by L, the relative arrival time A of job j is less than L.

In order to prove that R is a response-time bound of job j, we use hypothesis H_R_is_maximum. Note that the relative arrival time A does not necessarily belong to the search space. However, earlier (see file abstract.search_space) we have proven that for any A there exists another A_sp from the search space that shares the same IBF_P value. Moreover, since the function IBF_P(A, ⋅) is equivalent to the function IBF_P(A_sp, ⋅), a solution F for task_rtc tsk + IBF_P tsk A_sp F ≤ F also is a solution for task_rtc tsk + IBF_P tsk A F ≤ F. Thus, despite the fact that the relative arrival time may not lie in the search space, we can still use the assumption H_R_is_maximum. More formally, consider any A_sp such that:

(a) A_sp is less than or equal to A.

(b) IBF_P A x is equal to IBF_P A_sp x for all x less than L.

(c) A_sp is in the search space.

(d) F such that ...

... F is a solution of the response-time recurrence.

And finally, (e) task_cost tsk + IBF_NP tsk F (A_sp + R) is no greater than A_sp + R.

Case 1

First, we consider the case where the solution F is so large that the value of t1 + F goes beyond the busy interval. Depending on the pessimism of IBF_P and IBP_NP this might be either possible or impossible. Regardless, the response-time bound can be easily proven, since any job that completes by the end of the busy interval remains completed.

By assumption, suppose that t2 is less than or equal to t1 + F.

Then we prove that job_arrival j + R is no less than t2.

But since we know that the job is completed by the end of its busy interval, we can show that job j is completed by job arrival j + R.

Case 2

Next, we consider the case where the solution of the first recurrence is small (t1 + F < t2), but the solution of the second fixpoint goes beyond the busy interval. Although this case may be (also) impossible, the response-time bound can be easily proven, since any job that completes by the end of the busy interval remains completed.

Assume that t1 + F is less than t2, ...

... but t1 + (A_sp + R) is at least t2.

Then we prove that job_arrival j + R is no less than t2.

But since we know that the job is completed by the end of its busy interval, we can show that job j is completed by job arrival j + R.

Case 3

Next, we consider the case when both solutions are smaller than the length of the busy interval.

So, assume that t1 + F and t1 + (A_sp + R) are both smaller than t2.

First note that F is indeed less than L.

Next we consider two sub-cases.

Case 3.1

The cost of job j is smaller than or equal to the run-to-completion threshold of task tsk.

We assume that job_cost j ≤ task_rtc tsk.

Then we apply lemma j_receives_enough_service with parameters progress_of_job := job_cost j and delta := F to obtain the fact that the service of j by time t1 + F is no less than job_cost j (that is, the job is completed).

Case 3.2

The cost of job j is greater than or equal to the run-to-completion threshold of task tsk .

We assume that task_rtc tsk ≤ job_cost j.

We apply lemma j_receives_enough_service with parameters progress_of_job := task_rtc tsk and delta := F to obtain the fact that the service of j by time t1 + F is no less than task_rtc tsk.

Next, we again apply lemma j_receives_enough_service with parameters progress_of_job := job_cost j and delta := A_sp + R to obtain the fact that the service of j by time t1 + (A_sp + R) is no less than job_cost j.

Either way, job j is completed by time job_arrival j + R.

Response-Time Bound

Using the lemmas above, we prove that R is a response-time bound.