Library prosa.analysis.abstract.restricted_supply.search_space.edf

Abstract Search Space is a Subset of Restricted Supply EDF Search Space

A response-time analysis usually involves solving the response-time equation for various relative arrival times (w.r.t. the beginning of the corresponding busy interval) of a job under analysis. To reduce the time complexity of the analysis, the state of the art uses the notion of a search space. Intuitively, this corresponds to all "interesting" arrival offsets that the job under analysis might have with regard to the beginning of its busy window.
In this file, we prove that the search space derived from the aRSA theorem is a subset of the search space for the EDF scheduling policy with restricted supply. In other words, by solving the response-time equation for points in the EDF search space, one also checks all points in the aRTA search space, which makes EDF compatible with aRTA w.r.t. the search space.
Consider any type of tasks.
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskDeadline Task}.
  Context `{TaskMaxNonpreemptiveSegment Task}.

Consider an arbitrary task set ts.
  Variable ts : seq Task.

Let max_arrivals be a family of valid arrival curves.
Let tsk be any task in ts that is to be analyzed.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

Let L be an arbitrary positive constant. Normally, L denotes an upper bound on the length of a busy interval of a job of tsk. In this file, however, L can be any positive constant.
  Variable L : duration.
  Hypothesis H_L_positive : 0 < L.

For brevity, let's denote the relative deadline of a task as D.
  Let D tsk := task_deadline tsk.

We introduce rbf as an abbreviation of the task request bound function.
To reduce the time complexity of the analysis, we introduce the notion of a search space for EDF. Intuitively, this corresponds to all "interesting" arrival offsets that the job under analysis might have with regard to the beginning of its busy window.
In the case of the search space for EDF, we consider three conditions. First, we ask whether task_rbf A task_rbf (A + ε).
  Let task_rbf_changes_at (A : duration) :=
    rbf tsk A != rbf tsk (A + ε).

Second, we ask whether there exists a task tsko from ts such that tsko tsk and rbf(tsko, A + D tsk - D tsko) rbf(tsko, A + ε + D tsk - D tsko).
Third, we ask whether blocking_bound (A - ε) blocking_bound A.
The final search space for EDF is the set of offsets less than L and where priority_inversion_bound, task_rbf, or bound_on_total_hep_workload changes in value.
  Definition is_in_search_space (A : duration) :=
    (A < L) && (blocking_bound_changes_at A
                || task_rbf_changes_at A
                || bound_on_total_hep_workload_changes_at A).

To rule out pathological cases with the search space, we assume that the task cost is positive and the arrival curve is non-pathological.
  Hypothesis H_task_cost_pos : 0 < task_cost tsk.
  Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.

For brevity, let us introduce a shorthand for an intra-IBF. The abstract search space is derived via intra-IBF.
Then, abstract RTA's standard search space is a subset of the computation-oriented version defined above.
  Lemma search_space_sub :
     A,
      abstract.search_space.is_in_search_space L intra_IBF A
      is_in_search_space A.
  Proof.
    moveA [-> | [/andP [POSA LTL] [x [LTx INSP2]]]]; apply/andP; split ⇒ //.
    { apply/orP; left; apply/orP; right.
      rewrite /task_rbf_changes_at /rbf task_rbf_0_zero // eq_sym -lt0n add0n.
      by apply task_rbf_epsilon_gt_0 ⇒ //.
    }
    { apply contraT; rewrite !negb_or ⇒ /andP [/andP [/negPn/eqP PI /negPn/eqP RBF] WL].
      exfalso; apply INSP2.
      rewrite /intra_IBF subnK // RBF.
      apply /eqP; rewrite eqn_add2l PI eqn_add2l.
      rewrite /bound_on_athep_workload subnK //.
      apply /eqP; rewrite big_seq_cond [RHS]big_seq_cond.
      apply eq_big ⇒ // tsk_i /andP [TS OTHER].
      move: WL; rewrite /bound_on_total_hep_workload_changes_at /D ⇒ /hasPn WL.
      move: {WL} (WL tsk_i TS) ⇒ /nandP [/negPn/eqP EQ|/negPn/eqP WL];
                                  first by move: OTHER; rewrite EQ ⇒ /neqP.
      case: (ltngtP (A + ε + task_deadline tsk - task_deadline tsk_i) x) ⇒ [ltn_x|gtn_x|eq_x]; rewrite /minn.
      { by rewrite ifT //; lia. }
      { rewrite ifF //.
        by move: gtn_x; rewrite leq_eqVlt ⇒ /orP [/eqP EQ|LEQ]; lia. }
      { case: (A + task_deadline tsk - task_deadline tsk_i < x).
        - by rewrite -/rbf WL.
        - by rewrite eq_x. } }
  Qed.

End SearchSpaceSubset.