Library prosa.analysis.abstract.restricted_supply.abstract_seq_rta

Abstract Response-Time Analysis for Restricted-Supply Processors with Sequential Tasks

In this section we propose a general framework for response-time analysis (RTA) for real-time tasks with arbitrary arrival models and sequential _tasks under uni-processor scheduling subject to supply restrictions, characterized by a given SBF.
In this section, we assume tasks to be sequential. This allows us to establish a more precise response-time bound, 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 {jc : 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 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 ...
... with valid task run-to-completion thresholds. 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.
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 functions characterizing interference and interfering workload.
  Context `{Interference Job}.
  Context `{InterferingWorkload Job}.

Let's define a local name for clarity.
We assume that the scheduler is work-conserving.
Unlike the more general, underlying theorem uniprocessor_response_time_bound_restricted_supply, we assume that tasks are sequential.
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 task_intra_IBF is a bound on intra-supply interference incurred by task tsk. That is, task_intra_IBF bounds interference ignoring interference due to lack of supply and due to self-interference.
We use the function task_intra_IBF, which satisfies the hypothesis task_intra_interference_is_bounded_by, to construct a new function intra_IBF := (task_rbf (A + ε) - task_cost tsk) + task_intra_IBF A Δ that satisfies the hypothesis intra_interference_is_bounded_by. This is needed to later apply the lemma uniprocessor_response_time_bound_restricted_supply from file restricted_supply/abstract_rta (recall that it requires intra_IBF, not task_intra_IBF).
The logic behind intra_IBF is quite simple. Consider a job j of task tsk that arrives exactly A units after the beginning of the busy interval. Then 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_intra_IBF A Δ. Note that, for 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_intra_IBF(tsk, A, Δ).
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_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + task_intra_IBF A F SBF F, (3) and SBF F + (task_cost tsk - task_rtct tsk) SBF (A + R).
  Variable R : duration.
  Hypothesis H_R_is_maximum_seq_rs :
     (A : duration),
      is_in_search_space_rs A
       (F : duration),
        F A + R
         (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + task_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 aRSA are satisfied.
  Section aRSAPremises.

First, we show that intra_IBF correctly upper-bounds interference in the preemptive stage of execution.
    Lemma IBF_P_bounds_interference :
      intra_interference_is_bounded_by arr_seq sched tsk intra_IBF.
    Proof.
      movet1 t2 Δ j ARR TSK BUSY LT NCOM A PAR; move: (PAR _ _ BUSY) ⇒ EQ.
      have [ZERO|POS] := posnP (@job_cost _ jc j).
      { exfalso; move: NCOM ⇒ /negP NCOM; apply: NCOM.
        by rewrite /service.completed_by ZERO. }
      rewrite (cumul_cond_interference_ID _ (nonself arr_seq sched)).
      rewrite /intra_IBF addnC leq_add; first by done.
      { rewrite -(leq_add2r (cumul_task_interference arr_seq sched j t1 (t1 + Δ))).
        eapply leq_trans; first last.
        { by rewrite EQ; apply: task.cumulative_job_interference_bound ⇒ //. }
        { rewrite -big_split //= leq_sum // /cond_interferencet _.
          by case (interference j t), (has_supply sched t), (nonself arr_seq sched j t) ⇒ //. } }
      { rewrite (cumul_cond_interference_pred_eq _ (nonself_intra arr_seq sched)) ⇒ //.
        by moves t; split⇒ //; rewrite andbC. }
    Qed.

To rule out pathological cases with the H_R_is_maximum_seq_rs equation (such as task_cost tsk being greater than task_rbf (A + ε)), we assume that the arrival curve is non-pathological.
    Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.

To later apply the theorem uniprocessor_response_time_bound_restricted_supply, we need to provide the IBF, which bounds the total interference.
    Let IBF A Δ := Δ - SBF Δ + intra_IBF A Δ.

Next we prove that H_R_is_maximum_seq_rs implies H_R_is_maximum_rs from file (.../restricted_supply/abstract_rta.v). In other words, a solution to the response-time recurrence for restricted-supply processor models with sequential tasks can be translated to a solution for the same processor model with non-necessarily sequential tasks.
    Lemma sol_seq_rs_equation_impl_sol_rs_equation :
       (A : duration),
        is_in_search_space L IBF 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).
    Proof.
      rewrite /IBF; moveA SP.
      move: (H_R_is_maximum_seq_rs A) ⇒ T.
      feed T.
      { move: SP ⇒ [ZERO|[POS [x [LT NEQ]]]]; first by left.
        by right; split ⇒ //; x; split ⇒ //. }
      have [F [EQ0 [EQ1 EQ2]]] := T; clear T.
       F; split ⇒ //; split ⇒ //.
      rewrite /intra_IBF -(leqRW EQ1) addnA leq_add2r.
      rewrite addnBA; last first.
      { apply leq_trans with (task_rbf 1).
        - by apply: task_rbf_1_ge_task_cost ⇒ //.
        - by eapply task_rbf_monotone ⇒ //; rewrite addn1. }
      { rewrite subnBA.
        - by rewrite addnC.
        - by apply H_valid_run_to_completion_threshold. }
    Qed.

  End aRSAPremises.

Finally, we apply the uniprocessor_response_time_bound_restricted_supply theorem, and using the lemmas above, prove that all its requirements are satisfied. Hence, R is a response-time bound for task tsk.