Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.definitions.interference.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
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 :
forall j t1 t2 ,
cumul_cond_interference (fun _ _ => true) j t1 t2
= cumulative_interference j t1 t2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task
forall (j : Job) (t1 t2 : nat),
cumul_cond_interference (fun => xpredT) j t1 t2 =
cumulative_interference j t1 t2
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task
forall (j : Job) (t1 t2 : nat),
cumul_cond_interference (fun => xpredT) j t1 t2 =
cumulative_interference j t1 t2
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 :
forall j t1 t2 ,
cumul_cond_interference P j t1 t2 = \sum_(t1 <= t < t2 | P j t) interference j t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P : Job -> instant -> bool
forall (j : Job) (t1 t2 : nat),
cumul_cond_interference P j t1 t2 =
\sum_(t1 <= t < t2 | P j t) interference j t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P : Job -> instant -> bool
forall (j : Job) (t1 t2 : nat),
cumul_cond_interference P j t1 t2 =
\sum_(t1 <= t < t2 | P j t) interference j t
move => j t1 t2; rewrite [RHS]big_mkcond //=; apply eq_big_nat => t _.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P : Job -> instant -> bool j : Job t1, t2, t : nat
cond_interference P j t =
(if P j t then interference j t else 0 )
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 :
forall (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.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P : Job -> instant -> bool
forall (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 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P : Job -> instant -> bool
forall (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
move => j al ar bl br LE1 LE2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P : Job -> instant -> bool j : Job al, ar, bl, br : instant LE1 : bl <= al LE2 : ar <= br
cumul_cond_interference P j al ar <=
cumul_cond_interference P j bl br
rewrite !cumul_cond_interference_alt.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P : Job -> instant -> bool j : Job al, ar, bl, br : instant LE1 : bl <= al LE2 : ar <= br
\sum_(al <= t < ar | P j t) interference j t <=
\sum_(bl <= t < br | P j t) interference j t
case : (leqP al ar) => [LEQ|LT]; last by rewrite big_geq.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P : Job -> instant -> bool j : Job al, ar, bl, br : instant LE1 : bl <= al LE2 : ar <= br LEQ : al <= ar
\sum_(al <= t < ar | P j t) interference j t <=
\sum_(bl <= t < br | P j t) interference j t
rewrite [leqRHS](@big_cat_nat _ _ _ al) //=; last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P : Job -> instant -> bool j : Job al, ar, bl, br : instant LE1 : bl <= al LE2 : ar <= br LEQ : al <= ar
\sum_(al <= t < ar | P j t) interference j t <=
\sum_(bl <= i < al | P j i) interference j i +
\sum_(al <= i < br | P j i) interference j i
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 :
forall 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.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P : Job -> instant -> bool
forall (j : Job) (t t1 t2 : nat),
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 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P : Job -> instant -> bool
forall (j : Job) (t t1 t2 : nat),
t1 <= t <= t2 ->
cumul_cond_interference P j t1 t2 =
cumul_cond_interference P j t1 t +
cumul_cond_interference P j t t2
move => j t t1 t2 /andP [LE1 LE2].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P : Job -> instant -> bool j : Job t, t1, t2 : nat LE1 : t1 <= t LE2 : t <= t2
cumul_cond_interference P j t1 t2 =
cumul_cond_interference P j t1 t +
cumul_cond_interference P j t t2
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 :
forall 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.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P1, P2 : Job -> instant -> bool
forall (j : Job) (t1 t2 : nat),
cumul_cond_interference P1 j t1 t2 =
cumul_cond_interference
(fun (j0 : Job) (t : instant) => P1 j0 t && P2 j0 t)
j t1 t2 +
cumul_cond_interference
(fun (j0 : Job) (t : instant) =>
P1 j0 t && ~~ P2 j0 t) j t1 t2
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P1, P2 : Job -> instant -> bool
forall (j : Job) (t1 t2 : nat),
cumul_cond_interference P1 j t1 t2 =
cumul_cond_interference
(fun (j0 : Job) (t : instant) => P1 j0 t && P2 j0 t)
j t1 t2 +
cumul_cond_interference
(fun (j0 : Job) (t : instant) =>
P1 j0 t && ~~ P2 j0 t) j t1 t2
move => j t1 t2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P1, P2 : Job -> instant -> bool j : Job t1, t2 : nat
cumul_cond_interference P1 j t1 t2 =
cumul_cond_interference
(fun (j : Job) (t : instant) => P1 j t && P2 j t) j
t1 t2 +
cumul_cond_interference
(fun (j : Job) (t : instant) => P1 j t && ~~ P2 j t)
j t1 t2
rewrite -big_split //=; apply eq_bigr => t _.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P1, P2 : Job -> instant -> bool j : Job t1, t2, t : nat
cond_interference P1 j t =
cond_interference
(fun (j : Job) (t : instant) => P1 j t && P2 j t) j
t +
cond_interference
(fun (j : Job) (t : instant) => P1 j t && ~~ P2 j t)
j t
rewrite /cond_interference.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P1, P2 : Job -> instant -> bool j : Job t1, t2, t : nat
P1 j t && interference j t =
P1 j t && P2 j t && interference j t +
P1 j t && ~~ P2 j t && interference j t
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 :
forall (j : Job) (t1 t2 : instant),
(forall j t , P1 j t <-> P2 j t) ->
cumul_cond_interference P1 j t1 t2
= cumul_cond_interference P2 j t1 t2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P1, P2 : Job -> instant -> bool
forall (j : Job) (t1 t2 : instant),
(forall (j0 : Job) (t : instant), P1 j0 t <-> P2 j0 t) ->
cumul_cond_interference P1 j t1 t2 =
cumul_cond_interference P2 j t1 t2
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P1, P2 : Job -> instant -> bool
forall (j : Job) (t1 t2 : instant),
(forall (j0 : Job) (t : instant), P1 j0 t <-> P2 j0 t) ->
cumul_cond_interference P1 j t1 t2 =
cumul_cond_interference P2 j t1 t2
move => j t1 t2 EQU.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P1, P2 : Job -> instant -> bool j : Job t1, t2 : instant EQU : forall (j : Job) (t : instant),
P1 j t <-> P2 j t
cumul_cond_interference P1 j t1 t2 =
cumul_cond_interference P2 j t1 t2
apply eq_bigr => t _; rewrite /cond_interference.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P1, P2 : Job -> instant -> bool j : Job t1, t2 : instant EQU : forall (j : Job) (t : instant),
P1 j t <-> P2 j tt : nat
P1 j t && interference j t =
P2 j t && interference j t
move : (EQU j t).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : Interference Job H4 : InterferingWorkload Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched tsk : Task P1, P2 : Job -> instant -> bool j : Job t1, t2 : instant EQU : forall (j : Job) (t : instant),
P1 j t <-> P2 j tt : nat
P1 j t <-> P2 j t ->
P1 j t && interference j t =
P2 j t && interference j t
by case (P1 j t), (P2 j t), (interference _ _); move => CONTR => //=; exfalso ; apply notF, CONTR.
Qed .
End CondInterferenceRelation .
End InterferenceAndInterferingWorkloadAuxiliary .