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, where 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 proceeds by case analysis on whether the busy interval of j starts with service inversion.

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.

The proof of busy-interval boundedness proceeds by case analysis on whether the cumulative service inversion of j is positive or zero. The zero case is handled by the standard total_rbf L fixpoint argument. The positive case, however, requires a different approach: we introduce an auxiliary function longest_busy_interval_with_pi δ and establish here that it is a valid upper bound on the cumulative interference in any interval of length δ with positive service inversion.

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.

Under the above assumptions, we define a function δ ↦ longest_busy_interval_with_pi δ as an upper bound on the cumulative interference incurred by j in an interval [t1, t1 + δ).

Let lp_interference tsk_lp denote the maximum service inversion caused by a task tsk_lp.

Let hp_interference tsk_lp denote the total RBF workload of tasks with a strictly shorter deadline than tsk_lp. The interference on j comes from jobs jo with hep_job jo j, i.e., job_deadline jo ≤ job_deadline j. Since the outer condition requires D tsk_lp > D tsk (strict), we have job_deadline j < job_deadline jlp. Therefore:

                job_deadline jo ≤ job_deadline j < job_deadline jlp

No (HEP) job with job_deadline = D tsk_lp ever interferes with j, so D tsk_hp < D tsk_lp captures precisely the right set of tasks:

                 D tsk_hp   ≤     D tsk    <    D tsk_lp
                     |              |             |
          0 ─────────●──────────────●─────────────●──────→ deadline
                     │<──── hp_interference ─────>│
                         (D tsk_hp < D tsk_lp)

Then, the amount of interfering workload incurred by a job of task tsk is bounded by the maximum of lp_interference tsk_lp + hp_interference tsk_lp, where tsk_lp is such that D tsk_lp > D tsk.

We show that the cumulative service inversion, together with the interfering workload and the cost of j itself in the interval [t1, t1 + δ), does not exceed longest_busy_interval_with_pi δ.

Let L be any positive constant satisfying the total-RBF fixpoint condition. 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 the 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. For the case when there is service inversion, we show that longest_busy_interval_with_pi L is bounded by SBF L.

We additionally require that the maximum non-preemptive segment of each task in ts does not exceed its WCET.

We establish that SBF L bounds longest_busy_interval_with_pi L. This follows from the fixpoint condition, which dominates the higher-or-equal priority workload component, and from H_task_max_nps_le_task_cost, which bounds the service-inversion component.

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 longest_bi_with_pi_bounded_by_sbf 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 longest_bi_with_pi_bounded_by_sbf 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.