Library prosa.analysis.abstract.ideal.abstract_rta

Abstract Response-Time Analysis For Processor State with Ideal Uni-Service Progress Model

In this module, we present an instantiation of the general response-time analysis framework for models that satisfy the ideal uni-service progress assumptions.
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 no delays while executing non-preemptively.
Section AbstractRTAIdeal.

Consider any type of tasks ...
  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 uni-service ideal processor state model.
Consider any arrival sequence with consistent, non-duplicate arrivals.
Next, consider any schedule of this arrival sequence...
... where jobs do not execute before their arrival nor after completion.
Assume that the job costs are no larger than the task costs.
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.

Next, assume that interference_bound_function is a bound on the interference incurred by jobs of task tsk parametrized by the relative arrival time A.
To apply the generalized aRTA, we have to instantiate IBF_P and IBF_NP. In this file, we assume we are given a generic function interference_bound_function that bounds interference of jobs of tasks in ts and which have to be instantiated in subsequent files. We use this function to instantiate IBF_P.
However, we still have to 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 with a constant function λ F Δ F - task_rtct tsk.
  Let IBF_NP (F : duration) (Δ : duration) := F - task_rtct tsk.

Let us re-iterate on the intuitive interpretation of this function. Since F is a solution to the first equation task_rtct tsk + IBF_P tsk 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. Given this information, how can we bound the job's interference in an interval [t1, t1 + R)>>? 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, and there will no more interference. Hence, IBF_NP tsk F Δ := F - task_rtct tsk.
For simplicity, let's define a local name for the search space.
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 F + (task_cost tsk - task_rtc tsk) R.
  Variable R : duration.
  Hypothesis H_R_is_maximum_ideal :
     A,
      is_in_search_space A
       F,
        task_rtct tsk + interference_bound_function A (A + F) A + F
        F + (task_cost tsk - task_rtct tsk) R.

Using the lemma about IBF_NP, we instantiate the general RTA theorem's result to the ideal uniprocessor's case to prove that R is a response-time bound.