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