Library prosa.analysis.abstract.restricted_supply.bounded_bi.edf

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 ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskDeadline Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

For brevity, let's denote the relative deadline of a task as D.
  Let D tsk := task_deadline tsk.

Consider any kind of fully supply-consuming unit-supply uniprocessor model.
Consider any valid arrival sequence.
Next, consider a schedule of this arrival sequence, ...
  Variable sched : schedule PState.

... allow for any work-bearing notion of job readiness, ...
  Context `{!JobReady Job PState}.
  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

... and assume that the schedule is valid.
Assume that jobs have bounded non-preemptive segments.
Furthermore, we assume that the schedule is work-conserving ...
... and that it 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.
Consider an arbitrary task set ts, ...
  Variable ts : seq Task.

... 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.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

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.
    Variable j : Job.
    Hypothesis H_j_arrives : arrives_in arr_seq j.
    Hypothesis H_job_of_tsk : job_of_task tsk j.
    Hypothesis H_job_cost_positive : job_cost_positive j.

Let [t1, t2) be a busy-interval prefix.
    Variable t1 t2 : instant.
    Hypothesis H_busy_prefix : busy_interval_prefix arr_seq sched j t1 t2.

Consider an interval [t1, t1 + δ) ⊆ [t1, t2).
    Variable δ : duration.
    Hypothesis H_interval_in_busy_prefix : 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.
  Variable L : duration.
  Hypothesis H_L_positive : L > 0.

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.
  Section StepByStepProof.

Consider any job j of task tsk that has a positive job cost and is in the arrival sequence.
    Variable j : Job.
    Hypothesis H_j_arrives : arrives_in arr_seq j.
    Hypothesis H_job_of_tsk : job_of_task tsk j.
    Hypothesis H_job_cost_positive : job_cost_positive j.

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

Consider a time instant t1 such that [t1, job_arrival j]>> is a busy-interval prefix of j.
      Variable t1 : instant.
      Hypothesis H_arrives : t1 job_arrival j.
      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.

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.
      Local Lemma job_arrival_is_bounded :
        job_arrival j < t1 + L.
    End RelativeArrivalIsBounded.

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

Consider a time instant t1 such that [t1, job_arrival j]>> and [t1, t1 + L) are both busy-interval prefixes of job j.
      Variable t1 : instant.
      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
      Hypothesis H_busy_prefix_L : busy_interval_prefix arr_seq sched j t1 (t1 + L).

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.
      Local Lemma workload_is_bounded :
        workload_of_job arr_seq j t1 (t1 + L) + cumulative_interfering_workload j t1 (t1 + L) L.
It follows that t1 + L is a quiet time, which means that the busy prefix ends (i.e., it is bounded).
      Local Lemma busy_prefix_is_bounded_case1 :
         t2,
          job_arrival j < t2
           t2 t1 + L
           busy_interval arr_seq sched j t1 t2.

    End Case1.

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

Consider a time instant t1 such that [t1, job_arrival j]>> is a busy-interval prefix of j and [t1, t1 + L) is not.
      Variable t1 : instant.
      Hypothesis H_arrives : t1 job_arrival j.
      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
      Hypothesis H_no_busy_prefix_L : ¬ busy_interval_prefix arr_seq sched j t1 (t1 + L).

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.
      Local Lemma busy_prefix_is_bounded_case2:
         t2,
          job_arrival j < t2
           t2 t1 + L
           busy_interval arr_seq sched j t1 t2.
    End Case2.

  End StepByStepProof.

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