Library prosa.analysis.abstract.abstract_rta

Abstract Response-Time Analysis

In this module, we propose the general framework for response-time analysis (RTA) of uni-processor scheduling of real-time tasks with arbitrary arrival models. 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 do not rely on any hypotheses about job sequentiality.
Section Abstract_RTA.

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_rtct tsk is (1) no bigger than tsk's cost, (2) for any job of task tsk job_rtct is bounded by task_rtct.
Let's define some local names for clarity.
Assume we are provided with abstract functions for interference and interfering workload.
We assume that the scheduler is work-conserving.
For simplicity, let's define some local names.
Let L be a constant which bounds any busy interval of task tsk.
Next, assume that interference_bound_function is a bound on the interference incurred by jobs of task 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 R F + (task_cost tsk - task_rtct tsk).
  Variable R: nat.
  Hypothesis H_R_is_maximum:
     A,
      is_in_search_space A
       F,
        A + F task_rtct tsk
                + interference_bound_function tsk A (A + F)
        R F + (task_cost tsk - task_rtct tsk).

In this section we show a detailed proof of the main theorem that establishes that R is a response-time bound of task tsk.
  Section ProofOfTheorem.

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

Assume we have a busy interval [t1, t2) of job j that is bounded by L.
    Variable t1 t2: instant.
    Hypothesis H_busy_interval: busy_interval j t1 t2.

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

In order to prove that R is a response-time bound of job j, we use hypothesis H_R_is_maximum. Note that the relative arrival time (A) is not necessarily from the search space. However, earlier we have proven that for any A there exists another A_sp from the search space that shares the same IBF value. Moreover, we've also shown that there exists an F_sp such that F_sp is a solution of the response time recurrence for parameter A_sp. Thus, despite the fact that the relative arrival time may not lie in the search space, we can still use the assumption H_R_is_maximum.
More formally, consider any A_sp and F_sp such that:..
    Variable A_sp F_sp : duration.

(a) A_sp is less than or equal to A...
    Hypothesis H_A_gt_Asp : A_sp A.

(b) interference_bound_function(A, x) is equal to interference_bound_function(A_sp, x) for all x less than L...
    Hypothesis H_equivalent :
      are_equivalent_at_values_less_than
        (interference_bound_function tsk A)
        (interference_bound_function tsk A_sp) L.

(c) A_sp is in the search space, ...
(d) A_sp + F_sp is a solution of the response time recurrence...
(e) and finally, F_sp + (task_last - ε) is no greater than R.
    Hypothesis H_R_gt_Fsp : R F_sp + (task_cost tsk - task_rtct tsk).

In this section, we consider the case where the solution is so large that the value of t1 + A_sp + F_sp goes beyond the busy interval. Although this case may be impossible in some scenarios, it can be easily proven, since any job that completes by the end of the busy interval remains completed.
    Section FixpointOutsideBusyInterval.

By assumption, suppose that t2 is less than or equal to t1 + A_sp + F_sp.
      Hypothesis H_big_fixpoint_solution : t2 t1 + (A_sp + F_sp).

Then we prove that job_arrival j + R is no less than t2.
      Lemma t2_le_arrival_plus_R:
        t2 job_arrival j + R.

But since we know that the job is completed by the end of its busy interval, we can show that job j is completed by job arrival j + R.
In this section, we consider the complementary case where t1 + A_sp + F_sp lies inside the busy interval.
    Section FixpointInsideBusyInterval.

So, assume that t1 + A_sp + F_sp is less than t2.
      Hypothesis H_small_fixpoint_solution : t1 + (A_sp + F_sp) < t2.

Next, let's consider two other cases: CASE 1: the value of the fix-point is no less than the relative arrival time of job j.
      Section FixpointIsNoLessThanArrival.

Suppose that A_sp + F_sp is no less than relative arrival of job j.
In this section, we prove that the fact that job j is not completed by time job_arrival j + R leads to a contradiction. Which in turn implies that the opposite is true -- job j completes by time job_arrival j + R.
        Section ProofByContradiction.

Recall that by lemma "solution_for_A_exists" there is a solution F of the response-time recurrence for the given relative arrival time A (which is not necessarily from the search space).
Thus, consider a constant F such that:..
          Variable F : duration.
(a) the sum of A_sp and F_sp is equal to the sum of A and F...
          Hypothesis H_Asp_Fsp_eq_A_F : A_sp + F_sp = A + F.
(b) F is at mo1st F_sp...
          Hypothesis H_F_le_Fsp : F F_sp.
(c) and A + F is a solution for the response-time recurrence for A.
          Hypothesis H_A_F_fixpoint:
            A + F task_rtct tsk + interference_bound_function tsk A (A + F).

Next, we assume that job j is not completed by time job_arrival j + R.
          Hypothesis H_j_not_completed : ~~ completed_by sched j (job_arrival j + R).

Some additional reasoning is required since the term task_cost tsk - task_rtct tsk does not necessarily bound the term job_cost j - job_rtct j. That is, a job can have a small run-to-completion threshold, thereby becoming non-preemptive much earlier than guaranteed according to task run-to-completion threshold, while simultaneously executing the last non-preemptive segment that is longer than task_cost tsk - task_rtct tsk (e.g., this is possible in the case of floating non-preemptive sections).
In this case we cannot directly apply lemma "j_receives_at_least_run_to_completion_threshold". Therefore we introduce two temporal notions of the last non-preemptive region of job j and an execution optimism. We use these notions inside this proof, so we define them only locally.
Let the last non-preemptive region of job j (last) be the difference between the cost of the job and the j's run-to-completion threshold (i.e. job_cost j - job_rtct j). We know that after j has reached its run-to-completion threshold, it will additionally be executed job_last j units of time.
          Let job_last := job_cost j - job_rtct j.

And let execution optimism (optimism) be the difference between the tsk's run-to-completion threshold and the j's run-to-completion threshold (i.e. task_rtct - job_rtct). Intuitively, optimism is how much earlier job j has received its run-to-completion threshold than it could at worst.
          Let optimism := task_rtct tsk - job_rtct j.

From lemma "j_receives_at_least_run_to_completion_threshold" with parameters progress_of_job := job_rtct j and delta := (A + F) - optimism) we know that service of j by time t1 + (A + F) - optimism is no less than job_rtct j. Hence, job j is completed by time t1 + (A + F) - optimism + last.
          Lemma j_is_completed_by_t1_A_F_optimist_last :
            completed_by sched j (t1 + (A + F - optimism) + job_last).

However, t1 + (A + F) - optimism + last job_arrival j + R! To prove this fact we need a few auxiliary inequalities that are needed because we use the truncated subtraction in our development. So, for example a + (b - c) = a + b - c only if b c.
          Section AuxiliaryInequalities.

Recall that we consider a busy interval of a job j, and j has arrived A time units after the beginning the busy interval. From basic properties of a busy interval it follows that job j incurs interference at any time instant t ∈ [t1, t1 + A). Therefore interference_bound_function(tsk, A, A + F) is at least A.
            Lemma relative_arrival_le_interference_bound:
              A interference_bound_function tsk A (A + F).

As two trivial corollaries, we show that tsk's run-to-completion threshold is at most F_sp...
            Corollary tsk_run_to_completion_threshold_le_Fsp :
              task_rtct tsk F_sp.

... and optimism is at most F.
            Corollary optimism_le_F :
              optimism F.

          End AuxiliaryInequalities.

Next we show that t1 + (A + F) - optimism + last is at most job_arrival j + R, which is easy to see from the following sequence of inequalities:
t1 + (A + F) - optimism + last job_arrival j + (F - optimism) + job_last job_arrival j + (F_sp - optimism) + job_last job_arrival j + F_sp + (job_last - optimism) job_arrival j + F_sp + job_cost j - task_rtct tsk job_arrival j + F_sp + task_cost tsk - task_rtct tsk job_arrival j + R.
          Lemma t1_A_F_optimist_last_le_arrival_R :
            t1 + (A + F - optimism) + job_last job_arrival j + R.

... which contradicts the initial assumption about j is not completed by time job_arrival j + R.
          Lemma j_is_completed_earlier_contradiction : False.

        End ProofByContradiction.

Putting everything together, we conclude that j is completed by job_arrival j + R.
        Lemma job_completed_by_arrival_plus_R_2:
          completed_by sched j (job_arrival j + R).

      End FixpointIsNoLessThanArrival.

CASE 2: the value of the fix-point is less than the relative arrival time of job j (which turns out to be impossible, i.e. the solution of the response-time recurrence is always equal to or greater than the relative arrival time).
      Section FixpointCannotBeSmallerThanArrival.

Assume that A_sp + F_sp is less than A.
Note that the relative arrival time of job j is less than L.
        Lemma relative_arrival_is_bounded: A < L.

We can use j_receives_at_least_run_to_completion_threshold to prove that the service received by j by time t1 + (A_sp + F_sp) is no less than run-to-completion threshold.
        Lemma service_of_job_ge_run_to_completion_threshold:
          service sched j (t1 + (A_sp + F_sp)) job_rtct j.

However, this is a contradiction. Since job j has not yet arrived, its service is equal to 0. However, run-to-completion threshold is always positive.
        Lemma relative_arrival_time_is_no_less_than_fixpoint:
          False.

      End FixpointCannotBeSmallerThanArrival.

    End FixpointInsideBusyInterval.

  End ProofOfTheorem.

Using the lemmas above, we prove that R is a response-time bound.