Library prosa.analysis.facts.busy_interval.carry_in

Throughout this file, we assume ideal uniprocessor schedules.
Require Import prosa.model.processor.ideal.

Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model.
Require Import prosa.model.readiness.basic.

Existence of No Carry-In Instant

In this section, we derive an alternative condition for the existence of a busy interval. The new condition requires the total workload (instead of the high-priority workload) generated by the task set to be bounded.
Next, we derive a sufficient condition for existence of no carry-in instant for uniprocessor for JLFP schedulers
Section ExistsNoCarryIn.

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 arrival sequence with consistent arrivals.
Next, consider any ideal uniprocessor schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
Assume a given JLFP policy.
  Context `{JLFP_policy Job}.

For simplicity, let's define some local names.
The fact that there is no carry-in at time instant t trivially implies that t is a quiet time.
  Lemma no_carry_in_implies_quiet_time :
     j t,
      no_carry_in t
      quiet_time j t.

Assume that the schedule is work-conserving, ...
... and there are no duplicate job arrivals.
We show that an idle time implies no carry in at this time instant.
  Lemma idle_instant_implies_no_carry_in_at_t :
     t,
      is_idle sched t
      no_carry_in t.

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

Let the priority relation be reflexive.
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).
Assume that for some positive Δ, the sum of requested workload at time (t + Δ) is bounded by delta (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 + Δ) Δ.

Next we prove that since for any time instant t there is a point where the total workload is upper-bounded by the supply the processor encounters no carry-in instants at least every Δ time units.
  Section ProcessorIsNotTooBusy.

We start by proving that the processor has no carry-in at the beginning (i.e., has no carry-in at time instant 0).
    Lemma no_carry_in_at_the_beginning :
      no_carry_in 0.

In this section, we prove 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 the processor has no carry-in at time t.
      Hypothesis H_no_carry_in: no_carry_in t.

First, recall that the total service is bounded by the total workload. Therefore the total service of jobs in the interval [t, t + Δ) is bounded by Δ.
      Lemma total_service_is_bounded_by_Δ :
        total_service t (t + Δ) Δ.

Next we consider two cases: (1) The case when the total service is strictly less than Δ, (2) And when the total 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 :
        total_service t (t + Δ) < Δ
         δ, δ < Δ no_carry_in (t.+1 + δ).

In the second case, the total service within the time interval [t, t + Δ) is equal to Δ. On the other hand, we know that the total workload is lower-bounded by the total service and upper-bounded by Δ. Therefore, the total workload is equal to total service this implies completion of all jobs by time t + Δ and hence no carry-in at time t + Δ.
      Lemma completion_of_all_jobs_implies_no_carry_in :
        total_service t (t + Δ) = Δ
        no_carry_in (t + Δ).

    End ProcessorIsNotTooBusyInduction.

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 (t + δ).

  End ProcessorIsNotTooBusy.

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