Library prosa.analysis.abstract.restricted_supply.bounded_bi.jlfp

Sufficient Condition for Bounded Busy Intervals for RS JLFP

In this section, we show that the existence of L such that B + total_rbf L SBF L, where 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 JLFP scheduling with a restricted-supply processor model. Note that this is not the tightest bound, but it can be useful in case the blocking bound is small or zero.
Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost 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 a JLFP policy that indicates a higher-or-equal priority relation, and assume that the relation is reflexive and transitive.
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.
Furthermore, we assume that the schedule is work-conserving ...
... and that it respects the 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.
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.
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.
Let blocking_bound be a function that bounds the priority inversion caused by lower-priority jobs, where the argument blocking_bound takes is the relative offset (w.r.t. the beginning of the corresponding busy interval) of a job to be analyzed.
  Variable blocking_bound : (* A *) duration duration.

Assume that the service inversion is bounded by the blocking bound, ...
... and that blocking_bound reaches its maximum at 0.
  Hypothesis H_blocking_bound_max :
     A, blocking_bound 0 blocking_bound A.

Let L be any positive fixed point of busy-interval recurrence blocking_bound 0 + total_rbf ts L SBF L.
  Variable L : duration.
  Hypothesis H_L_positive : 0 < L.
  Hypothesis H_fixed_point :
    blocking_bound 0 + total_request_bound_function ts 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.

We consider two cases: (1) when the busy-interval prefix continues until time instant t1 + 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 t1 + L.
    Section Case1.

Consider a time instant t1 such 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, in this section (only), we assume the existence of both prefixes.
      Variable t1 : instant.
      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
      Hypothesis H_busy_prefix_L : busy_interval_prefix arr_seq sched j t1 (t1 + L).

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 t1 (t1 + L) + cumulative_interfering_workload j t1 (t1 + L) L.
      Proof.
        rewrite (cumulative_interfering_workload_split _ _ _).
        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (t1 + 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 ⇒ //.
        rewrite -(leqRW H_fixed_point); apply leq_add.
        - by rewrite (leqRW (H_service_inversion_bounded _ _ _ _ _ _ _)) //=.
        - rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
          by apply hep_workload_le_total_rbf.
      Qed.

It follows that t1 + 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 < t2
           t2 t1 + L
           busy_interval arr_seq sched j t1 t2.
      Proof.
        have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival ⇒ //.
        enough( t2, job_arrival j < t2 t2 t1 + L definitions.busy_interval sched j t1 t2) as BUSY.
        { have [t2 [LE1 [LE2 BUSY2]]] := BUSY.
          eexists; split; first by exact: LE1.
          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 eapply instantiated_i_and_w_are_coherent_with_schedule; 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 a time instant t1 such that [t1, job_arrival j]>> is a busy-interval prefix of j and [t1, t1 + L) is not.
      Variable t1 : instant.
      Hypothesis H_arrives : t1 job_arrival j.
      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
      Hypothesis H_no_busy_prefix_L : ¬ busy_interval_prefix arr_seq sched j t1 (t1 + L).

From the properties of busy intervals, one can conclude that j's arrival time is less than t1 + L.
      Local Lemma job_arrival_is_bounded :
        job_arrival j < t1 + 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 ⇒ //.
          rewrite -(leqRW H_fixed_point); apply leq_add.
          { rewrite (leqRW (service_inversion_widen _ _ _ t1 _ _ (job_arrival j).+1 _ _ )).
            - by rewrite (leqRW (H_service_inversion_bounded _ _ _ _ _ _ _)) //=.
            - by done.
            - by lia.
          }
          { rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
            by apply hep_workload_le_total_rbf.
          }
        }
      Qed.

Lemma job_arrival_is_bounded implies that the busy-interval prefix starts at time t1, continues until job_arrival j + 1, and then terminates before t1 + L. Or, in other words, there is point in time t2 such that (1) j's arrival is bounded by t2, (2) t2 is bounded by t1 + L, and (3) [t1, t2) is busy interval of job j.
      Local Lemma busy_prefix_is_bounded_case2:
         t2, job_arrival j < t2 t2 t1 + L busy_interval arr_seq sched j t1 t2.
      Proof.
        have LE: job_arrival j < t1 + 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 [t2 BUS]; clear BUSY; try apply TSK; eauto 2 ⇒ //.
        { moveT; apply: NOPREF.
          by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in T ⇒ //.
        }
         t2; split; last split.
        { by 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.
          - by 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_jlfp :
    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 ⇒ //.
    edestruct ( busy_interval_prefix_exists) as [t1 [GE PREFIX]]; eauto 2.
     t1.
    enough( t2, job_arrival j < t2 t2 t1 + L busy_interval arr_seq sched j t1 t2) as BUSY.
    { move: BUSY ⇒ [t2 [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 t1 (t1 + 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.