Sufficient Condition for Bounded Busy Intervals for RS EDF

In this section, we show that the existence of L such that total_rbf L ≤ SBF L ∧ longest_busy_interval_with_pi ≤ SBF L, where longest_busy_interval_with_pi is the length of the longest busy interval starting with a priority inversion (w.r.t. a job of a task under analysis) and SBF is a supply-bound function, is a sufficient condition for the existence of bounded busy intervals under EDF scheduling with a restricted-supply processor model. The proof uses the following observation. Consider the beginning of a busy interval of a job j to be analyzed. If there is service inversion, one can derive an upper bound on the relative arrival of job j, which in turn can be used to derive a bound on the total higher-or-equal priority workload (longest_busy_interval_with_pi). If there is no service inversion, we use the standard fixpoint approach with total_rbf L.

Consider any type of tasks ...

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

For brevity, let's denote the relative deadline of a task as D.

Consider any kind of fully supply-consuming unit-supply uniprocessor model.

Consider any valid arrival sequence.

Next, consider a schedule of this arrival sequence, ...

... allow for any work-bearing notion of job readiness, ...

... and assume that the schedule is valid.

Assume that jobs have bounded non-preemptive segments.

Furthermore, assume that the schedule respects the scheduling policy.

Recall that busy_intervals_are_bounded_by is an abstract notion. Hence, we need to introduce interference and interfering workload. We will use the restricted-supply instantiations. We say that job j incurs interference at time t iff it cannot execute due to (1) the lack of supply at time t, (2) service inversion (i.e., a lower-priority job receiving service at t), or a higher-or-equal-priority job receiving service.

The interfering workload, in turn, is defined as the sum of the blackout predicate, service inversion predicate, and the interfering workload of jobs with higher or equal priority.

Assume that the schedule is work-conserving in the abstract sense.

Consider an arbitrary task set ts, ...

... assume that all jobs come from the task set, ...

... and that the cost of a job does not exceed its task's WCET.

Let max_arrivals be a family of valid arrival curves.

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

Consider a unit SBF valid in busy intervals (w.r.t. task tsk). That is, (1) SBF 0 = 0, (2) for any duration Δ, the supply produced during a busy-interval prefix of length Δ is at least SBF Δ, and (3) SBF makes steps of at most one.

First, we show that the constant longest_busy_interval_with_pi ts tsk indeed bounds the cumulative interference incurred by job j.

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

Let [t1, t2) be a busy-interval prefix.

Consider an interval [t1, t1 + δ) ⊆ [t1, t2).

Assume that cumulative service inversion of job j in this interval is positive.

The LHS of the following inequality represents all possible interference as well as the cost of the job itself in a prefix of length δ. On the RHS of the inequality, there is a constant longest_busy_interval_with_pi. We prove that this inequality is indeed true. This implies that if the cumulative service inversion of job j is positive, its busy interval cannot possibly be longer than longest_busy_interval_with_pi.

We introduce the main assumption of this section. Let L be any positive constant that satisfies two properties.

First, we assume that SBF L bounds longest_busy_interval_with_pi ts tsk. As discussed, when a busy interval starts with service inversion, one can upper-bound the total interfering workload that a job under analysis incurs via longest_busy_interval_with_pi ts tsk. The time to consume this workload is SBF L.

And second, we assume that total_RBF L ≤ SBF L. When there is no service inversion at the beginning of a busy interval, one can show that there is no carry-in workload (including the lower-priority workload). This allows us to bound interfering workload within a busy interval with total_RBF L without adding an extra + blocking_bound as in the case of the general JLFP bound.

In the following, we prove busy-interval boundedness via a case analysis on two cases: (1) when the busy-interval prefix is at least L time units long and (2) when the busy interval prefix terminates earlier. In either case, we can show that the busy-interval prefix is bounded.

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

As a preparation step, we show that L bounds the relative arrival time of job j.

Consider a time instant t1 such that [t1, job_arrival j]>> is a busy-interval prefix of j.

From the properties of the workload (defined by hypotheses H_L_bounds_bi_with_pi and H_fixed_point), we show that j's arrival time is necessarily less than t1 + L.

We start with the first case, where the busy-interval prefix continues until time instant t1 + L.

Consider a time instant t1 such that [t1, job_arrival j]>> and [t1, t1 + L) are both busy-interval prefixes of job j.

The crucial point to note is that the sum of the job's cost (represented as workload_of_job) and the interfering workload in the interval [t1, t1 + L) is bounded by L due to hypotheses H_L_bounds_bi_with_pi and H_fixed_point.

It follows that t1 + L is a quiet time, which means that the busy prefix ends (i.e., it is bounded).

Next, we consider the case when the interval [t1, t1 + L) is not a busy-interval prefix.

Consider a time instant t1 such that [t1, job_arrival j]>> is a busy-interval prefix of j and [t1, t1 + L) is not.

Lemma job_arrival_is_bounded implies that the busy-interval prefix starts at time t1, continues until job_arrival j + 1, and then terminates before t1 + L. Or, in other words, there is point in time t2 such that (1) j's arrival is bounded by t2, (2) t2 is bounded by t1 + L, and (3) [t1, t2) is busy interval of job j.

Combining the cases analyzed above, we conclude that busy intervals of jobs released by task tsk are bounded by L.