Library prosa.analysis.abstract.restricted_supply.bounded_bi.aux

Require Export prosa.analysis.abstract.restricted_supply.iw_instantiation.

Helper Lemmas for Bounded Busy Interval Lemmas

In this section, we introduce a few lemmas that facilitate the proof of an upper bound on busy intervals for various priority policies in the context of the restricted-supply processor model.
Section BoundedBusyIntervalsAux.

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.
  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive : reflexive_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.

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.

Assume that the schedule is work-conserving in the abstract sense.
  Hypothesis H_work_conserving : abstract.definitions.work_conserving arr_seq sched.

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_cost_positive : job_cost_positive j.

First, we note that, since job j is pending at time job_arrival j, there is a (potentially unbounded) busy interval that starts no later than with the arrival of j.
  Lemma busy_interval_prefix_exists :
    ∃ t1,
      t1 ≤ job_arrival j
      ∧ busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
  Proof.
    have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival ⇒ //.
    have PREFIX := busy_interval.exists_busy_interval_prefix ltac:(eauto) j.
    feed (PREFIX (job_arrival j)); first by done.
    move: PREFIX ⇒ [t1 [PREFIX /andP [GE1 _]]].
    by eexists; split; last by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix ⇒ //.
  Qed.

Let <t1, t2)>> be a busy-interval prefix.
  Variable t1 t2 : instant.
  Hypothesis H_busy_prefix : busy_interval_prefix arr_seq sched j t1 t2.

We show that the service of higher-or-equal-priority jobs is less than the workload of higher-or-equal-priority jobs in any subinterval [t1, t) of the interval [t1, t2).
  Lemma service_lt_workload_in_busy :
    ∀ t,
      t1 < t < t2 →
      service_of_hep_jobs arr_seq sched j t1 t < workload_of_hep_jobs arr_seq j t1 t.
  Proof.
    move⇒ t /andP [LT1 LT2]; move: (H_busy_prefix) ⇒ PREF.
    move_neq_up LE.
    have EQ: workload_of_hep_jobs arr_seq j t1 t = service_of_hep_jobs arr_seq sched j t1 t.
    { apply/eqP; rewrite eqn_leq; apply/andP; split ⇒ //.
      by apply service_of_jobs_le_workload ⇒ //.
    }
    clear LE; move: PREF ⇒ [LT [QT1 [NQT QT2]]].
    specialize (NQT t ltac:(lia)); apply: NQT ⇒ s ARR HEP BF.
    have EQ2: workload_of_hep_jobs arr_seq j 0 t = service_of_hep_jobs arr_seq sched j 0 t.
    { rewrite /workload_of_hep_jobs (workload_of_jobs_cat _ t1); last by lia.
      rewrite /service_of_hep_jobs (service_of_jobs_cat_scheduling_interval _ _ _ _ _ 0 t t1) //; last by lia.
      rewrite /workload_of_hep_jobs in EQ; rewrite EQ; clear EQ.
      apply/eqP; rewrite eqn_add2r.
      replace (service_of_jobs sched (hep_job^~ j) (arrivals_between arr_seq 0 t1) t1 t) with 0; last first.
      { symmetry; apply: big1_seq ⇒ h /andP [HEPh BWh].
        apply big1_seq ⇒ t' /andP [_ IN].
        apply not_scheduled_implies_no_service, completed_implies_not_scheduled ⇒ //.
        apply: completion_monotonic; last apply QT1 ⇒ //.
        { by rewrite mem_index_iota in IN; lia. }
        { by apply: in_arrivals_implies_arrived. }
        { by apply: in_arrivals_implies_arrived_before. }
      }
      rewrite addn0; apply/eqP.
      apply all_jobs_have_completed_impl_workload_eq_service ⇒ //.
      move ⇒ h ARRh HEPh; apply: QT1 ⇒ //.
      - by apply: in_arrivals_implies_arrived.
      - by apply: in_arrivals_implies_arrived_before.
    }
    by apply: workload_eq_service_impl_all_jobs_have_completed ⇒ //.
  Qed.

Consider a subinterval [t1, t1 + Δ) of the interval [t1, t2)>>. We show that the sum of j's workload and the cumulative workload in [t1, t1 + Δ) is strictly larger than Δ.
  Lemma workload_exceeds_interval :
    ∀ Δ,
      0 < Δ →
      t1 + Δ < t2 →
      Δ < workload_of_job arr_seq j t1 (t1 + Δ) + cumulative_interfering_workload j t1 (t1 + Δ).
  Proof.
    move⇒ δ POS LE; move: (H_busy_prefix) ⇒ PREF.
    apply leq_ltn_trans with (service_during sched j t1 (t1 + δ) + cumulative_interference j t1 (t1 + δ)).
    { rewrite /service_during /cumulative_interference /cumul_cond_interference /cond_interference /service_at.
      rewrite -big_split //= -{1}(sum_of_ones t1 δ) big_nat [in X in _ ≤ X]big_nat.
      apply leq_sum ⇒ x /andP[Lo Hi].
      { move: (H_work_conserving j t1 t2 x) ⇒ Workj.
        feed_n 4 Workj; try done.
        { by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix. }
        { by apply/andP; split; eapply leq_trans; eauto. }
        destruct interference.
        - by lia.
        - by rewrite //= addn0; apply Workj.
      }
    }
    rewrite cumulative_interfering_workload_split // cumulative_interference_split //.
    rewrite cumulative_iw_hep_eq_workload_of_ohep cumulative_i_ohep_eq_service_of_ohep //; last by apply PREF.
    rewrite -[leqRHS]addnC -[leqRHS]addnA [(_ + workload_of_job _ _ _ _ )]addnC.
    rewrite workload_job_and_ahep_eq_workload_hep //.
    rewrite -addnC -addnA [(_ + service_during _ _ _ _ )]addnC.
    rewrite service_plus_ahep_eq_service_hep //; last by move: PREF ⇒ [_ [_ [_ /andP [A B]]]].
    rewrite ltn_add2l.
    by apply: service_lt_workload_in_busy; eauto; lia.
  Qed.

End BoundedBusyIntervalsAux.