Response-Time Analysis for the ELF Scheduling Policy

In the following, we derive a response-time analysis for ELF schedulers, assuming a workload of sporadic real-time tasks characterized by arbitrary arrival curves executing upon an ideal uniprocessor. To this end, we instantiate the abstract Response-Time Analysis (aRTA) as provided in the prosa.analysis.abstract module. Note that this analysis is currently specific to workloads where each task has bounded nonpreemptive segments. This specificity will be further explained by the assumptions which depend on it. The analysis catering to the more general model with bounded priority inversion remains future work.

A. Defining the System Model

Before any formal claims can be stated, an initial setup is needed to define the system model under consideration. To this end, we next introduce and define the following notions using Prosa's standard definitions and behavioral semantics:

• tasks, jobs, and their parameters,
• the sequence of job arrivals,
• worst-case execution time (WCET) and the absence of self-suspensions,
• the set of tasks under analysis,
• the task under analysis, and, finally,
• an arbitrary schedule of the task set.

Tasks and Jobs

Consider any type of tasks, each characterized by a WCET task_cost, a run-to-completion threshold task_rtct, a maximum non-preemptive segment length task_max_nonpreemptive_segment, an arrival curve max_arrivals, and a relative priority point task_priority_point ...

... and any type of jobs associated with these tasks, where each job has an arrival time job_arrival, a cost job_cost, and an arbitrary preemption model indicated by job_preemptable.

The Job Arrival Sequence

Consider any valid arrival sequence arr_seq.

Absence of Self-Suspensions and WCET Compliance

We assume the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready.

We further require that a job's cost cannot exceed its task's stated WCET.

The Task Set

We consider an arbitrary task set ts...

... and assume that all jobs stem from tasks in this task set.

Furthermore, we assume that max_arrivals is a family of valid arrival curves that constrains the arrival sequence arr_seq, i.e., for any task tsk in ts, max_arrival tsk is (1) an arrival bound of tsk, and ...

... (2) a monotonic function that equals 0 for the empty interval delta = 0.

The Task Under Analysis

Let tsk be any task in ts that is to be analyzed.

We assume that tsk is described by a valid task run-to-completion threshold. That is, there exists a task parameter task_rtct such that task_rtct tsk is

• (1) no larger than tsk's WCET, and
• (2) for any job of task tsk, the job's run-to-completion threshold job_rtct is bounded by task_rtct tsk.

The Schedule

Finally, we consider any arbitrary, valid ideal uni-processor schedule of the given arrival sequence arr_seq.

Now, we assume that the fixed-priority policy FP that parameterizes the ELF policy is...

... reflexive, transitive, and total.

We further assume that the schedule complies with the preemption model ...

... and finally, that it respects the ELF scheduling policy.

B. Interference and Interfering Workload

With the system model in place, the next step is to encode the scheduling policy and preemption model such that aRTA becomes applicable. To this end, we encode the semantics of the scheduling policy and preemption model by instantiating two functions, called interference and interfering_workload. We can simply reuse the existing general definitions of interference and interfering workload that apply to job-level fixed-priority (JLFP) policy (as provided in the module analysis.abstract.ideal.iw_instantiation).

C. Classic and Abstract Work Conservation

We assume that the schedule is work-conserving in the classic sense.

This allows us to apply instantiated_i_and_w_are_coherent_with_schedule to conclude that abstract work-conservation also holds.

D. The Priority Inversion Bound and its Validity

In this file, we break the priority inversion experienced by any job into two categories :

• (1) priority inversion caused by jobs belonging to tasks with lower priority than tsk
• (2) priority inversion caused by jobs belonging to tasks with equal priority as tsk

Note that, by definition of the ELF policy, no job from a task with higher priority than tsk can cause priority inversion. We define a predicate to identify jobs from lower-priority tasks, or tasks for which tsk has higher priority.

We assume there exists a bound on the maximum length of priority inversion from these jobs that is incurred by any job of task tsk.

Similarly, we define a predicate to select jobs whose tasks have equal priority as tsk...

... and assume that there exists a bound on the maximum length of priority inversion caused by them to any job of tsk.

We then define the priority inversion bound as a maximum of the bounds on the two categories. Note that this definition is only applicable when all tasks have bounded nonpreemptive segments.

Now, we define the following predicate to identify tasks that can release jobs.

We also define a predicate to identify equal priority tasks that cannot cause priority inversion for a job j, given that j's busy interval starts that instant t1.

Using the above, we define the condition that an equal-priority task must satisfy for any of its jobs to cause blocking (or priority inversion) to a job j in j's busy interval starting at t1.

Finally, we assume that the priority_inversion_ep_tasks_bound is bounded by the maximum task_cost of tasks which satisfy the above condition. Note that this assumption is valid only for the model where tasks have bounded nonpreemptive segments.

Having defined bounds on two separate categories of priority inversion, we now show that the defined priority_inversion_bound upper-bounds the priority inversion faced by any job belonging to tsk, regardless of its cause.

E. Maximum Busy-Window Length

The next step is to establish a bound on the maximum busy-window length, which aRTA requires to be given. Using the sum of individual request bound functions, we define the request bound function of all tasks with higher-or-equal priority FP (with respect to tsk).

To this end, we assume that we are given a positive value L ...

... that is a fixed point of the following equation.

Given this definition of L, we prove that L bounds the length of the busy window.

F. The Interference-Bound Function

Next, we define the interference task_IBF and prove that task_IBF bounds the interference incurred by any job of tsk. Note that task_IBF only takes the interference from jobs of other tasks into account i.e., self-interference is not included. We first consider the interference incurred due to strictly higher-priority tasks i.e., those which have strictly higher-priority according to the FP policy.

We define the following parameterized end point of the interval during which interfering jobs of equal-priority tasks must arrive. The implicit beginning of the interval is the start of the busy window, i.e., at time t1.

Using this interval end point, we define the bound on the total equal-priority (EP) workload produced during the interval Δ as the sum of the RBFs of all tasks (with equal priority as tsk) in the task set ts (excluding tsk) over the minimum of Δ and ep_task_intf_interval.

Finally, task_IBF for an interval Δ is defined as the sum of priority_inversion_bound, bound_on_total_ep_workload, and total_hp_rbf on Δ.

In this section, we prove the soundness of task_IBF.

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 (in the abstract sense) is given by [t1,t2).

Consider any arbitrary length Δ interval [t1, t1+ Δ) within the busy window.

We define the service needed by jobs belongings to other equal-priority tasks, that have higher-or-equal priority than j...

...and show that it is equivalent to the cumulative interference incurred by j due to these jobs.

Similarly, we define the service required by jobs belonging to other strictly higher-priority tasks, that have higher-or-equal priority than j, ...

... and show that it is equivalent to the cumulative interference incurred by j due to these jobs.

Assume the arrival time of j relative to the busy window start is given by A.

First, consider the case where ep_task_intf_interval ≤ Δ.

Consider any equal-priority task tsk_o distinct from tsk. Assume that tsk_o is in ts.

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

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

... then the workload of jobs satisfying the predicate hp_jobs_from in the interval [t1,t1 + Δ) is bounded by the workload in the interval [t1, t1 + ep_task_intf_interval [tsk_o] [A]).

Then, we establish that the cumulative interference incurred by j due to all higher-or-equal-priority jobs from equal-priority tasks is bounded by the bound_on_ep_workload, ...

... and that the cumulative interference incurred by j due to all higher-or-equal priority jobs from higher-priority tasks is bounded by the total_hp_rbf].

Finally, we use the above two lemmas to prove that task_IBF bounds the interference incurred by tsk.

G. Defining the Search Space

In this section, we define the concrete search space for ELF. Then, we prove that, if a given A is in the abstract search space, then it is also included in the concrete search space. For tsk, the total interference bound is defined as the sum of the interference due to

• (1) jobs belonging to the same task (self interference) and
• (2) jobs belonging to other tasks task_IBF.

In the case of ELF, of the four terms that constitute the total interference bound, only the priority_inversion_bound, task RBF and the bound on total equal-priority workload are dependent on the offset A. Therefore, in order to define the concrete search space, we define predicates that capture when these values change for successive values of the offset A.

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 total equal-priority workload changes.

In this section, we prove that, for any job j of task 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.

Any point A in the abstract search space...

... is also in the concrete search space.

H. The Response-Time Bound R

Finally, we define the response-time bound R as the maximum offset by which any job j of task tsk has completed.

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

We have established that if A is in the abstract search then it is in the concrete search space, too. We also know by assumption 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.

I. Soundness of the Response-Time Bound

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