Library prosa.analysis.facts.busy_interval.carry_in

Busy Interval From Workload Bound

In the following, we derive an alternative condition for the existence of a busy interval based on the total workload. If the total workload generated by the task set is bounded, then there necessarily exists a moment without any carry-in workload, from which it follows that a busy interval has ended.
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 valid arrival sequence.
Allow for any fully-consuming uniprocessor model.
Next, consider any schedule of the arrival sequence ...
... where jobs do not execute before their arrival or after completion.
Assume a given reflexive JLFP policy.
Further, 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 work-conserving.

Times without Carry-In

As the first step, we derive a sufficient condition for the existence of a no-carry-in instant for uniprocessor for JLFP schedulers.
We start by noting that, trivially, the processor has no carry-in at the beginning (i.e., has no carry-in at time instant 0).
  Lemma no_carry_in_at_zero :
    no_carry_in arr_seq sched 0.

Next, we relate idle times to the no-carry-in condition. First, the presence of a pending job implies that the processor isn't idle due to work-conservation.
  Lemma pending_job_not_idle :
     j t,
      arrives_in arr_seq j
      pending sched j t
      ¬ is_idle arr_seq sched t.

Second, an idle time implies no carry in at this time instant.
  Lemma idle_instant_no_carry_in :
     t,
      is_idle arr_seq sched t
      no_carry_in arr_seq sched t.

Moreover, an idle time implies no carry in at the next time instant, too.
  Lemma idle_instant_next_no_carry_in :
     t,
      is_idle arr_seq sched t
      no_carry_in arr_seq sched t.+1.

Bounded-Workload Assumption

We now introduce the central assumption from which we deduce the existence of a busy interval.
To this end, recall the notion of workload of all jobs released in a given interval [t1, t2)...
... and total service of jobs within some time interval [t1, t2).
We assume that, for some positive Δ, the sum of the total blackout and the total workload generated in any interval of length Δ starting with no carry-in is bounded by Δ. 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,
      no_carry_in arr_seq sched t
      blackout_during sched t (t + Δ) + total_workload t (t + Δ) Δ.

In the following, we also require a unit-speed processor.

Existence of a No-Carry-In Instant

Next we prove that, if for any time instant t there is a point where the total workload generated since t is upper-bounded by the length of the interval, there must exist a no-carry-in instant.
  Section ProcessorIsNotTooBusy.

As a stepping stone, we prove in the following section that for any time instant t there exists another time instant t' ∈ (t, t + Δ] such that the processor has no carry-in at time t'.
Consider an arbitrary time instant t ...
      Variable t : duration.

... such that there is no carry-in at time t.
      Hypothesis H_no_carry_in : no_carry_in arr_seq sched t.

First, recall that the total service is bounded by the total workload. Therefore the sum of the total blackout and the total service of jobs in the interval [t, t + Δ) is bounded by Δ.
      Lemma total_service_is_bounded_by_Δ :
        blackout_during sched t (t + Δ) + total_service t (t + Δ) Δ.
Next we consider two cases: (1) The case when the sum of blackout and service is strictly less than Δ, and (2) the case when the sum of blackout and service is equal to Δ.
In the first case, we use the pigeonhole principle to conclude that there is an idle time instant; which in turn implies existence of a time instant with no carry-in.
      Lemma low_total_service_implies_existence_of_time_with_no_carry_in :
        blackout_during sched t (t + Δ) + total_service t (t + Δ) < Δ
         δ,
          δ < Δ no_carry_in arr_seq sched (t.+1 + δ).

In the second case, the sum of blackout and service within the time interval [t, t + Δ) is equal to Δ. We also know that the total workload is lower-bounded by the total service and upper-bounded by Δ. Therefore, the total workload is equal to the total service, which implies completion of all jobs by time t + Δ and hence no carry-in at time t + Δ.
Finally, we show that any interval of length Δ contains a time instant with no carry-in.
    Lemma processor_is_not_too_busy :
       t, δ,
        δ < Δ no_carry_in arr_seq sched (t + δ).

  End ProcessorIsNotTooBusy.

Busy Interval Existence

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.