Library prosa.analysis.abstract.restricted_supply.abstract_rta

Abstract Response-Time Analysis for Restricted-Supply Processors (aRSA)

In this section we propose a general framework for response-time analysis (RTA) for real-time tasks with arbitrary arrival models under uni-processor scheduling subject to supply restrictions, characterized by a given SBF.
We prove that the maximum (with respect to the set of offsets) among the solutions of the response-time bound recurrence is a response-time bound for tsk. Note that in this section we add additional restrictions on the processor state. These assumptions allow us to eliminate the second equation from aRTA+'s recurrence since jobs experience delays only due to the lack of supply while executing non-preemptively.
Consider any type of tasks with a run-to-completion threshold ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskRunToCompletionThreshold Task}.

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

Consider any kind of fully supply-consuming unit-supply processor state model.
Consider any valid arrival sequence.
Consider any restricted supply uniprocessor schedule of this arrival sequence ...
... where jobs do not execute before their arrival nor after completion.
Assume we are given valid WCETs for all tasks.
Consider a task set ts...
  Variable ts : list Task.

... and a task tsk of ts that is to be analyzed.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

Consider a valid preemption model ...
...and a valid task run-to-completion threshold function. That is, task_rtc tsk is (1) no bigger than tsk's cost and (2) for any job j of task tsk job_rtct j is bounded by task_rtct tsk.
Assume we are provided with abstract functions for Interference and Interfering Workload.
  Context `{Interference Job}.
  Context `{InterferingWorkload Job}.

We assume that the scheduler is work-conserving.
Let L be a constant that bounds any busy interval of task tsk.
  Variable L : duration.
  Hypothesis H_busy_interval_exists :
    busy_intervals_are_bounded_by arr_seq sched tsk L.

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.
Next, we assume that intra_IBF is a bound on the intra-supply interference incurred by task tsk.
Given any job j of task tsk that arrives exactly A units after the beginning of the busy interval, the bound on the interference incurred by j within an interval of length Δ is no greater than (Δ - SBF Δ) + intra_IBF A Δ.
  Let IBF_P (A Δ : duration) :=
    (Δ - SBF Δ) + intra_IBF A Δ.

Next, we instantiate function IBF_NP, which is a function that bounds interference in a non-preemptive stage of execution. We prove that this function can be instantiated as λ tsk F Δ (F - task_rtct tsk) + (Δ - SBF Δ - (F - SBF F)).
Let us reiterate on the intuitive interpretation of this function. Since F is a solution to the first equation task_rtct tsk + IBF_P A F F, we know that by time instant t1 + F a job receives task_rtct tsk units of service and, hence, it becomes non-preemptive. Knowing this information, how can we bound the job's interference in an interval [t1, t1 + Δ)>>? Note that this interval starts with the beginning of the busy interval. We know that the job receives F - task_rtct tsk units of interference. In the non-preemptive mode, a job under analysis can still experience some interference due to a lack of supply. This interference is bounded by (Δ - SBF Δ) - (F - SBF F) since part of this interference has already been accounted for in the preemptive part of the execution (F - SBF F).
  Let IBF_NP (F Δ : duration) :=
    (F - task_rtct tsk) + (Δ - SBF Δ - (F - SBF F)).

In the next section, we prove a few helper lemmas.
  Section AuxiliaryLemmas.

Consider any job j of tsk.
      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.

Consider the busy interval [t1, t2) of job j.
      Variable t1 t2 : instant.
      Hypothesis H_busy_interval : busy_interval_prefix sched j t1 t2.

Let's define A as a relative arrival time of job j (with respect to time t1).
      Let A : duration := job_arrival j - t1.

Consider an arbitrary time Δ ...
      Variable Δ : duration.
... such that t1 + Δ is inside the busy interval...
      Hypothesis H_inside_busy_interval : t1 + Δ < t2.
... the job j is not completed by time (t1 + Δ).
      Hypothesis H_job_j_is_not_completed : ~~ completed_by sched j (t1 + Δ).

First, we show that blackout is counted as interference.
      Lemma blackout_impl_interference :
         t,
          t1 t < t2
          is_blackout sched t
          interference j t.

Next, we show that interference is equal to a sum of two functions: is_blackout and intra_interference.
      Lemma blackout_plus_local_is_interference :
         t,
          t1 t < t2
          is_blackout sched t + intra_interference sched j t
          = interference j t.

As a corollary, cumulative interference during a time interval [t1, t1 + Δ) can be split into a sum of total blackouts in [t1, t1 + Δ) and cumulative intra-supply interference during [t1, t1 + Δ).
Moreover, since the total blackout duration in an interval of length Δ is bounded by Δ - SBF Δ, the cumulative interference during the time interval [t1, t1 + Δ) is bounded by the sum of Δ - SBF Δ and cumulative intra-supply interference during [t1, t1 + Δ).
      Corollary cumulative_job_interference_bound :
        cumulative_interference j t1 (t1 + Δ)
         (Δ - SBF Δ) + cumul_intra_interference sched j t1 (t1 + Δ).

Next, consider a duration F such that F Δ and job j has enough service to become non-preemptive by time instant t1 + F.
      Variable F : duration.
      Hypothesis H_F_le_Δ : F Δ.
      Hypothesis H_enough_service : task_rtct tsk service sched j (t1 + F).

Then, we show that job j does not experience any intra-supply interference in the time interval [t1 + F, t1 + Δ)>>.
      Lemma no_intra_interference_after_F :
        cumul_intra_interference sched j (t1 + F) (t1 + Δ) = 0.

  End AuxiliaryLemmas.

For clarity, let's define a local name for the search space.
We use the following equation to bound the response-time of a job of task tsk. Consider any value R that upper-bounds the solution of each response-time recurrence, i.e., for any relative arrival time A in the search space, there exists a corresponding solution F such that (1) F A + R, (2) task_rtct tsk + intra_IBF tsk A F SBF F and SBF F + (task_cost tsk - task_rtct tsk) SBF (A + R).
Note that, compared to "ideal RTA," there is an additional requirement F A + R. Intuitively, it is needed to rule out a nonsensical situation when the non-preemptive stage completes earlier than the preemptive stage.
  Variable R : duration.
  Hypothesis H_R_is_maximum_rs :
     (A : duration),
      is_in_search_space_rs A
       (F : duration),
        F A + R
         task_rtct tsk + intra_IBF A F SBF F
         SBF F + (task_cost tsk - task_rtct tsk) SBF (A + R).

In the following section we prove that all the premises of abstract RTA are satisfied.
  Section RSaRTAPremises.

First, we show that IBF_P correctly upper-bounds interference in the preemptive stage of execution.
Next, we prove that IBF_NP correctly bounds interference in the non-preemptive stage given a solution to the preemptive stage F.
Next, we prove that F is bounded by task_cost tsk + IBF_NP F Δ for any F and Δ. As explained in file analysis/abstract/abstract_rta, this shows that the second stage indeed takes into account service received in the first stage.
    Lemma IBF_P_sol_le_IBF_NP :
       (F Δ : duration),
        F task_cost tsk + IBF_NP F Δ.

Next we prove that H_R_is_maximum_rs implies H_R_is_maximum.
    Lemma max_in_rs_hypothesis_impl_max_in_arta_hypothesis :
       (A : duration),
        is_in_search_space L IBF_P A
         (F : duration),
          task_rtct tsk + (F - SBF F + intra_IBF A F) F
           task_cost tsk + (F - task_rtct tsk + (A + R - SBF (A + R) - (F - SBF F))) A + R.

  End RSaRTAPremises.

Finally, we apply the uniprocessor_response_time_bound theorem, and using the lemmas above, we prove that all the requirements are satisfied. So, R is a response time bound.