Abstract RTA for GEL-Schedulers with Bounded Priority Inversion

In this module we instantiate the abstract response-time analysis (aRTA) for GEL-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 meaningful 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.

We consider tasks and jobs with the given parameters.

We assume the basic readiness model.

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 is consistent and does not contain duplicates.

We consider a valid, ideal uniprocessor schedule...

... that respects the GEL policy at every preemption point.

We assume that all arrivals have valid job costs.

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 assume 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 priority inversion for the task tsk is bound 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

Next, we define L as the fixed point of the given equation. Given this definition of L, we can apply the theorem instantiated_busy_intervals_are_bounded to prove that L bounds the length of the busy window.

E. Defining task_IBF

Next, we define task_IBF and prove that task_IBF bounds the interference incurred by any job of tsk. Consider the following parametrized interval.

We define the bound on the total higher-or-equal-priority (HEP) workload produced during the interval Δ as the sum of the RBFs of all tasks in the task set ts (excluding tsk) over the minimum of Δ and interval.

Finally, task_IBF for an interval R is defined as the sum of bound_on_total_hep_workload in R and priority_inversion_bound.

For convenience, we define the following acronym.

In this section, we prove the soundness of task_IBF. We start by establishing a bound on the HEP workload.

Consider any job j of task tsk that has a positive job cost and is in the arrival sequence.

Assume the busy interval of j is given by [t1,t2).

Assume the relative arrival time of j is given by A.

Consider any arbitrary interval Δ within the busy window.

Consider the set of jobs arriving in [t1, t1 + Δ).

We define a predicate to identify higher priority jobs coming from the task tsk.

First, consider the case where interval ≤ Δ.

Consider any task tsk_o distinct from tsk. Assume tsk_o is in ts.

If Δ is greater than interval for tsk_o and A, ...

... then the workload of jobs satisfying the predicate GEL_from in the interval [t1,t1 + Δ) is equal to the workload in the interval [t1, t1 + interval [tsk_o] [A]). Note that, we use the functions Z.to_nat to Z.of_nat to convert integers to natural numbers and vice-versa.

Using the above lemma, we prove that bound_on_total_hep_workload bounds the sum of higher-priority workload over all tasks in ts.

Finally, we prove that task_IBF bounds the interference incurred by tsk.

F. Defining the Search Space

In this section, we define the concrete search space for GEL. Then, we prove that, if a given A is in the abstract search space, then it is also included in the concrete search space. In order to define the concrete search space, we define the predicates task_rbf_changes_at, ...

... bound_on_total_hep_workload_changes_at, ...

... and priority_inversion_changes_at.

Finally, we define the concrete search space as the set containing all points less than L at which any of the bounds on priority inversion, task rbf, or bound on total HEP workload changes.

In this section, we prove that for any job j of tsk, if A is in the abstract search space, then it is also in the concrete search space.

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.

For j, the total interference bound is defined as follows.

Consider any point A 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.

In order to connect the concrete definition of R with the shape of response-time bound equation that aRTA expects, we prove the theorem correct_search_space. 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 define the total interference as defined above.

We know that if A is in the abstract search then it is in the concrete search space. 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 the task tsk.