Library prosa.analysis.abstract.busy_interval

Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.behavior.all.
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 ideal uni-processor 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.

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.

End LemmasAboutAbstractBusyInterval.