Library prosa.analysis.abstract.iw_auxiliary

Auxiliary Lemmas About Interference and Interfering Workload.

In this file we provide a set of auxiliary 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}.

Consider any kind of fully supply-consuming uniprocessor model.
Consider any valid arrival sequence with consistent arrivals ...
... and any uni-processor schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
Let tsk be any task.
  Variable tsk : Task.

For convenience, we define a function that "folds" cumulative conditional interference with a predicate fun _ _ true to cumulative (unconditional) interference.
  Lemma fold_cumul_interference :
     j t1 t2,
      cumul_cond_interference (fun _ _true) j t1 t2
      = cumulative_interference j t1 t2.
  Proof. by rewrite /cumulative_interference. Qed.

In this section, we prove a few basic properties of conditional interference w.r.t. a generic predicate P.
In the following, consider a predicate P.
    Variable P : Job instant bool.

First, we show that the cumulative conditional interference within a time interval [t1, t2) can be rewritten as a sum over all time instances satisfying P j.
    Lemma cumul_cond_interference_alt :
       j t1 t2,
        cumul_cond_interference P j t1 t2 = \sum_(t1 t < t2 | P j t) interference j t.
    Proof.
      movej t1 t2; rewrite [RHS]big_mkcond //=; apply eq_big_natt _.
      by rewrite /cond_interference; case: (P j t).
    Qed.

Next, 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
        cumul_cond_interference P j al ar cumul_cond_interference P j bl br.
    Proof.
      movej al ar bl br LE1 LE2.
      rewrite !cumul_cond_interference_alt.
      case: (leqP al ar) ⇒ [LEQ|LT]; last by rewrite big_geq.
      rewrite [leqRHS](@big_cat_nat _ _ _ al) //=; last by lia.
      by rewrite [in X in _ _ + X](@big_cat_nat _ _ _ ar) //=; lia.
    Qed.

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
        cumul_cond_interference P j t1 t2
        = cumul_cond_interference P j t1 t + cumul_cond_interference P j t t2.
    Proof.
      movej t t1 t2 /andP [LE1 LE2].
      by rewrite !cumul_cond_interference_alt {1}(@big_cat_nat _ _ _ t) //=.
    Qed.

  End CondInterferencePredicate.

Next, we show a few relations between interference functions conditioned on different predicates.
Consider predicates P1, P2.
    Variables P1 P2 : Job instant bool.

We introduce a lemma (similar to ssreflect's bigID lemma) that allows us to split the cumulative conditional interference w.r.t predicate P1 into a sum of two cumulative conditional interference w.r.t. predicates P1 && P2 and P1 && ~~ P2, respectively.
    Lemma cumul_cond_interference_ID :
       j t1 t2,
        cumul_cond_interference P1 j t1 t2
        = cumul_cond_interference (fun j tP1 j t && P2 j t) j t1 t2
          + cumul_cond_interference (fun j tP1 j t && ~~ P2 j t) j t1 t2.
    Proof.
      movej t1 t2.
      rewrite -big_split //=; apply eq_bigrt _.
      rewrite /cond_interference.
      by case (P1 _ _), (P2 _ _ ), (interference _ _).
    Qed.

If two predicates P1 and P2 are equivalent, then they can be used interchangeably with cumul_cond_interference.
    Lemma cumul_cond_interference_pred_eq :
       (j : Job) (t1 t2 : instant),
        ( j t, P1 j t P2 j t)
        cumul_cond_interference P1 j t1 t2
        = cumul_cond_interference P2 j t1 t2.
    Proof.
      movej t1 t2 EQU.
      apply eq_bigrt _; rewrite /cond_interference.
      move: (EQU j t).
      by case (P1 j t), (P2 j t), (interference _ _); moveCONTR ⇒ //=; exfalso; apply notF, CONTR.
    Qed.

  End CondInterferenceRelation.

End InterferenceAndInterferingWorkloadAuxiliary.