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.
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.
    movej al ar bl br LE1 LE2.
    destruct (leqP al ar) as [NEQ|NEQ].
    - rewrite /cumulative_interference /definitions.cumulative_interference.
      rewrite [in X in _ X](@big_cat_nat _ _ _ al) //=; try lia.
      by rewrite [in X in _ _ + X](@big_cat_nat _ _ _ ar) //=; lia.
    - by rewrite /cumulative_interference /definitions.cumulative_interference big_geq; lia.

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.
    movej t t1 t2 /andP [LE1 LE2].
    rewrite /cumulative_interference /definitions.cumulative_interference.
    by rewrite {1}(@big_cat_nat _ _ _ t) //=.

End InterferenceAndInterferingWorkloadAuxiliary.