Project Page Index Table of Contents

# Library prosa.analysis.abstract.iw_auxiliary

Require Export prosa.analysis.definitions.interference.
Require Export prosa.analysis.definitions.task_schedule.
Require Export prosa.analysis.facts.priority.classes.
Require Export prosa.analysis.abstract.restricted_supply.busy_prefix.
Require Export prosa.model.aggregate.service_of_jobs.
Require Export prosa.analysis.facts.model.service_of_jobs.

# 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.
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}.
Consider any kind of fully supply-consuming uniprocessor model.
Context `{PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
Consider any valid arrival sequence with consistent arrivals ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
... and any uni-processor schedule of this arrival sequence ...
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
... 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.
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.
Section CondInterferencePredicate.
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.
move⇒ j t1 t2; rewrite [RHS]big_mkcond //=; apply eq_big_nat ⇒ t _.
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.
move ⇒ j 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.
move ⇒ j 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.
Section CondInterferenceRelation.
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 t ⇒ P1 j t && P2 j t) j t1 t2
+ cumul_cond_interference (fun j t ⇒ P1 j t && ~~ P2 j t) j t1 t2.
Proof.
move⇒ j t1 t2.
rewrite -big_split //=; apply eq_bigr ⇒ t _.
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.
move⇒ j t1 t2 EQU.
apply eq_bigr ⇒ t _; rewrite /cond_interference.
move: (EQU j t).
by case (P1 j t), (P2 j t), (interference _ _); move⇒ CONTR ⇒ //=; exfalso; apply notF, CONTR.
Qed.
End CondInterferenceRelation.
End InterferenceAndInterferingWorkloadAuxiliary.