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

Require Export prosa.analysis.abstract.restricted_supply.abstract_rta.
Require Export prosa.analysis.abstract.restricted_supply.iw_instantiation.
Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.aux.
Require Export prosa.analysis.facts.busy_interval.carry_in.
Require Export prosa.analysis.definitions.sbf.busy.

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.
Section BoundedBusyIntervals.

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.
  Context `{PState : ProcessorState Job}.
  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.

Consider a JLFP policy that indicates a higher-or-equal priority relation, and assume that the relation is reflexive and transitive.
  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
  Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.

Consider any valid arrival sequence.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

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.
  Hypothesis H_sched_valid : valid_schedule sched arr_seq.

Assume that jobs have bounded non-preemptive segments.
  Context `{JobPreemptable Job}.
  Context `{TaskMaxNonpreemptiveSegment Task}.
  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.

Furthermore, we assume that the schedule is work-conserving ...
  Hypothesis H_work_conserving : work_conserving arr_seq sched.

... and that it respects the scheduling policy.
  Hypothesis H_respects_policy :
    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.

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.
  #[local] Instance rs_jlfp_interference : Interference Job :=
    rs_jlfp_interference arr_seq sched.

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.
  #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
    rs_jlfp_interfering_workload arr_seq sched.

Consider an arbitrary task set ts, ...
  Variable ts : list Task.

... assume that all jobs come from the task set, ...
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

... and that the cost of a job does not exceed its task's WCET.
  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.

Let max_arrivals be a family of valid arrival curves.
  Context `{MaxArrivals Task}.
  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.

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.
  Context {SBF : SupplyBoundFunction}.
  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.

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, ...
  Hypothesis H_service_inversion_bounded :
    service_inversion_is_bounded_by arr_seq sched tsk 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 ⇒ //.
        { move ⇒ T; 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.
          - move⇒ t 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.
    move ⇒ j 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⇒ //.
        move⇒ NP; apply: NOPREF.
        by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix ⇒ //.
      }
    }
  Qed.

End BoundedBusyIntervals.