Library prosa.analysis.abstract.ideal.abstract_seq_rta

Abstract Response-Time Analysis with sequential tasks

In this section we propose the general framework for response-time analysis (RTA) of uni-processor scheduling of real-time tasks with arbitrary arrival models and sequential tasks.
We prove that the maximum among the solutions of the response-time bound recurrence for some set of parameters is a response-time bound for tsk. Note that in this section we do rely on the hypothesis about task sequentiality. This allows us to provide a more precise response-time bound function, since jobs of the same task will be executed strictly in the order they arrive.
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 valid arrival sequence with consistent, non-duplicate arrivals...
... and any ideal 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 an arbitrary task set.
  Variable ts : list Task.

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 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 max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts, max_arrival tsk is (1) an arrival bound of tsk, and (2) it is a monotonic function that equals 0 for the empty interval delta = 0.
Assume we are provided with abstract functions for interference and interfering workload.
  Context `{Interference Job}.
  Context `{InterferingWorkload Job}.

Let's define some local names for clarity.
In this section, we introduce a few new definitions to make it easier to express the new bound on the worst-case interference.
  Section Definitions.

When assuming sequential tasks, we can introduce an additional hypothesis that ensures that the values of interference and workload remain consistent. It is important to note that before a busy interval of a job j of task tsk begins, both the cumulative task workload and task service must be equal within the interval [0, t1). This has an implication that a busy interval for job j cannot begin if there is another pending job of the same task tsk. This requirement makes sense only in the context of sequential tasks.
    Definition interference_and_workload_consistent_with_sequential_tasks :=
       (j : Job) (t1 t2 : instant),
        arrives_in arr_seq j
        job_of_task tsk j
        job_cost j > 0
        busy_interval sched j t1 t2
        task_workload_between arr_seq tsk 0 t1 = task_service_of_jobs_in sched tsk (arrivals_between 0 t1) 0 t1.

Next we introduce the notion of task interference. Intuitively, task tsk incurs interference when some of the jobs of task tsk incur interference. As a result, tsk cannot make any progress. More formally, task tsk experiences interference at a time instant time t, if at time t task tsk is not scheduled and there exists a job of tsk that (1) experiences interference and (2) has arrived before some time instant upper_bound.
It is important to note two subtle points: according to our semantics of the interference function, jobs from the same task can cause interference to each other. In the definition of interference of a task we want to avoid such situations. That is why we use the term ~~ task_scheduled_at tsk t.
Moreover, in order to make the definition constructive, we introduce an upper bound on the arrival time of jobs from task tsk. As a result, we need to consider only a finite number of jobs. For the function to produce the correct values it is enough to specify a sufficiently large upper_bound. Usually as upper_bound one can use the end of the corresponding busy interval.
We also define a decidable counterpart of this definition...
... and prove that the propositional and decidable definitions are equivalent.
Next we define the cumulative task interference.
We say that task interference is bounded by task_interference_bound_function (task_IBF) iff for any job j of task tsk cumulative task interference within the interval t1, t1 + R) is bounded by function [task_IBF(tsk, A, R)]. Note that this definition is almost the same as the definition of [job_interference_is_bounded_by] from the non-necessarily-sequential case. However, in this case we ignore the interference that comes from jobs from the same task.
    Definition task_interference_is_bounded_by
               (task_interference_bound_function : Task duration duration duration) :=
       j R t1 t2,
        arrives_in arr_seq j
        job_of_task tsk j
        t1 + R < t2
        ~~ completed_by sched j (t1 + R)
        busy_interval sched j t1 t2
        let offset := job_arrival j - t1 in
        cumul_task_interference tsk t2 t1 (t1 + R) task_interference_bound_function tsk offset R.

  End Definitions.

In this section, we prove that the maximum among the solutions of the response-time bound recurrence is a response-time bound for tsk.
  Section ResponseTimeBound.

We assume that the schedule is work-conserving.
Unlike the previous theorem uniprocessor_response_time_bound_ideal, we assume that (1) tasks are sequential, moreover (2) functions interference and interfering_workload are consistent with the hypothesis of sequential tasks.
Assume we have a constant L that bounds the busy interval of any of tsk's jobs.
    Variable L : duration.
    Hypothesis H_busy_interval_exists:
      busy_intervals_are_bounded_by arr_seq sched tsk L.

Next, we assume that task_interference_bound_function is a bound on interference incurred by the task.
Given any job j of task tsk that arrives exactly A units after the beginning of the busy interval, the bound on the total interference incurred by j within an interval of length Δ is no greater than task_rbf (A + ε) - task_cost tsk + task's IBF Δ. Note that in case of sequential tasks the bound consists of two parts: (1) the part that bounds the interference received from other jobs of task tsk -- task_rbf (A + ε) - task_cost tsk and (2) any other interference that is bounded by task_IBF(tsk, A, Δ).
Note that since we consider the modified interference bound function, the search space has also changed. One can see that the new search space is guaranteed to include any A for which task_rbf (A) task_rbf (A + ε), since this implies the fact that total_interference_bound (tsk, A, Δ) total_interference_bound (tsk, A + ε, Δ).
Consider any value R, and assume that for any relative arrival time A from the search space there is a solution F of the response-time recurrence that is bounded by R. In contrast to the formula in "non-sequential" Abstract RTA, assuming that tasks are sequential leads to a more precise response-time bound. Now we can explicitly express the interference caused by other jobs of the task under consideration.
To understand the right part of the fix-point in the equation, it is helpful to note that the bound on the total interference (bound_of_total_interference) is equal to task_rbf (A + ε) - task_cost tsk + task_IBF tsk A Δ. Besides, a job must receive enough service to become non-preemptive task_lock_in_service tsk. The sum of these two quantities is exactly the right-hand side of the equation.
    Variable R : duration.
    Hypothesis H_R_is_maximum_seq :
       (A : duration),
        is_in_search_space_seq A
         (F : duration),
          A + F (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
                  + task_interference_bound_function tsk A (A + F)
          R F + (task_cost tsk - task_rtct tsk).

In this section we prove a few simple lemmas about the completion of jobs from the task considering the busy interval of the job under consideration.
    Section CompletionOfJobsFromSameTask.

Consider any two jobs j1 j2 of tsk.
      Variable j1 j2 : Job.
      Hypothesis H_j1_arrives : arrives_in arr_seq j1.
      Hypothesis H_j2_arrives : arrives_in arr_seq j2.
      Hypothesis H_j1_from_tsk : job_of_task tsk j1.
      Hypothesis H_j2_from_tsk : job_of_task tsk j2.
      Hypothesis H_j1_cost_positive : job_cost_positive j1.

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

We prove that if a job from task tsk arrived before the beginning of the busy interval, then it must be completed before the beginning of the busy interval
      Lemma completed_before_beginning_of_busy_interval:
        job_arrival j2 < t1
        completed_by sched j2 t1.

Next we prove that if a job is pending after the beginning of the busy interval [t1, t2) then it arrives after t1.
      Lemma arrives_after_beginning_of_busy_interval:
         t,
          t1 t
          pending sched j2 t
          arrived_between j2 t1 t.+1.

    End CompletionOfJobsFromSameTask.

Since we are going to use the uniprocessor_response_time_bound_ideal theorem to prove the theorem of this section, we have to show that all the hypotheses are satisfied. Namely, we need to show that hypotheses H_sequential_tasks, H_i_w_are_task_consistent and H_task_interference_is_bounded_by imply H_job_interference_is_bounded, and the fact that H_R_is_maximum_seq implies H_R_is_maximum.
In this section we show that there exists a bound for cumulative interference for any job of task tsk, i.e., the hypothesis H_job_interference_is_bounded holds.
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 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 x ...
      Variable x : duration.

... such that t1 + x is inside the busy interval...
      Hypothesis H_inside_busy_interval : t1 + x < t2.

... and job j is not completed by time t1 + x.
      Hypothesis H_job_j_is_not_completed : ~~ completed_by sched j (t1 + x).

In this section, we show that the cumulative interference of job j in the interval [t1, t1 + x) is bounded by the sum of the task workload in the interval t1, t1 + A + ε) and the cumulative interference of [j]'s task in the interval [t1, t1 + x). Note that the task workload is computed only on the interval [t1, t1 + A + ε). Thanks to the hypothesis about sequential tasks, jobs of task [tsk] that arrive after [t1 + A + ε] cannot interfere with [j].
      Section TaskInterferenceBoundsInterference.

We start by proving a simpler analog of the lemma that states that at any time instant t ∈ [t1, t1 + x) the sum of interference j t and scheduled_at j t is no larger than the sum of the service received by jobs of task tsk at time t and task_iterference tsk t.
Next we consider 4 cases.
        Section CaseAnalysis.

Consider an arbitrary time instant t[t1, t1 + x).
          Variable t : instant.
          Hypothesis H_t_in_interval : t1 t < t1 + x.

          Section Case1.

Assume the processor is idle at time t.
            Hypothesis H_idle : sched t = None.

In case when the processor is idle, one can show that interference j t = 1, scheduled_at j t = 0. But since interference doesn't come from a job of task tsk task_interference tsk = 1. Which reduces to 1 1.
            Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_idle:
              interference j t + scheduled_at sched j t
               service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
                + task_interference_received_before_dec tsk t2 t.

          End Case1.

          Section Case2.

Assume a job j' from another task is scheduled at time t.
            Variable j' : Job.
            Hypothesis H_sched : sched t = Some j'.
            Hypothesis H_not_job_of_tsk : ~~ job_of_task tsk j'.

If a job j' from another task is scheduled at time t, then interference j t = 1, scheduled_at j t = 0. But since interference doesn't come from a job of task tsk task_interference tsk = 1. Which reduces to 1 1.
            Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_task:
              interference j t + scheduled_at sched j t
              service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t +
              task_interference_received_before_dec tsk t2 t.

          End Case2.

          Section Case3.

Assume a job j' (different from j) of task tsk is scheduled at time t.
            Variable j' : Job.
            Hypothesis H_sched : scheduled_at sched j' t.
            Hypothesis H_not_job_of_tsk : job_of_task tsk j'.
            Hypothesis H_j_neq_j' : j != j'.

If a job j' (different from j) of task tsk is scheduled at time t, then interference j t = 1, scheduled_at j t = 0. Moreover, since interference comes from a job of the same task task_interference tsk = 0. However, in this case service_of_jobs of tsk = 1. Which reduces to 1 1.
            Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_job:
              interference j t + scheduled_at sched j t
               service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
                + task_interference_received_before_dec tsk t2 t.
          End Case3.

          Section Case4.

Assume that job j is scheduled at time t.
            Hypothesis H_sched : sched t = Some j.

If job j is scheduled at time t, then interference = 0, scheduled_at = 1, but note that service_of_jobs of tsk = 1, therefore inequality reduces to 1 1.
            Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_j:
              interference j t + scheduled_at sched j t
               service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
                + task_interference_received_before_dec tsk t2 t.

          End Case4.

We use the above case analysis to prove that any time instant t ∈ [t1, t1 + x) the sum of interference j t and scheduled_at j t is no larger than the sum of the service received by jobs of task tsk at time t and task_iterference tsk t.
          Lemma interference_plus_sched_le_serv_of_task_plus_task_interference:
            interference j t + scheduled_at sched j t
             service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
              + task_interference_received_before_dec tsk t2 t.

        End CaseAnalysis.

Next we prove cumulative version of the lemma above.
On the other hand, the service terms in the inequality above can be upper-bound by the workload terms.
        Lemma serv_of_task_le_workload_of_task_plus:
          task_service_of_jobs_in sched tsk (arrivals_between t1 (t1 + A + ε)) t1 (t1 + x)
          - service_during sched j t1 (t1 + x) + cumul_task_interference tsk t2 t1 (t1 + x)
           (task_workload_between arr_seq tsk t1 (t1 + A + ε) - job_cost j)
            + cumul_task_interference tsk t2 t1 (t1 + x).

Finally, we show that the cumulative interference of job j in the interval [t1, t1 + x) is bounded by the sum of the task workload in the interval t1, t1 + A + ε) and the cumulative interference of [j]'s task in the interval <<[t1, t1 + x)>>.
        Lemma cumulative_job_interference_le_task_interference_bound:
          cumulative_interference j t1 (t1 + x)
           (task_workload_between arr_seq tsk t1 (t1 + A + ε) - job_cost j)
            + cumul_task_interference tsk t2 t1 (t1 + x).

      End TaskInterferenceBoundsInterference.

In order to obtain a more convenient bound on the cumulative interference, we need to abandon the actual workload in favor of a bound that depends on task parameters only. So, we show that the actual workload of the task excluding workload of any job j is no greater than the bound on the workload excluding the cost of job j's task.
Finally, we use the lemmas above to obtain the bound on interference in terms of task_rbf and task_interference.
In this section, we prove that H_R_is_maximum_seq implies H_R_is_maximum.
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.

For simplicity, let's define a local name for the search space.
      Let is_in_search_space A :=
        is_in_search_space tsk L total_interference_bound A.

We prove that H_R_is_maximum holds.
      Lemma max_in_seq_hypothesis_implies_max_in_nonseq_hypothesis:
         (A : duration),
          is_in_search_space A
           (F : duration),
            A + F task_rtct tsk +
                    (task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A (A + F))
            R F + (task_cost tsk - task_rtct tsk).

    End MaxInSeqHypothesisImpMaxInNonseqHypothesis.

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.