Library prosa.analysis.abstract.restricted_supply.bounded_bi.elf

Sufficient Condition for Bounded Busy Intervals for RS ELF

In this section, we show that the existence of L such that B + total_hep_rbf L SBF L, where B is the blocking bound and SBF is a supply-bound function, is a sufficient condition for the existence of bounded busy intervals under ELF scheduling with a restricted-supply processor model.
Consider any type of tasks with relative priority-points ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{PriorityPoint Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any kind of fully supply-consuming unit-supply uniprocessor model.
Consider an FP policy that indicates a higher-or-equal priority relation, and assume that the relation is reflexive, transitive. and total.
Consider any valid arrival sequence.
Next, consider a schedule of this arrival sequence, ...
  Variable sched : schedule PState.

... allow for any work-bearing notion of job readiness, ...
  Context `{!JobReady Job PState}.
  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

... and assume that the schedule is valid.
Assume that jobs have bounded non-preemptive segments.
Further assume that the schedule follows the ELF scheduling policy.
Recall that busy_intervals_are_bounded_by is an abstract notion. Hence, we need to introduce interference and interfering workload. We will use the restricted-supply instantiations.
We say that job j incurs interference at time t iff it cannot execute due to (1) the lack of supply at time t, (2) service inversion (i.e., a lower-priority job receiving service at t), or a higher-or-equal-priority job receiving service.
The interfering workload, in turn, is defined as the sum of the blackout predicate, service inversion predicate, and the interfering workload of jobs with higher or equal priority.
Assume that the schedule is work-conserving in the abstract sense.
Consider an arbitrary task set ts, ...
  Variable ts : list Task.

... assume that all jobs come from the task set, ...
... and that the cost of a job does not exceed its task's WCET.
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 = 0.
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 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.
The next step is to establish a bound on the maximum busy-window length, which aRSA requires to be given. To this end, let L be any positive fixed point of the busy-interval recurrence. As the lemma busy_intervals_are_bounded_rs_elf shows, under ELF scheduling, this is sufficient to guarantee that all busy intervals are bounded by L.
  Variable L : duration.
  Hypothesis H_L_positive : 0 < L.

  Hypothesis H_fixed_point:
     (A : duration),
      blocking_bound ts tsk A + total_hep_request_bound_function_FP ts tsk L SBF L.

Next, we provide a step-by-step proof of busy-interval boundedness.
  Section StepByStepProof.

Consider any job j of task tsk that has a positive job cost and is in the arrival sequence.
    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 to be the start of the busy-interval.
    Variable : instant.

Now we have two cases: (1) when the busy-interval prefix continues until time instant + L and (2) when the busy interval prefix terminates earlier. In either case, we can show that the busy-interval prefix is bounded.
We start with the first case, where the busy-interval prefix continues until time instant + L.
    Section Case1.

Consider that [t1, job_arrival j] and [t1, t1 + L) are both busy-interval prefixes of job j. Note that at this point we do not necessarily know that job_arrival j L; hence, we assume the existence of both prefixes.
The crucial point to note is that the sum of the job's cost (represented as workload_of_job) and the interfering workload in the interval [t1, t1 + L) is bounded by L due to the fixed point H_fixed_point.
      Local Lemma workload_is_bounded :
        workload_of_job arr_seq j ( + L) + cumulative_interfering_workload j ( + L) L.
      Proof.
        rewrite (cumulative_interfering_workload_split _ _ _).
        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ ( + L) _ _ _)); (try apply H_valid_SBF) ⇒ //.
        rewrite // addnC -!addnA.
        have E: a b c, a c b c - a a + b c by move ⇒ ? ? ? ? ?; lia.
        apply: E; first by lia.
        rewrite subKn; last by apply: sbf_bounded_by_duration ⇒ //.
        specialize (H_fixed_point (job_arrival j - )).
        rewrite -(leqRW H_fixed_point); apply leq_add.
        - apply: leq_trans; first apply: service_inversion_is_bounded ⇒ //.
          + instantiate (1 := fun (A : duration) ⇒ blocking_bound ts tsk A) ⇒ //=.
            by movejo t t' ARRo TSKo PREFo; apply: nonpreemptive_segments_bounded_by_blocking ⇒ //.
          + by done.
        - rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
          apply workload_of_jobs_bounded ⇒ //.
          movej'.
          move: H_job_of_tsk ⇒ /eqP .
          by apply hep_job_implies_hep_task.
        Qed.


It follows that + L is a quiet time, which means that the busy prefix ends (i.e., it is bounded).
      Local Lemma busy_prefix_is_bounded_case1 :
         t2,
          job_arrival j <
           + L
           busy_interval arr_seq sched j .
      Proof.
        have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival ⇒ //.
        enough( t2, job_arrival j < + L definitions.busy_interval sched j ) as BUSY.
        { have [ [ [ ]]] := BUSY.
          eexists; split; first by exact: .
          split; first by done.
          by apply instantiated_busy_interval_equivalent_busy_interval.
        }
        eapply busy_interval.busy_interval_is_bounded; eauto 2 ⇒ //.
        - by eapply instantiated_i_and_w_no_speculative_execution; eauto 2 ⇒ //.
        - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix ⇒ //.
        - by apply workload_is_bounded ⇒ //.
      Qed.


    End Case1.

Next, we consider the case when the interval [t1, t1 + L) is not a busy-interval prefix.
    Section Case2.

Consider that [t1, job_arrival j] is a busy-interval prefix of j and [t1, t1 + L) is not.
      Hypothesis H_arrives : job_arrival j.
      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j (job_arrival j).+1.
      Hypothesis H_no_busy_prefix_L : ¬ busy_interval_prefix arr_seq sched j ( + L).

From the properties of busy intervals, one can conclude that j's arrival time is less than + L.
      Local Lemma job_arrival_is_bounded :
        job_arrival j < + L.
      Proof.
        move_neq_up FF.
        move: (H_busy_prefix_arr) (H_busy_prefix_arr) ⇒ PREFIX PREFIXA.
        apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in PREFIXA ⇒ //.
        move: (PREFIXA) ⇒ GTC.
        eapply workload_exceeds_interval with (Δ := L) in PREFIX ⇒ //.
        { move_neq_down PREFIX.
          rewrite (cumulative_interfering_workload_split _ _ _).
          rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (job_arrival j).+1 _ _ _)); (try apply H_valid_SBF) ⇒ //.
          rewrite addnC -!addnA.
          have E: a b c, a c b c - a a + b c by move ⇒ ? ? ? ? ?; lia.
          apply: E; first by lia.
          rewrite subKn; last by apply: sbf_bounded_by_duration ⇒ //.
          specialize (H_fixed_point (job_arrival j - )).
          rewrite -(leqRW H_fixed_point); apply leq_add.
          { rewrite (leqRW (service_inversion_widen _ _ _ _ _ (job_arrival j).+1 _ _ )).
            - apply: leq_trans.
              + apply: service_inversion_is_bounded ⇒ //.
                move ⇒ *; instantiate (1 := fun (A : duration) ⇒ blocking_bound ts tsk A) ⇒ //.
                by apply: nonpreemptive_segments_bounded_by_blocking ⇒ //.
              + by done.
            - by done.
            - lia.
          }
          { rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
            apply workload_of_jobs_bounded ⇒ //.
            movej'.
            move: H_job_of_tsk ⇒ /eqP .
            by apply hep_job_implies_hep_task. }
        }
      Qed.


Lemma job_arrival_is_bounded implies that the busy-interval prefix starts at time , continues until job_arrival j + 1, and then terminates before + L. Or, in other words, there is point in time such that (1) j's arrival is bounded by , (2) is bounded by + L, and (3) [t1, t2) is the busy interval of job j.
      Local Lemma busy_prefix_is_bounded_case2:
         t2, job_arrival j < + L busy_interval arr_seq sched j .
      Proof.
        have LE: job_arrival j < + L
          by apply job_arrival_is_bounded ⇒ //; try apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
        move: (H_busy_prefix_arr) ⇒ PREFIX.
        move: (H_no_busy_prefix_L) ⇒ NOPREF.
        apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in PREFIX ⇒ //.
        have BUSY := terminating_busy_prefix_is_busy_interval _ _ _ _ _ _ _ PREFIX.
        edestruct BUSY as [ BUS]; clear BUSY; try apply TSK; eauto 2 ⇒ //.
        { moveT; apply: NOPREF.
          by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in T ⇒ //.
        }
         ; split; last split.
        { move: BUS ⇒ [[A _] _]; lia. }
        { move_neq_up FA.
          apply: NOPREF; split; [lia | split; first by apply H_busy_prefix_arr].
          split.
          - movet NEQ.
            apply abstract_busy_interval_classic_busy_interval_prefix in BUS ⇒ //.
            by apply BUS; lia.
          - lia.
        }
        { by apply instantiated_busy_interval_equivalent_busy_interval ⇒ //. }
      Qed.


    End Case2.

  End StepByStepProof.

Combining the cases analyzed above, we conclude that busy intervals of jobs released by task tsk are bounded by L.
  Lemma busy_intervals_are_bounded_rs_elf :
    busy_intervals_are_bounded_by arr_seq sched tsk L.
  Proof.
    movej ARR TSK POS.
    have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival ⇒ //.
    have [ [GE PREFIX]]:
       t1, job_arrival j
             busy_interval_prefix arr_seq sched j (job_arrival j).+1
        by apply: busy_interval_prefix_exists.
     .
    enough( t2, job_arrival j < + L busy_interval arr_seq sched j ) as BUSY.
    { move: BUSY ⇒ [ [LT [LE BUSY]]]; eexists; split; last first.
      { split; first by exact: LE.
        by apply instantiated_busy_interval_equivalent_busy_interval. }
      { by apply/andP; split. }
    }
    { have [LPREF|NOPREF] := busy_interval_prefix_case ltac:(eauto) j ( + L).
      { apply busy_prefix_is_bounded_case1 ⇒ //.
        by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix ⇒ //. }
      { apply busy_prefix_is_bounded_case2⇒ //.
        moveNP; apply: NOPREF.
        by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix ⇒ //.
      }
    }
  Qed.


End BoundedBusyIntervals.