Library prosa.analysis.abstract.iw_auxiliary

Require Export prosa.util.nat.
Require Export prosa.analysis.abstract.definitions.

Auxiliary Lemmas About Interference and Interfering Workload.

In this file we provide a set of auxiliary definitions and lemmas about generic properties of Interference and Interfering Workload.

Section InterferenceAndInterferingWorkloadAuxiliary.

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

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

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

First, we show that cumulative interference on an interval [al, ar) is bounded by the cumulative interference on an interval [bl,br) if [al,ar) ⊆ [bl,br).

  Lemma cumulative_interference_sub :
    ∀ (j : Job) (al ar bl br : instant),
      bl ≤ al →
      ar ≤ br →
      cumulative_interference j al ar ≤ cumulative_interference j bl br.

We show that the cumulative interference of a job can be split into disjoint intervals.

  Lemma cumulative_interference_cat :
    ∀ j t t1 t2,
      t1 ≤ t ≤ t2 →
      cumulative_interference j t1 t2 = cumulative_interference j t1 t + cumulative_interference j t t2.

End InterferenceAndInterferingWorkloadAuxiliary.