Library prosa.analysis.abstract.busy_interval

Require Export prosa.analysis.abstract.iw_auxiliary.
Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.abstract.definitions.

Lemmas About Abstract Busy Intervals

In this file we prove a few basic lemmas about the notion of an abstract busy interval.

Section LemmasAboutAbstractBusyInterval.

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.

Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.

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.

  Lemma busy_interval_prefix_case :
    ∀ t1 t2,
      busy_interval_prefix sched j t1 t2 ∨ ¬ busy_interval_prefix sched j t1 t2.

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.

  Lemma terminating_busy_prefix_is_busy_interval :
    ∀ t1 t2 t2',
      t2 ≤ t2' →
      busy_interval_prefix sched j t1 t2 →
      ¬ busy_interval_prefix sched j t1 t2' →
      ∃ t2'', busy_interval sched j t1 t2''.

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.

Lemma job_completes_within_busy_interval :
completed_by sched j t2.

We show that, similarly to the classical notion of busy interval, the job does not receive service before the busy interval starts.

Lemma no_service_before_busy_interval :
∀ t, service sched j t = service_during sched j t1 t.

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.

Lemma service_within_busy_interval_ge_job_cost :
job_cost j ≤ service_during sched j t1 t2.

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.

  Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
  Fact abstract_busy_interval_arrivals_before :
    j \in arrivals_before arr_seq t2.

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

Fact abstract_busy_interval_prefix_job_arrival :
∀ t t', busy_interval_prefix sched j t t' → t ≤ job_arrival j.

... and complete busy-intervals.

Fact abstract_busy_interval_job_arrival :
t1 ≤ job_arrival j.

Next, let us assume that the introduced processor model is unit-supply.

Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.

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.

  Lemma service_and_interference_bound :
    ∀ Δ,
      t1 + Δ ≤ t2 →
      service_during sched j t1 (t1 + Δ) + cumulative_interference j t1 (t1 + Δ) ≤ Δ.

End LemmasAboutAbstractBusyInterval.

In the following section, we derive a sufficient condition for the existence of abstract busy intervals for unit-service processors.

Section AbstractBusyIntervalExists.

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.

Context {PState : ProcessorState Job}.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.

Assume we are provided with abstract functions for interference and interfering workload ...

Context `{Interference Job}.
Context `{InterferingWorkload Job}.

... that do not allow speculative execution.

Hypothesis H_no_speculative_exec : no_speculative_execution.

Consider any arrival sequence with consistent, non-duplicate arrivals.

  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
  Hypothesis H_arrival_sequence_is_a_set : arrival_sequence_uniq arr_seq.

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.

Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

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

Section CumulativeIntIntWorkExtension.

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.

      Local Lemma cumul_iw_bounded_by_cumul_i :
        cumulative_interfering_workload j 0 (t1 + δ) ≤ cumulative_interference j 0 (t1 + δ).

  End CumulativeIntIntWorkExtension.

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.

    Let quiet_time t := quiet_time sched j t.
    Let busy_interval_prefix := busy_interval_prefix sched j.
    Let busy_interval := busy_interval sched j.

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

Lemma busy_interval_has_uninterrupted_service :
δ ≤ service_during sched j t1 (t1 + δ) + cumulative_interference j t1 (t1 + δ).

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.