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.

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

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

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.

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 + Δ).

End BoundedBusyIntervalsAux.