Library prosa.results.fixed_priority.rta.bounded_pi_non_seq

Abstract RTA Instantiation for FP-Schedulers with Bounded Priority Inversion

In this module we instantiate the abstract response-time analysis (aRTA) for FP-schedulers assuming the ideal uni-processor model and real-time tasks with arbitrary arrival models.
The important feature of this instantiation is that it allows reasoning about the notion of priority inversion. However, we do not specify the exact cause of priority inversion (as there may be different reasons for this, like execution of a non-preemptive segment or blocking due to resource locking). We only assume that the duration of priority inversion is bounded.
The difference in this RTA and the other RTA for FP (from the file bounded_pi.v) is that here we drop the sequential-tasks assumption and instead explicitly account for self-interference.
We consider tasks and jobs with the listed parameters.
  Context {Task : TaskType}
          `{TaskCost Task}
          `{TaskRunToCompletionThreshold Task}
          `{!MaxArrivals Task}.
  Context {Job : JobType}
          `{JobTask Job Task}
          `{Arrival : !JobArrival Job}
          `{Cost : !JobCost Job}
          `{!JobPreemptable Job}.

We allow for any work-bearing readiness model. (The work_bearing_readiness restriction is introduced further down because it requires a schedule to be introduced first; see H_job_ready below.)
  Context `{!JobReady Job (ideal.processor_state Job)}.

A. Defining the System Model

We begin by defining the system model. First, we model arrivals using an arrival sequence. We assume that the arrival sequence is valid and that all arriving jobs comply with the WCET assumption.
Next, we consider any fixed-priority policy that is reflexive.
  Context `{FP : !FP_policy Task}.
  Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.

We consider a valid, ideal uniprocessor schedule that follows a work-bearing readiness model.
We model the tasks in the system using a task set ts. We assume that all jobs in the system come from this task set.
  Variable ts : seq Task.
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

We assume that the task set respects the arrival curve defined by max_arrivals.
The task under consideration tsk is contained in ts.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

While we do not assume an explicit preemption model, we require that any preemption model under consideration is valid. We also assume that the run-to-completion-threshold of the task tsk is valid.
As mentioned, we assume that the duration of priority inversion incurred by the task tsk is bounded by priority_inversion_bound.

B. Encoding the Scheduling Policy and Preemption Model

Next, we encode the scheduling policy and preemption model using the functions interference and interfering_workload. To this end, we simply reuse the general definitions of interference and interfering workload that apply to any JLFP policy, as defined in the module analysis.abstract.ideal.iw_instantiation.

C. Abstract Work Conservation

Let us recall the abstract and classic notations of work conservation.
We assume that the schedule is work-conserving in the classic sense, which allows us to apply instantiated_i_and_w_are_coherent_with_schedule to conclude that abstract work-conservation also holds.

D. Bounding the Maximum Busy-Window Length

For convenience, we define the following acronyms.
Next, we define L as a positive fixed point of the given equation ...
  Variable L : duration.
  Hypothesis H_L_positive : L > 0.
  Hypothesis H_fixed_point :
    L = priority_inversion_bound + total_hep_rbf L.

... and prove that it is a bound on the maximum length of a busy interval.
  Lemma instantiated_busy_intervals_are_bounded :
    busy_intervals_are_bounded_by arr_seq sched tsk L.
  Proof.
    movej ARR TSK POS.
    edestruct (exists_busy_interval) with
      (delta := L) (priority_inversion_bound := (fun (d : duration) ⇒ priority_inversion_bound))
      as [t1 [t2 [T1 [T2 BI]]]] ⇒ //; last first.
    { t1, t2; split⇒ [//|]; split⇒ [//|].
      by eapply instantiated_busy_interval_equivalent_busy_interval. }
    { intros; rewrite {2}H_fixed_point leq_add //.
      by apply: hep_workload_le_total_hep_rbf. }
  Qed.

E. Defining the Interference Bound Function (IBF)

Next, we define task_IBF and prove that task_IBF bounds the interference incurred by any job of tsk. Note that the maxn here is required to avoid the case in which the interval under consideration is shorter than A. While intuitively it might seem that this case is irrelevant, aRTA does not allow for this case to be ignored.
  Definition IBF (A: instant) (Δ : duration) :=
    priority_inversion_bound
    + (task_rbf (maxn (A + ε) Δ) - task_cost tsk)
    + total_ohep_rbf (Δ).

First we prove bounds on self-interference, that is, interference incurred from other jobs of the same task. Note that since we do not require a sequential task model, we need to account for the case of later jobs of the same task causing interference.
  Section SelfInterferenceBound.

Consider any interval [t1, t1 + Δ).
    Variable t1 : instant.
    Variable Δ : duration.

Next, consider any job j of the task tsk that has a positive cost and arrives in the arrival sequence after the interval under consideration has started.
    Variable j : Job.
    Hypothesis H_job_cost_positive : job_cost_positive j.
    Hypothesis H_job_of_task : job_of_task tsk j.
    Hypothesis H_j_in_arr_seq : arrives_in arr_seq j.
    Hypothesis H_t1_le_job_arrival : t1 job_arrival j.

First, we consider the case where the job arrives before the end of the interval under consideration.
    Section SelfInterferenceBoundCase1.

      Hypothesis H_j_arrives_before_Δ : job_arrival j < t1 + Δ.

In this case, we bound the interference caused by the task under consideration itself by the cost of the workload released by the tasks in the interval (given by the RBF). However, we do not want to account for the job under consideration itself as interference and hence we subtract the cost of the task.
      Lemma self_intf_bound_case1:
        workload_of_jobs
          (another_hep_job_of_same_task^~ j)
          (arrivals_between arr_seq t1 (t1 + Δ))
         task_rbf Δ - task_cost (tsk).
      Proof.
        eapply leq_trans; last eapply leq_trans;
          last eapply task_rbf_without_job_under_analysis ⇒ //=.
        - rewrite (workload_of_jobs_equiv_pred _ _
                     (another_hep_job_of_same_task^~ j));
            last by movejo IN1; lia.
          set (hep_job_of_same_task := (fun x : Jobhep_job x j && (job_task x == tsk))).
          rewrite (workload_of_jobs_equiv_pred _ _ (fun xhep_job_of_same_task x && (x != j) ));
            last first.
          { movej' _.
            rewrite /another_hep_job_of_same_task /hep_job_of_same_task /another_hep_job.
            move : H_job_of_task ⇒ /eqP →.
            lia. }
          rewrite workload_minus_job_cost'; [apply leqnn| by done|].
          rewrite job_arrival_in_bounds //=.
          by split; [| apply /andP; split] ⇒ //=.
        - rewrite /task_workload_between /task_workload.
           move : H_job_of_taskTSK.
           move : TSK ⇒ /eqP TSK.
           rewrite /hep_job /FP_to_JLFP H_priority_is_reflexive andTb TSK eq_refl //=.
           apply leq_sub; last by done.
           apply workload_of_jobs_weaken.
           move ⇒ ? /andP[_ /eqP EQ].
           by apply /eqP.
      Qed.

    End SelfInterferenceBoundCase1.

Next, we consider the case where the job arrives after the interval under consideration has ended.
    Section SelfInterferenceBoundCase2.

      Hypothesis H_j_arrives_after_Δ : t1 + Δ job_arrival j.

In this case we proceed similarly to the first case. However in order to safely subtract the task cost from the RBF, we need to consider the interval up to the arrival of the job under consideration.
      Lemma self_intf_bound_case2 :
        workload_of_jobs
          (another_hep_job_of_same_task^~ j)
          (arrivals_between arr_seq t1 (t1 + Δ))
         task_rbf ((job_arrival j - t1) + ε) - task_cost tsk.
      Proof.
        eapply leq_trans with
          (workload_of_jobs (another_hep_job_of_same_task^~ j)
             (arrivals_between arr_seq t1 ( (job_arrival j) + 1)));
          first by apply workload_of_jobs_reduce_range ⇒ //=;lia.
        eapply leq_trans; last first.
        - eapply task_rbf_without_job_under_analysis with (t1 := t1) ⇒ //=.
          lia.
        -
          set (hep_job_of_same_task := (fun x : Jobhep_job x j && (job_task x == tsk))).
          rewrite (workload_of_jobs_equiv_pred _ _ (fun xhep_job_of_same_task x && (x != j) ));
            last first.
          { movej' _.
            rewrite /another_hep_job_of_same_task /hep_job_of_same_task /another_hep_job.
            move : H_job_of_task ⇒ /eqP →.
            lia. }
          rewrite workload_minus_job_cost' //=.
          + apply leq_sub; last first.
            × rewrite /hep_job_of_same_task.
              case (hep_job j j && (job_task j == tsk)) eqn: EQ1; try done.
              contradict EQ1.
              move : H_job_of_task ⇒ /eqP TSK.
              by rewrite /hep_job /FP_to_JLFP H_priority_is_reflexive TSK eq_refl //=.
            × rewrite /task_workload_between /task_workload addnA.
              have → :t1 + (job_arrival j - t1) + ε = job_arrival j + ε by lia.
              apply workload_of_jobs_weaken.
              move : H_job_of_task ⇒ /eqP TSK.
              by movejo /andP[_ /eqP TSK']; apply /eqP; rewrite -TSK TSK'.
          + apply arrived_between_implies_in_arrivals ⇒ //=.
            apply /andP; split; [done| lia].
      Qed.

    End SelfInterferenceBoundCase2.

Combining the above two bounds, we obtain the final bound on the self-interference incurred by any job j of task tsk.
    Lemma self_intf_bound :
      workload_of_jobs
        (another_hep_job_of_same_task^~ j)
        (arrivals_between arr_seq t1 (t1 + Δ))
       task_rbf (maxn ((job_arrival j - t1) + ε) Δ) - (task_cost tsk).
    Proof.
      case ((t1 + Δ) > (job_arrival j)) eqn: MAX.
      - have ->: maxn ((job_arrival j - t1) + ε) Δ = Δ by lia.
        by apply self_intf_bound_case1 ⇒ //=.
      - have ->: maxn ((job_arrival j - t1) + ε) Δ = ((job_arrival j - t1) + ε) by lia.
        apply self_intf_bound_case2 ⇒ //=.
        by lia.
    Qed.

  End SelfInterferenceBound.

Next, we use the above bound on self-interference to state a bound on the total interference incurred by any job j of task tsk.
  Lemma instantiated_task_interference_is_bounded :
    job_interference_is_bounded_by arr_seq sched tsk IBF
      (relative_arrival_time_of_job_is_A sched).
  Proof.
    movet1 t2 Δ j ARR TSK BUSY LT NCOMPL A OFF.
    rewrite /IBF.
    move: (posnP (@job_cost _ Cost j)) ⇒ [ZERO''|POS];
                                          first by exfalso; rewrite /completed_by ZERO'' in NCOMPL.
    have X := cumulative_interference_split.
    rewrite /cumulative_interference in X.
    rewrite X //=.
    clear X.
    rewrite /IBF -addnA leq_add //.
    - pose PI_fun :duration duration := fun priority_inversion_bound.
      have: cumulative_priority_inversion arr_seq sched j t1 (t1 + Δ) PI_fun 0;
        last by apply.
      apply: cumulative_priority_inversion_is_bounded ⇒ //.
    - erewrite cumulative_i_ohep_eq_service_of_ohep ⇒ //;
                                                         last by eauto 6 with basic_rt_facts.
      apply: leq_trans; first by apply service_of_jobs_le_workload ⇒ //=.
      rewrite workload_of_other_jobs_split.
      rewrite -[leqLHS]addnC.
      apply leq_add.
      + specialize (OFF t1 t2 BUSY).
        rewrite OFF.
        by eapply self_intf_bound ⇒ //=.
      + by apply ohep_workload_le_rbf ⇒ //.
  Qed.

F. Defining the Search Space

In this section, we define the concrete search space for FP scheduling. Then, we prove that, if a given A is in the abstract search space, then it is also included in the concrete search space. First, let us recall the definition of the abstract search space as defined in the aRTA framework.
We begin by defining the concrete search space as follows.
    Definition is_in_concrete_search_space A :=
      (A < L) && (task_rbf A != task_rbf (A + ε)).

To rule out pathological cases with the concrete 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 ε.

Then, for any relative arrival time A, we prove that, ...
    Variable A : duration.

... if A is in the abstract search space, ...
... then A is also in the concrete search space.
    Lemma A_is_in_concrete_search_space :
      is_in_concrete_search_space A.
    Proof.
      move: H_A_is_in_abstract_search_space ⇒ [INSP | [/andP [POSA LTL] [x [LTx INSP2]]]].
      - rewrite INSP.
        apply/andP; split; first by done.
        rewrite neq_ltn; apply/orP; left.
        rewrite {1}/task_rbf; erewrite task_rbf_0_zero; eauto 2; try done.
        rewrite add0n /task_rbf; apply leq_trans with (task_cost tsk); try lia.
        exact: task_rbf_1_ge_task_cost.
      - apply/andP; split; first by done.
        apply/negP; intros EQ; move: EQ ⇒ /eqP EQ.
        rewrite /IBF subn1 addn1 prednK // in INSP2.
        apply INSP2.
        case (A < x) eqn: EQ1.
        + have ->: maxn A x = x by lia.
          by have ->: maxn (A + ε) x = x by lia.
        + have ->: maxn A x = A by lia.
          by have ->: maxn (A + ε) x = (A + ε) by lia.
    Qed.

  End ConcreteSearchSpace.

G. Stating the Response-Time Bound R

Finally, we define the response-time bound R as follows. Note the condition 0 < F in the equation below. While this condition is not needed in the RTAs for sequential tasks, it is required here to ensure that we consider the least positive fix point.
  Variable R : duration.
  Hypothesis H_R_is_maximum:
     (A : duration),
      is_in_concrete_search_space A
       (F : duration),
        0 < F
         A + F priority_inversion_bound + total_hep_rbf (A + F)
                    - (task_cost tsk - task_rtct tsk)
         R F + (task_cost tsk - task_rtct tsk).

Next, in this section, we prove that, if a solution to the above equation exists, then a solution to the response-time equation as stated in aRTA also exists.
  Section ResponseTimeReccurence.

To rule out pathological cases with the concrete 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 ε.

We know that, if A is in the abstract search, then it is in the concrete search space, too. We also know that, if A is in the concrete search space, then there exists an R that satisfies H_R_is_maximum. Using these facts, here we prove that, if A is in the abstract search space then, there exists a solution to the response-time equation as stated in the aRTA.
    Corollary correct_search_space :
       A,
        is_in_abstract_search_space A
         F : nat,
          task_rtct tsk + IBF A (A + F) A + F
           F + (task_cost tsk - task_rtct tsk) R.
    Proof.
      moveA IN.
      move: (H_R_is_maximum A) ⇒ FIX.
      feed FIX; first by apply A_is_in_concrete_search_space.
      move: FIX ⇒ [F [GE1 [FIX NEQ]]].
      rewrite /IBF.
       F.
      split; last by done.
      rewrite /IBF.
      eapply leq_trans; last by apply FIX.
      move: H_valid_run_to_completion_threshold ⇒ [BOUND _].
      rewrite /task_rtc_bounded_by_cost in BOUND.
      have F2 : task_rbf (maxn (A + ε) (A + F)) task_cost tsk.
      { eapply (task_rbf_ge_task_cost _ _ _ _) ⇒ //=.
        lia. }
      have MAXX : maxn (A + 1) (A + F) = A + F by lia.
      rewrite MAXX in F2.
      rewrite MAXX.
      have SPLITLE : total_hep_rbf (A + F) total_ohep_rbf (A + F) + task_rbf (A + F).
      { apply split_hep_rbf_weaken ⇒ //. }
      by lia.
      Unshelve.
      all: by done.
    Qed.

  End ResponseTimeReccurence.

H. Soundness of the Response-Time Bound

Finally, we prove that R is a bound on the response time of task tsk.
  Theorem uniprocessor_response_time_bound_fp :
    task_response_time_bound arr_seq sched tsk R.
  Proof.
    intros js ARRs TSKs.
    move: (posnP (@job_cost _ Cost js)) ⇒ [ZERO|POS].
    { by rewrite /job_response_time_bound /completed_by ZERO. }
    eapply uniprocessor_response_time_bound_ideal ⇒ //.
    - exact: instantiated_i_and_w_are_coherent_with_schedule.
    - exact: instantiated_busy_intervals_are_bounded.
    - exact: instantiated_task_interference_is_bounded.
    - by apply : correct_search_space ⇒ //.
  Qed.

End AbstractRTAforFPwithArrivalCurves.