Library prosa.analysis.facts.busy_interval.ideal.carry_in

Require Export prosa.analysis.facts.busy_interval.carry_in.
Require Export prosa.analysis.facts.busy_interval.ideal.busy_interval.

The following lemma conceptually belongs in prosa.analysis.facts.busy_interval.carry_in, but still has dependencies with a baked-in ideal uniprocessor assumption. When these dependencies get generalized, then this lemma should be generalized as well and moved elsewhere.

Section BusyWindowExistence.

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 {Arrival: JobArrival Job}.
  Context {Cost : JobCost Job}.

Consider any valid arrival sequence.

Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arr_seq : valid_arrival_sequence arr_seq.

Next, consider any well-behaved ideal uni-processor schedule of this arrival sequence.

  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_jobs_come_from_arrival_sequence:
    jobs_come_from_arrival_sequence sched arr_seq.
  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Assume a given reflexive JLFP policy.

Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.

Further, allow for any work-bearing notion of job readiness ...

Context `{@JobReady Job (ideal.processor_state Job ) Cost Arrival}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

... and assume that the schedule is work-conserving.

Hypothesis H_work_conserving : work_conserving arr_seq sched.

Recall the notion of workload of all jobs released in a given interval [t1, t2).

Let total_workload t1 t2 :=
workload_of_jobs predT (arrivals_between arr_seq t1 t2).

Assume that for some positive Δ, the sum of requested workload at time t + Δ is bounded by Δ (i.e., the supply). Note that this assumption bounds the total workload of jobs released in a time interval [t, t + Δ) regardless of their priorities.

  Variable Δ : duration.
  Hypothesis H_delta_positive : Δ > 0.
  Hypothesis H_workload_is_bounded : ∀ t, total_workload t (t + Δ) ≤ Δ.

Consider an arbitrary job j with positive cost.

  Variable j : Job.
  Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
  Hypothesis H_job_cost_positive : job_cost_positive j.

We show that there must exist a busy interval [t1, t2) that contains the arrival time of j.

  Corollary exists_busy_interval_from_total_workload_bound :
    ∃ t1 t2 ,
      t1 ≤ job_arrival j < t2 ∧
      t2 ≤ t1 + Δ ∧
      busy_interval arr_seq sched j t1 t2.

End BusyWindowExistence.