Abstract RTA Instantiation for FP-Schedulers with Bounded Priority Inversion

In this module we instantiate the abstract response-time analysis (aRTA) for FP-schedulers assuming the ideal uni-processor model and real-time tasks with arbitrary arrival models. The important feature of this instantiation is that it allows reasoning about the notion of priority inversion. However, we do not specify the exact cause of priority inversion (as there may be different reasons for this, like execution of a non-preemptive segment or blocking due to resource locking). We only assume that the duration of priority inversion is bounded. The difference in this RTA and the other RTA for FP (from the file bounded_pi.v) is that here we drop the sequential-tasks assumption and instead explicitly account for self-interference.

We consider tasks and jobs with the listed parameters.

We allow for any work-bearing readiness model. (The work_bearing_readiness restriction is introduced further down because it requires a schedule to be introduced first; see H_job_ready below.)

A. Defining the System Model

We begin by defining the system model. First, we model arrivals using an arrival sequence. We assume that the arrival sequence is valid and that all arriving jobs comply with the WCET assumption.

Next, we consider any fixed-priority policy that is reflexive.

We consider a valid, ideal uniprocessor schedule that follows a work-bearing readiness model.

We model the tasks in the system using a task set ts. We assume that all jobs in the system come from this task set.

We assume that the task set respects the arrival curve defined by max_arrivals.

The task under consideration tsk is contained in ts.

While we do not assume an explicit preemption model, we require that any preemption model under consideration is valid. We also assume that the run-to-completion-threshold of the task tsk is valid.

As mentioned, we assume that the duration of priority inversion incurred by the task tsk is bounded by priority_inversion_bound.

B. Encoding the Scheduling Policy and Preemption Model

Next, we encode the scheduling policy and preemption model using the functions interference and interfering_workload. To this end, we simply reuse the general definitions of interference and interfering workload that apply to any JLFP policy, as defined in the module analysis.abstract.ideal.iw_instantiation.

C. Abstract Work Conservation

Let us recall the abstract and classic notations of work conservation.

We assume that the schedule is work-conserving in the classic sense, which allows us to apply instantiated_i_and_w_are_coherent_with_schedule to conclude that abstract work-conservation also holds.

D. Bounding the Maximum Busy-Window Length

For convenience, we define the following acronyms.

Next, we define L as a positive fixed point of the given equation ...

... and prove that it is a bound on the maximum length of a busy interval.

E. Defining the Interference Bound Function (IBF)

Next, we define task_IBF and prove that task_IBF bounds the interference incurred by any job of tsk. Note that the maxn here is required to avoid the case in which the interval under consideration is shorter than A. While intuitively it might seem that this case is irrelevant, aRTA does not allow for this case to be ignored.

First we prove bounds on self-interference, that is, interference incurred from other jobs of the same task. Note that since we do not require a sequential task model, we need to account for the case of later jobs of the same task causing interference.

Consider any interval [t1, t1 + Δ).

Next, consider any job j of the task tsk that has a positive cost and arrives in the arrival sequence after the interval under consideration has started.

First, we consider the case where the job arrives before the end of the interval under consideration.

In this case, we bound the interference caused by the task under consideration itself by the cost of the workload released by the tasks in the interval (given by the RBF). However, we do not want to account for the job under consideration itself as interference and hence we subtract the cost of the task.

Next, we consider the case where the job arrives after the interval under consideration has ended.

In this case we proceed similarly to the first case. However in order to safely subtract the task cost from the RBF, we need to consider the interval up to the arrival of the job under consideration.

Combining the above two bounds, we obtain the final bound on the self-interference incurred by any job j of task tsk.

Next, we use the above bound on self-interference to state a bound on the total interference incurred by any job j of task tsk.

F. Defining the Search Space

In this section, we define the concrete search space for FP scheduling. Then, we prove that, if a given A is in the abstract search space, then it is also included in the concrete search space. First, let us recall the definition of the abstract search space as defined in the aRTA framework.

We begin by defining the concrete search space as follows.

To rule out pathological cases with the concrete search space, we assume that the task cost is positive and the arrival curve is non-pathological.

Then, for any relative arrival time A, we prove that, ...

... if A is in the abstract search space, ...

... then A is also in the concrete search space.

G. Stating the Response-Time Bound R

Finally, we define the response-time bound R as follows. Note the condition 0 < F in the equation below. While this condition is not needed in the RTAs for sequential tasks, it is required here to ensure that we consider the least positive fix point.

Next, in this section, we prove that, if a solution to the above equation exists, then a solution to the response-time equation as stated in aRTA also exists.

To rule out pathological cases with the concrete search space, we assume that the task cost is positive and the arrival curve is non-pathological.

We know that, if A is in the abstract search, then it is in the concrete search space, too. We also know that, if A is in the concrete search space, then there exists an R that satisfies H_R_is_maximum. Using these facts, here we prove that, if A is in the abstract search space then, there exists a solution to the response-time equation as stated in the aRTA.

H. Soundness of the Response-Time Bound

Finally, we prove that R is a bound on the response time of task tsk.