Library prosa.analysis.abstract.busy_interval

Lemmas About Abstract Busy Intervals

In this file we prove a few basic lemmas about the notion of an abstract busy interval.
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 processor state model.
  Context {PState : ProcessorState Job}.

Assume we are provided with abstract functions for interference and interfering workload.
  Context `{Interference Job}.
  Context `{InterferingWorkload Job}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Consider an arbitrary task tsk.
  Variable tsk : Task.

Next, consider any work-conserving schedule of this arrival sequence ...
  Variable sched : schedule PState.
  Hypothesis H_work_conserving : work_conserving arr_seq sched.

... where jobs do not execute before their arrival.
Consider an arbitrary job j with positive cost. Notice that a positive-cost assumption is required to ensure that one cannot construct a busy interval without any workload inside of it.
  Variable j : Job.
  Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
  Hypothesis H_job_cost_positive : job_cost_positive j.

We first prove that any interval [t1, t2) is either a busy interval of job j or not.
Consider two intervals [t1, t2)[t1, t2'), where [t1, t2) is a busy-interval prefix and [t1, t2') is not a busy-interval prefix. Then there exists t2'' such that [t1, t2'') is a busy interval.
Next, consider a busy interval [t1, t2) of job j.
  Variable t1 t2 : instant.
  Hypothesis H_busy_interval : busy_interval sched j t1 t2.

First, we prove that job j completes by the end of the busy interval. Note that the busy interval contains the execution of job j; in addition, time instant t2 is a quiet time. Thus by the definition of a quiet time the job must be completed before time t2.
We show that, similarly to the classical notion of busy interval, the job does not receive service before the busy interval starts.
Since the job cannot arrive before the busy interval starts and completes by the end of the busy interval, it receives at least job_cost j units of service within the interval.
Trivially, job j arrives before the end of the busy window (if arrival times are consistent), which is a useful fact to observe for proof automation.
For the same reason, we note the trivial fact that by definition j arrives no earlier than at time t1. For automation, we note this both as a fact on busy-interval prefixes ...
... and complete busy-intervals.
Next, let us assume that the introduced processor model is unit-supply.
Under this assumption, the sum of the total service during the time interval [t1, t1 + Δ) and the cumulative interference during the same interval is bounded by the length of the time interval.
In the following section, we derive a sufficient condition for the existence of abstract busy intervals for unit-service processors.
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 of unit-service processor model.
Assume we are provided with abstract functions for interference and interfering workload ...
  Context `{Interference Job}.
  Context `{InterferingWorkload Job}.

... that do not allow speculative execution.
Consider any arrival sequence with consistent, non-duplicate arrivals.
Consider an arbitrary task tsk.
  Variable tsk : Task.

Next, consider any work-conserving (in the abstract sense) schedule of this arrival sequence ...
  Variable sched : schedule PState.
  Hypothesis H_work_conserving : work_conserving arr_seq sched.

... where jobs do not execute before their arrival or after completion.
Consider an arbitrary job j from task tsk with positive cost.
  Variable j : Job.
  Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
  Hypothesis H_job_task : job_of_task tsk j.
  Hypothesis H_job_cost_positive : job_cost_positive j.

In this section, we prove a fact that allows one to extend an inequality between cumulative interference and interfering workload from a busy-interval prefix [t1, t) to the whole timeline [0, t).
Consider any busy-interval prefix of job j.
    Variable t1 t_busy : instant.
    Hypothesis H_is_busy_prefix : busy_interval_prefix sched j t1 t_busy.+1.

We assume that, for some positive δ, the cumulative interfering workload within interval [t1, t1 + δ) is bounded by cumulative interference in the same interval.
    Variable δ : duration.
    Hypothesis H_iw_bounded :
      cumulative_interfering_workload j t1 (t1 + δ) cumulative_interference j t1 (t1 + δ).

Then the cumulative interfering workload within interval [0, t1 + δ)>> is bounded by the cumulative interference in the same interval.
In the following section, we show that the busy interval is bounded. More specifically, we show that the length of any abstract busy interval is bounded, as long as there is enough supply to accommodate the interfering workload.
  Section BoundingBusyInterval.

For simplicity, let us define some local names.
Suppose that job j is pending at time t_busy.
    Variable t_busy : instant.
    Hypothesis H_j_is_pending : pending sched j t_busy.

First, we show that there must exist a busy interval prefix.
    Section LowerBound.

Since job j is pending at time t_busy, there is a (potentially unbounded) busy interval that starts no later than with the arrival of j.
      Lemma exists_busy_interval_prefix :
         t1,
          busy_interval_prefix t1 t_busy.+1
          t1 job_arrival j t_busy.

    End LowerBound.

Next we prove that, if there is a point where the requested workload is upper-bounded by the supply, then the busy interval eventually ends.
    Section UpperBound.

Consider any busy interval prefix of job j.
      Variable t1 : instant.
      Hypothesis H_is_busy_prefix : busy_interval_prefix t1 t_busy.+1.

We assume that for some positive δ, the cumulative interfering workload within interval [t1, t1 + δ) is bounded by δ.
      Variable δ : duration.
      Hypothesis H_δ_positive : δ > 0.
      Hypothesis H_workload_is_bounded :
        workload_of_job arr_seq j t1 (t1 + δ)
        + cumulative_interfering_workload j t1 (t1 + δ) δ.

If there is a quiet time by time t1 + δ, it trivially follows that the busy interval is bounded. Thus, let's consider first the harder case where there is no quiet time, which turns out to be impossible.
      Section CannotBeBusyForSoLong.

Assume that there is no quiet time in the interval (t1, t1 + δ].
        Hypothesis H_no_quiet_time : t, t1 < t t1 + δ ¬ quiet_time t.

We prove that the sum of cumulative service and cumulative interference in the interval [t, t + δ) is equal to δ.
Since the interval is always non-quiet, the processor is always busy processing job j and the job's interference and, hence, the sum of service of j and its cumulative interference within the interval [t1, t1 + δ) is greater than or equal to δ.
However, since the total workload is bounded (see H_workload_is_bounded), the sum of j's cost and its interfering workload within the interval [t1, t1 + δ) is bounded by j's service and its interference within the same time interval.
        Lemma busy_interval_too_much_workload :
          job_cost j + cumulative_interfering_workload j t1 (t1 + δ)
          service_during sched j t1 (t1 + δ) + cumulative_interference j t1 (t1 + δ).

The latter two lemmas imply that t1 + δ is a quiet time ...
        Lemma t1δ_is_quiet : quiet_time (t1 + δ).

... which is a contradiction with the initial assumption.
        Lemma t1δ_is_quiet_contra : False.

      End CannotBeBusyForSoLong.

Since the interval cannot remain busy for so long, we prove that the busy interval finishes at some point t2 t1 + δ.
      Lemma busy_interval_is_bounded :
         t2,
          t_busy < t2
           t2 t1 + δ
           busy_interval t1 t2.

    End UpperBound.

  End BoundingBusyInterval.

End AbstractBusyIntervalExists.

We add some facts into the "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically where needed.
Global Hint Resolve
  abstract_busy_interval_arrivals_before
  job_completes_within_busy_interval
  abstract_busy_interval_prefix_job_arrival
  abstract_busy_interval_job_arrival
  : basic_rt_facts.