From d5cf8f9d9ec6654eb7b16cada5f241dce1e2eda3 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Tue, 3 May 2016 16:57:18 +0200
Subject: [PATCH] Keep only the definition of parallel interference
---
analysis/basic/bertogna_edf_theory.v | 355 ++++++---
analysis/basic/bertogna_fp_theory.v | 366 ++++++---
analysis/basic/interference_bound_edf.v | 77 +-
analysis/jitter/bertogna_edf_theory.v | 393 ++++++----
analysis/jitter/bertogna_fp_theory.v | 866 ++++++++++++---------
analysis/jitter/interference_bound_edf.v | 40 +-
analysis/parallel/bertogna_edf_theory.v | 6 +-
analysis/parallel/bertogna_fp_theory.v | 10 +-
analysis/parallel/interference_bound_edf.v | 4 +-
implementation/basic/schedule.v | 6 +-
implementation/jitter/schedule.v | 7 +-
model/basic/interference.v | 260 ++-----
model/basic/interference_edf.v | 44 +-
model/basic/platform.v | 7 +-
model/basic/platform_fp.v | 7 +-
model/basic/schedule.v | 69 +-
model/jitter/interference.v | 276 ++-----
model/jitter/interference_edf.v | 28 +-
model/jitter/platform.v | 8 +-
model/jitter/platform_fp.v | 8 +-
model/jitter/schedule.v | 110 ++-
21 files changed, 1649 insertions(+), 1298 deletions(-)
diff --git a/analysis/basic/bertogna_edf_theory.v b/analysis/basic/bertogna_edf_theory.v
index 4224b7250..beb291777 100644
--- a/analysis/basic/bertogna_edf_theory.v
+++ b/analysis/basic/bertogna_edf_theory.v
@@ -125,8 +125,8 @@ Module ResponseTimeAnalysisEDF.
(* Let's call x the interference incurred by job j due to tsk_other, ...*)
Let x (tsk_other: sporadic_task) :=
- task_interference_sequential job_cost job_task sched j
- tsk_other (job_arrival j) (job_arrival j + R).
+ task_interference job_cost job_task sched j tsk_other
+ (job_arrival j) (job_arrival j + R).
(* and X the total interference incurred by job j due to any task. *)
Let X := total_interference job_cost sched j (job_arrival j) (job_arrival j + R).
@@ -183,7 +183,7 @@ Module ResponseTimeAnalysisEDF.
have INts := bertogna_edf_tsk_other_in_ts.
apply leq_trans with (n := workload job_task sched tsk_other
(job_arrival j) (job_arrival j + R));
- first by apply task_interference_seq_le_workload.
+ first by apply task_interference_le_workload.
by apply workload_bounded_by_W with (task_deadline0 := task_deadline)
(job_cost0 := job_cost) (job_deadline0 := job_deadline); try (by ins); last 2 first;
[ by apply bertogna_edf_R_other_ge_cost
@@ -215,46 +215,43 @@ Module ResponseTimeAnalysisEDF.
Lemma bertogna_edf_too_much_interference : X >= R - task_cost tsk + 1.
Proof.
rename H_completed_jobs_dont_execute into COMP,
- H_valid_job_parameters into PARAMS,
- H_job_of_tsk into JOBtsk,
- H_j_not_completed into NOTCOMP.
+ H_valid_job_parameters into PARAMS, H_response_time_is_fixed_point into REC,
+ H_job_of_tsk into JOBtsk, H_j_not_completed into NOTCOMP.
unfold completed, valid_sporadic_job in *.
-
- (* Since j has not completed, recall the time when it is not
- executing is the total interference. *)
- exploit (complement_of_interf_equals_service job_cost sched j (job_arrival j)
- (job_arrival j + R));
- last intro EQinterf; ins; unfold has_arrived; first by apply leqnn.
- rewrite {2}[_ + R]addnC -addnBA // subnn addn0 in EQinterf.
- rewrite addn1.
- move: NOTCOMP; rewrite neq_ltn; move => /orP NOTCOMP; des;
- last first.
+ unfold X, total_interference; rewrite addn1.
+ rewrite -(ltn_add2r (task_cost tsk)).
+ rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
+ rewrite -addnBA // subnn addn0.
+ move: (NOTCOMP) => /negP NOTCOMP'.
+ rewrite neq_ltn in NOTCOMP.
+ move: NOTCOMP => /orP [LT | BUG]; last first.
{
- apply (leq_ltn_trans (COMP j (job_arrival j + R))) in NOTCOMP.
- by rewrite ltnn in NOTCOMP.
+ exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
+ by apply cumulative_service_le_job_cost.
}
- apply leq_trans with (n := R - service sched j (job_arrival j + R)); last first.
+ apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
+ backlogged job_cost sched j t) +
+ service sched j (job_arrival j + R)); last first.
{
- unfold service; rewrite service_before_arrival_eq_service_during; ins.
- rewrite EQinterf subKn; first by done.
- {
- unfold total_interference.
- rewrite -{1}[_ j]add0n big_addn addnC -addnBA // subnn addn0.
- rewrite -{2}[R]subn0 -[R-_]mul1n -[1*_]addn0 -iter_addn.
- by rewrite -big_const_nat leq_sum //; ins; apply leq_b1.
- }
- }
- {
- apply ltn_sub2l; last first.
- {
- apply leq_trans with (n := job_cost j); first by ins.
- rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS0.
- }
- apply leq_trans with (n := job_cost j); first by ins.
- apply leq_trans with (n := task_cost tsk);
- first by rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS0.
- by rewrite bertogna_edf_R_other_ge_cost.
+ rewrite -addn1 -addnA leq_add2l addn1.
+ apply leq_trans with (n := job_cost j); first by done.
+ by specialize (PARAMS j); des; rewrite -JOBtsk.
}
+ unfold service; rewrite service_before_arrival_eq_service_during //.
+ rewrite -big_split /=.
+ apply leq_trans with (n := \sum_(job_arrival j <= i < job_arrival j + R) 1);
+ first by rewrite big_const_nat iter_addn mul1n addn0 addKn.
+ rewrite big_nat_cond [\sum_(_ <= _ < _ | true) _]big_nat_cond.
+ apply leq_sum; move => i /andP [/andP [GEi LTi] _].
+ destruct (backlogged job_cost sched j i) eqn:BACK;
+ first by rewrite -addn1 addnC; apply leq_add.
+ apply negbT in BACK.
+ rewrite add0n lt0n -not_scheduled_no_service negbK.
+ rewrite /backlogged negb_and negbK in BACK.
+ move: BACK => /orP [/negP NOTPENDING | SCHED]; last by done.
+ exfalso; apply NOTPENDING; unfold pending; apply/andP; split; first by done.
+ apply/negP; red; intro BUG; apply NOTCOMP'.
+ by apply completion_monotonic with (t := i); try (by done); apply ltnW.
Qed.
Let scheduled_task_other_than_tsk (t: time) (tsk_other: sporadic_task) :=
@@ -304,8 +301,62 @@ Module ResponseTimeAnalysisEDF.
}
}
Qed.
+
+ (* 2) Prove that during the scheduling window of j, any job that is scheduled while j is
+ backlogged comes from a different task. *)
+ Lemma bertogna_edf_interference_by_different_tasks :
+ forall t j_other,
+ job_arrival j <= t < job_arrival j + R ->
+ backlogged job_cost sched j t ->
+ scheduled sched j_other t ->
+ job_task j_other != tsk.
+ Proof.
+ rename H_all_jobs_from_taskset into FROMTS,
+ H_valid_task_parameters into PARAMS,
+ H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
+ H_work_conserving into WORK,
+ H_tsk_R_in_rt_bounds into INbounds,
+ H_all_previous_jobs_completed_on_time into BEFOREok,
+ H_tasks_miss_no_deadlines into NOMISS,
+ H_constrained_deadlines into CONSTR.
+ move => t j_other /andP [LEt GEt] BACK SCHED.
+ apply/eqP; red; intro SAMEtsk.
+ move: SCHED => /existsP [cpu SCHED].
+ assert (SCHED': scheduled sched j_other t).
+ by apply/existsP; exists cpu.
+ clear SCHED; rename SCHED' into SCHED.
+ move: (SCHED) => PENDING.
+ apply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING; try (by done).
+ destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
+ {
+ move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
+ specialize (BEFOREok j_other tsk R SAMEtsk INbounds LT).
+ move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
+ apply completion_monotonic with (t0 := job_arrival j_other + R); try (by done).
+ apply leq_trans with (n := job_arrival j); last by done.
+ apply leq_trans with (n := job_arrival j_other + task_deadline tsk);
+ first by rewrite leq_add2l; apply NOMISS.
+ apply leq_trans with (n := job_arrival j_other + task_period tsk);
+ first by rewrite leq_add2l; apply CONSTR; rewrite -JOBtsk FROMTS.
+ rewrite -SAMEtsk; apply SPO; [ | by rewrite JOBtsk | by apply ltnW].
+ by red; intro EQ; subst; rewrite ltnn in BEFOREother.
+ }
+ {
+ move: PENDING => /andP [ARRIVED _].
+ exploit (SPO j j_other); [ | by rewrite SAMEtsk | by done | ]; last first.
+ {
+ apply/negP; rewrite -ltnNge.
+ apply leq_ltn_trans with (n := t); first by done.
+ apply leq_trans with (n := job_arrival j + R); first by done.
+ by rewrite leq_add2l; apply leq_trans with (n := task_deadline tsk);
+ [by apply NOMISS | by rewrite JOBtsk CONSTR // -JOBtsk FROMTS].
+ }
+ by red; intros EQtsk; subst; rewrite /backlogged SCHED andbF in BACK.
+ }
+ Qed.
+
- (* 2) Next, we prove that the sum of the interference of each task is equal
+ (* 3) Next, we prove that the sum of the interference of each task is equal
to the total interference multiplied by the number of processors. This
holds because interference only occurs when all processors are busy. *)
Lemma bertogna_edf_all_cpus_busy :
@@ -313,43 +364,82 @@ Module ResponseTimeAnalysisEDF.
Proof.
rename H_all_jobs_from_taskset into FROMTS,
H_valid_task_parameters into PARAMS,
- H_job_of_tsk into JOBtsk,
- H_sporadic_tasks into SPO,
+ H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
+ H_work_conserving into WORK,
H_tsk_R_in_rt_bounds into INbounds,
H_all_previous_jobs_completed_on_time into BEFOREok,
H_tasks_miss_no_deadlines into NOMISS,
H_rt_bounds_contains_all_tasks into UNZIP,
- H_constrained_deadlines into RESTR.
+ H_constrained_deadlines into CONSTR.
unfold sporadic_task_model in *.
unfold x, X, total_interference, task_interference.
- rewrite -big_mkcond -exchange_big big_distrl /=.
+ rewrite -big_mkcond -exchange_big big_distrl /= mul1n.
rewrite [\sum_(_ <= _ < _ | backlogged _ _ _ _) _]big_mkcond.
- apply eq_big_nat; move => t LEt.
- destruct (backlogged job_cost sched j t) eqn:BACK;
- last by rewrite (eq_bigr (fun i => 0));
- [by rewrite big_const_seq iter_addn mul0n addn0 | by done].
- rewrite big_mkcond mul1n /=.
- rewrite big_filter big_mkcond.
- rewrite (eq_bigr (fun i => if (scheduled_task_other_than_tsk t i) then 1 else 0));
- last first.
+ apply eq_big_nat; move => t /andP [GEt LTt].
+ destruct (backlogged job_cost sched j t) eqn:BACK; last first.
{
- unfold scheduled_task_other_than_tsk; intros i _; clear -i.
- by destruct (task_is_scheduled job_task sched i t); rewrite ?andFb ?andTb ?andbT //; desf.
+ rewrite (eq_bigr (fun i => 0));
+ first by rewrite big_const_seq iter_addn mul0n addn0.
+ by intros i _; rewrite (eq_bigr (fun i => 0));
+ first by rewrite big_const_seq iter_addn mul0n addn0.
}
- rewrite -big_mkcond sum1_count.
- by apply bertogna_edf_scheduling_invariant.
+ rewrite big_mkcond /=.
+ rewrite exchange_big /=.
+ apply eq_trans with (y := \sum_(cpu < num_cpus) 1); last by simpl_sum_const.
+ apply eq_bigr; intros cpu _.
+ move: (WORK j t BACK cpu) => [j_other /eqP SCHED]; unfold scheduled_on in *.
+ rewrite (bigD1_seq (job_task j_other)) /=; last by rewrite filter_uniq.
+ {
+ rewrite (eq_bigr (fun i => 0));
+ last by intros i DIFF; rewrite /task_scheduled_on SCHED;apply/eqP;rewrite eqb0 eq_sym.
+ rewrite big_const_seq iter_addn mul0n 2!addn0; apply/eqP; rewrite eqb1.
+ by unfold task_scheduled_on; rewrite SCHED.
+ }
+ rewrite mem_filter; apply/andP; split; last by apply FROMTS.
+ unfold jldp_can_interfere_with.
+ apply bertogna_edf_interference_by_different_tasks with (t := t); [by auto | by done |].
+ by apply/existsP; exists cpu; apply/eqP.
+ Qed.
+
+ (* 4) Show that by the induction hypothesis, all jobs released
+ before the end of the interval complete by their periods. *)
+ Lemma bertogna_edf_all_previous_jobs_complete_by_their_period:
+ forall t (j0: JobIn arr_seq),
+ t < job_arrival j + R ->
+ job_arrival j0 + task_period (job_task j0) <= t ->
+ completed job_cost sched j0
+ (job_arrival j0 + task_period (job_task j0)).
+ Proof.
+ rename H_rt_bounds_contains_all_tasks into UNZIP,
+ H_constrained_deadlines into CONSTR,
+ H_tasks_miss_no_deadlines into NOMISS,
+ H_all_jobs_from_taskset into FROMTS,
+ H_all_previous_jobs_completed_on_time into BEFOREok.
+ intros t j0 LEt LE.
+ cut ((job_task j0) \in unzip1 rt_bounds); [intro IN | by rewrite UNZIP FROMTS].
+ move: IN => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
+ apply completion_monotonic with (t0 := job_arrival j0 + R0); first by done.
+ {
+ rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
+ [by apply NOMISS | by apply CONSTR; rewrite FROMTS].
+ }
+ apply BEFOREok with (tsk_other := (job_task j0)); try by done.
+ apply leq_ltn_trans with (n := t); last by done.
+ apply leq_trans with (n := job_arrival j0 + task_period (job_task j0)); last by done.
+ by rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
+ [by apply NOMISS | apply CONSTR; rewrite FROMTS].
Qed.
(* Let (cardGE delta) be the number of interfering tasks whose interference
is larger than delta. *)
Let cardGE (delta: time) := count (fun i => x i >= delta) ts_interf.
- (* 3) If there is at least one of such tasks (e.g., cardGE > 0), then the
+ (* 5) If there is at least one of such tasks (e.g., cardGE > 0), then the
cumulative interference caused by the complementary set of interfering
tasks fills at least (num_cpus - cardGE) processors. *)
Lemma bertogna_edf_helper_lemma :
forall delta,
- cardGE delta > 0 ->
+ 0 < cardGE delta < num_cpus ->
\sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
Proof.
rename H_all_jobs_from_taskset into FROMTS,
@@ -359,19 +449,21 @@ Module ResponseTimeAnalysisEDF.
H_tsk_R_in_rt_bounds into INbounds,
H_all_previous_jobs_completed_on_time into BEFOREok,
H_tasks_miss_no_deadlines into NOMISS,
- H_constrained_deadlines into RESTR.
+ H_constrained_deadlines into CONSTR,
+ H_sequential_jobs into SEQ.
unfold sporadic_task_model in *.
- intros delta HAS.
+ move => delta /andP [HAS LT].
+ rewrite -has_count in HAS.
+
set some_interference_A := fun t =>
- backlogged job_cost sched j t &&
- has (fun tsk_k => ((x tsk_k >= delta) &&
- task_is_scheduled job_task sched tsk_k t)) ts_interf.
+ has (fun tsk_k => backlogged job_cost sched j t &&
+ (x tsk_k >= delta) &&
+ task_is_scheduled job_task sched tsk_k t) ts_interf.
set total_interference_B := fun t =>
backlogged job_cost sched j t *
count (fun tsk_k => (x tsk_k < delta) &&
- task_is_scheduled job_task sched tsk_k t) ts_interf.
+ task_is_scheduled job_task sched tsk_k t) ts_interf.
- rewrite -has_count in HAS.
apply leq_trans with ((\sum_(job_arrival j <= t < job_arrival j + R)
some_interference_A t) * (num_cpus - cardGE delta)).
{
@@ -379,39 +471,69 @@ Module ResponseTimeAnalysisEDF.
move: HAS => /hasP HAS; destruct HAS as [tsk_a INa LEa].
apply leq_trans with (n := x tsk_a); first by apply LEa.
unfold x, task_interference, some_interference_A.
- apply leq_sum; ins.
- destruct (backlogged job_cost sched j i);
- [rewrite 2!andTb | by ins].
- destruct (task_is_scheduled job_task sched tsk_a i) eqn:SCHEDa;
- [apply eq_leq; symmetry | by ins].
- apply/eqP; rewrite eqb1.
- by apply/hasP; exists tsk_a; last by apply/andP.
+ apply leq_sum_nat; move => t /andP [GEt LTt] _.
+ destruct (backlogged job_cost sched j t) eqn:BACK;
+ last by rewrite (eq_bigr (fun x => 0)); [by simpl_sum_const | by ins].
+ destruct ([exists cpu, task_scheduled_on job_task sched tsk_a cpu t]) eqn:SCHED;
+ last first.
+ {
+ apply negbT in SCHED; rewrite negb_exists in SCHED; move: SCHED => /forallP ALL.
+ rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const.
+ by intros cpu _; specialize (ALL cpu); apply negbTE in ALL; rewrite ALL.
+ }
+ move: SCHED => /existsP [cpu SCHED].
+ apply leq_trans with (n := 1); last first.
+ {
+ rewrite lt0b; apply/hasP; exists tsk_a; first by done.
+ by rewrite LEa 2!andTb; apply/existsP; exists cpu.
+ }
+ rewrite (bigD1 cpu) /= // SCHED.
+ rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const; rewrite leq_b1.
+ intros cpu' DIFF.
+ apply/eqP; rewrite eqb0; apply/negP.
+ intros SCHED'.
+ move: DIFF => /negP DIFF; apply DIFF; apply/eqP.
+ unfold task_scheduled_on in *.
+ destruct (sched cpu t) as [j1|] eqn:SCHED1; last by done.
+ destruct (sched cpu' t) as [j2|] eqn:SCHED2; last by done.
+ move: SCHED SCHED' => /eqP JOB /eqP JOB'.
+ subst tsk_a; symmetry in JOB'.
+ assert (PENDING1: pending job_cost sched j1 t).
+ {
+ apply scheduled_implies_pending; try by done.
+ by apply/existsP; exists cpu; apply/eqP.
+ }
+ assert (PENDING2: pending job_cost sched j2 t).
+ {
+ apply scheduled_implies_pending; try by done.
+ by apply/existsP; exists cpu'; apply/eqP.
+ }
+ assert (BUG: j1 = j2).
+ {
+ apply platform_at_most_one_pending_job_of_each_task with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (tsk0 := tsk)
+ (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) (j0 := j) (t0 := t);
+ rewrite ?JOBtsk ?SAMEtsk //; first by apply PARAMS; rewrite -JOBtsk FROMTS.
+ intros j0 tsk0 TSK0 LE.
+ by apply (bertogna_edf_all_previous_jobs_complete_by_their_period t); rewrite ?TSK0.
+ }
+ by subst j2; apply SEQ with (j := j1) (t := t).
}
+
apply leq_trans with (\sum_(job_arrival j <= t < job_arrival j + R)
total_interference_B t).
{
rewrite big_distrl /=.
- rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
- apply leq_sum; move => t /andP [LEt _].
+ apply leq_sum_nat; move => t LEt _.
unfold some_interference_A, total_interference_B.
destruct (backlogged job_cost sched j t) eqn:BACK;
- [rewrite andTb mul1n | by done].
+ [rewrite mul1n /= | by rewrite has_pred0 //].
+
destruct (has (fun tsk_k : sporadic_task => (delta <= x tsk_k) &&
task_is_scheduled job_task sched tsk_k t) ts_interf) eqn:HAS';
last by done.
- rewrite mul1n; move: HAS => /hasP HAS.
- destruct HAS as [tsk_k INk LEk].
-
- have COUNT := bertogna_edf_scheduling_invariant t LEt BACK.
-
+ rewrite mul1n; move: HAS => /hasP [tsk_k INk LEk].
unfold cardGE.
- set interfering_tasks_at_t :=
- [seq tsk_k <- ts_interf | task_is_scheduled job_task
- sched tsk_k t].
-
- rewrite -(count_filter (fun i => true)) in COUNT.
- fold interfering_tasks_at_t in COUNT.
- rewrite count_predT in COUNT.
apply leq_trans with (n := num_cpus -
count (fun i => (x i >= delta) &&
task_is_scheduled job_task sched i t) ts_interf).
@@ -420,48 +542,32 @@ Module ResponseTimeAnalysisEDF.
rewrite -2!sum1_count big_mkcond /=.
rewrite [\sum_(_ <- _ | _ <= _)_]big_mkcond /=.
apply leq_sum; intros i _.
- destruct (task_is_scheduled job_task sched i t);
+ by destruct (task_is_scheduled job_task sched i t);
[by rewrite andbT | by rewrite andbF].
}
-
- rewrite leq_subLR -count_predUI.
- apply leq_trans with (n :=
- count (predU (fun i : sporadic_task =>
- (delta <= x i) &&
- task_is_scheduled job_task sched i t)
- (fun tsk_k0 : sporadic_task =>
- (x tsk_k0 < delta) &&
- task_is_scheduled job_task sched tsk_k0 t))
- ts_interf); last by apply leq_addr.
- apply leq_trans with (n := size interfering_tasks_at_t).
- {
- rewrite -COUNT.
- rewrite leq_eqVlt; apply/orP; left; apply/eqP; f_equal.
- unfold interfering_tasks_at_t.
- rewrite -filter_predI; apply eq_filter; red; simpl.
- by intros i; rewrite andbC.
- }
- unfold interfering_tasks_at_t.
- rewrite -count_predT count_filter.
- rewrite leq_eqVlt; apply/orP; left; apply/eqP.
- apply eq_count; red; simpl.
- intros i.
- destruct (task_is_scheduled job_task sched i t);
- rewrite 3?andTb ?andFb ?andbF ?andbT /=; try ins.
- by rewrite leqNgt orNb.
+ rewrite -count_filter -[count _ ts_interf]count_filter.
+ eapply leq_trans with (n := count (predC (fun tsk => delta <= x tsk)) _);
+ last by apply eq_leq, eq_in_count; red; ins; rewrite ltnNge.
+ rewrite leq_subLR count_predC size_filter.
+ apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
+ first by rewrite bertogna_edf_scheduling_invariant.
+ by rewrite count_filter.
}
{
- unfold x at 2, task_interference.
- rewrite exchange_big /=; apply leq_sum; intros t _.
- unfold total_interference_B.
- destruct (backlogged job_cost sched j t); last by ins.
- rewrite mul1n -sum1_count.
- rewrite big_seq_cond big_mkcond [\sum_(i <- ts_interf | _ < _) _]big_mkcond.
- by apply leq_sum; ins; clear -i; desf; des; rewrite ?Heq2.
+ unfold x at 2, total_interference_B.
+ rewrite exchange_big /=; apply leq_sum; intros t _.
+ destruct (backlogged job_cost sched j t) eqn:BACK; last by ins.
+ rewrite mul1n -sum1_count.
+ rewrite big_mkcond [\sum_(i <- ts_interf | _ < _) _]big_mkcond /=.
+ apply leq_sum_seq; move => tsk_k IN _.
+ destruct (x tsk_k < delta); [rewrite andTb | by rewrite andFb].
+ destruct (task_is_scheduled job_task sched tsk_k t) eqn:SCHED; last by done.
+ move: SCHED => /existsP [cpu SCHED].
+ by rewrite (bigD1 cpu) /= // SCHED.
}
Qed.
- (* 4) Next, we prove that, for any interval delta, if the sum of per-task
+ (* 6) Next, we prove that, for any interval delta, if the sum of per-task
interference exceeds delta * num_cpus, the same applies for the
sum of the minimum between the interference and delta. *)
Lemma bertogna_edf_minimum_exceeds_interference :
@@ -507,10 +613,11 @@ Module ResponseTimeAnalysisEDF.
apply leq_trans with (n := delta * cardGE delta +
delta * (num_cpus - cardGE delta));
first by rewrite -mulnDr subnKC //; apply ltnW.
- by rewrite leq_add2l; apply bertogna_edf_helper_lemma; rewrite -has_count.
+ by rewrite leq_add2l; apply bertogna_edf_helper_lemma; apply/andP; split;
+ first by rewrite -has_count.
Qed.
- (* 5) Now, we prove that the Bertogna's interference bound
+ (* 7) Now, we prove that the Bertogna's interference bound
is not enough to cover the sum of the "minimum" term over
all tasks (artifact of the proof by contradiction). *)
Lemma bertogna_edf_sum_exceeds_total_interference:
@@ -554,7 +661,7 @@ Module ResponseTimeAnalysisEDF.
by apply bertogna_edf_too_much_interference.
Qed.
- (* 6) After concluding that the sum of the minimum exceeds (R - e_i + 1),
+ (* 8) After concluding that the sum of the minimum exceeds (R - e_i + 1),
we prove that there exists a tuple (tsk_k, R_k) such that
min (x_k, R - e_i + 1) > min (W_k, edf_bound, R - e_i + 1). *)
Lemma bertogna_edf_exists_task_that_exceeds_bound :
diff --git a/analysis/basic/bertogna_fp_theory.v b/analysis/basic/bertogna_fp_theory.v
index 748ef0bcb..5fce53b10 100644
--- a/analysis/basic/bertogna_fp_theory.v
+++ b/analysis/basic/bertogna_fp_theory.v
@@ -9,9 +9,9 @@ Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisFP.
- Export Job SporadicTaskset Schedule Workload Interference InterferenceBoundFP
+ Export Job SporadicTaskset ScheduleOfSporadicTask Workload Interference InterferenceBoundFP
Platform PlatformFP Schedulability ResponseTime Priority SporadicTaskArrival WorkloadBound.
-
+
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
@@ -132,8 +132,8 @@ Module ResponseTimeAnalysisFP.
(* Let's call x the interference incurred by job j due to tsk_other, ...*)
Let x (tsk_other: sporadic_task) :=
- task_interference_sequential job_cost job_task sched j
- tsk_other (job_arrival j) (job_arrival j + R).
+ task_interference job_cost job_task sched j tsk_other
+ (job_arrival j) (job_arrival j + R).
(* and X the total interference incurred by job j due to any task. *)
Let X := total_interference job_cost sched j (job_arrival j) (job_arrival j + R).
@@ -194,7 +194,7 @@ Module ResponseTimeAnalysisFP.
have INts := bertogna_fp_tsk_other_in_ts.
apply leq_trans with (n := workload job_task sched tsk_other
(job_arrival j) (job_arrival j + R));
- first by apply task_interference_seq_le_workload.
+ first by apply task_interference_le_workload.
by apply workload_bounded_by_W with (task_deadline0 := task_deadline)
(job_cost0 := job_cost) (job_deadline0 := job_deadline);
try (by ins); last 2 first;
@@ -216,45 +216,43 @@ Module ResponseTimeAnalysisFP.
Proof.
rename H_completed_jobs_dont_execute into COMP,
H_valid_job_parameters into PARAMS,
- H_job_of_tsk into JOBtsk,
- H_j_not_completed into NOTCOMP.
+ H_response_time_recurrence_holds into REC,
+ H_job_of_tsk into JOBtsk, H_j_not_completed into NOTCOMP.
unfold completed, valid_sporadic_job in *.
-
- (* Since j has not completed, recall the time when it is not
- executing is the total interference. *)
- exploit (complement_of_interf_equals_service job_cost sched j (job_arrival j)
- (job_arrival j + R));
- last intro EQinterf; ins; unfold has_arrived; first by apply leqnn.
- rewrite {2}[_ + R]addnC -addnBA // subnn addn0 in EQinterf.
- rewrite addn1.
- move: NOTCOMP; rewrite neq_ltn; move => /orP NOTCOMP; des;
- last first.
+ unfold X, total_interference; rewrite addn1.
+ rewrite -(ltn_add2r (task_cost tsk)).
+ rewrite subh1; last by rewrite [R](REC) // leq_addr.
+ rewrite -addnBA // subnn addn0.
+ move: (NOTCOMP) => /negP NOTCOMP'.
+ rewrite neq_ltn in NOTCOMP.
+ move: NOTCOMP => /orP [LT | BUG]; last first.
{
- apply (leq_ltn_trans (COMP j (job_arrival j + R))) in NOTCOMP.
- by rewrite ltnn in NOTCOMP.
+ exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
+ by apply cumulative_service_le_job_cost.
}
- apply leq_trans with (n := R - service sched j (job_arrival j + R)); last first.
+ apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
+ backlogged job_cost sched j t) +
+ service sched j (job_arrival j + R)); last first.
{
- unfold service; rewrite service_before_arrival_eq_service_during; ins.
- rewrite EQinterf subKn; first by done.
- {
- unfold total_interference.
- rewrite -{1}[_ j]add0n big_addn addnC -addnBA // subnn addn0.
- rewrite -{2}[R]subn0 -[R-_]mul1n -[1*_]addn0 -iter_addn.
- by rewrite -big_const_nat leq_sum //; ins; apply leq_b1.
- }
- }
- {
- apply ltn_sub2l; last first.
- {
- apply leq_trans with (n := job_cost j); first by ins.
- rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS0.
- }
- apply leq_trans with (n := job_cost j); first by ins.
- apply leq_trans with (n := task_cost tsk);
- first by rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS0.
- by rewrite H_response_time_recurrence_holds; apply leq_addr.
+ rewrite -addn1 -addnA leq_add2l addn1.
+ apply leq_trans with (n := job_cost j); first by done.
+ by specialize (PARAMS j); des; rewrite -JOBtsk.
}
+ unfold service; rewrite service_before_arrival_eq_service_during //.
+ rewrite -big_split /=.
+ apply leq_trans with (n := \sum_(job_arrival j <= i < job_arrival j + R) 1);
+ first by rewrite big_const_nat iter_addn mul1n addn0 addKn.
+ rewrite big_nat_cond [\sum_(_ <= _ < _ | true) _]big_nat_cond.
+ apply leq_sum; move => i /andP [/andP [GEi LTi] _].
+ destruct (backlogged job_cost sched j i) eqn:BACK;
+ first by rewrite -addn1 addnC; apply leq_add.
+ apply negbT in BACK.
+ rewrite add0n lt0n -not_scheduled_no_service negbK.
+ rewrite /backlogged negb_and negbK in BACK.
+ move: BACK => /orP [/negP NOTPENDING | SCHED]; last by done.
+ exfalso; apply NOTPENDING; unfold pending; apply/andP; split; first by done.
+ apply/negP; red; intro BUG; apply NOTCOMP'.
+ by apply completion_monotonic with (t := i); try (by done); apply ltnW.
Qed.
Let scheduled_task_other_than_tsk (t: time) (tsk_other: sporadic_task) :=
@@ -316,55 +314,131 @@ Module ResponseTimeAnalysisFP.
Qed.
- (* 2) Next, we prove that the sum of the interference of each task is equal
+ (* 2) Prove that during the scheduling window of j, any job that is scheduled while j is
+ backlogged comes from a different task. *)
+ Lemma bertogna_fp_interference_by_different_tasks :
+ forall t j_other,
+ job_arrival j <= t < job_arrival j + R ->
+ backlogged job_cost sched j t ->
+ scheduled sched j_other t ->
+ job_task j_other != tsk.
+ Proof.
+ rename H_all_jobs_from_taskset into FROMTS,
+ H_valid_task_parameters into PARAMS,
+ H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
+ H_work_conserving into WORK,
+ H_constrained_deadlines into CONSTR,
+ H_previous_jobs_of_tsk_completed into PREV,
+ H_response_time_no_larger_than_deadline into NOMISS.
+ move => t j_other /andP [LEt GEt] BACK SCHED.
+ apply/eqP; red; intro SAMEtsk.
+ move: SCHED => /existsP [cpu SCHED].
+ assert (SCHED': scheduled sched j_other t).
+ by apply/existsP; exists cpu.
+ clear SCHED; rename SCHED' into SCHED.
+ move: (SCHED) => PENDING.
+ apply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING; try (by done).
+ destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
+ {
+ move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
+ specialize (PREV j_other SAMEtsk BEFOREother).
+ move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
+ apply completion_monotonic with (t0 := job_arrival j_other + R); try (by done).
+ apply leq_trans with (n := job_arrival j); last by done.
+ apply leq_trans with (n := job_arrival j_other + task_deadline tsk);
+ first by rewrite leq_add2l; apply NOMISS.
+ apply leq_trans with (n := job_arrival j_other + task_period tsk);
+ first by rewrite leq_add2l; apply CONSTR; rewrite -JOBtsk FROMTS.
+ rewrite -SAMEtsk; apply SPO; [ | by rewrite JOBtsk | by apply ltnW].
+ by intro EQ; subst j_other; rewrite ltnn in BEFOREother.
+ }
+ {
+ move: PENDING => /andP [ARRIVED _].
+ exploit (SPO j j_other); [ | by rewrite SAMEtsk | by done | ]; last first.
+ {
+ apply/negP; rewrite -ltnNge.
+ apply leq_ltn_trans with (n := t); first by done.
+ apply leq_trans with (n := job_arrival j + R); first by done.
+ by rewrite leq_add2l; apply leq_trans with (n := task_deadline tsk);
+ [by apply NOMISS | by rewrite JOBtsk CONSTR // -JOBtsk FROMTS].
+ }
+ by red; intros EQtsk; subst j_other; rewrite /backlogged SCHED andbF in BACK.
+ }
+ Qed.
+
+ (* 3) Next, we prove that the sum of the interference of each task is equal
to the total interference multiplied by the number of processors. This
holds because interference only occurs when all processors are busy. *)
Lemma bertogna_fp_all_cpus_busy :
\sum_(tsk_k <- ts_interf) x tsk_k = X * num_cpus.
Proof.
+ rename H_work_conserving into WORK, H_enforces_FP_policy into FP,
+ H_all_jobs_from_taskset into FROMTS, H_job_of_tsk into JOBtsk.
+ unfold sporadic_task_model in *.
unfold x, X, total_interference, task_interference.
- rewrite -big_mkcond -exchange_big big_distrl /=.
+ rewrite -big_mkcond -exchange_big big_distrl /= mul1n.
rewrite [\sum_(_ <= _ < _ | backlogged _ _ _ _) _]big_mkcond.
- apply eq_big_nat; move => t LTt.
+ apply eq_big_nat; move => t /andP [GEt LTt].
destruct (backlogged job_cost sched j t) eqn:BACK;
- last by rewrite (eq_bigr (fun i => 0));
- [by rewrite big_const_seq iter_addn mul0n addn0 | by done].
- rewrite big_mkcond mul1n /=.
- rewrite big_filter big_mkcond.
- rewrite (eq_bigr (fun i => if (scheduled_task_other_than_tsk t i) then 1 else 0));
- last first.
+ last by rewrite big1 //; ins; rewrite big1.
+ rewrite big_mkcond /=.
+ rewrite exchange_big /=.
+ apply eq_trans with (y := \sum_(cpu < num_cpus) 1); last by simpl_sum_const.
+ apply eq_bigr; intros cpu _.
+ move: (WORK j t BACK cpu) => [j_other /eqP SCHED]; unfold scheduled_on in *.
+ rewrite (bigD1_seq (job_task j_other)) /=; last by rewrite filter_uniq.
{
- intros i _; clear -i.
- unfold scheduled_task_other_than_tsk.
- by destruct (task_is_scheduled job_task sched i t); rewrite ?andFb ?andTb ?andbT //; desf.
+ rewrite (eq_bigr (fun i => 0));
+ last by intros i DIFF; rewrite /task_scheduled_on SCHED;apply/eqP;rewrite eqb0 eq_sym.
+ rewrite big_const_seq iter_addn mul0n 2!addn0; apply/eqP; rewrite eqb1.
+ by unfold task_scheduled_on; rewrite SCHED.
}
- rewrite -big_mkcond sum1_count.
- by apply bertogna_fp_scheduling_invariant.
+ rewrite mem_filter; apply/andP; split; last by apply FROMTS.
+ unfold can_interfere_with_tsk, fp_can_interfere_with; apply/andP; split.
+ {
+ rewrite -JOBtsk; apply FP with (t := t); try by done.
+ by apply/existsP; exists cpu; apply/eqP.
+ }
+ apply bertogna_fp_interference_by_different_tasks with (t := t); [by auto | by done |].
+ by apply/existsP; exists cpu; apply/eqP.
Qed.
(* Let (cardGE delta) be the number of interfering tasks whose interference
is larger than delta. *)
Let cardGE (delta: time) := count (fun i => x i >= delta) ts_interf.
- (* 3) If there is at least one of such tasks (e.g., cardGE > 0), then the
+ (* 4) If there is at least one of such tasks (e.g., cardGE > 0), then the
cumulative interference caused by the complementary set of interfering
tasks fills at least (num_cpus - cardGE) processors. *)
Lemma bertogna_fp_helper_lemma :
forall delta,
- cardGE delta > 0 ->
+ 0 < cardGE delta < num_cpus ->
\sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
- Proof.
- intros delta HAS.
+ Proof.
+ rename H_all_jobs_from_taskset into FROMTS,
+ H_valid_task_parameters into PARAMS,
+ H_job_of_tsk into JOBtsk,
+ H_sporadic_tasks into SPO,
+ H_previous_jobs_of_tsk_completed into BEFOREok,
+ H_response_time_no_larger_than_deadline into NOMISS,
+ H_constrained_deadlines into CONSTR,
+ H_sequential_jobs into SEQ,
+ H_enforces_FP_policy into FP,
+ H_hp_bounds_has_interfering_tasks into UNZIP,
+ H_interfering_tasks_miss_no_deadlines into NOMISSHP.
+ unfold sporadic_task_model in *.
+ move => delta /andP [HAS LT].
+ rewrite -has_count in HAS.
+
set some_interference_A := fun t =>
- backlogged job_cost sched j t &&
- has (fun tsk_k => ((x tsk_k >= delta) &&
- task_is_scheduled job_task sched tsk_k t)) ts_interf.
+ has (fun tsk_k => backlogged job_cost sched j t &&
+ (x tsk_k >= delta) &&
+ task_is_scheduled job_task sched tsk_k t) ts_interf.
set total_interference_B := fun t =>
backlogged job_cost sched j t *
count (fun tsk_k => (x tsk_k < delta) &&
- task_is_scheduled job_task sched tsk_k t) ts_interf.
+ task_is_scheduled job_task sched tsk_k t) ts_interf.
- rewrite -has_count in HAS.
apply leq_trans with ((\sum_(job_arrival j <= t < job_arrival j + R)
some_interference_A t) * (num_cpus - cardGE delta)).
{
@@ -372,39 +446,108 @@ Module ResponseTimeAnalysisFP.
move: HAS => /hasP HAS; destruct HAS as [tsk_a INa LEa].
apply leq_trans with (n := x tsk_a); first by apply LEa.
unfold x, task_interference, some_interference_A.
- apply leq_sum; ins.
- destruct (backlogged job_cost sched j i);
- [rewrite 2!andTb | by ins].
- destruct (task_is_scheduled job_task sched tsk_a i) eqn:SCHEDa;
- [apply eq_leq; symmetry | by ins].
- apply/eqP; rewrite eqb1.
- by apply/hasP; exists tsk_a; last by apply/andP.
+ apply leq_sum_nat; move => t /andP [GEt LTt] _.
+ destruct (backlogged job_cost sched j t) eqn:BACK;
+ last by rewrite (eq_bigr (fun x => 0)); [by simpl_sum_const | by ins].
+ destruct ([exists cpu, task_scheduled_on job_task sched tsk_a cpu t]) eqn:SCHED;
+ last first.
+ {
+ apply negbT in SCHED; rewrite negb_exists in SCHED; move: SCHED => /forallP ALL.
+ rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const.
+ by intros cpu _; specialize (ALL cpu); apply negbTE in ALL; rewrite ALL.
+ }
+ move: SCHED => /existsP [cpu SCHED].
+ apply leq_trans with (n := 1); last first.
+ {
+ rewrite lt0b; apply/hasP; exists tsk_a; first by done.
+ by rewrite LEa 2!andTb; apply/existsP; exists cpu.
+ }
+ rewrite (bigD1 cpu) /= // SCHED.
+ rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const; rewrite leq_b1.
+ intros cpu' DIFF.
+ apply/eqP; rewrite eqb0; apply/negP.
+ intros SCHED'.
+ move: DIFF => /negP DIFF; apply DIFF; apply/eqP.
+ unfold task_scheduled_on in *.
+ destruct (sched cpu t) as [j1|] eqn:SCHED1; last by done.
+ destruct (sched cpu' t) as [j2|] eqn:SCHED2; last by done.
+ move: SCHED SCHED' => /eqP JOB /eqP JOB'.
+ subst tsk_a; symmetry in JOB'.
+ assert (PENDING1: pending job_cost sched j1 t).
+ {
+ apply scheduled_implies_pending; try by done.
+ by apply/existsP; exists cpu; apply/eqP.
+ }
+ assert (PENDING2: pending job_cost sched j2 t).
+ {
+ apply scheduled_implies_pending; try by done.
+ by apply/existsP; exists cpu'; apply/eqP.
+ }
+ assert (BUG: j1 = j2).
+ {
+ destruct (job_task j1 == tsk) eqn:SAMEtsk.
+ {
+ move: SAMEtsk => /eqP SAMEtsk.
+ move: (PENDING1) => SAMEjob.
+ apply platform_fp_no_multiple_jobs_of_tsk with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline)
+ (job_task0 := job_task) (tsk0 := tsk) (j0 := j) in SAMEjob; try (by done);
+ [ | by apply PARAMS | |]; last 2 first.
+ {
+ apply (leq_trans LTt); rewrite leq_add2l.
+ by apply leq_trans with (n := task_deadline tsk); last by apply CONSTR.
+ }
+ {
+ intros j0 JOB0 LT0.
+ apply completion_monotonic with (t0 := job_arrival j0 + R); try (by done);
+ last by apply BEFOREok.
+ rewrite leq_add2l.
+ by apply leq_trans with (n := task_deadline tsk); last by apply CONSTR.
+ }
+ move: BACK => /andP [_ /negP NOTSCHED]; exfalso; apply NOTSCHED.
+ by rewrite -SAMEjob; apply/existsP; exists cpu; apply/eqP.
+ }
+ {
+ assert (INTERF: fp_can_interfere_with higher_eq_priority tsk (job_task j1)).
+ {
+ apply/andP; split; last by rewrite SAMEtsk.
+ rewrite -JOBtsk; apply FP with (t := t); first by done.
+ by apply/existsP; exists cpu; apply/eqP.
+ }
+ apply platform_fp_no_multiple_jobs_of_interfering_tasks with
+ (task_period0 := task_period) (tsk0 := tsk) (higher_eq_priority0 := higher_eq_priority)
+ (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) (t0 := t);
+ rewrite ?JOBtsk ?SAMEtsk //.
+ {
+ intros j0 tsk0 JOB0 INTERF0.
+ assert (IN: tsk0 \in (unzip1 hp_bounds)).
+ by rewrite -UNZIP mem_filter; apply/andP; split; last by rewrite -JOB0 FROMTS.
+ move: IN => /mapP [p IN EQ]; destruct p as [tsk0' R0]; simpl in *; subst tsk0'.
+ apply completion_monotonic with (t0 := job_arrival j0 + R0); try (by done);
+ last by eapply H_response_time_of_interfering_tasks_is_known; first by apply IN.
+ rewrite leq_add2l.
+ by apply leq_trans with (n := task_deadline tsk0);
+ [by apply NOMISSHP | by apply CONSTR; rewrite -JOB0 FROMTS].
+ }
+ }
+ }
+ by subst j2; apply SEQ with (j := j1) (t := t).
}
+
apply leq_trans with (\sum_(job_arrival j <= t < job_arrival j + R)
total_interference_B t).
{
rewrite big_distrl /=.
- rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
- apply leq_sum; move => t /andP [LEt _].
+ apply leq_sum_nat; move => t LEt _.
unfold some_interference_A, total_interference_B.
destruct (backlogged job_cost sched j t) eqn:BACK;
- [rewrite andTb mul1n | by done].
+ [rewrite mul1n /= | by rewrite has_pred0 //].
+
destruct (has (fun tsk_k : sporadic_task => (delta <= x tsk_k) &&
task_is_scheduled job_task sched tsk_k t) ts_interf) eqn:HAS';
last by done.
- rewrite mul1n; move: HAS => /hasP HAS.
- destruct HAS as [tsk_k INk LEk].
-
- have COUNT := bertogna_fp_scheduling_invariant t LEt BACK.
-
+ rewrite mul1n; move: HAS => /hasP [tsk_k INk LEk].
unfold cardGE.
- set interfering_tasks_at_t :=
- [seq tsk_k <- ts_interf | task_is_scheduled job_task
- sched tsk_k t].
-
- rewrite -(count_filter (fun i => true)) in COUNT.
- fold interfering_tasks_at_t in COUNT.
- rewrite count_predT in COUNT.
apply leq_trans with (n := num_cpus -
count (fun i => (x i >= delta) &&
task_is_scheduled job_task sched i t) ts_interf).
@@ -413,44 +556,28 @@ Module ResponseTimeAnalysisFP.
rewrite -2!sum1_count big_mkcond /=.
rewrite [\sum_(_ <- _ | _ <= _)_]big_mkcond /=.
apply leq_sum; intros i _.
- destruct (task_is_scheduled job_task sched i t);
+ by destruct (task_is_scheduled job_task sched i t);
[by rewrite andbT | by rewrite andbF].
}
-
- rewrite leq_subLR -count_predUI.
- apply leq_trans with (n :=
- count (predU (fun i : sporadic_task =>
- (delta <= x i) &&
- task_is_scheduled job_task sched i t)
- (fun tsk_k0 : sporadic_task =>
- (x tsk_k0 < delta) &&
- task_is_scheduled job_task sched tsk_k0 t))
- ts_interf); last by apply leq_addr.
- apply leq_trans with (n := size interfering_tasks_at_t).
- {
- rewrite -COUNT.
- rewrite leq_eqVlt; apply/orP; left; apply/eqP; f_equal.
- unfold interfering_tasks_at_t.
- rewrite -filter_predI; apply eq_filter; red; simpl.
- by intros i; rewrite andbC.
- }
- unfold interfering_tasks_at_t.
- rewrite -count_predT count_filter.
- rewrite leq_eqVlt; apply/orP; left; apply/eqP.
- apply eq_count; red; simpl.
- intros i.
- destruct (task_is_scheduled job_task sched i t);
- rewrite 3?andTb ?andFb ?andbF ?andbT /=; try ins.
- by rewrite leqNgt orNb.
+ rewrite -count_filter -[count _ ts_interf]count_filter.
+ eapply leq_trans with (n := count (predC (fun tsk => delta <= x tsk)) _);
+ last by apply eq_leq, eq_in_count; red; ins; rewrite ltnNge.
+ rewrite leq_subLR count_predC size_filter.
+ apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
+ first by rewrite bertogna_fp_scheduling_invariant.
+ by rewrite count_filter.
}
{
- unfold x at 2, task_interference.
- rewrite exchange_big /=; apply leq_sum; intros t _.
- unfold total_interference_B.
- destruct (backlogged job_cost sched j t); last by ins.
- rewrite mul1n -sum1_count.
- rewrite big_seq_cond big_mkcond [\sum_(i <- ts_interf | _ < _) _]big_mkcond.
- by apply leq_sum; ins; clear -i; desf; des; rewrite ?Heq2.
+ unfold x at 2, total_interference_B.
+ rewrite exchange_big /=; apply leq_sum; intros t _.
+ destruct (backlogged job_cost sched j t) eqn:BACK; last by ins.
+ rewrite mul1n -sum1_count.
+ rewrite big_mkcond [\sum_(i <- ts_interf | _ < _) _]big_mkcond /=.
+ apply leq_sum_seq; move => tsk_k IN _.
+ destruct (x tsk_k < delta); [rewrite andTb | by rewrite andFb].
+ destruct (task_is_scheduled job_task sched tsk_k t) eqn:SCHED; last by done.
+ move: SCHED => /existsP [cpu SCHED].
+ by rewrite (bigD1 cpu) /= // SCHED.
}
Qed.
@@ -500,7 +627,8 @@ Module ResponseTimeAnalysisFP.
apply leq_trans with (n := delta * cardGE delta +
delta * (num_cpus - cardGE delta));
first by rewrite -mulnDr subnKC //; apply ltnW.
- by rewrite leq_add2l; apply bertogna_fp_helper_lemma; rewrite -has_count.
+ rewrite leq_add2l; apply bertogna_fp_helper_lemma.
+ by apply/andP; split; first by rewrite -has_count.
Qed.
(* 5) Now, we prove that the Bertogna's interference bound
diff --git a/analysis/basic/interference_bound_edf.v b/analysis/basic/interference_bound_edf.v
index 6169970ed..23c108885 100644
--- a/analysis/basic/interference_bound_edf.v
+++ b/analysis/basic/interference_bound_edf.v
@@ -193,8 +193,8 @@ Module InterferenceBoundEDF.
(* Let's call x the task interference incurred by job j due to tsk_k. *)
Let x :=
- task_interference_sequential job_cost job_task sched j_i
- tsk_k (job_arrival j_i) (job_arrival j_i + delta).
+ task_interference job_cost job_task sched j_i tsk_k
+ (job_arrival j_i) (job_arrival j_i + delta).
(* Also, recall the EDF-specific interference bound for EDF. *)
Let interference_bound :=
@@ -210,7 +210,7 @@ Module InterferenceBoundEDF.
Let n_k := div_floor D_i p_k.
(* Let's give a simpler name to job interference. *)
- Let interference_caused_by := job_interference_sequential job_cost sched j_i.
+ Let interference_caused_by := job_interference job_cost sched j_i.
(* Identify the subset of jobs that actually cause interference *)
Let interfering_jobs :=
@@ -299,7 +299,7 @@ Module InterferenceBoundEDF.
intros j; rewrite mem_filter; move => /andP [/andP [/eqP JOBj _] _].
specialize (PARAMS j); des.
apply leq_trans with (n := service_during sched j t1 t2);
- first by apply job_interference_seq_le_service.
+ first by apply job_interference_le_service.
by apply cumulative_service_le_task_cost with (job_task0 := job_task)
(task_deadline0 := task_deadline) (job_cost0 := job_cost)
(job_deadline0 := job_deadline).
@@ -393,7 +393,7 @@ Module InterferenceBoundEDF.
destruct FST as [_ [ FSTserv _]].
move: FSTserv => /negP FSTserv; apply FSTserv.
rewrite -leqn0; apply leq_trans with (n := service_during sched j_fst t1 t2);
- first by apply job_interference_seq_le_service.
+ first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
try (by done); apply ltnW.
@@ -435,20 +435,20 @@ Module InterferenceBoundEDF.
completed job_cost sched j_fst (a_fst + R_k).
Lemma interference_bound_edf_holds_for_single_job_that_completes_on_time :
- job_interference_sequential job_cost sched j_i j_fst t1 t2 <= D_i - (D_k - R_k).
+ job_interference job_cost sched j_i j_fst t1 t2 <= D_i - (D_k - R_k).
Proof.
rename H_j_fst_completed_by_rt_bound into RBOUND.
have AFTERt1 :=
interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval RBOUND.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [_ [ LEdl _]].
- apply interference_seq_under_edf_implies_shorter_deadlines with
+ apply interference_under_edf_implies_shorter_deadlines with
(job_deadline0 := job_deadline) in LEdl; try (by done).
destruct (D_k - R_k <= D_i) eqn:LEdk; last first.
{
apply negbT in LEdk; rewrite -ltnNge in LEdk.
apply leq_trans with (n := 0); last by done.
- apply leq_trans with (n := job_interference_sequential job_cost sched j_i j_fst
+ apply leq_trans with (n := job_interference job_cost sched j_i j_fst
(a_fst + R_k) t2).
{
apply extend_sum; last by apply leqnn.
@@ -460,7 +460,7 @@ Module InterferenceBoundEDF.
by apply ltnW; rewrite -ltn_subRL.
}
apply leq_trans with (n := service_during sched j_fst (a_fst + R_k) t2);
- first by apply job_interference_seq_le_service.
+ first by apply job_interference_le_service.
unfold service_during; rewrite leqn0; apply/eqP.
by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
try (by done); apply leqnn.
@@ -473,7 +473,7 @@ Module InterferenceBoundEDF.
rewrite addnC -subnBA; last by apply leq_addr.
by rewrite addnC -addnBA // subnn addn0.
}
- apply leq_trans with (n := job_interference_sequential job_cost sched j_i j_fst t1
+ apply leq_trans with (n := job_interference job_cost sched j_i j_fst t1
(a_fst + D_k) + (D_k - R_k)).
{
rewrite leq_add2r.
@@ -484,15 +484,15 @@ Module InterferenceBoundEDF.
by rewrite leq_add2l; apply H_R_k_le_deadline.
}
{
- unfold job_interference_sequential.
+ unfold job_interference.
apply negbT in LEt2; rewrite -ltnNge in LEt2.
rewrite -> big_cat_nat with (n := a_fst + R_k);
[simpl | by apply AFTERt1 | by apply ltnW].
- apply leq_trans with (n := job_interference_sequential job_cost sched j_i j_fst t1
+ apply leq_trans with (n := job_interference job_cost sched j_i j_fst t1
(a_fst + R_k) + service_during sched j_fst (a_fst + R_k) t2).
{
rewrite leq_add2l.
- by apply job_interference_seq_le_service.
+ by apply job_interference_le_service.
}
unfold service_during.
rewrite -> cumulative_service_after_job_rt_zero with
@@ -502,14 +502,14 @@ Module InterferenceBoundEDF.
}
}
- unfold job_interference_sequential.
+ unfold job_interference.
rewrite -> big_cat_nat with (n := a_fst + R_k);
[simpl| by apply AFTERt1 | by rewrite leq_add2l; apply H_R_k_le_deadline].
- apply leq_trans with (n := job_interference_sequential job_cost sched j_i j_fst t1
+ apply leq_trans with (n := job_interference job_cost sched j_i j_fst t1
(a_fst+R_k) + service_during sched j_fst (a_fst+R_k) (a_fst+D_k) + (D_k-R_k)).
{
rewrite leq_add2r leq_add2l.
- by apply job_interference_seq_le_service.
+ by apply job_interference_le_service.
}
unfold service_during.
rewrite -> cumulative_service_after_job_rt_zero with
@@ -519,7 +519,9 @@ Module InterferenceBoundEDF.
\sum_(a_fst + R_k <= t < a_fst + D_k) 1).
{
apply leq_add; last by rewrite SUBST.
- by unfold job_interference_sequential; apply leq_sum; ins; apply leq_b1.
+ rewrite big_const_nat iter_addn mul1n addn0.
+ rewrite -{1}[a_fst + R_k](addKn t1) -addnBA //.
+ by apply job_interference_le_delta.
}
rewrite -big_cat_nat;
[simpl | by apply AFTERt1 | by rewrite leq_add2l; apply H_R_k_le_deadline ].
@@ -565,7 +567,7 @@ Module InterferenceBoundEDF.
by apply interference_bound_edf_response_time_bound_of_j_fst_after_interval.
}
apply/eqP; rewrite -[_ _ _ _ == 0]negbK; apply/negP; red; intro BUG.
- apply interference_seq_under_edf_implies_shorter_deadlines with
+ apply interference_under_edf_implies_shorter_deadlines with
(job_deadline0 := job_deadline) in BUG; try (by done).
rewrite interference_bound_edf_j_fst_deadline
interference_bound_edf_j_i_deadline in BUG.
@@ -583,14 +585,19 @@ Module InterferenceBoundEDF.
destruct FST as [FSTtask [LEdl _]].
have LTr := interference_bound_edf_response_time_bound_of_j_fst_after_interval.
apply subh3; last by apply LEdk.
- apply leq_trans with (n := job_interference_sequential job_cost sched j_i j_fst t1
+ apply leq_trans with (n := job_interference job_cost sched j_i j_fst t1
(job_arrival j_fst + R_k) + (D_k - R_k));
first by rewrite leq_add2r; apply extend_sum; [by apply leqnn|].
apply leq_trans with (n := \sum_(t1 <= t < a_fst + R_k) 1 +
\sum_(a_fst + R_k <= t < a_fst + D_k)1).
{
- apply leq_add; unfold job_interference;
- first by apply leq_sum; ins; apply leq_b1.
+ apply leq_add.
+ {
+ rewrite big_const_nat iter_addn mul1n addn0.
+ rewrite -{1}[job_arrival j_fst + R_k](addKn t1) -addnBA;
+ first by apply job_interference_le_delta.
+ by apply leq_trans with (n := t1 + delta); first by apply leq_addr.
+ }
rewrite big_const_nat iter_addn mul1n addn0 addnC.
rewrite -subnBA; last by apply leq_addr.
by rewrite addnC -addnBA // subnn addn0.
@@ -604,7 +611,7 @@ Module InterferenceBoundEDF.
rewrite big_const_nat iter_addn mul1n addn0 leq_subLR.
unfold D_i, D_k, t1, a_fst; rewrite -interference_bound_edf_j_fst_deadline
-interference_bound_edf_j_i_deadline.
- by apply interference_seq_under_edf_implies_shorter_deadlines with
+ by apply interference_under_edf_implies_shorter_deadlines with
(job_deadline0 := job_deadline) in LEdl.
Qed.
@@ -703,7 +710,7 @@ Module InterferenceBoundEDF.
instantiate (1 := elem); move => [LSTtsk [/eqP LSTserv LSTin]].
apply LSTserv; apply/eqP; rewrite -leqn0.
apply leq_trans with (n := service_during sched j_lst t1 t2);
- first by apply job_interference_seq_le_service.
+ first by apply job_interference_le_service.
rewrite leqn0; apply/eqP; unfold service_during.
by apply cumulative_service_before_job_arrival_zero.
Qed.
@@ -727,7 +734,7 @@ Module InterferenceBoundEDF.
rewrite ltnNge; apply/negP; red; intro BUG; apply SNDserv.
apply/eqP; rewrite -leqn0; apply leq_trans with (n := service_during
sched j_snd t1 t2);
- first by apply job_interference_seq_le_service.
+ first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
by apply cumulative_service_before_job_arrival_zero.
}
@@ -826,7 +833,7 @@ Module InterferenceBoundEDF.
}
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [_ [ LEdl _]].
- apply interference_seq_under_edf_implies_shorter_deadlines with
+ apply interference_under_edf_implies_shorter_deadlines with
(job_deadline0 := job_deadline) in LEdl; try (by done).
unfold D_i, D_k in DIST; rewrite interference_bound_edf_j_lst_deadline
interference_bound_edf_j_i_deadline in LEdl.
@@ -911,7 +918,7 @@ Module InterferenceBoundEDF.
destruct LST as [_ [ LSTserv _]].
unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
-interference_bound_edf_j_i_deadline.
- by apply interference_seq_under_edf_implies_shorter_deadlines with
+ by apply interference_under_edf_implies_shorter_deadlines with
(job_deadline0 := job_deadline) in LSTserv.
Qed.
@@ -938,19 +945,23 @@ Module InterferenceBoundEDF.
}
destruct (leqP t2 (a_fst + R_k)) as [LEt2 | GTt2].
{
- apply leq_trans with (n := job_interference_sequential job_cost sched j_i j_fst t1
+ apply leq_trans with (n := job_interference job_cost sched j_i j_fst t1
(a_fst + R_k));
first by apply extend_sum; rewrite ?leqnn.
- by apply leq_sum; ins; rewrite leq_b1.
+ simpl_sum_const; rewrite -{1}[_ + R_k](addKn t1) -addnBA //.
+ by apply job_interference_le_delta.
}
{
- unfold interference_caused_by, job_interference_sequential.
+ unfold interference_caused_by, job_interference.
rewrite -> big_cat_nat with (n := a_fst + R_k);
[simpl | by apply AFTERt1 | by apply ltnW].
- rewrite -[\sum_(_ <= _ < _) 1]addn0; apply leq_add;
- first by apply leq_sum; ins; apply leq_b1.
+ rewrite -[\sum_(_ <= _ < _) 1]addn0; apply leq_add.
+ {
+ simpl_sum_const; rewrite -{1}[_ + R_k](addKn t1) -addnBA //.
+ by apply job_interference_le_delta.
+ }
apply leq_trans with (n := service_during sched j_fst (a_fst + R_k) t2);
- first by apply job_interference_seq_le_service.
+ first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
[ by done | | by apply leqnn].
@@ -1029,7 +1040,7 @@ Module InterferenceBoundEDF.
destruct LST as [_ [ LSTserv _]].
unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
-interference_bound_edf_j_i_deadline.
- by apply interference_seq_under_edf_implies_shorter_deadlines
+ by apply interference_under_edf_implies_shorter_deadlines
with (job_deadline0 := job_deadline) in LSTserv.
Qed.
diff --git a/analysis/jitter/bertogna_edf_theory.v b/analysis/jitter/bertogna_edf_theory.v
index 25a6cba3d..ceaa3f3b4 100644
--- a/analysis/jitter/bertogna_edf_theory.v
+++ b/analysis/jitter/bertogna_edf_theory.v
@@ -10,7 +10,7 @@ Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisEDFJitter.
- Export JobWithJitter SporadicTaskset ScheduleWithJitter ScheduleOfSporadicTask Workload
+ Export JobWithJitter SporadicTaskset ScheduleOfSporadicTaskWithJitter Workload
Schedulability ResponseTime Priority SporadicTaskArrival WorkloadBoundJitter
InterferenceBoundEDFJitter Platform Interference.
@@ -228,50 +228,44 @@ Module ResponseTimeAnalysisEDFJitter.
Lemma bertogna_edf_too_much_interference : X >= R - task_cost tsk + 1.
Proof.
rename H_completed_jobs_dont_execute into COMP,
- H_valid_job_parameters into PARAMS,
- H_job_of_tsk into JOBtsk,
- H_j_not_completed into NOTCOMP.
+ H_valid_job_parameters into PARAMS, H_response_time_is_fixed_point into REC,
+ H_job_of_tsk into JOBtsk, H_j_not_completed into NOTCOMP.
unfold completed, valid_sporadic_job_with_jitter, valid_sporadic_job in *.
-
- (* Since j has not completed, recall the time when it is not
- executing is the total interference. *)
- exploit (complement_of_interf_equals_service job_cost job_jitter sched j t1 (t1 + R));
- try (by done); first by apply leqnn.
- intros EQinterf.
- rewrite {2}[_ + R]addnC -addnBA // subnn addn0 in EQinterf.
- rewrite addn1.
- move: NOTCOMP; rewrite neq_ltn; move => /orP NOTCOMP; des;
- last first.
- {
- apply (leq_ltn_trans (COMP j (t1 + R))) in NOTCOMP.
- by rewrite ltnn in NOTCOMP.
- }
- apply leq_trans with (n := R - service sched j (t1 + R)); last first.
+ unfold X, total_interference; rewrite addn1.
+ rewrite -(ltn_add2r (task_cost tsk)).
+ rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
+ rewrite -addnBA // subnn addn0.
+ move: (NOTCOMP) => /negP NOTCOMP'.
+ rewrite neq_ltn in NOTCOMP.
+ move: NOTCOMP => /orP [LT | BUG]; last first.
{
- unfold service.
- rewrite -> big_cat_nat with (n := t1); [simpl | by done | by apply leq_addr].
- rewrite -> cumulative_service_before_jitter_zero with (job_jitter0 := job_jitter);
- [rewrite add0n | by done | by apply leqnn].
- rewrite EQinterf subKn; first by done.
- {
- unfold total_interference.
- apply leq_trans with (n := \sum_(t1 <= t < t1 + R) 1);
- first by apply leq_sum; ins; apply leq_b1.
- rewrite big_const_nat iter_addn mul1n addn0.
- by rewrite addnC -addnBA // subnn addn0.
- }
+ exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
+ by apply cumulative_service_le_job_cost.
}
+ apply leq_ltn_trans with (n := (\sum_(t1 <= t < t1 + R)
+ backlogged job_cost job_jitter sched j t) +
+ service sched j (t1 + R)); last first.
{
- apply ltn_sub2l; last first.
- {
- apply leq_trans with (n := job_cost j); first by ins.
- rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS1.
- }
- apply leq_trans with (n := job_cost j); first by ins.
- apply leq_trans with (n := task_cost tsk);
- first by rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS1.
- by rewrite bertogna_edf_R_other_ge_cost.
+ rewrite -addn1 -addnA leq_add2l addn1.
+ apply leq_trans with (n := job_cost j); first by done.
+ by specialize (PARAMS j); des; rewrite -JOBtsk.
}
+ unfold service.
+ rewrite -> big_cat_nat with (n := t1) (m := 0); rewrite ?leq_addr // /=.
+ rewrite (cumulative_service_before_jitter_zero job_jitter) // add0n.
+ rewrite -big_split /=.
+ apply leq_trans with (n := \sum_(t1 <= i < t1 + R) 1);
+ first by simpl_sum_const; rewrite addKn.
+ apply leq_sum_nat; move => i /andP [GEi LTi] _.
+ destruct (backlogged job_cost job_jitter sched j i) eqn:BACK;
+ first by rewrite -addn1 addnC; apply leq_add.
+ apply negbT in BACK.
+ rewrite add0n lt0n -not_scheduled_no_service negbK.
+ rewrite /backlogged negb_and negbK in BACK.
+ move: BACK => /orP [/negP NOTPENDING | SCHED]; last by done.
+ exfalso; apply NOTPENDING; unfold pending; apply/andP; split; first by done.
+ apply/negP; red; intro BUG; apply NOTCOMP'.
+ by apply completion_monotonic with (t := i); try (by done); apply ltnW.
Qed.
Let scheduled_task_other_than_tsk (t: time) (tsk_other: sporadic_task) :=
@@ -296,13 +290,12 @@ Module ResponseTimeAnalysisEDFJitter.
H_rt_bounds_contains_all_tasks into UNZIP,
H_constrained_deadlines into RESTR,
H_work_conserving into WORK.
- unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
+ unfold x, X, total_interference, task_interference,
+ valid_sporadic_job_with_jitter, valid_sporadic_job in *.
move => t /andP [LEt LTt] BACK.
unfold scheduled_task_other_than_tsk in *.
eapply platform_cpus_busy_with_interfering_tasks; try (by done);
- [ by apply WORK
- | by done
- | by apply SPO
+ [ by apply WORK | by done | by apply SPO
| apply PARAMS; rewrite -JOBtsk; apply FROMTS
| by apply JOBtsk | by apply BACK | ].
{
@@ -332,7 +325,80 @@ Module ResponseTimeAnalysisEDFJitter.
}
Qed.
- (* 2) Next, we prove that the sum of the interference of each task is equal
+ (* 2) Prove that during the scheduling window of j, any job that is scheduled while j is
+ backlogged comes from a different task. *)
+ Lemma bertogna_edf_interference_by_different_tasks :
+ forall t j_other,
+ t1 <= t < t1 + R ->
+ backlogged job_cost job_jitter sched j t ->
+ scheduled sched j_other t ->
+ job_task j_other != tsk.
+ Proof.
+ rename H_all_jobs_from_taskset into FROMTS,
+ H_valid_task_parameters into PARAMS,
+ H_valid_job_parameters into JOBPARAMS,
+ H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
+ H_work_conserving into WORK,
+ H_tsk_R_in_rt_bounds into INbounds,
+ H_all_previous_jobs_completed_on_time into BEFOREok,
+ H_tasks_miss_no_deadlines into NOMISS,
+ H_constrained_deadlines into CONSTR.
+ unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
+ move => t j_other /andP [LEt GEt] BACK SCHED.
+ apply/eqP; red; intro SAMEtsk.
+ move: SCHED => /existsP [cpu SCHED].
+ assert (SCHED': scheduled sched j_other t).
+ by apply/existsP; exists cpu.
+ clear SCHED; rename SCHED' into SCHED.
+ move: (SCHED) => PENDING.
+ apply scheduled_implies_pending with (job_cost0 := job_cost) (job_jitter0 := job_jitter)
+ in PENDING; try (by done).
+ destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
+ {
+ move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
+ exploit (BEFOREok j_other tsk R SAMEtsk INbounds).
+ {
+ rewrite -addnA [_ + R]addnC addnA -[(_ + _) + R]addnA [_ tsk + R]addnC addnA.
+ by rewrite ltn_add2r.
+ }
+ intros COMP.
+ move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
+ apply completion_monotonic with (t0 := job_arrival j_other + task_jitter tsk + R);
+ try by done.
+ apply leq_trans with (n := job_arrival j);
+ last by apply leq_trans with (n := t1); [by apply leq_addr | by done].
+ apply leq_trans with (n := job_arrival j_other + task_period tsk).
+ {
+ rewrite -addnA leq_add2l.
+ by apply leq_trans with (n := task_deadline tsk);
+ [by apply NOMISS | by apply CONSTR; rewrite -JOBtsk FROMTS].
+ }
+ rewrite -SAMEtsk; apply SPO; [ | by rewrite JOBtsk | by apply ltnW].
+ by red; intro EQ; subst; rewrite ltnn in BEFOREother.
+ }
+ {
+ move: PENDING => /andP [ARRIVED _].
+ exploit (SPO j j_other); [ | by rewrite SAMEtsk | by done | ]; last first.
+ {
+ apply/negP; rewrite -ltnNge JOBtsk.
+ apply leq_trans with (n := job_arrival j + task_deadline tsk);
+ last by rewrite leq_add2l; apply CONSTR; rewrite -JOBtsk FROMTS.
+ apply leq_trans with (n := job_arrival j + task_jitter tsk + R);
+ last by rewrite -addnA leq_add2l; apply NOMISS.
+ apply leq_trans with (n := t1 + R); last first.
+ {
+ rewrite leq_add2r leq_add2l -JOBtsk.
+ by specialize (JOBPARAMS j); des.
+ }
+ apply leq_ltn_trans with (n := job_arrival j_other + job_jitter j_other);
+ first by apply leq_addr.
+ by apply leq_ltn_trans with (n := t).
+ }
+ by intros EQtsk; subst j_other; rewrite /backlogged SCHED andbF in BACK.
+ }
+ Qed.
+
+ (* 3) Next, we prove that the sum of the interference of each task is equal
to the total interference multiplied by the number of processors. This
holds because interference only occurs when all processors are busy. *)
Lemma bertogna_edf_all_cpus_busy :
@@ -340,43 +406,87 @@ Module ResponseTimeAnalysisEDFJitter.
Proof.
rename H_all_jobs_from_taskset into FROMTS,
H_valid_task_parameters into PARAMS,
- H_valid_job_parameters into JOBPARAMS,
- H_job_of_tsk into JOBtsk,
- H_sporadic_tasks into SPO,
+ H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
+ H_work_conserving into WORK,
H_tsk_R_in_rt_bounds into INbounds,
H_all_previous_jobs_completed_on_time into BEFOREok,
H_tasks_miss_no_deadlines into NOMISS,
- H_constrained_deadlines into RESTR.
- unfold sporadic_task_model, valid_sporadic_job_with_jitter, valid_sporadic_job in *.
+ H_rt_bounds_contains_all_tasks into UNZIP,
+ H_constrained_deadlines into CONSTR.
+ unfold sporadic_task_model in *.
unfold x, X, total_interference, task_interference.
- rewrite -big_mkcond -exchange_big big_distrl /=.
+ rewrite -big_mkcond -exchange_big big_distrl /= mul1n.
rewrite [\sum_(_ <= _ < _ | backlogged _ _ _ _ _) _]big_mkcond.
- apply eq_big_nat; move => t LEt.
+ apply eq_big_nat; move => t /andP [GEt LTt].
destruct (backlogged job_cost job_jitter sched j t) eqn:BACK;
- last by rewrite (eq_bigr (fun i => 0));
- [by rewrite big_const_seq iter_addn mul0n addn0 | by done].
- rewrite big_mkcond mul1n /=.
- rewrite big_filter big_mkcond.
- rewrite (eq_bigr (fun i => if (scheduled_task_other_than_tsk t i) then 1 else 0)); last first.
+ last by rewrite big1 //; ins; rewrite big1.
+ rewrite big_mkcond /=.
+ rewrite exchange_big /=.
+ apply eq_trans with (y := \sum_(cpu < num_cpus) 1); last by simpl_sum_const.
+ apply eq_bigr; intros cpu _.
+ move: (WORK j t BACK cpu) => [j_other /eqP SCHED]; unfold scheduled_on in *.
+ rewrite (bigD1_seq (job_task j_other)) /=; last by rewrite filter_uniq.
{
- unfold scheduled_task_other_than_tsk; intros i _; clear -i.
- by destruct (task_is_scheduled job_task sched i t);
- rewrite ?andFb ?andTb ?andbT //; desf.
+ rewrite (eq_bigr (fun i => 0));
+ last by intros i DIFF; rewrite /task_scheduled_on SCHED;apply/eqP;rewrite eqb0 eq_sym.
+ simpl_sum_const; apply/eqP; rewrite eqb1.
+ by unfold task_scheduled_on; rewrite SCHED.
}
- rewrite -big_mkcond sum1_count.
- by apply bertogna_edf_scheduling_invariant.
+ rewrite mem_filter; apply/andP; split; last by apply FROMTS.
+ unfold jldp_can_interfere_with.
+ apply bertogna_edf_interference_by_different_tasks with (t := t); [by auto | by done |].
+ by apply/existsP; exists cpu; apply/eqP.
Qed.
+ (* 4) Show that by the induction hypothesis, all jobs released
+ before the end of the interval complete by their periods. *)
+ Lemma bertogna_edf_all_previous_jobs_complete_by_their_period:
+ forall t (j0: JobIn arr_seq),
+ t < t1 + R ->
+ job_arrival j0 + task_period (job_task j0) <= t ->
+ completed job_cost sched j0
+ (job_arrival j0 + task_period (job_task j0)).
+ Proof.
+ rename H_valid_job_parameters into JOBPARAMS,
+ H_rt_bounds_contains_all_tasks into UNZIP,
+ H_job_of_tsk into JOBtsk,
+ H_constrained_deadlines into CONSTR,
+ H_tasks_miss_no_deadlines into NOMISS,
+ H_all_jobs_from_taskset into FROMTS,
+ H_all_previous_jobs_completed_on_time into BEFOREok.
+ unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
+ intros t j0 LEt LE.
+ cut ((job_task j0) \in unzip1 rt_bounds); [intro IN | by rewrite UNZIP FROMTS].
+ move: IN => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
+ apply completion_monotonic with (t0 := job_arrival j0 +
+ task_jitter (job_task j0) + R0); first by done.
+ {
+ rewrite -addnA leq_add2l.
+ apply leq_trans with (n := task_deadline (job_task j0));
+ [by apply NOMISS | by apply CONSTR; rewrite FROMTS].
+ }
+ apply BEFOREok with (tsk_other := (job_task j0)); try by done.
+ apply leq_ltn_trans with (n := t); last first.
+ {
+ apply leq_trans with (n := t1 + R); first by done.
+ rewrite leq_add2r leq_add2l -JOBtsk.
+ by specialize (JOBPARAMS j); des.
+ }
+ apply leq_trans with (n := job_arrival j0 + task_period (job_task j0)); last by done.
+ by rewrite -addnA leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
+ [by apply NOMISS | apply CONSTR; rewrite FROMTS].
+ Qed.
+
(* Let (cardGE delta) be the number of interfering tasks whose interference
is larger than delta. *)
Let cardGE (delta: time) := count (fun i => x i >= delta) ts_interf.
- (* 3) If there is at least one of such tasks (e.g., cardGE > 0), then the
+ (* 5) If there is at least one of such tasks (e.g., cardGE > 0), then the
cumulative interference caused by the complementary set of interfering
tasks fills at least (num_cpus - cardGE) processors. *)
Lemma bertogna_edf_helper_lemma :
forall delta,
- cardGE delta > 0 ->
+ 0 < cardGE delta < num_cpus ->
\sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
Proof.
rename H_all_jobs_from_taskset into FROMTS,
@@ -386,19 +496,21 @@ Module ResponseTimeAnalysisEDFJitter.
H_tsk_R_in_rt_bounds into INbounds,
H_all_previous_jobs_completed_on_time into BEFOREok,
H_tasks_miss_no_deadlines into NOMISS,
- H_constrained_deadlines into RESTR.
+ H_constrained_deadlines into CONSTR,
+ H_sequential_jobs into SEQ.
unfold sporadic_task_model in *.
- intros delta HAS.
+ move => delta /andP [HAS LT].
+ rewrite -has_count in HAS.
+
set some_interference_A := fun t =>
- backlogged job_cost job_jitter sched j t &&
- has (fun tsk_k => ((x tsk_k >= delta) &&
- task_is_scheduled job_task sched tsk_k t)) ts_interf.
+ has (fun tsk_k => backlogged job_cost job_jitter sched j t &&
+ (x tsk_k >= delta) &&
+ task_is_scheduled job_task sched tsk_k t) ts_interf.
set total_interference_B := fun t =>
backlogged job_cost job_jitter sched j t *
count (fun tsk_k => (x tsk_k < delta) &&
- task_is_scheduled job_task sched tsk_k t) ts_interf.
+ task_is_scheduled job_task sched tsk_k t) ts_interf.
- rewrite -has_count in HAS.
apply leq_trans with ((\sum_(t1 <= t < t1 + R)
some_interference_A t) * (num_cpus - cardGE delta)).
{
@@ -406,39 +518,69 @@ Module ResponseTimeAnalysisEDFJitter.
move: HAS => /hasP HAS; destruct HAS as [tsk_a INa LEa].
apply leq_trans with (n := x tsk_a); first by apply LEa.
unfold x, task_interference, some_interference_A.
- apply leq_sum; ins.
- destruct (backlogged job_cost job_jitter sched j i);
- [rewrite 2!andTb | by ins].
- destruct (task_is_scheduled job_task sched tsk_a i) eqn:SCHEDa;
- [apply eq_leq; symmetry | by ins].
- apply/eqP; rewrite eqb1.
- by apply/hasP; exists tsk_a; last by apply/andP.
+ apply leq_sum_nat; move => t /andP [GEt LTt] _.
+ destruct (backlogged job_cost job_jitter sched j t) eqn:BACK;
+ last by rewrite (eq_bigr (fun x => 0)); [by simpl_sum_const | by ins].
+ destruct ([exists cpu, task_scheduled_on job_task sched tsk_a cpu t]) eqn:SCHED;
+ last first.
+ {
+ apply negbT in SCHED; rewrite negb_exists in SCHED; move: SCHED => /forallP ALL.
+ rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const.
+ by intros cpu _; specialize (ALL cpu); apply negbTE in ALL; rewrite ALL.
+ }
+ move: SCHED => /existsP [cpu SCHED].
+ apply leq_trans with (n := 1); last first.
+ {
+ rewrite lt0b; apply/hasP; exists tsk_a; first by done.
+ by rewrite LEa 2!andTb; apply/existsP; exists cpu.
+ }
+ rewrite (bigD1 cpu) /= // SCHED.
+ rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const; rewrite leq_b1.
+ intros cpu' DIFF.
+ apply/eqP; rewrite eqb0; apply/negP.
+ intros SCHED'.
+ move: DIFF => /negP DIFF; apply DIFF; apply/eqP.
+ unfold task_scheduled_on in *.
+ destruct (sched cpu t) as [j1|] eqn:SCHED1; last by done.
+ destruct (sched cpu' t) as [j2|] eqn:SCHED2; last by done.
+ move: SCHED SCHED' => /eqP JOB /eqP JOB'.
+ subst tsk_a; symmetry in JOB'.
+ assert (PENDING1: pending job_cost job_jitter sched j1 t).
+ {
+ apply scheduled_implies_pending; try by done.
+ by apply/existsP; exists cpu; apply/eqP.
+ }
+ assert (PENDING2: pending job_cost job_jitter sched j2 t).
+ {
+ apply scheduled_implies_pending; try by done.
+ by apply/existsP; exists cpu'; apply/eqP.
+ }
+ assert (BUG: j1 = j2).
+ {
+ apply platform_at_most_one_pending_job_of_each_task with (task_cost0 := task_cost)
+ (job_jitter0 := job_jitter) (task_period0 := task_period) (job_cost0 := job_cost)
+ (task_deadline0 := task_deadline) (tsk0 := tsk) (job_task0 := job_task) (sched0 := sched)
+ (j0 := j) (t0 := t);
+ rewrite ?JOBtsk ?SAMEtsk //; first by apply PARAMS; rewrite -JOBtsk FROMTS.
+ intros j0 tsk0 TSK0 LE.
+ by apply (bertogna_edf_all_previous_jobs_complete_by_their_period t); rewrite ?TSK0.
+ }
+ by subst j2; apply SEQ with (j := j1) (t := t).
}
- apply leq_trans with (\sum_(t1 <= t < t1 + R)
- total_interference_B t).
+
+ apply leq_trans with (\sum_(t1 <= t < t1 + R) total_interference_B t).
{
rewrite big_distrl /=.
- rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
- apply leq_sum; move => t /andP [LEt _].
+ apply leq_sum_nat; move => t LEt _.
unfold some_interference_A, total_interference_B.
destruct (backlogged job_cost job_jitter sched j t) eqn:BACK;
- [rewrite andTb mul1n | by done].
+ [rewrite mul1n /= | by rewrite has_pred0 //].
+
destruct (has (fun tsk_k : sporadic_task => (delta <= x tsk_k) &&
task_is_scheduled job_task sched tsk_k t) ts_interf) eqn:HAS';
last by done.
- rewrite mul1n; move: HAS => /hasP HAS.
- destruct HAS as [tsk_k INk LEk].
-
- have COUNT := bertogna_edf_scheduling_invariant t LEt BACK.
-
+ rewrite mul1n; move: HAS => /hasP [tsk_k INk LEk].
unfold cardGE.
- set interfering_tasks_at_t :=
- [seq tsk_k <- ts_interf | task_is_scheduled job_task
- sched tsk_k t].
-
- rewrite -(count_filter (fun i => true)) in COUNT.
- fold interfering_tasks_at_t in COUNT.
- rewrite count_predT in COUNT.
apply leq_trans with (n := num_cpus -
count (fun i => (x i >= delta) &&
task_is_scheduled job_task sched i t) ts_interf).
@@ -447,48 +589,32 @@ Module ResponseTimeAnalysisEDFJitter.
rewrite -2!sum1_count big_mkcond /=.
rewrite [\sum_(_ <- _ | _ <= _)_]big_mkcond /=.
apply leq_sum; intros i _.
- destruct (task_is_scheduled job_task sched i t);
+ by destruct (task_is_scheduled job_task sched i t);
[by rewrite andbT | by rewrite andbF].
}
-
- rewrite leq_subLR -count_predUI.
- apply leq_trans with (n :=
- count (predU (fun i : sporadic_task =>
- (delta <= x i) &&
- task_is_scheduled job_task sched i t)
- (fun tsk_k0 : sporadic_task =>
- (x tsk_k0 < delta) &&
- task_is_scheduled job_task sched tsk_k0 t))
- ts_interf); last by apply leq_addr.
- apply leq_trans with (n := size interfering_tasks_at_t).
- {
- rewrite -COUNT.
- rewrite leq_eqVlt; apply/orP; left; apply/eqP; f_equal.
- unfold interfering_tasks_at_t.
- rewrite -filter_predI; apply eq_filter; red; simpl.
- by intros i; rewrite andbC.
- }
- unfold interfering_tasks_at_t.
- rewrite -count_predT count_filter.
- rewrite leq_eqVlt; apply/orP; left; apply/eqP.
- apply eq_count; red; simpl.
- intros i.
- destruct (task_is_scheduled job_task sched i t);
- rewrite 3?andTb ?andFb ?andbF ?andbT /=; try ins.
- by rewrite leqNgt orNb.
+ rewrite -count_filter -[count _ ts_interf]count_filter.
+ eapply leq_trans with (n := count (predC (fun tsk => delta <= x tsk)) _);
+ last by apply eq_leq, eq_in_count; red; ins; rewrite ltnNge.
+ rewrite leq_subLR count_predC size_filter.
+ apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
+ first by rewrite bertogna_edf_scheduling_invariant.
+ by rewrite count_filter.
}
{
- unfold x at 2, task_interference.
- rewrite exchange_big /=; apply leq_sum; intros t _.
- unfold total_interference_B.
- destruct (backlogged job_cost job_jitter sched j t); last by ins.
- rewrite mul1n -sum1_count.
- rewrite big_seq_cond big_mkcond [\sum_(i <- ts_interf | _ < _) _]big_mkcond.
- by apply leq_sum; ins; clear -i; desf; des; rewrite ?Heq2.
+ unfold x at 2, total_interference_B.
+ rewrite exchange_big /=; apply leq_sum; intros t _.
+ destruct (backlogged job_cost job_jitter sched j t) eqn:BACK; last by ins.
+ rewrite mul1n -sum1_count.
+ rewrite big_mkcond [\sum_(i <- ts_interf | _ < _) _]big_mkcond /=.
+ apply leq_sum_seq; move => tsk_k IN _.
+ destruct (x tsk_k < delta); [rewrite andTb | by rewrite andFb].
+ destruct (task_is_scheduled job_task sched tsk_k t) eqn:SCHED; last by done.
+ move: SCHED => /existsP [cpu SCHED].
+ by rewrite (bigD1 cpu) /= // SCHED.
}
Qed.
- (* 4) Next, we prove that, for any interval delta, if the sum of per-task
+ (* 6) Next, we prove that, for any interval delta, if the sum of per-task
interference exceeds delta * num_cpus, the same applies for the
sum of the minimum between the interference and delta. *)
Lemma bertogna_edf_minimum_exceeds_interference :
@@ -534,10 +660,11 @@ Module ResponseTimeAnalysisEDFJitter.
apply leq_trans with (n := delta * cardGE delta +
delta * (num_cpus - cardGE delta));
first by rewrite -mulnDr subnKC //; apply ltnW.
- by rewrite leq_add2l; apply bertogna_edf_helper_lemma; rewrite -has_count.
+ rewrite leq_add2l; apply bertogna_edf_helper_lemma.
+ by apply/andP; split; first by rewrite -has_count.
Qed.
- (* 5) Now, we prove that the Bertogna's interference bound
+ (* 7) Now, we prove that the Bertogna's interference bound
is not enough to cover the sum of the "minimum" term over
all tasks (artifact of the proof by contradiction). *)
Lemma bertogna_edf_sum_exceeds_total_interference:
@@ -581,7 +708,7 @@ Module ResponseTimeAnalysisEDFJitter.
by apply bertogna_edf_too_much_interference.
Qed.
- (* 6) After concluding that the sum of the minimum exceeds (R - e_i + 1),
+ (* 8) After concluding that the sum of the minimum exceeds (R - e_i + 1),
we prove that there exists a tuple (tsk_k, R_k) such that
min (x_k, R - e_i + 1) > min (W_k, edf_bound, R - e_i + 1). *)
Lemma bertogna_edf_exists_task_that_exceeds_bound :
diff --git a/analysis/jitter/bertogna_fp_theory.v b/analysis/jitter/bertogna_fp_theory.v
index 4105f5d6c..ac6124dc5 100644
--- a/analysis/jitter/bertogna_fp_theory.v
+++ b/analysis/jitter/bertogna_fp_theory.v
@@ -9,9 +9,9 @@ Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisFP.
- Export JobWithJitter SporadicTaskset ScheduleWithJitter Workload Interference Platform PlatformFP
- Schedulability ResponseTime Priority SporadicTaskArrival WorkloadBoundJitter
- Interference InterferenceBoundFP.
+ Export JobWithJitter SporadicTaskset ScheduleOfSporadicTaskWithJitter Workload Interference
+ Platform PlatformFP Schedulability ResponseTime Priority SporadicTaskArrival
+ WorkloadBoundJitter Interference InterferenceBoundFP.
Section ResponseTimeBound.
@@ -218,369 +218,524 @@ Module ResponseTimeAnalysisFP.
(* Next we prove some lemmas that help to derive a contradiction.*)
Section DerivingContradiction.
- (* 0) Since job j did not complete by its response time bound, it follows that
- the total interference X >= R - e_k + 1. *)
- Lemma bertogna_fp_too_much_interference : X >= R - task_cost tsk + 1.
- Proof.
- rename H_completed_jobs_dont_execute into COMP,
- H_valid_job_parameters into PARAMS,
- H_job_of_tsk into JOBtsk,
- H_j_not_completed into NOTCOMP.
- unfold completed, valid_sporadic_job_with_jitter, valid_sporadic_job in *.
-
- (* Since j has not completed, recall the time when it is not
- executing is the total interference. *)
- exploit (complement_of_interf_equals_service job_cost job_jitter sched j t1 (t1 + R));
- try (by done); first by apply leqnn.
- intro EQinterf; rewrite {2}[_ + R]addnC -addnBA // subnn addn0 in EQinterf.
- rewrite addn1.
- move: NOTCOMP; rewrite neq_ltn; move => /orP NOTCOMP; des;
- last first.
- {
- apply (leq_ltn_trans (COMP j (t1 + R))) in NOTCOMP.
- by rewrite ltnn in NOTCOMP.
- }
- apply leq_trans with (n := R - service sched j (t1 + R)); last first.
- {
+ (* 0) Since job j did not complete by its response time bound, it follows that
+ the total interference X >= R - e_k + 1. *)
+ Lemma bertogna_fp_too_much_interference : X >= R - task_cost tsk + 1.
+ Proof.
+ rename H_completed_jobs_dont_execute into COMP,
+ H_valid_job_parameters into PARAMS,
+ H_response_time_recurrence_holds into REC,
+ H_job_of_tsk into JOBtsk, H_j_not_completed into NOTCOMP.
+ unfold completed, valid_sporadic_job_with_jitter, valid_sporadic_job in *.
+ unfold X, total_interference; rewrite addn1.
+ rewrite -(ltn_add2r (task_cost tsk)).
+ rewrite subh1; last by rewrite [R](REC) // leq_addr.
+ rewrite -addnBA // subnn addn0.
+ move: (NOTCOMP) => /negP NOTCOMP'.
+ rewrite neq_ltn in NOTCOMP.
+ move: NOTCOMP => /orP [LT | BUG]; last first.
+ {
+ exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
+ by apply cumulative_service_le_job_cost.
+ }
+ apply leq_ltn_trans with (n := (\sum_(t1 <= t < t1 + R)
+ backlogged job_cost job_jitter sched j t) +
+ service sched j (t1 + R)); last first.
+ {
+ rewrite -addn1 -addnA leq_add2l addn1.
+ apply leq_trans with (n := job_cost j); first by done.
+ by specialize (PARAMS j); des; rewrite -JOBtsk.
+ }
unfold service.
- rewrite -> big_cat_nat with (n := t1); [simpl | by done | by apply leq_addr].
- rewrite -> cumulative_service_before_jitter_zero with (job_jitter0 := job_jitter);
- [rewrite add0n | by done | by apply leqnn].
- rewrite EQinterf subKn; first by done.
+ rewrite -> big_cat_nat with (n := t1) (m := 0); rewrite ?leq_addr // /=.
+ rewrite (cumulative_service_before_jitter_zero job_jitter) // add0n.
+ rewrite -big_split /=.
+ apply leq_trans with (n := \sum_(t1 <= i < t1 + R) 1);
+ first by simpl_sum_const; rewrite addKn.
+ apply leq_sum_nat; move => i /andP [GEi LTi] _.
+ destruct (backlogged job_cost job_jitter sched j i) eqn:BACK;
+ first by rewrite -addn1 addnC; apply leq_add.
+ apply negbT in BACK.
+ rewrite add0n lt0n -not_scheduled_no_service negbK.
+ rewrite /backlogged negb_and negbK in BACK.
+ move: BACK => /orP [/negP NOTPENDING | SCHED]; last by done.
+ exfalso; apply NOTPENDING; unfold pending; apply/andP; split; first by done.
+ apply/negP; red; intro BUG; apply NOTCOMP'.
+ by apply completion_monotonic with (t := i); try (by done); apply ltnW.
+ Qed.
+
+ Let scheduled_task_other_than_tsk (t: time) (tsk_other: sporadic_task) :=
+ task_is_scheduled job_task sched tsk_other t &&
+ can_interfere_with_tsk tsk_other.
+
+ (* 1) At all times that j is backlogged, all processors are busy with other tasks. *)
+ Lemma bertogna_fp_scheduling_invariant:
+ forall t,
+ t1 <= t < t1 + R ->
+ backlogged job_cost job_jitter sched j t ->
+ count (scheduled_task_other_than_tsk t) ts = num_cpus.
+ Proof.
+ rename H_valid_task_parameters into PARAMS,
+ H_job_of_tsk into JOBtsk,
+ H_all_jobs_from_taskset into FROMTS,
+ H_sporadic_tasks into SPO,
+ H_valid_job_parameters into JOBPARAMS,
+ H_constrained_deadlines into RESTR,
+ H_hp_bounds_has_interfering_tasks into UNZIP,
+ H_interfering_tasks_miss_no_deadlines into NOMISS,
+ H_response_time_of_interfering_tasks_is_known into PREV,
+ H_previous_jobs_of_tsk_completed into PREVtsk.
+ unfold sporadic_task_model, is_response_time_bound_of_task,
+ valid_sporadic_job_with_jitter in *.
+ move => t /andP [LEt LTt] BACK.
+
+ apply platform_fp_cpus_busy_with_interfering_tasks with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (job_task0 := job_task)
+ (ts0 := ts) (tsk0 := tsk) (higher_eq_priority0 := higher_eq_priority) in BACK;
+ try (by done); first by apply PARAMS; rewrite -JOBtsk FROMTS.
{
- unfold total_interference.
- apply leq_trans with (n := \sum_(t1 <= t < t1 + R) 1);
- first by apply leq_sum; ins; apply leq_b1.
- rewrite big_const_nat iter_addn mul1n addn0.
- by rewrite addnC -addnBA // subnn addn0.
+ apply leq_trans with (n := job_arrival j + job_jitter j + R); first by done.
+ rewrite -addnA leq_add2l.
+ apply leq_trans with (n := task_deadline tsk); last by apply RESTR.
+ apply leq_trans with (n := task_jitter tsk + R); last by done.
+ by rewrite leq_add2r -JOBtsk; specialize (JOBPARAMS j); des.
}
- }
- {
- apply ltn_sub2l; last first.
{
- apply leq_trans with (n := job_cost j); first by ins.
- rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS1.
+ intros j_other tsk_other JOBother INTERF.
+ move: UNZIP => UNZIP.
+ cut (tsk_other \in unzip1 hp_bounds); last first.
+ {
+ rewrite -UNZIP mem_filter; apply/andP; split; first by done.
+ by rewrite -JOBother; apply FROMTS.
+ } intro IN.
+ move: IN => /mapP [p IN EQ]; destruct p as [tsk' R']; simpl in *; subst tsk'.
+ apply completion_monotonic with (t0 := job_arrival j_other + task_jitter tsk_other + R');
+ try (by done); last by rewrite -addnA; apply PREV.
+ by rewrite -addnA leq_add2l; apply leq_trans with (n := task_deadline tsk_other);
+ [by apply NOMISS | by apply RESTR; rewrite -JOBother].
}
- apply leq_trans with (n := job_cost j); first by ins.
- apply leq_trans with (n := task_cost tsk);
- first by rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS1.
- by rewrite H_response_time_recurrence_holds leq_addr.
- }
- Qed.
-
- Let scheduled_task_other_than_tsk (t: time) (tsk_other: sporadic_task) :=
- task_is_scheduled job_task sched tsk_other t &&
- can_interfere_with_tsk tsk_other.
-
- (* 1) At all times that j is backlogged, all processors are busy with other tasks. *)
- Lemma bertogna_fp_scheduling_invariant:
- forall t,
- job_arrival j + job_jitter j <= t < job_arrival j + job_jitter j + R ->
- backlogged job_cost job_jitter sched j t ->
- count (scheduled_task_other_than_tsk t) ts = num_cpus.
- Proof.
- rename H_valid_task_parameters into PARAMS,
- H_job_of_tsk into JOBtsk,
- H_all_jobs_from_taskset into FROMTS,
- H_sporadic_tasks into SPO,
- H_valid_job_parameters into JOBPARAMS,
- H_constrained_deadlines into RESTR,
- H_hp_bounds_has_interfering_tasks into UNZIP,
- H_interfering_tasks_miss_no_deadlines into NOMISS,
- H_response_time_of_interfering_tasks_is_known into PREV,
- H_previous_jobs_of_tsk_completed into PREVtsk.
- unfold sporadic_task_model, is_response_time_bound_of_task,
- valid_sporadic_job_with_jitter in *.
- move => t /andP [LEt LTt] BACK.
-
- apply platform_fp_cpus_busy_with_interfering_tasks with (task_cost0 := task_cost)
- (task_period0 := task_period) (task_deadline0 := task_deadline) (job_task0 := job_task)
- (ts0 := ts) (tsk0 := tsk) (higher_eq_priority0 := higher_eq_priority) in BACK;
- try (by done); first by apply PARAMS; rewrite -JOBtsk FROMTS.
- {
- apply leq_trans with (n := job_arrival j + job_jitter j + R); first by done.
- rewrite -addnA leq_add2l.
- apply leq_trans with (n := task_deadline tsk); last by apply RESTR.
- apply leq_trans with (n := task_jitter tsk + R); last by done.
- by rewrite leq_add2r -JOBtsk; specialize (JOBPARAMS j); des.
- }
- {
- intros j_other tsk_other JOBother INTERF.
- move: UNZIP => UNZIP.
- cut (tsk_other \in unzip1 hp_bounds); last first.
{
- rewrite -UNZIP mem_filter; apply/andP; split; first by done.
- by rewrite -JOBother; apply FROMTS.
- } intro IN.
- move: IN => /mapP [p IN EQ]; destruct p as [tsk' R']; simpl in *; subst tsk'.
- apply completion_monotonic with (t0 := job_arrival j_other + task_jitter tsk_other + R');
- try (by done); last by rewrite -addnA; apply PREV.
- by rewrite -addnA leq_add2l; apply leq_trans with (n := task_deadline tsk_other);
- [by apply NOMISS | by apply RESTR; rewrite -JOBother].
- }
- {
- ins; apply completion_monotonic with (t0 := job_arrival j0 + task_jitter tsk + R);
- try (by done); last by apply PREVtsk.
- rewrite -addnA leq_add2l.
- by apply leq_trans with (n := task_deadline tsk); [by done | by apply RESTR].
- }
- Qed.
-
- (* 2) Next, we prove that the sum of the interference of each task is equal
- to the total interference multiplied by the number of processors. This
- holds because interference only occurs when all processors are busy. *)
- Lemma bertogna_fp_all_cpus_busy :
- \sum_(tsk_k <- ts_interf) x tsk_k = X * num_cpus.
- Proof.
- unfold x, X, total_interference, task_interference.
- rewrite -big_mkcond -exchange_big big_distrl /=.
- rewrite [\sum_(_ <= _ < _ | backlogged _ _ _ _ _) _]big_mkcond.
- apply eq_big_nat; move => t LTt.
- destruct (backlogged job_cost job_jitter sched j t) eqn:BACK;
- last by rewrite (eq_bigr (fun i => 0));
- [by rewrite big_const_seq iter_addn mul0n addn0 | by done].
- rewrite big_mkcond mul1n /=.
- rewrite big_filter big_mkcond.
- rewrite (eq_bigr (fun i => if (scheduled_task_other_than_tsk t i) then 1 else 0));
- last first.
- {
- intros i _; clear -i.
- unfold scheduled_task_other_than_tsk.
- by destruct (task_is_scheduled job_task sched i t); rewrite ?andFb ?andTb ?andbT //; desf.
- }
- rewrite -big_mkcond sum1_count.
- by apply bertogna_fp_scheduling_invariant.
- Qed.
-
- (* Let (cardGE delta) be the number of interfering tasks whose interference
- is larger than delta. *)
- Let cardGE (delta: time) := count (fun i => x i >= delta) ts_interf.
-
- (* 3) If there is at least one of such tasks (e.g., cardGE > 0), then the
- cumulative interference caused by the complementary set of interfering
- tasks fills at least (num_cpus - cardGE) processors. *)
- Lemma bertogna_fp_helper_lemma :
- forall delta,
- cardGE delta > 0 ->
- \sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
- Proof.
- intros delta HAS.
- set some_interference_A := fun t =>
- backlogged job_cost job_jitter sched j t &&
- has (fun tsk_k => ((x tsk_k >= delta) &&
- task_is_scheduled job_task sched tsk_k t)) ts_interf.
- set total_interference_B := fun t =>
- backlogged job_cost job_jitter sched j t *
- count (fun tsk_k => (x tsk_k < delta) &&
- task_is_scheduled job_task sched tsk_k t) ts_interf.
-
- rewrite -has_count in HAS.
- apply leq_trans with ((\sum_(t1 <= t < t1 + R)
- some_interference_A t) * (num_cpus - cardGE delta)).
- {
- rewrite leq_mul2r; apply/orP; right.
- move: HAS => /hasP HAS; destruct HAS as [tsk_a INa LEa].
- apply leq_trans with (n := x tsk_a); first by apply LEa.
- unfold x, task_interference, some_interference_A.
- apply leq_sum; ins.
- destruct (backlogged job_cost job_jitter sched j i);
- [rewrite 2!andTb | by ins].
- destruct (task_is_scheduled job_task sched tsk_a i) eqn:SCHEDa;
- [apply eq_leq; symmetry | by ins].
- apply/eqP; rewrite eqb1.
- by apply/hasP; exists tsk_a; last by apply/andP.
- }
- apply leq_trans with (\sum_(t1 <= t < t1 + R)
- total_interference_B t).
- {
- rewrite big_distrl /=.
- rewrite big_nat_cond [\sum_(_ <= _ < _ | true) _]big_nat_cond.
- apply leq_sum; move => t /andP [LEt _].
- unfold some_interference_A, total_interference_B.
+ ins; apply completion_monotonic with (t0 := job_arrival j0 + task_jitter tsk + R);
+ try (by done); last by apply PREVtsk.
+ rewrite -addnA leq_add2l.
+ by apply leq_trans with (n := task_deadline tsk); [by done | by apply RESTR].
+ }
+ Qed.
+
+ (* 2) Prove that during the scheduling window of j, any job that is scheduled while j is
+ backlogged comes from a different task. *)
+ Lemma bertogna_fp_interference_by_different_tasks :
+ forall t j_other,
+ t1 <= t < t1 + R ->
+ backlogged job_cost job_jitter sched j t ->
+ scheduled sched j_other t ->
+ job_task j_other != tsk.
+ Proof.
+ rename H_all_jobs_from_taskset into FROMTS,
+ H_valid_job_parameters into JOBPARAMS, H_valid_task_parameters into PARAMS,
+ H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
+ H_work_conserving into WORK,
+ H_constrained_deadlines into CONSTR,
+ H_previous_jobs_of_tsk_completed into PREV,
+ H_response_time_no_larger_than_deadline into NOMISS.
+ unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
+ move => t j_other /andP [LEt GEt] BACK SCHED.
+ apply/eqP; red; intro SAMEtsk.
+ move: SCHED => /existsP [cpu SCHED].
+ assert (SCHED': scheduled sched j_other t).
+ by apply/existsP; exists cpu.
+ clear SCHED; rename SCHED' into SCHED.
+ move: (SCHED) => PENDING.
+ apply scheduled_implies_pending with (job_cost0 := job_cost) (job_jitter0 := job_jitter)
+ in PENDING; try (by done).
+ destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
+ {
+ move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
+ specialize (PREV j_other SAMEtsk BEFOREother).
+ move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
+ apply completion_monotonic with (t0 := job_arrival j_other + task_jitter tsk + R);
+ try by done.
+ apply leq_trans with (n := job_arrival j);
+ last by apply leq_trans with (n := t1); [by apply leq_addr | by done].
+ apply leq_trans with (n := job_arrival j_other + task_period tsk).
+ {
+ rewrite -addnA leq_add2l.
+ by apply leq_trans with (n := task_deadline tsk);
+ [by apply NOMISS | by apply CONSTR; rewrite -JOBtsk FROMTS].
+ }
+ rewrite -SAMEtsk; apply SPO; [ | by rewrite JOBtsk | by apply ltnW].
+ by red; intro EQ; subst j_other; rewrite ltnn in BEFOREother.
+ }
+ {
+ move: PENDING => /andP [ARRIVED _].
+ exploit (SPO j j_other); [ | by rewrite SAMEtsk | by done | ]; last first.
+ {
+ apply/negP; rewrite -ltnNge JOBtsk.
+ apply leq_trans with (n := job_arrival j + task_deadline tsk);
+ last by rewrite leq_add2l; apply CONSTR; rewrite -JOBtsk FROMTS.
+ apply leq_trans with (n := job_arrival j + task_jitter tsk + R);
+ last by rewrite -addnA leq_add2l; apply NOMISS.
+ apply leq_trans with (n := t1 + R); last first.
+ {
+ rewrite leq_add2r leq_add2l -JOBtsk.
+ by specialize (JOBPARAMS j); des.
+ }
+ apply leq_ltn_trans with (n := job_arrival j_other + job_jitter j_other);
+ first by apply leq_addr.
+ by apply leq_ltn_trans with (n := t).
+ }
+ by intros EQtsk; subst j_other; rewrite /backlogged SCHED andbF in BACK.
+ }
+ Qed.
+
+ (* 3) Next, we prove that the sum of the interference of each task is equal
+ to the total interference multiplied by the number of processors. This
+ holds because interference only occurs when all processors are busy. *)
+ Lemma bertogna_fp_all_cpus_busy :
+ \sum_(tsk_k <- ts_interf) x tsk_k = X * num_cpus.
+ Proof.
+ rename H_all_jobs_from_taskset into FROMTS,
+ H_valid_task_parameters into PARAMS,
+ H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
+ H_work_conserving into WORK,
+ H_constrained_deadlines into CONSTR,
+ H_previous_jobs_of_tsk_completed into PREV,
+ H_enforces_priority into FP,
+ H_response_time_no_larger_than_deadline into NOMISS.
+ unfold sporadic_task_model in *.
+ unfold x, X, total_interference, task_interference.
+ rewrite -big_mkcond -exchange_big big_distrl /= mul1n.
+ rewrite [\sum_(_ <= _ < _ | backlogged _ _ _ _ _) _]big_mkcond.
+ apply eq_big_nat; move => t /andP [GEt LTt].
destruct (backlogged job_cost job_jitter sched j t) eqn:BACK;
- [rewrite andTb mul1n | by done].
- destruct (has (fun tsk_k : sporadic_task => (delta <= x tsk_k) &&
- task_is_scheduled job_task sched tsk_k t) ts_interf) eqn:HAS';
- last by done.
- rewrite mul1n; move: HAS => /hasP HAS.
- destruct HAS as [tsk_k INk LEk].
-
- have COUNT := bertogna_fp_scheduling_invariant t LEt BACK.
-
- unfold cardGE.
- set interfering_tasks_at_t :=
- [seq tsk_k <- ts_interf | task_is_scheduled job_task
- sched tsk_k t].
-
- rewrite -(count_filter (fun i => true)) in COUNT.
- fold interfering_tasks_at_t in COUNT.
- rewrite count_predT in COUNT.
- apply leq_trans with (n := num_cpus -
- count (fun i => (x i >= delta) &&
- task_is_scheduled job_task sched i t) ts_interf).
+ last by rewrite big1 //; ins; rewrite big1.
+ rewrite big_mkcond /=.
+ rewrite exchange_big /=.
+ apply eq_trans with (y := \sum_(cpu < num_cpus) 1); last by simpl_sum_const.
+ apply eq_bigr; intros cpu _.
+ move: (WORK j t BACK cpu) => [j_other /eqP SCHED]; unfold scheduled_on in *.
+ rewrite (bigD1_seq (job_task j_other)) /=; last by rewrite filter_uniq.
+ {
+ rewrite (eq_bigr (fun i => 0));
+ last by intros i DIFF; rewrite /task_scheduled_on SCHED;apply/eqP;rewrite eqb0 eq_sym.
+ simpl_sum_const; apply/eqP; rewrite eqb1.
+ by unfold task_scheduled_on; rewrite SCHED.
+ }
+ rewrite mem_filter; apply/andP; split; last by apply FROMTS.
+ unfold can_interfere_with_tsk, fp_can_interfere_with; apply/andP; split.
{
- apply leq_sub2l.
- rewrite -2!sum1_count big_mkcond /=.
- rewrite [\sum_(_ <- _ | _ <= _)_]big_mkcond /=.
- apply leq_sum; intros i _.
- destruct (task_is_scheduled job_task sched i t);
- [by rewrite andbT | by rewrite andbF].
+ rewrite -JOBtsk; apply FP with (t := t); try by done.
+ by apply/existsP; exists cpu; apply/eqP.
}
+ apply bertogna_fp_interference_by_different_tasks with (t := t); [by auto | by done |].
+ by apply/existsP; exists cpu; apply/eqP.
+ Qed.
- rewrite leq_subLR -count_predUI.
- apply leq_trans with (n :=
- count (predU (fun i : sporadic_task =>
- (delta <= x i) &&
- task_is_scheduled job_task sched i t)
- (fun tsk_k0 : sporadic_task =>
- (x tsk_k0 < delta) &&
- task_is_scheduled job_task sched tsk_k0 t))
- ts_interf); last by apply leq_addr.
- apply leq_trans with (n := size interfering_tasks_at_t).
+ (* Let (cardGE delta) be the number of interfering tasks whose interference
+ is larger than delta. *)
+ Let cardGE (delta: time) := count (fun i => x i >= delta) ts_interf.
+
+ (* 4) If there is at least one of such tasks (e.g., cardGE > 0), then the
+ cumulative interference caused by the complementary set of interfering
+ tasks fills at least (num_cpus - cardGE) processors. *)
+ Lemma bertogna_fp_helper_lemma :
+ forall delta,
+ 0 < cardGE delta < num_cpus ->
+ \sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
+ Proof.
+ rename H_all_jobs_from_taskset into FROMTS,
+ H_valid_task_parameters into PARAMS,
+ H_valid_job_parameters into JOBPARAMS,
+ H_job_of_tsk into JOBtsk,
+ H_sporadic_tasks into SPO,
+ H_previous_jobs_of_tsk_completed into BEFOREok,
+ H_response_time_no_larger_than_deadline into NOMISS,
+ H_constrained_deadlines into CONSTR,
+ H_sequential_jobs into SEQ,
+ H_enforces_priority into FP,
+ H_hp_bounds_has_interfering_tasks into UNZIP,
+ H_interfering_tasks_miss_no_deadlines into NOMISSHP.
+ unfold sporadic_task_model, valid_sporadic_job_with_jitter, valid_sporadic_job in *.
+ move => delta /andP [HAS LT].
+ rewrite -has_count in HAS.
+
+ set some_interference_A := fun t =>
+ has (fun tsk_k => backlogged job_cost job_jitter sched j t &&
+ (x tsk_k >= delta) &&
+ task_is_scheduled job_task sched tsk_k t) ts_interf.
+ set total_interference_B := fun t =>
+ backlogged job_cost job_jitter sched j t *
+ count (fun tsk_k => (x tsk_k < delta) &&
+ task_is_scheduled job_task sched tsk_k t) ts_interf.
+
+ apply leq_trans with ((\sum_(t1 <= t < t1 + R)
+ some_interference_A t) * (num_cpus - cardGE delta)).
{
- rewrite -COUNT.
- rewrite leq_eqVlt; apply/orP; left; apply/eqP; f_equal.
- unfold interfering_tasks_at_t.
- rewrite -filter_predI; apply eq_filter; red; simpl.
- by intros i; rewrite andbC.
+ rewrite leq_mul2r; apply/orP; right.
+ move: HAS => /hasP HAS; destruct HAS as [tsk_a INa LEa].
+ apply leq_trans with (n := x tsk_a); first by apply LEa.
+ unfold x, task_interference, some_interference_A.
+ apply leq_sum_nat; move => t /andP [GEt LTt] _.
+ destruct (backlogged job_cost job_jitter sched j t) eqn:BACK;
+ last by rewrite (eq_bigr (fun x => 0)); [by simpl_sum_const | by ins].
+ destruct ([exists cpu, task_scheduled_on job_task sched tsk_a cpu t]) eqn:SCHED;
+ last first.
+ {
+ apply negbT in SCHED; rewrite negb_exists in SCHED; move: SCHED => /forallP ALL.
+ rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const.
+ by intros cpu _; specialize (ALL cpu); apply negbTE in ALL; rewrite ALL.
+ }
+ move: SCHED => /existsP [cpu SCHED].
+ apply leq_trans with (n := 1); last first.
+ {
+ rewrite lt0b; apply/hasP; exists tsk_a; first by done.
+ by rewrite LEa 2!andTb; apply/existsP; exists cpu.
+ }
+ rewrite (bigD1 cpu) /= // SCHED.
+ rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const; rewrite leq_b1.
+ intros cpu' DIFF.
+ apply/eqP; rewrite eqb0; apply/negP.
+ intros SCHED'.
+ move: DIFF => /negP DIFF; apply DIFF; apply/eqP.
+ unfold task_scheduled_on in *.
+ destruct (sched cpu t) as [j1|] eqn:SCHED1; last by done.
+ destruct (sched cpu' t) as [j2|] eqn:SCHED2; last by done.
+ move: SCHED SCHED' => /eqP JOB /eqP JOB'.
+ subst tsk_a; symmetry in JOB'.
+ assert (PENDING1: pending job_cost job_jitter sched j1 t).
+ {
+ apply scheduled_implies_pending; try by done.
+ by apply/existsP; exists cpu; apply/eqP.
+ }
+ assert (PENDING2: pending job_cost job_jitter sched j2 t).
+ {
+ apply scheduled_implies_pending; try by done.
+ by apply/existsP; exists cpu'; apply/eqP.
+ }
+ assert (BUG: j1 = j2).
+ {
+ destruct (job_task j1 == tsk) eqn:SAMEtsk.
+ {
+ move: SAMEtsk => /eqP SAMEtsk.
+ move: (PENDING1) => SAMEjob.
+ apply platform_fp_no_multiple_jobs_of_tsk with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline)
+ (job_task0 := job_task) (tsk0 := tsk) (j0 := j) in SAMEjob; try (by done);
+ [ | by apply PARAMS | |]; last 2 first.
+ {
+ apply (leq_trans LTt); rewrite -addnA leq_add2l.
+ apply leq_trans with (n := task_deadline tsk); last by apply CONSTR.
+ apply leq_trans with (n := task_jitter tsk + R); last by apply NOMISS.
+ by rewrite leq_add2r -JOBtsk; specialize (JOBPARAMS j); des.
+ }
+ {
+ intros j0 JOB0 LT0.
+ apply completion_monotonic with (t0 := job_arrival j0 + task_jitter tsk + R); try (by done);
+ last by apply BEFOREok.
+ rewrite -addnA leq_add2l.
+ by apply leq_trans with (n := task_deadline tsk); last by apply CONSTR.
+ }
+ move: BACK => /andP [_ /negP NOTSCHED]; exfalso; apply NOTSCHED.
+ by rewrite -SAMEjob; apply/existsP; exists cpu; apply/eqP.
+ }
+ {
+ assert (INTERF: fp_can_interfere_with higher_eq_priority tsk (job_task j1)).
+ {
+ apply/andP; split; last by rewrite SAMEtsk.
+ rewrite -JOBtsk; apply FP with (t := t); first by done.
+ by apply/existsP; exists cpu; apply/eqP.
+ }
+ apply platform_fp_no_multiple_jobs_of_interfering_tasks with
+ (task_period0 := task_period) (tsk0 := tsk)
+ (higher_eq_priority0 := higher_eq_priority) (job_jitter0 := job_jitter)
+ (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) (t0 := t);
+ rewrite ?JOBtsk ?SAMEtsk //.
+ {
+ intros j0 tsk0 JOB0 INTERF0.
+ assert (IN: tsk0 \in (unzip1 hp_bounds)).
+ by rewrite -UNZIP mem_filter; apply/andP; split; last by rewrite -JOB0 FROMTS.
+ move: IN => /mapP [p IN EQ]; destruct p as [tsk0' R0]; simpl in *; subst tsk0'.
+ apply completion_monotonic with (t0 := job_arrival j0 + task_jitter tsk0 + R0);
+ try (by done).
+ {
+ rewrite -addnA leq_add2l.
+ by apply leq_trans with (n := task_deadline tsk0);
+ [by apply NOMISSHP | by apply CONSTR; rewrite -JOB0 FROMTS].
+ }
+ rewrite -addnA.
+ by eapply H_response_time_of_interfering_tasks_is_known; first by apply IN.
+ }
+ }
+ }
+ by subst j2; apply SEQ with (j := j1) (t := t).
}
- unfold interfering_tasks_at_t.
- rewrite -count_predT count_filter.
- rewrite leq_eqVlt; apply/orP; left; apply/eqP.
- apply eq_count; red; simpl.
- intros i.
- destruct (task_is_scheduled job_task sched i t);
- rewrite 3?andTb ?andFb ?andbF ?andbT /=; try ins.
- by rewrite leqNgt orNb.
- }
- {
- unfold x at 2, task_interference.
+
+ apply leq_trans with (\sum_(t1 <= t < t1 + R)
+ total_interference_B t).
+ {
+ rewrite big_distrl /=.
+ apply leq_sum_nat; move => t LEt _.
+ unfold some_interference_A, total_interference_B.
+ destruct (backlogged job_cost job_jitter sched j t) eqn:BACK;
+ [rewrite mul1n /= | by rewrite has_pred0 //].
+
+ destruct (has (fun tsk_k : sporadic_task => (delta <= x tsk_k) &&
+ task_is_scheduled job_task sched tsk_k t) ts_interf) eqn:HAS';
+ last by done.
+ rewrite mul1n; move: HAS => /hasP [tsk_k INk LEk].
+ unfold cardGE.
+ apply leq_trans with (n := num_cpus -
+ count (fun i => (x i >= delta) &&
+ task_is_scheduled job_task sched i t) ts_interf).
+ {
+ apply leq_sub2l.
+ rewrite -2!sum1_count big_mkcond /=.
+ rewrite [\sum_(_ <- _ | _ <= _)_]big_mkcond /=.
+ apply leq_sum; intros i _.
+ by destruct (task_is_scheduled job_task sched i t);
+ [by rewrite andbT | by rewrite andbF].
+ }
+ rewrite -count_filter -[count _ ts_interf]count_filter.
+ eapply leq_trans with (n := count (predC (fun tsk => delta <= x tsk)) _);
+ last by apply eq_leq, eq_in_count; red; ins; rewrite ltnNge.
+ rewrite leq_subLR count_predC size_filter.
+ apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
+ first by rewrite bertogna_fp_scheduling_invariant.
+ by rewrite count_filter.
+ }
+ {
+ unfold x at 2, total_interference_B.
rewrite exchange_big /=; apply leq_sum; intros t _.
- unfold total_interference_B.
- destruct (backlogged job_cost job_jitter sched j t); last by ins.
+ destruct (backlogged job_cost job_jitter sched j t) eqn:BACK; last by ins.
rewrite mul1n -sum1_count.
- rewrite big_seq_cond big_mkcond [\sum_(i <- ts_interf | _ < _) _]big_mkcond.
- by apply leq_sum; ins; clear -i; desf; des; rewrite ?Heq2.
- }
- Qed.
-
- (* 4) Next, we prove that, for any interval delta, if the sum of per-task
- interference exceeds delta * num_cpus, the same applies for the
- sum of the minimum between the interference and delta. *)
- Lemma bertogna_fp_minimum_exceeds_interference :
- forall delta,
- \sum_(tsk_k <- ts_interf) x tsk_k >= delta * num_cpus ->
- \sum_(tsk_k <- ts_interf) minn (x tsk_k) delta >=
- delta * num_cpus.
- Proof.
- intros delta SUMLESS.
- set more_interf := fun tsk_k => x tsk_k >= delta.
- rewrite [\sum_(_ <- _) minn _ _](bigID more_interf) /=.
- unfold more_interf, minn.
- rewrite [\sum_(_ <- _ | delta <= _)_](eq_bigr (fun i => delta));
- last by intros i COND; rewrite leqNgt in COND; destruct (delta > x i).
- rewrite [\sum_(_ <- _ | ~~_)_](eq_big (fun i => x i < delta)
- (fun i => x i));
- [| by red; ins; rewrite ltnNge
- | by intros i COND; rewrite -ltnNge in COND; rewrite COND].
-
- (* Case 1: cardGE = 0 *)
- destruct (~~ has (fun i => delta <= x i) ts_interf) eqn:HASa.
- {
- rewrite [\sum_(_ <- _ | _ <= _) _]big_hasC; last by apply HASa.
- rewrite big_seq_cond; move: HASa => /hasPn HASa.
- rewrite add0n (eq_bigl (fun i => (i \in ts_interf) && true));
- last by red; intros tsk_k; destruct (tsk_k \in ts_interf) eqn:INk;
- [by rewrite andTb ltnNge; apply HASa | by rewrite andFb].
- by rewrite -big_seq_cond.
- } apply negbFE in HASa.
-
- (* Case 2: cardGE >= num_cpus *)
- destruct (cardGE delta >= num_cpus) eqn:CARD.
- {
- apply leq_trans with (delta * cardGE delta);
- first by rewrite leq_mul2l; apply/orP; right.
- unfold cardGE; rewrite -sum1_count big_distrr /=.
- rewrite -[\sum_(_ <- _ | _) _]addn0.
- by apply leq_add; [by apply leq_sum; ins; rewrite muln1|by ins].
- } apply negbT in CARD; rewrite -ltnNge in CARD.
-
- (* Case 3: cardGE < num_cpus *)
- rewrite big_const_seq iter_addn addn0; fold cardGE.
- apply leq_trans with (n := delta * cardGE delta +
- delta * (num_cpus - cardGE delta));
- first by rewrite -mulnDr subnKC //; apply ltnW.
- by rewrite leq_add2l; apply bertogna_fp_helper_lemma; rewrite -has_count.
- Qed.
-
- (* 5) Now, we prove that the Bertogna's interference bound
- is not enough to cover the sum of the "minimum" term over
- all tasks (artifact of the proof by contradiction). *)
- Lemma bertogna_fp_sum_exceeds_total_interference:
- \sum_((tsk_k, R_k) <- hp_bounds)
- minn (x tsk_k) (R - task_cost tsk + 1) >
- total_interference_bound_fp task_cost task_period task_jitter tsk hp_bounds
- R higher_eq_priority.
- Proof.
- rename H_hp_bounds_has_interfering_tasks into UNZIP,
- H_response_time_recurrence_holds into REC.
- apply leq_trans with (n := \sum_(tsk_k <- ts_interf) minn (x tsk_k) (R - task_cost tsk + 1));
- last first.
- {
- rewrite (eq_bigr (fun i => minn (x (fst i)) (R - task_cost tsk + 1)));
- last by ins; destruct i.
- rewrite big_filter.
- have MAP := big_map (fun x => fst x) (fun i => true) (fun i => minn (x i) (R - task_cost tsk + 1)).
- by unfold unzip1 in *; rewrite -MAP -UNZIP -big_filter.
- }
- apply ltn_div_trunc with (d := num_cpus);
- first by apply H_at_least_one_cpu.
- unfold div_floor in REC.
- rewrite -(ltn_add2l (task_cost tsk)) -REC.
- rewrite -addn1 -leq_subLR.
- rewrite -[R + 1 - _]subh1; last by rewrite REC; apply leq_addr.
- rewrite leq_divRL; last by apply H_at_least_one_cpu.
- apply bertogna_fp_minimum_exceeds_interference.
- apply leq_trans with (n := X * num_cpus);
- last by rewrite bertogna_fp_all_cpus_busy.
- rewrite leq_mul2r; apply/orP; right.
- by apply bertogna_fp_too_much_interference.
- Qed.
-
- (* 6) After concluding that the sum of the minimum exceeds (R' - e_i + 1),
- we prove that there exists a tuple (tsk_k, R_k) such that
- min (x_k, R' - e_i + 1) > min (W_k, R' - e_i + 1). *)
- Lemma bertogna_fp_exists_task_that_exceeds_bound :
- exists tsk_k R_k,
- (tsk_k, R_k) \in hp_bounds /\
- (minn (x tsk_k) (R - task_cost tsk + 1) >
- minn (workload_bound tsk_k R_k) (R - task_cost tsk + 1)).
- Proof.
- rename H_hp_bounds_has_interfering_tasks into UNZIP.
- assert (HAS: has (fun tup : task_with_response_time =>
- let (tsk_k, R_k) := tup in
- (minn (x tsk_k) (R - task_cost tsk + 1) >
- minn (workload_bound tsk_k R_k)(R - task_cost tsk + 1)))
- hp_bounds).
- {
- apply/negP; unfold not; intro NOTHAS.
- move: NOTHAS => /negP /hasPn ALL.
- have SUM := bertogna_fp_sum_exceeds_total_interference.
- rewrite -[_ < _]negbK in SUM.
- move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
- unfold total_interference_bound_fp.
- rewrite [\sum_(i <- _ | let '(tsk_other, _) := i in _)_]big_mkcond.
- rewrite big_seq_cond [\sum_(i <- _ | true) _]big_seq_cond.
- apply leq_sum; move => tsk_k /andP [HPk _]; destruct tsk_k as [tsk_k R_k].
- specialize (ALL (tsk_k, R_k) HPk).
- rewrite -leqNgt in ALL.
- have INTERFk := bertogna_fp_tsk_other_interferes tsk_k R_k HPk.
- fold (can_interfere_with_tsk); rewrite INTERFk.
- by apply ALL.
- }
- move: HAS => /hasP HAS; destruct HAS as [[tsk_k R_k] HPk MINk]; exists tsk_k, R_k.
- by repeat split.
- Qed.
+ rewrite big_mkcond [\sum_(i <- ts_interf | _ < _) _]big_mkcond /=.
+ apply leq_sum_seq; move => tsk_k IN _.
+ destruct (x tsk_k < delta); [rewrite andTb | by rewrite andFb].
+ destruct (task_is_scheduled job_task sched tsk_k t) eqn:SCHED; last by done.
+ move: SCHED => /existsP [cpu SCHED].
+ by rewrite (bigD1 cpu) /= // SCHED.
+ }
+ Qed.
+
+ (* 5) Next, we prove that, for any interval delta, if the sum of per-task
+ interference exceeds delta * num_cpus, the same applies for the
+ sum of the minimum between the interference and delta. *)
+ Lemma bertogna_fp_minimum_exceeds_interference :
+ forall delta,
+ \sum_(tsk_k <- ts_interf) x tsk_k >= delta * num_cpus ->
+ \sum_(tsk_k <- ts_interf) minn (x tsk_k) delta >=
+ delta * num_cpus.
+ Proof.
+ intros delta SUMLESS.
+ set more_interf := fun tsk_k => x tsk_k >= delta.
+ rewrite [\sum_(_ <- _) minn _ _](bigID more_interf) /=.
+ unfold more_interf, minn.
+ rewrite [\sum_(_ <- _ | delta <= _)_](eq_bigr (fun i => delta));
+ last by intros i COND; rewrite leqNgt in COND; destruct (delta > x i).
+ rewrite [\sum_(_ <- _ | ~~_)_](eq_big (fun i => x i < delta)
+ (fun i => x i));
+ [| by red; ins; rewrite ltnNge
+ | by intros i COND; rewrite -ltnNge in COND; rewrite COND].
+
+ (* Case 1: cardGE = 0 *)
+ destruct (~~ has (fun i => delta <= x i) ts_interf) eqn:HASa.
+ {
+ rewrite [\sum_(_ <- _ | _ <= _) _]big_hasC; last by apply HASa.
+ rewrite big_seq_cond; move: HASa => /hasPn HASa.
+ rewrite add0n (eq_bigl (fun i => (i \in ts_interf) && true));
+ last by red; intros tsk_k; destruct (tsk_k \in ts_interf) eqn:INk;
+ [by rewrite andTb ltnNge; apply HASa | by rewrite andFb].
+ by rewrite -big_seq_cond.
+ } apply negbFE in HASa.
+
+ (* Case 2: cardGE >= num_cpus *)
+ destruct (cardGE delta >= num_cpus) eqn:CARD.
+ {
+ apply leq_trans with (delta * cardGE delta);
+ first by rewrite leq_mul2l; apply/orP; right.
+ unfold cardGE; rewrite -sum1_count big_distrr /=.
+ rewrite -[\sum_(_ <- _ | _) _]addn0.
+ by apply leq_add; [by apply leq_sum; ins; rewrite muln1|by ins].
+ } apply negbT in CARD; rewrite -ltnNge in CARD.
+
+ (* Case 3: cardGE < num_cpus *)
+ rewrite big_const_seq iter_addn addn0; fold cardGE.
+ apply leq_trans with (n := delta * cardGE delta +
+ delta * (num_cpus - cardGE delta));
+ first by rewrite -mulnDr subnKC //; apply ltnW.
+ rewrite leq_add2l; apply bertogna_fp_helper_lemma.
+ by apply/andP; split; first by rewrite -has_count.
+ Qed.
+
+ (* 6) Now, we prove that the Bertogna's interference bound
+ is not enough to cover the sum of the "minimum" term over
+ all tasks (artifact of the proof by contradiction). *)
+ Lemma bertogna_fp_sum_exceeds_total_interference:
+ \sum_((tsk_k, R_k) <- hp_bounds)
+ minn (x tsk_k) (R - task_cost tsk + 1) >
+ total_interference_bound_fp task_cost task_period task_jitter tsk hp_bounds
+ R higher_eq_priority.
+ Proof.
+ rename H_hp_bounds_has_interfering_tasks into UNZIP,
+ H_response_time_recurrence_holds into REC.
+ apply leq_trans with (n := \sum_(tsk_k <- ts_interf) minn (x tsk_k) (R - task_cost tsk + 1));
+ last first.
+ {
+ rewrite (eq_bigr (fun i => minn (x (fst i)) (R - task_cost tsk + 1)));
+ last by ins; destruct i.
+ rewrite big_filter.
+ have MAP := big_map (fun x => fst x) (fun i => true) (fun i => minn (x i)
+ (R - task_cost tsk + 1)).
+ by unfold unzip1 in *; rewrite -MAP -UNZIP -big_filter.
+ }
+ apply ltn_div_trunc with (d := num_cpus);
+ first by apply H_at_least_one_cpu.
+ unfold div_floor in REC.
+ rewrite -(ltn_add2l (task_cost tsk)) -REC.
+ rewrite -addn1 -leq_subLR.
+ rewrite -[R + 1 - _]subh1; last by rewrite REC; apply leq_addr.
+ rewrite leq_divRL; last by apply H_at_least_one_cpu.
+ apply bertogna_fp_minimum_exceeds_interference.
+ apply leq_trans with (n := X * num_cpus);
+ last by rewrite bertogna_fp_all_cpus_busy.
+ rewrite leq_mul2r; apply/orP; right.
+ by apply bertogna_fp_too_much_interference.
+ Qed.
+
+ (* 7) After concluding that the sum of the minimum exceeds (R' - e_i + 1),
+ we prove that there exists a tuple (tsk_k, R_k) such that
+ min (x_k, R' - e_i + 1) > min (W_k, R' - e_i + 1). *)
+ Lemma bertogna_fp_exists_task_that_exceeds_bound :
+ exists tsk_k R_k,
+ (tsk_k, R_k) \in hp_bounds /\
+ (minn (x tsk_k) (R - task_cost tsk + 1) >
+ minn (workload_bound tsk_k R_k) (R - task_cost tsk + 1)).
+ Proof.
+ rename H_hp_bounds_has_interfering_tasks into UNZIP.
+ assert (HAS: has (fun tup : task_with_response_time =>
+ let (tsk_k, R_k) := tup in
+ (minn (x tsk_k) (R - task_cost tsk + 1) >
+ minn (workload_bound tsk_k R_k)(R - task_cost tsk + 1)))
+ hp_bounds).
+ {
+ apply/negP; unfold not; intro NOTHAS.
+ move: NOTHAS => /negP /hasPn ALL.
+ have SUM := bertogna_fp_sum_exceeds_total_interference.
+ rewrite -[_ < _]negbK in SUM.
+ move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
+ unfold total_interference_bound_fp.
+ rewrite [\sum_(i <- _ | let '(tsk_other, _) := i in _)_]big_mkcond.
+ rewrite big_seq_cond [\sum_(i <- _ | true) _]big_seq_cond.
+ apply leq_sum; move => tsk_k /andP [HPk _]; destruct tsk_k as [tsk_k R_k].
+ specialize (ALL (tsk_k, R_k) HPk).
+ rewrite -leqNgt in ALL.
+ have INTERFk := bertogna_fp_tsk_other_interferes tsk_k R_k HPk.
+ fold (can_interfere_with_tsk); rewrite INTERFk.
+ by apply ALL.
+ }
+ move: HAS => /hasP HAS; destruct HAS as [[tsk_k R_k] HPk MINk]; exists tsk_k, R_k.
+ by repeat split.
+ Qed.
End DerivingContradiction.
@@ -630,11 +785,12 @@ Module ResponseTimeAnalysisFP.
destruct EX as [tsk_k [R_k [HPk LTmin]]].
unfold minn at 1 in LTmin.
have WORKLOAD := bertogna_fp_workload_bounds_interference j tsk_k R_k HPk.
- destruct (W_jitter task_cost task_period task_jitter tsk_k R_k R < R - task_cost tsk + 1); rewrite leq_min in LTmin;
+ destruct (W_jitter task_cost task_period task_jitter tsk_k R_k R < R - task_cost tsk + 1);
+ rewrite leq_min in LTmin;
last by move: LTmin => /andP [_ BUG]; rewrite ltnn in BUG.
move: LTmin => /andP [BUG _]; des.
- apply leq_trans with (p := W_jitter task_cost task_period task_jitter tsk_k R_k R) in BUG; last by done.
- by rewrite ltnn in BUG.
+ by apply leq_trans with (p := W_jitter task_cost task_period task_jitter tsk_k R_k R) in BUG;
+ first by rewrite ltnn in BUG.
Qed.
End ResponseTimeBound.
diff --git a/analysis/jitter/interference_bound_edf.v b/analysis/jitter/interference_bound_edf.v
index 8256f7da2..525ebeb7e 100644
--- a/analysis/jitter/interference_bound_edf.v
+++ b/analysis/jitter/interference_bound_edf.v
@@ -556,23 +556,18 @@ Module InterferenceBoundEDFJitter.
\sum_(a_fst + J_k + R_k <= t < a_fst + D_k) 1).
{
apply leq_add; last by rewrite SUBST.
- by unfold job_interference; apply leq_sum; ins; apply leq_b1.
+ simpl_sum_const; rewrite -{1}[_ + R_k](addKn a_i) -addnBA //;
+ last by apply leq_trans with (n := t1); first by apply leq_addr.
+ by apply job_interference_le_delta.
}
- rewrite -big_cat_nat; simpl; last first.
+ rewrite -big_cat_nat; simpl; last by rewrite -addnA leq_add2l H_R_k_le_deadline.
{
- rewrite -addnA leq_add2l.
- by apply H_R_k_le_deadline.
- }
- {
- by apply leq_trans with (n := t1); first by apply leq_addr.
- }
- {
- rewrite big_const_nat iter_addn mul1n addn0 leq_subLR.
- unfold D_i, D_k, t1, a_fst.
+ simpl_sum_const; rewrite leq_subLR; unfold D_i, D_k, t1, a_fst.
by rewrite -interference_bound_edf_j_fst_deadline
-interference_bound_edf_j_i_deadline.
}
+ by apply leq_trans with (n := t1); first by apply leq_addr.
Qed.
End ResponseTimeOfSingleJobBounded.
@@ -652,9 +647,16 @@ Module InterferenceBoundEDFJitter.
apply leq_trans with (n := \sum_(t1 <= t < a_fst + J_k + R_k) 1 +
\sum_(a_fst + J_k + R_k <= t < a_fst + D_k)1).
{
- apply leq_add; unfold job_interference;
- first by apply leq_sum; ins; apply leq_b1.
- rewrite big_const_nat iter_addn mul1n addn0 addnC.
+ apply leq_add; unfold job_interference.
+ {
+ simpl_sum_const.
+ rewrite -{1}[job_arrival j_fst + J_k + R_k](addKn t1) -addnBA;
+ first by apply job_interference_le_delta.
+ apply leq_trans with (n := a_i + J_i + delta); last by done.
+ apply leq_trans with (n := a_i + J_i); last by apply leq_addr.
+ by rewrite leq_add2l /J_i -H_job_of_tsk_i; apply PARAMS0.
+ }
+ simpl_sum_const; rewrite addnC.
rewrite -subnBA; last by rewrite -addnA leq_addr.
rewrite [a_fst + _]addnC -addnA [a_fst + _]addnC addnA.
rewrite -addnBA // subnn addn0.
@@ -1034,14 +1036,18 @@ Module InterferenceBoundEDFJitter.
apply leq_trans with (n := job_interference job_cost job_jitter sched j_i j_fst t1
(a_fst + J_k + R_k));
first by apply extend_sum; rewrite ?leqnn.
- by apply leq_sum; ins; rewrite leq_b1.
+ simpl_sum_const; rewrite -{1}[_ + _ + R_k](addKn t1) -addnBA //.
+ by apply job_interference_le_delta.
}
{
unfold interference_caused_by, job_interference.
rewrite -> big_cat_nat with (n := a_fst + J_k + R_k);
[simpl | by apply AFTERt1 | by apply ltnW].
- rewrite -[\sum_(_ <= _ < _) 1]addn0; apply leq_add;
- first by apply leq_sum; ins; apply leq_b1.
+ rewrite -[\sum_(_ <= _ < _) 1]addn0; apply leq_add.
+ {
+ simpl_sum_const; rewrite -{1}[_ + _ + R_k](addKn t1) -addnBA //.
+ by apply job_interference_le_delta.
+ }
apply leq_trans with (n := service_during sched j_fst (a_fst + J_k + R_k) t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
diff --git a/analysis/parallel/bertogna_edf_theory.v b/analysis/parallel/bertogna_edf_theory.v
index 198f4c427..e08261eff 100644
--- a/analysis/parallel/bertogna_edf_theory.v
+++ b/analysis/parallel/bertogna_edf_theory.v
@@ -290,9 +290,9 @@ Module ResponseTimeAnalysisEDF.
rewrite (bigD1_seq (job_task j_other)) /=; last by rewrite filter_uniq.
{
rewrite (eq_bigr (fun i => 0));
- last by intros i DIFF; rewrite /schedules_job_of_task SCHED;apply/eqP;rewrite eqb0 eq_sym.
+ last by intros i DIFF; rewrite /task_scheduled_on SCHED;apply/eqP;rewrite eqb0 eq_sym.
rewrite big_const_seq iter_addn mul0n 2!addn0; apply/eqP; rewrite eqb1.
- by unfold schedules_job_of_task; rewrite SCHED.
+ by unfold task_scheduled_on; rewrite SCHED.
}
rewrite mem_filter; apply/andP; split; last by apply FROMTS.
unfold jldp_can_interfere_with.
@@ -300,7 +300,7 @@ Module ResponseTimeAnalysisEDF.
assert (SCHED': scheduled sched j_other t).
{
unfold scheduled, scheduled_on.
- by apply/exists_inP; exists cpu; [by done | rewrite SCHED].
+ by apply/existsP; exists cpu; rewrite SCHED.
}
clear SCHED; rename SCHED' into SCHED.
move: (SCHED) => PENDING.
diff --git a/analysis/parallel/bertogna_fp_theory.v b/analysis/parallel/bertogna_fp_theory.v
index aefd03eee..a990c5ff6 100644
--- a/analysis/parallel/bertogna_fp_theory.v
+++ b/analysis/parallel/bertogna_fp_theory.v
@@ -9,7 +9,7 @@ Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisFP.
- Export Job SporadicTaskset Schedule Workload Interference InterferenceBoundFP
+ Export Job SporadicTaskset ScheduleOfSporadicTask Workload Interference InterferenceBoundFP
Platform PlatformFP Schedulability ResponseTime Priority SporadicTaskArrival WorkloadBound.
Section ResponseTimeBound.
@@ -281,23 +281,23 @@ Module ResponseTimeAnalysisFP.
rewrite (bigD1_seq (job_task j_other)) /=; last by rewrite filter_uniq.
{
rewrite (eq_bigr (fun i => 0));
- last by intros i DIFF; rewrite /schedules_job_of_task SCHED;apply/eqP;rewrite eqb0 eq_sym.
+ last by intros i DIFF; rewrite /task_scheduled_on SCHED;apply/eqP;rewrite eqb0 eq_sym.
rewrite big_const_seq iter_addn mul0n 2!addn0; apply/eqP; rewrite eqb1.
- by unfold schedules_job_of_task; rewrite SCHED.
+ by unfold task_scheduled_on; rewrite SCHED.
}
rewrite mem_filter; apply/andP; split; last by apply FROMTS.
unfold can_interfere_with_tsk, fp_can_interfere_with.
apply/andP; split.
{
rewrite -JOBtsk; apply FP with (t := t); first by done.
- by apply/exists_inP; exists cpu; last by apply/eqP.
+ by apply/existsP; exists cpu; apply/eqP.
}
{
apply/eqP; intro SAMEtsk.
assert (SCHED': scheduled sched j_other t).
{
unfold scheduled, scheduled_on.
- by apply/exists_inP; exists cpu; [by done | rewrite SCHED].
+ by apply/existsP; exists cpu; rewrite SCHED.
} clear SCHED; rename SCHED' into SCHED.
move: (SCHED) => PENDING.
apply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING; try (by done).
diff --git a/analysis/parallel/interference_bound_edf.v b/analysis/parallel/interference_bound_edf.v
index 7e512bc22..b7721cf74 100644
--- a/analysis/parallel/interference_bound_edf.v
+++ b/analysis/parallel/interference_bound_edf.v
@@ -240,9 +240,9 @@ Module InterferenceBoundEDF.
last by rewrite andFb (eq_bigr (fun x => 0));
first by rewrite big_const_seq iter_addn mul0n addn0.
rewrite andTb.
- destruct (schedules_job_of_task job_task sched tsk_k cpu t) eqn:SCHED;
+ destruct (task_scheduled_on job_task sched tsk_k cpu t) eqn:SCHED;
last by done.
- unfold schedules_job_of_task in *.
+ unfold task_scheduled_on in *.
destruct (sched cpu t) eqn:SOME; last by done.
rewrite big_mkcond /= (bigD1_seq j) /=; last by apply undup_uniq.
{
diff --git a/implementation/basic/schedule.v b/implementation/basic/schedule.v
index c0521c1ba..c8c28fb75 100644
--- a/implementation/basic/schedule.v
+++ b/implementation/basic/schedule.v
@@ -157,7 +157,7 @@ Module ConcreteScheduler.
nth_or_none (sorted_jobs t) cpu = Some j.
Proof.
intros j t SCHED.
- move: SCHED => /exists_inP [cpu INcpu /eqP SCHED]; exists cpu.
+ move: SCHED => /existsP [cpu /eqP SCHED]; exists cpu.
by apply scheduler_nth_or_none_mapping.
Qed.
@@ -181,7 +181,7 @@ Module ConcreteScheduler.
exists n; split; first by done.
rewrite leqNgt; apply/negP; red; intro LT.
apply NOTCOMP; clear NOTCOMP PENDING.
- apply/exists_inP; exists (Ordinal LT); [by done | apply/eqP].
+ apply/existsP; exists (Ordinal LT); apply/eqP.
unfold sorted_jobs in *; clear sorted_jobs.
unfold sched, scheduler, schedule_prefix in *; clear sched.
destruct t.
@@ -220,7 +220,7 @@ Module ConcreteScheduler.
Proof.
unfold jobs_must_arrive_to_execute.
intros j t SCHED.
- move: SCHED => /existsP [cpu /andP [INcpu /eqP SCHED]].
+ move: SCHED => /existsP [cpu /eqP SCHED].
unfold sched, scheduler, schedule_prefix in SCHED.
destruct t.
{
diff --git a/implementation/jitter/schedule.v b/implementation/jitter/schedule.v
index b81b5d2f3..cc099f56e 100644
--- a/implementation/jitter/schedule.v
+++ b/implementation/jitter/schedule.v
@@ -159,8 +159,7 @@ Module ConcreteScheduler.
exists (cpu: processor num_cpus),
nth_or_none (sorted_jobs t) cpu = Some j.
Proof.
- intros j t SCHED.
- move: SCHED => /exists_inP [cpu INcpu /eqP SCHED]; exists cpu.
+ move => j t /existsP [cpu /eqP SCHED]; exists cpu.
by apply scheduler_nth_or_none_mapping.
Qed.
@@ -186,7 +185,7 @@ Module ConcreteScheduler.
exists n; split; first by done.
rewrite leqNgt; apply/negP; red; intro LT.
apply NOTCOMP; clear NOTCOMP PENDING.
- apply/exists_inP; exists (Ordinal LT); [by done | apply/eqP].
+ apply/existsP; exists (Ordinal LT); apply/eqP.
unfold sorted_jobs in *; clear sorted_jobs.
unfold sched, scheduler, schedule_prefix in *; clear sched.
destruct t.
@@ -225,7 +224,7 @@ Module ConcreteScheduler.
Proof.
unfold jobs_must_arrive_to_execute.
intros j t SCHED.
- move: SCHED => /existsP [cpu /andP [INcpu /eqP SCHED]].
+ move: SCHED => /existsP [cpu /eqP SCHED].
unfold sched, scheduler, schedule_prefix in SCHED.
destruct t.
{
diff --git a/model/basic/interference.v b/model/basic/interference.v
index 7fb37147a..496342b63 100644
--- a/model/basic/interference.v
+++ b/model/basic/interference.v
@@ -73,7 +73,8 @@ Module Interference.
(* Let job_other be a job that interferes with j. *)
Variable job_other: JobIn arr_seq.
- (* The interference caused by job_other is defined as follows. *)
+ (* We define the total interference caused by job_other during [t1, t2) as the
+ cumulative service received by job_other while j is backlogged. *)
Definition job_interference (t1 t2: time) :=
\sum_(t1 <= t < t2)
\sum_(cpu < num_cpus)
@@ -81,65 +82,28 @@ Module Interference.
End JobInterference.
- Section JobInterferenceSequential.
-
- (* Let job_other be a job that interferes with j. *)
- Variable job_other: JobIn arr_seq.
-
- (* If jobs are sequential, the interference caused by job_other
- is defined as follows. *)
- Definition job_interference_sequential (t1 t2: time) :=
- \sum_(t1 <= t < t2)
- (job_is_backlogged t && scheduled sched job_other t).
-
- End JobInterferenceSequential.
-
Section TaskInterference.
(* In order to define task interference, consider any interfering task tsk_other. *)
Variable tsk_other: sporadic_task.
- Definition schedules_job_of_task (cpu: processor num_cpus) (t: time) :=
- match (sched cpu t) with
- | Some j' => job_task j' == tsk_other
- | None => false
- end.
-
- (* We know that tsk is scheduled at time t if there exists a processor
- scheduling a job of tsk. *)
- Definition task_is_scheduled (t: time) :=
- [exists cpu in processor num_cpus, schedules_job_of_task cpu t].
-
- (* We define the total interference caused by tsk during [t1, t2) as the
- cumulative time in which j is backlogged while tsk is scheduled. *)
+ (* We define the total interference caused by tsk during [t1, t2) as
+ the cumulative service received by tsk while j is backlogged. *)
Definition task_interference (t1 t2: time) :=
\sum_(t1 <= t < t2)
\sum_(cpu < num_cpus)
- (job_is_backlogged t && schedules_job_of_task cpu t).
+ (job_is_backlogged t &&
+ task_scheduled_on job_task sched tsk_other cpu t).
End TaskInterference.
- Section TaskInterferenceSequential.
-
- (* In order to define task interference, consider any interfering task tsk_other. *)
- Variable tsk_other: sporadic_task.
-
- (* If jobs are sequential, we define the total interference caused by
- tsk during [t1, t2) as the cumulative time in which j is backlogged
- while tsk is scheduled. *)
- Definition task_interference_sequential (t1 t2: time) :=
- \sum_(t1 <= t < t2)
- (job_is_backlogged t && task_is_scheduled tsk_other t).
-
- End TaskInterferenceSequential.
-
Section TaskInterferenceJobList.
Variable tsk_other: sporadic_task.
- Definition task_interference_sequential_joblist (t1 t2: time) :=
+ Definition task_interference_joblist (t1 t2: time) :=
\sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_other)
- job_interference_sequential j t1 t2.
+ job_interference j t1 t2.
End TaskInterferenceJobList.
@@ -156,29 +120,6 @@ Module Interference.
by rewrite big_const_nat iter_addn mul1n addn0 leqnn.
Qed.
- Lemma job_interference_seq_le_delta :
- forall j_other t1 delta,
- job_interference_sequential j_other t1 (t1 + delta) <= delta.
- Proof.
- unfold job_interference; intros j_other t1 delta.
- apply leq_trans with (n := \sum_(t1 <= t < t1 + delta) 1);
- first by apply leq_sum; ins; apply leq_b1.
- by rewrite big_const_nat iter_addn mul1n addn0 addKn leqnn.
- Qed.
-
- Lemma job_interference_seq_le_service :
- forall j_other t1 t2,
- job_interference_sequential j_other t1 t2 <= service_during sched j_other t1 t2.
- Proof.
- intros j_other t1 t2; unfold job_interference_sequential, service_during.
- apply leq_trans with (n := \sum_(t1 <= t < t2) scheduled sched j_other t);
- first by apply leq_sum; ins; destruct (job_is_backlogged i); rewrite ?andTb ?andFb.
- apply leq_sum; intros t _.
- destruct (scheduled sched j_other t) eqn:SCHED; last by done.
- move: SCHED => /existsP EX; destruct EX as [cpu]; move: H => /andP [IN SCHED].
- unfold service_at; rewrite (bigD1 cpu); last by done.
- by apply leq_trans with (n := 1).
- Qed.
Lemma job_interference_le_service :
forall j_other t1 t2,
@@ -192,23 +133,6 @@ Module Interference.
by destruct (scheduled_on sched j_other cpu t).
Qed.
- Lemma task_interference_seq_le_workload :
- forall tsk t1 t2,
- task_interference_sequential tsk t1 t2 <= workload job_task sched tsk t1 t2.
- Proof.
- unfold task_interference, workload; intros tsk t1 t2.
- apply leq_sum; intros t _.
- rewrite -mulnb -[\sum_(_ < _) _]mul1n.
- apply leq_mul; first by apply leq_b1.
- destruct (task_is_scheduled tsk t) eqn:SCHED; last by ins.
- unfold task_is_scheduled in SCHED.
- move: SCHED =>/exists_inP SCHED.
- destruct SCHED as [cpu _ HAScpu].
- rewrite -> bigD1 with (j := cpu); simpl; last by ins.
- apply ltn_addr; unfold service_of_task, schedules_job_of_task in *.
- by destruct (sched cpu t); [rewrite HAScpu | by done].
- Qed.
-
Lemma task_interference_le_workload :
forall tsk t1 t2,
task_interference tsk t1 t2 <= workload job_task sched tsk t1 t2.
@@ -217,135 +141,85 @@ Module Interference.
apply leq_sum; intros t _.
apply leq_sum; intros cpu _.
destruct (job_is_backlogged t); [rewrite andTb | by rewrite andFb].
- unfold schedules_job_of_task, service_of_task.
+ unfold task_scheduled_on, service_of_task.
by destruct (sched cpu t).
Qed.
End BasicLemmas.
- (* The sequential per-job interference bounds the actual interference. *)
- Section BoundUsingPerJobInterference.
+ Section InterferenceSequentialJobs.
- Lemma interference_le_interference_joblist :
- forall tsk t1 t2,
- task_interference_sequential tsk t1 t2 <=
- task_interference_sequential_joblist tsk t1 t2.
+ (* If jobs are sequential, ... *)
+ Hypothesis H_sequential_jobs: sequential_jobs sched.
+
+ (* ... then the interference incurred by a job in an interval
+ of length delta is at most delta. *)
+ Lemma job_interference_le_delta :
+ forall j_other t1 delta,
+ job_interference j_other t1 (t1 + delta) <= delta.
Proof.
- intros tsk t1 t2; unfold task_interference_sequential, task_interference_sequential_joblist, job_interference.
- rewrite [\sum_(j <- jobs_scheduled_between _ _ _ | _) _]exchange_big /=.
- rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
- apply leq_sum; intro t; rewrite andbT; intro LT.
- destruct (job_is_backlogged t && task_is_scheduled tsk t) eqn:BACK;
- last by done.
- move: BACK => /andP [BACK SCHED].
- move: SCHED => /existsP SCHED; destruct SCHED as [x IN]; move: IN => /andP [IN SCHED].
- unfold schedules_job_of_task in SCHED; desf.
- rename SCHED into EQtsk0, Heq into SCHED; move: EQtsk0 => /eqP EQtsk0.
- rewrite big_mkcond (bigD1_seq j0) /=; last by rewrite undup_uniq.
+ rename H_sequential_jobs into SEQ.
+ unfold job_interference, sequential_jobs in *.
+ intros j_other t1 delta.
+ apply leq_trans with (n := \sum_(t1 <= t < t1 + delta) 1);
+ last by rewrite big_const_nat iter_addn mul1n addn0 addKn leqnn.
+ apply leq_sum; intros t _.
+ destruct ([exists cpu, scheduled_on sched j_other cpu t]) eqn:EX.
{
- rewrite -addn1 addnC; apply leq_add; last by done.
- rewrite EQtsk0 BACK andTb.
- apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
- unfold scheduled, scheduled_on.
- by apply/exists_inP; exists x; [by done | by rewrite SCHED].
+ move: EX => /existsP [cpu SCHED].
+ rewrite (bigD1 cpu) // /=.
+ rewrite big_mkcond (eq_bigr (fun x => 0)) /=;
+ first by simpl_sum_const; rewrite leq_b1.
+ intros cpu' _; des_if_goal; last by done.
+ destruct (scheduled_on sched j_other cpu' t) eqn:SCHED'; last by rewrite andbF.
+ move: SCHED SCHED' => /eqP SCHED /eqP SCHED'.
+ by specialize (SEQ j_other t cpu cpu' SCHED SCHED'); rewrite SEQ in Heq.
}
{
- unfold jobs_scheduled_between.
- rewrite mem_undup.
- apply mem_bigcat_nat with (j := t); first by auto.
- unfold jobs_scheduled_at.
- apply mem_bigcat_ord with (j := x); first by apply ltn_ord.
- by unfold make_sequence; rewrite SCHED mem_seq1 eq_refl.
+ apply negbT in EX; rewrite negb_exists in EX.
+ move: EX => /forallP EX.
+ rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const.
+ by intros cpu _; specialize (EX cpu); apply negbTE in EX; rewrite EX andbF.
}
Qed.
-
- End BoundUsingPerJobInterference.
- Section CorrespondenceWithService.
-
- Variable t1 t2: time.
-
- (* Assume that jobs are sequential, ...*)
- Hypothesis H_sequential_jobs: sequential_jobs sched.
+ End InterferenceSequentialJobs.
- (* ..., and that jobs only execute after they arrived
- and no longer than their execution costs. *)
- Hypothesis H_jobs_must_arrive_to_execute:
- jobs_must_arrive_to_execute sched.
- Hypothesis H_completed_jobs_dont_execute:
- completed_jobs_dont_execute job_cost sched.
-
- (* If job j had already arrived at time t1 and did not yet
- complete by time t2, ...*)
- Hypothesis H_job_has_arrived :
- has_arrived j t1.
- Hypothesis H_job_is_not_complete :
- ~~ completed job_cost sched j t2.
-
- (* ... then the service received by j during [t1, t2) equals
- the cumulative time in which it did not incur interference. *)
- Lemma complement_of_interf_equals_service :
- \sum_(t1 <= t < t2) service_at sched j t =
- t2 - t1 - total_interference t1 t2.
+ (* The sequential per-job interference bounds the actual interference. *)
+ Section BoundUsingPerJobInterference.
+ Lemma interference_le_interference_joblist :
+ forall tsk t1 t2,
+ task_interference tsk t1 t2 <= task_interference_joblist tsk t1 t2.
Proof.
- unfold completed, total_interference, job_is_backlogged,
- backlogged, service_during, pending.
- rename H_sequential_jobs into NOPAR,
- H_jobs_must_arrive_to_execute into MUSTARRIVE,
- H_completed_jobs_dont_execute into COMP,
- H_job_is_not_complete into NOTCOMP.
-
- (* Reorder terms... *)
- apply/eqP; rewrite subh4; first last.
- {
- rewrite -[t2 - t1]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
- by apply leq_sum; ins; apply leq_b1.
- }
- {
- rewrite -[t2 - t1]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
- by apply leq_sum; ins; apply service_at_most_one.
- }
- apply/eqP.
-
- apply eq_trans with (y := \sum_(t1 <= t < t2)
- (1 - service_at sched j t));
- last first.
+ intros tsk t1 t2.
+ unfold task_interference, task_interference_joblist, job_interference, job_is_backlogged.
+ rewrite [\sum_(_ <- _ sched _ _ | _) _]exchange_big /=.
+ rewrite big_nat_cond [\sum_(_ <= _ < _ | true) _]big_nat_cond.
+ apply leq_sum; move => t /andP [LEt _].
+ rewrite exchange_big /=.
+ apply leq_sum; intros cpu _.
+ destruct (backlogged job_cost sched j t) eqn:BACK;
+ last by rewrite andFb (eq_bigr (fun x => 0));
+ first by rewrite big_const_seq iter_addn mul0n addn0.
+ rewrite andTb.
+ destruct (task_scheduled_on job_task sched tsk cpu t) eqn:SCHED; last by done.
+ unfold scheduled_on, task_scheduled_on in *.
+ destruct (sched cpu t) as [j' |] eqn:SOME; last by done.
+ rewrite big_mkcond /= (bigD1_seq j') /=; last by apply undup_uniq.
{
- apply/eqP; rewrite <- eqn_add2r with (p := \sum_(t1 <= t < t2)
- service_at sched j t).
- rewrite subh1; last first.
- rewrite -[t2 - t1]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
- by apply leq_sum; ins; apply service_at_most_one.
- rewrite -addnBA // subnn addn0 -big_split /=.
- rewrite -[t2 - t1]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
- apply/eqP; apply eq_bigr; ins; rewrite subh1;
- [by rewrite -addnBA // subnn addn0 | by apply service_at_most_one].
+ by rewrite SCHED eq_refl.
}
- rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
- apply eq_bigr; intro t; rewrite andbT; move => /andP [GEt1 LTt2].
- destruct (~~ scheduled sched j t) eqn:SCHED; last first.
{
- apply negbFE in SCHED; unfold scheduled in *.
- move: SCHED => /exists_inP SCHED; destruct SCHED as [cpu INcpu SCHEDcpu].
- rewrite andbF; apply/eqP.
- rewrite -(eqn_add2r (service_at sched j t)) add0n.
- rewrite subh1; last by apply service_at_most_one.
- rewrite -addnBA // subnn addn0.
- rewrite eqn_leq; apply/andP; split; first by apply service_at_most_one.
- unfold service_at; rewrite (bigD1 cpu) /=; last by apply SCHEDcpu.
- by apply leq_trans with (n := 1).
+ unfold jobs_scheduled_between.
+ rewrite mem_undup; apply mem_bigcat_nat with (j := t);
+ first by done.
+ apply mem_bigcat_ord with (j := cpu); first by apply ltn_ord.
+ by unfold make_sequence; rewrite SOME mem_seq1 eq_refl.
}
- rewrite not_scheduled_no_service in SCHED.
- move: SCHED => /eqP SCHED.
- rewrite SCHED subn0 andbT; apply/eqP; rewrite eqb1.
- apply/andP; split; first by apply leq_trans with (n := t1).
- apply/negP; unfold not; intro BUG.
- apply completion_monotonic with (t' := t2) in BUG; [ | by ins | by apply ltnW].
- by rewrite BUG in NOTCOMP.
Qed.
-
- End CorrespondenceWithService.
-
+
+ End BoundUsingPerJobInterference.
+
End InterferenceDefs.
End Interference.
\ No newline at end of file
diff --git a/model/basic/interference_edf.v b/model/basic/interference_edf.v
index 28b3f5403..fa427fa27 100644
--- a/model/basic/interference_edf.v
+++ b/model/basic/interference_edf.v
@@ -28,34 +28,7 @@ Module InterferenceEDF.
Hypothesis H_scheduler_uses_EDF:
enforces_JLDP_policy job_cost sched (EDF job_deadline).
- (* Under EDF scheduling, a job only causes sequential interference if its deadline
- is not larger than the deadline of the analyzed job. *)
- Lemma interference_seq_under_edf_implies_shorter_deadlines :
- forall (j j': JobIn arr_seq) t1 t2,
- job_interference_sequential job_cost sched j' j t1 t2 != 0 ->
- job_arrival j + job_deadline j <= job_arrival j' + job_deadline j'.
- Proof.
- rename H_scheduler_uses_EDF into PRIO.
- intros j j' t1 t2 INTERF.
- unfold job_interference_sequential in INTERF.
- destruct ([exists t': 'I_t2, (t' >= t1) && backlogged job_cost sched j' t' &&
- scheduled sched j t']) eqn:EX.
- {
- move: EX => /existsP EX; destruct EX as [t' EX];move: EX => /andP [/andP [LE BACK] SCHED].
- by eapply PRIO in SCHED; last by apply BACK.
- }
- {
- apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL.
- rewrite big_nat_cond (eq_bigr (fun x => 0)) in INTERF;
- first by rewrite -big_nat_cond big_const_nat iter_addn mul0n addn0 eq_refl in INTERF.
- intros i; rewrite andbT; move => /andP [GT LT].
- specialize (ALL (Ordinal LT)); simpl in ALL.
- rewrite -andbA negb_and -implybE in ALL; move: ALL => /implyP ALL.
- by specialize (ALL GT); apply/eqP; rewrite eqb0.
- }
- Qed.
-
- (* Under EDF scheduling, a job only causes (parallel) interference if its deadline
+ (* Under EDF scheduling, a job only causes interference if its deadline
is not larger than the deadline of the analyzed job. *)
Lemma interference_under_edf_implies_shorter_deadlines :
forall (j j': JobIn arr_seq) t1 t2,
@@ -67,11 +40,13 @@ Module InterferenceEDF.
unfold job_interference in INTERF.
destruct ([exists t': 'I_t2,
[exists cpu: processor num_cpus,
- (t' >= t1) && backlogged job_cost sched j' t' &&
- scheduled sched j t']]) eqn:EX.
+ (t' >= t1) &&
+ backlogged job_cost sched j' t' &&
+ scheduled_on sched j cpu t']]) eqn:EX.
{
move: EX => /existsP [t' /existsP [cpu /andP [/andP [LE BACK] SCHED]]].
- by eapply PRIO in SCHED; last by apply BACK.
+ apply PRIO with (t := t'); first by done.
+ by apply/existsP; exists cpu.
}
{
apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL.
@@ -86,13 +61,10 @@ Module InterferenceEDF.
intros cpu _; specialize (ALL cpu); simpl in ALL.
destruct (backlogged job_cost sched j' i); last by rewrite andFb.
rewrite GEi 2!andTb in ALL; rewrite andTb.
- rewrite negb_exists in ALL; move: ALL => /forallP NOTSCHED.
- specialize (NOTSCHED cpu); rewrite negb_and in NOTSCHED.
- move: NOTSCHED => /orP [BUG | NOTSCHED]; first by done.
- by apply/eqP; rewrite eqb0.
+ by apply negbTE in ALL; rewrite ALL.
}
Qed.
-
+
End Lemmas.
End InterferenceEDF.
\ No newline at end of file
diff --git a/model/basic/platform.v b/model/basic/platform.v
index de01fd8e3..b95db94ca 100644
--- a/model/basic/platform.v
+++ b/model/basic/platform.v
@@ -274,7 +274,7 @@ Module Platform.
apply count_exists; first by done.
{
intros cpu x1 x2 SCHED1 SCHED2.
- unfold schedules_job_of_task in *.
+ unfold task_scheduled_on in *.
destruct (sched cpu t); last by done.
move: SCHED1 SCHED2 => /eqP SCHED1 /eqP SCHED2.
by rewrite -SCHED1 -SCHED2.
@@ -300,9 +300,8 @@ Module Platform.
rewrite mem_scheduled_jobs_eq_scheduled in SCHED'.
unfold scheduled_task_other_than; apply/andP; split.
{
- move: SCHED' => /exists_inP [cpu INcpu /eqP SCHED'].
- apply/exists_inP; exists cpu; first by done.
- by unfold schedules_job_of_task; rewrite SCHED' eq_refl.
+ move: SCHED' => /existsP [cpu /eqP SCHED'].
+ by apply/existsP; exists cpu; rewrite /task_scheduled_on SCHED' eq_refl.
}
{
apply/eqP; red; intro SAMEtsk; symmetry in SAMEtsk.
diff --git a/model/basic/platform_fp.v b/model/basic/platform_fp.v
index b77b13f07..4b434d6cf 100644
--- a/model/basic/platform_fp.v
+++ b/model/basic/platform_fp.v
@@ -206,7 +206,7 @@ Module PlatformFP.
apply count_exists; first by done.
{
intros cpu x1 x2 SCHED1 SCHED2.
- unfold schedules_job_of_task in *.
+ unfold task_scheduled_on in *.
destruct (sched cpu t); last by done.
move: SCHED1 SCHED2 => /eqP SCHED1 /eqP SCHED2.
by rewrite -SCHED1 -SCHED2.
@@ -248,9 +248,8 @@ Module PlatformFP.
rewrite mem_scheduled_jobs_eq_scheduled in SCHED'.
apply/andP; split.
{
- move: SCHED' => /exists_inP [cpu INcpu /eqP SCHED'].
- apply/exists_inP; exists cpu; first by done.
- by unfold schedules_job_of_task; rewrite SCHED' eq_refl.
+ move: SCHED' => /existsP [cpu /eqP SCHED'].
+ by apply/existsP; exists cpu; rewrite /task_scheduled_on SCHED' eq_refl.
}
apply/andP; split; first by rewrite -JOBtsk; apply PRIO with (t := t).
{
diff --git a/model/basic/schedule.v b/model/basic/schedule.v
index 5e716d823..5246d4155 100644
--- a/model/basic/schedule.v
+++ b/model/basic/schedule.v
@@ -49,7 +49,7 @@ Module Schedule.
(* A job j is scheduled at time t iff there exists a cpu where it is mapped.*)
Definition scheduled (t: time) :=
- [exists cpu in 'I_(num_cpus), scheduled_on cpu t].
+ [exists cpu, scheduled_on cpu t].
(* A processor cpu is idle at time t if it doesn't contain any jobs. *)
Definition is_idle (cpu: 'I_(num_cpus)) (t: time) :=
@@ -150,21 +150,19 @@ Module Schedule.
unfold scheduled, service_at, scheduled_on; intros t; apply/idP/idP.
{
intros NOTSCHED.
- rewrite negb_exists_in in NOTSCHED.
- move: NOTSCHED => /forall_inP NOTSCHED.
+ rewrite negb_exists in NOTSCHED.
+ move: NOTSCHED => /forallP NOTSCHED.
rewrite big_seq_cond.
rewrite -> eq_bigr with (F2 := fun i => 0);
first by rewrite big_const_seq iter_addn mul0n addn0.
- move => cpu /andP [_ SCHED].
- exploit (NOTSCHED cpu); [by ins | clear NOTSCHED].
- by move: SCHED => /eqP SCHED; rewrite SCHED eq_refl.
+ move => cpu /andP [_ /eqP SCHED].
+ by specialize (NOTSCHED cpu); rewrite SCHED eq_refl in NOTSCHED.
}
{
intros NOSERV; rewrite big_mkcond -sum_nat_eq0_nat in NOSERV.
move: NOSERV => /allP ALL.
- rewrite negb_exists; apply/forall_inP.
- move => x /andP [IN SCHED].
- by exploit (ALL x); [by apply mem_index_enum | by desf].
+ rewrite negb_exists; apply/forallP; intros cpu.
+ exploit (ALL cpu); [by apply mem_index_enum | by desf].
}
Qed.
@@ -224,25 +222,21 @@ Module Schedule.
unfold service_at, sequential_jobs in *; ins.
destruct (scheduled sched j t) eqn:SCHED; unfold scheduled in SCHED.
{
- move: SCHED => /exists_inP SCHED; des.
- move: H2 => /eqP SCHED.
- rewrite -big_filter.
- rewrite (bigD1_seq x);
- [simpl | | by rewrite filter_index_enum enum_uniq]; last first.
- {
- by rewrite mem_filter; apply/andP; split;
- [by apply/eqP | by rewrite mem_index_enum].
- }
+ move: SCHED => /existsP [cpu SCHED]; des.
+ rewrite -big_filter (bigD1_seq cpu);
+ [simpl | | by rewrite filter_index_enum enum_uniq];
+ last by rewrite mem_filter; apply/andP; split.
rewrite -big_filter -filter_predI big_filter.
rewrite -> eq_bigr with (F2 := fun cpu => 0);
first by rewrite /= big_const_seq iter_addn mul0n 2!addn0.
- intro i; move => /andP [/eqP NEQ /eqP SCHEDi].
- by apply H_sequential_jobs with (cpu1 := x) in SCHEDi; subst.
+ intro cpu'; move => /andP [/eqP NEQ /eqP SCHED'].
+ exfalso; apply NEQ.
+ by apply H_sequential_jobs with (j := j) (t := t); last by apply/eqP.
}
{
- apply negbT in SCHED; rewrite negb_exists_in in SCHED.
- move: SCHED => /forall_inP SCHED.
- by rewrite big_pred0; red; ins; apply negbTE, SCHED.
+ apply negbT in SCHED; rewrite negb_exists in SCHED.
+ move: SCHED => /forallP SCHED.
+ rewrite big_pred0; red; ins; apply negbTE, SCHED.
}
Qed.
@@ -339,11 +333,9 @@ Module Schedule.
(b := has_arrived j t) in ARR;
last by rewrite -ltnNge.
apply/eqP; rewrite -leqn0; unfold service_at.
- rewrite -> eq_bigr with (F2 := fun cpu => 0);
- first by rewrite big_const_seq iter_addn mul0n addn0.
- intros i SCHED; move: ARR; rewrite negb_exists_in; move => /forall_inP ARR.
- unfold scheduled_on in *.
- by exploit (ARR i); [by ins | ins]; destruct (sched i t == Some j).
+ rewrite big_pred0 //; red.
+ intros cpu; apply negbTE.
+ by move: ARR; rewrite negb_exists; move => /forallP ARR; apply ARR.
Qed.
(* The same applies for the cumulative service received by job j. *)
@@ -434,12 +426,12 @@ Module Schedule.
{
intros IN.
apply mem_bigcat_ord_exists in IN; des.
- apply/exists_inP; exists i; first by done.
+ apply/existsP; exists i.
destruct (sched i t); last by done.
by rewrite mem_seq1 in IN; move: IN => /eqP IN; subst.
}
{
- move => /exists_inP EX; destruct EX as [i IN SCHED].
+ move => /existsP EX; destruct EX as [i SCHED].
apply mem_bigcat_ord with (j := i); first by apply ltn_ord.
by move: SCHED => /eqP SCHED; rewrite SCHED /= mem_seq1 eq_refl.
}
@@ -524,7 +516,8 @@ End Schedule.
(* Specific properties of a schedule of sporadic jobs. *)
Module ScheduleOfSporadicTask.
- Import SporadicTask Job Schedule.
+ Import SporadicTask Job.
+ Export Schedule.
Section ScheduledJobs.
@@ -540,11 +533,21 @@ Module ScheduleOfSporadicTask.
(* Given a task tsk, ...*)
Variable tsk: sporadic_task.
- (* ..., we define the list of jobs scheduled during [t1, t2). *)
+ (* ..., we we can state that tsk is scheduled on cpu at time t as follows. *)
+ Definition task_scheduled_on (cpu: processor num_cpus) (t: time) :=
+ if (sched cpu t) is Some j then
+ (job_task j == tsk)
+ else false.
+
+ (* Likewise, we can state that tsk is scheduled on some processor. *)
+ Definition task_is_scheduled (t: time) :=
+ [exists cpu, task_scheduled_on cpu t].
+
+ (* We also define the list of jobs scheduled during [t1, t2). *)
Definition jobs_of_task_scheduled_between (t1 t2: time) :=
filter (fun (j: JobIn arr_seq) => job_task j == tsk)
(jobs_scheduled_between sched t1 t2).
-
+
End ScheduledJobs.
Section ScheduleProperties.
diff --git a/model/jitter/interference.v b/model/jitter/interference.v
index 6e44fbbb1..583240d1b 100644
--- a/model/jitter/interference.v
+++ b/model/jitter/interference.v
@@ -7,7 +7,7 @@ Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Interference.
- Import ScheduleWithJitter ScheduleOfSporadicTask Priority Workload.
+ Import ScheduleOfSporadicTaskWithJitter Priority Workload.
(* We import some of the basic definitions, but we need to re-define almost everything
since the definition of backlogged (and thus the definition of interference)
@@ -51,10 +51,13 @@ Module Interference.
(* Let job_other be a job that interferes with j. *)
Variable job_other: JobIn arr_seq.
- (* The interference caused by job_other is defined as follows. *)
+ (* We define the total interference caused by job_other during [t1, t2) as the
+ cumulative service received by job_other while j is backlogged. *)
Definition job_interference (t1 t2: time) :=
\sum_(t1 <= t < t2)
- (job_is_backlogged t && scheduled sched job_other t).
+ \sum_(cpu < num_cpus)
+ (job_is_backlogged t &&
+ scheduled_on sched job_other cpu t).
End JobInterference.
@@ -63,22 +66,13 @@ Module Interference.
(* In order to define task interference, consider any interfering task tsk_other. *)
Variable tsk_other: sporadic_task.
- Definition schedules_job_of_tsk (cpu: processor num_cpus) (t: time) :=
- match (sched cpu t) with
- | Some j' => job_task j' == tsk_other
- | None => false
- end.
-
- (* We know that tsk is scheduled at time t if there exists a processor
- scheduling a job of tsk. *)
- Definition task_is_scheduled (t: time) :=
- [exists cpu in processor num_cpus, schedules_job_of_tsk cpu t].
-
(* We define the total interference caused by tsk during [t1, t2) as
- the cumulative time in which j is backlogged while tsk is scheduled. *)
+ the cumulative service received by tsk while j is backlogged. *)
Definition task_interference (t1 t2: time) :=
\sum_(t1 <= t < t2)
- (job_is_backlogged t && task_is_scheduled t).
+ \sum_(cpu < num_cpus)
+ (job_is_backlogged t &&
+ task_scheduled_on job_task sched tsk_other cpu t).
End TaskInterference.
@@ -105,28 +99,16 @@ Module Interference.
by rewrite big_const_nat iter_addn mul1n addn0 leqnn.
Qed.
- Lemma job_interference_le_delta :
- forall j_other t1 delta,
- job_interference j_other t1 (t1 + delta) <= delta.
- Proof.
- unfold job_interference; intros j_other t1 delta.
- apply leq_trans with (n := \sum_(t1 <= t < t1 + delta) 1);
- first by apply leq_sum; ins; apply leq_b1.
- by rewrite big_const_nat iter_addn mul1n addn0 addKn leqnn.
- Qed.
-
Lemma job_interference_le_service :
forall j_other t1 t2,
job_interference j_other t1 t2 <= service_during sched j_other t1 t2.
Proof.
intros j_other t1 t2; unfold job_interference, service_during.
- apply leq_trans with (n := \sum_(t1 <= t < t2) scheduled sched j_other t);
- first by apply leq_sum; ins; destruct (job_is_backlogged i); rewrite ?andTb ?andFb.
apply leq_sum; intros t _.
- destruct (scheduled sched j_other t) eqn:SCHED; last by done.
- move: SCHED => /existsP EX; destruct EX as [cpu]; move: H => /andP [IN SCHED].
- unfold service_at; rewrite (bigD1 cpu); last by done.
- by apply leq_trans with (n := 1).
+ unfold service_at; rewrite [\sum_(_ < _ | scheduled_on _ _ _ _)_]big_mkcond.
+ apply leq_sum; intros cpu _.
+ destruct (job_is_backlogged t); [rewrite andTb | by rewrite andFb].
+ by destruct (scheduled_on sched j_other cpu t).
Qed.
Lemma task_interference_le_workload :
@@ -135,206 +117,88 @@ Module Interference.
Proof.
unfold task_interference, workload; intros tsk t1 t2.
apply leq_sum; intros t _.
- rewrite -mulnb -[\sum_(_ < _) _]mul1n.
- apply leq_mul; first by apply leq_b1.
- destruct (task_is_scheduled tsk t) eqn:SCHED; last by ins.
- unfold task_is_scheduled in SCHED.
- move: SCHED =>/exists_inP SCHED.
- destruct SCHED as [cpu _ HAScpu].
- rewrite -> bigD1 with (j := cpu); simpl; last by ins.
- apply ltn_addr; unfold service_of_task, schedules_job_of_tsk in *.
- by destruct (sched cpu t); [rewrite HAScpu | by done].
+ apply leq_sum; intros cpu _.
+ destruct (job_is_backlogged t); [rewrite andTb | by rewrite andFb].
+ unfold task_scheduled_on, service_of_task.
+ by destruct (sched cpu t).
Qed.
End BasicLemmas.
- (* If we assume no intra-task parallelism, the two definitions
- of interference are the same. *)
- Section EquivalenceWithPerJobInterference.
+ Section InterferenceSequentialJobs.
- Hypothesis H_no_intratask_parallelism:
- jobs_of_same_task_dont_execute_in_parallel job_task sched.
-
- Lemma interference_eq_interference_joblist :
- forall tsk t1 t2,
- task_interference tsk t1 t2 = task_interference_joblist tsk t1 t2.
+ (* If jobs are sequential, ... *)
+ Hypothesis H_sequential_jobs: sequential_jobs sched.
+
+ (* ... then the interference incurred by a job in an interval
+ of length delta is at most delta. *)
+ Lemma job_interference_le_delta :
+ forall j_other t1 delta,
+ job_interference j_other t1 (t1 + delta) <= delta.
Proof.
- intros tsk t1 t2; unfold task_interference, task_interference_joblist, job_interference.
- rewrite [\sum_(j <- jobs_scheduled_between _ _ _ | _) _]exchange_big /=.
- apply eq_big_nat; unfold service_at; intros t LEt.
- destruct (job_is_backlogged t && task_is_scheduled tsk t) eqn:BACK.
+ rename H_sequential_jobs into SEQ.
+ unfold job_interference, sequential_jobs in *.
+ intros j_other t1 delta.
+ apply leq_trans with (n := \sum_(t1 <= t < t1 + delta) 1);
+ last by rewrite big_const_nat iter_addn mul1n addn0 addKn leqnn.
+ apply leq_sum; intros t _.
+ destruct ([exists cpu, scheduled_on sched j_other cpu t]) eqn:EX.
{
- move: BACK => /andP [BACK SCHED]; symmetry.
- move: SCHED => /existsP SCHED; destruct SCHED as [x IN]; move: IN => /andP [IN SCHED].
- unfold schedules_job_of_tsk in SCHED; desf.
- rename SCHED into EQtsk0, Heq into SCHED; move: EQtsk0 => /eqP EQtsk0.
- assert (SCHEDULED: scheduled sched j0 t).
- {
- unfold scheduled, scheduled_on.
- apply/existsP; exists x; apply/andP; split; [by done | by rewrite SCHED eq_refl].
- }
- rewrite big_mkcond (bigD1_seq j0) /=; last by rewrite undup_uniq.
- {
- rewrite EQtsk0 BACK SCHEDULED andbT big_mkcond.
- rewrite (eq_bigr (fun x => 0));
- first by rewrite big_const_seq iter_addn mul0n addn0 addn0.
- intros j1 _; desf; try by done.
- apply/eqP; rewrite eqb0; apply/negP; unfold not; intro SCHEDULED'.
- exploit (H_no_intratask_parallelism j0 j1 t); try by eauto.
- }
- {
- rewrite mem_undup.
- apply mem_bigcat_nat with (j := t); first by auto.
- apply mem_bigcat_ord with (j := x); first by apply ltn_ord.
- by rewrite SCHED mem_seq1.
- }
+ move: EX => /existsP [cpu SCHED].
+ rewrite (bigD1 cpu) // /=.
+ rewrite big_mkcond (eq_bigr (fun x => 0)) /=;
+ first by simpl_sum_const; rewrite leq_b1.
+ intros cpu' _; des_if_goal; last by done.
+ destruct (scheduled_on sched j_other cpu' t) eqn:SCHED'; last by rewrite andbF.
+ move: SCHED SCHED' => /eqP SCHED /eqP SCHED'.
+ by specialize (SEQ j_other t cpu cpu' SCHED SCHED'); rewrite SEQ in Heq.
}
{
- rewrite big_mkcond (eq_bigr (fun x => 0));
- first by rewrite big_const_seq iter_addn mul0n addn0.
- intros i _; desf; rewrite // ?BACK ?andFb //.
- unfold task_is_scheduled in BACK.
- apply negbT in BACK; rewrite negb_exists in BACK.
- move: BACK => /forallP BACK.
- assert (NOTSCHED: scheduled sched i t = false).
- {
- apply negbTE; rewrite negb_exists; apply/forallP.
- intros x; rewrite negb_and.
- specialize (BACK x); rewrite negb_and in BACK; ins.
- unfold schedules_job_of_tsk in BACK; unfold scheduled_on.
- destruct (sched x t) eqn:SCHED; last by ins.
- apply/negP; unfold not; move => /eqP BUG; inversion BUG; subst.
- by move: BACK => /negP BACK; apply BACK.
- }
- by rewrite NOTSCHED andbF.
+ apply negbT in EX; rewrite negb_exists in EX.
+ move: EX => /forallP EX.
+ rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const.
+ by intros cpu _; specialize (EX cpu); apply negbTE in EX; rewrite EX andbF.
}
Qed.
- End EquivalenceWithPerJobInterference.
+ End InterferenceSequentialJobs.
- (* If we don't assume intra-task parallelism, the per-job interference
- bounds the actual interference. *)
+ (* The sequential per-job interference bounds the actual interference. *)
Section BoundUsingPerJobInterference.
-
+
Lemma interference_le_interference_joblist :
forall tsk t1 t2,
task_interference tsk t1 t2 <= task_interference_joblist tsk t1 t2.
Proof.
- intros tsk t1 t2; unfold task_interference, task_interference_joblist, job_interference.
- rewrite [\sum_(j <- jobs_scheduled_between _ _ _ | _) _]exchange_big /=.
- rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
- apply leq_sum; intro t; rewrite andbT; intro LT.
- destruct (job_is_backlogged t && task_is_scheduled tsk t) eqn:BACK;
- last by done.
- move: BACK => /andP [BACK SCHED].
- move: SCHED => /existsP SCHED; destruct SCHED as [x IN]; move: IN => /andP [IN SCHED].
- unfold schedules_job_of_tsk in SCHED; desf.
- rename SCHED into EQtsk0, Heq into SCHED; move: EQtsk0 => /eqP EQtsk0.
- rewrite big_mkcond (bigD1_seq j0) /=; last by rewrite undup_uniq.
+ intros tsk t1 t2.
+ unfold task_interference, task_interference_joblist, job_interference, job_is_backlogged.
+ rewrite [\sum_(_ <- _ sched _ _ | _) _]exchange_big /=.
+ rewrite big_nat_cond [\sum_(_ <= _ < _ | true) _]big_nat_cond.
+ apply leq_sum; move => t /andP [LEt _].
+ rewrite exchange_big /=.
+ apply leq_sum; intros cpu _.
+ destruct (backlogged job_cost job_jitter sched j t) eqn:BACK;
+ last by rewrite andFb (eq_bigr (fun x => 0));
+ first by rewrite big_const_seq iter_addn mul0n addn0.
+ rewrite andTb.
+ destruct (task_scheduled_on job_task sched tsk cpu t) eqn:SCHED; last by done.
+ unfold scheduled_on, task_scheduled_on in *.
+ destruct (sched cpu t) as [j' |] eqn:SOME; last by done.
+ rewrite big_mkcond /= (bigD1_seq j') /=; last by apply undup_uniq.
{
- rewrite -addn1 addnC; apply leq_add; last by done.
- rewrite EQtsk0 BACK andTb.
- apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
- unfold scheduled, scheduled_on.
- by apply/exists_inP; exists x; [by done | by rewrite SCHED].
+ by rewrite SCHED eq_refl.
}
{
unfold jobs_scheduled_between.
- rewrite mem_undup.
- apply mem_bigcat_nat with (j := t); first by auto.
- unfold jobs_scheduled_at.
- apply mem_bigcat_ord with (j := x); first by apply ltn_ord.
- by unfold make_sequence; rewrite SCHED mem_seq1.
+ rewrite mem_undup; apply mem_bigcat_nat with (j := t);
+ first by done.
+ apply mem_bigcat_ord with (j := cpu); first by apply ltn_ord.
+ by unfold make_sequence; rewrite SOME mem_seq1 eq_refl.
}
Qed.
End BoundUsingPerJobInterference.
-
- Section CorrespondenceWithService.
-
- Variable t1 t2: time.
-
- (* Assume that jobs are sequential, ...*)
- Hypothesis H_sequential_jobs: sequential_jobs sched.
-
- (* ..., and that jobs only execute after the jitter
- and no longer than their execution costs. *)
- Hypothesis H_jobs_execute_after_jitter:
- jobs_execute_after_jitter job_jitter sched.
- Hypothesis H_completed_jobs_dont_execute:
- completed_jobs_dont_execute job_cost sched.
-
- Let j_jitter_has_passed := jitter_has_passed job_jitter j.
-
- (* If job j had actually by time t1 and did not yet
- complete by time t2, ...*)
- Hypothesis H_job_has_actually_arrived : j_jitter_has_passed t1.
- Hypothesis H_job_is_not_complete : ~~ completed job_cost sched j t2.
-
- (* then the service received by j during [t1, t2) equals
- the cumulative time in which it did not incur interference. *)
- Lemma complement_of_interf_equals_service :
- \sum_(t1 <= t < t2) service_at sched j t =
- t2 - t1 - total_interference t1 t2.
- Proof.
- unfold completed, total_interference, job_is_backlogged,
- backlogged, service_during, pending.
- rename H_sequential_jobs into NOPAR,
- H_jobs_execute_after_jitter into JITTER,
- H_completed_jobs_dont_execute into COMP,
- H_job_is_not_complete into NOTCOMP.
-
- (* Reorder terms... *)
- apply/eqP; rewrite subh4; first last.
- {
- rewrite -[t2 - t1]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
- by apply leq_sum; ins; apply leq_b1.
- }
- {
- rewrite -[t2 - t1]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
- by apply leq_sum; ins; apply service_at_most_one.
- }
- apply/eqP.
-
- apply eq_trans with (y := \sum_(t1 <= t < t2)
- (1 - service_at sched j t));
- last first.
- {
- apply/eqP; rewrite <- eqn_add2r with (p := \sum_(t1 <= t < t2)
- service_at sched j t).
- rewrite subh1; last first.
- rewrite -[t2 - t1]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
- by apply leq_sum; ins; apply service_at_most_one.
- rewrite -addnBA // subnn addn0 -big_split /=.
- rewrite -[t2 - t1]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
- apply/eqP; apply eq_bigr; ins; rewrite subh1;
- [by rewrite -addnBA // subnn addn0 | by apply service_at_most_one].
- }
- rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
- apply eq_bigr; intro t; rewrite andbT; move => /andP [GEt1 LTt2].
- destruct (~~ scheduled sched j t) eqn:SCHED; last first.
- {
- apply negbFE in SCHED; unfold scheduled in *.
- move: SCHED => /exists_inP SCHED; destruct SCHED as [cpu INcpu SCHEDcpu].
- rewrite andbF; apply/eqP.
- rewrite -(eqn_add2r (service_at sched j t)) add0n.
- rewrite subh1; last by apply service_at_most_one.
- rewrite -addnBA // subnn addn0.
- rewrite eqn_leq; apply/andP; split; first by apply service_at_most_one.
- unfold service_at; rewrite (bigD1 cpu) /=; last by apply SCHEDcpu.
- by apply leq_trans with (n := 1).
- }
- rewrite not_scheduled_no_service in SCHED.
- move: SCHED => /eqP SCHED.
- rewrite SCHED subn0 andbT; apply/eqP; rewrite eqb1.
- apply/andP; split; first by apply leq_trans with (n := t1).
- apply/negP; unfold not; intro BUG.
- apply completion_monotonic with (t' := t2) in BUG; [ | by ins | by apply ltnW].
- by rewrite BUG in NOTCOMP.
- Qed.
-
- End CorrespondenceWithService.
-
+
End InterferenceDefs.
End Interference.
\ No newline at end of file
diff --git a/model/jitter/interference_edf.v b/model/jitter/interference_edf.v
index e7352ba70..1277e3ee0 100644
--- a/model/jitter/interference_edf.v
+++ b/model/jitter/interference_edf.v
@@ -39,20 +39,30 @@ Module InterferenceEDF.
rename H_scheduler_uses_EDF into PRIO.
intros j j' t1 t2 INTERF.
unfold job_interference in INTERF.
- destruct ([exists t': 'I_t2, (t' >= t1) && backlogged job_cost job_jitter sched j' t' &&
- scheduled sched j t']) eqn:EX.
+ destruct ([exists t': 'I_t2,
+ [exists cpu: processor num_cpus,
+ (t' >= t1) &&
+ backlogged job_cost job_jitter sched j' t' &&
+ scheduled_on sched j cpu t']]) eqn:EX.
{
- move: EX => /existsP EX; destruct EX as [t' EX];move: EX => /andP [/andP [LE BACK] SCHED].
- by eapply PRIO in SCHED; last by apply BACK.
+ move: EX => /existsP [t' /existsP [cpu /andP [/andP [LE BACK] SCHED]]].
+ apply PRIO with (t := t'); first by done.
+ by apply/existsP; exists cpu.
}
{
- apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL.
+ apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL.
rewrite big_nat_cond (eq_bigr (fun x => 0)) in INTERF;
first by rewrite -big_nat_cond big_const_nat iter_addn mul0n addn0 eq_refl in INTERF.
- intros i; rewrite andbT; move => /andP [GT LT].
- specialize (ALL (Ordinal LT)); simpl in ALL.
- rewrite -andbA negb_and -implybE in ALL; move: ALL => /implyP ALL.
- by specialize (ALL GT); apply/eqP; rewrite eqb0.
+ move => i /andP [/andP [GEi LTi] _].
+ specialize (ALL (Ordinal LTi)).
+ rewrite negb_exists in ALL.
+ move: ALL => /forallP ALL.
+ rewrite (eq_bigr (fun x => 0));
+ first by rewrite big_const_ord iter_addn mul0n addn0.
+ intros cpu _; specialize (ALL cpu); simpl in ALL.
+ destruct (backlogged job_cost job_jitter sched j' i); last by rewrite andFb.
+ rewrite GEi 2!andTb in ALL; rewrite andTb.
+ by apply negbTE in ALL; rewrite ALL.
}
Qed.
diff --git a/model/jitter/platform.v b/model/jitter/platform.v
index 3cb0aba12..e02219128 100644
--- a/model/jitter/platform.v
+++ b/model/jitter/platform.v
@@ -6,7 +6,7 @@ Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module Platform.
- Import Job SporadicTaskset ScheduleWithJitter ScheduleOfSporadicTask SporadicTaskset SporadicTaskArrival Interference Priority.
+ Import Job SporadicTaskset ScheduleOfSporadicTaskWithJitter SporadicTaskset SporadicTaskArrival Interference Priority.
Section SchedulingInvariants.
@@ -281,7 +281,6 @@ Module Platform.
apply count_exists; first by done.
{
intros cpu x1 x2 SCHED1 SCHED2.
- unfold schedules_job_of_tsk in *.
destruct (sched cpu t); last by done.
move: SCHED1 SCHED2 => /eqP SCHED1 /eqP SCHED2.
by rewrite -SCHED1 -SCHED2.
@@ -309,9 +308,8 @@ Module Platform.
rewrite mem_scheduled_jobs_eq_scheduled in SCHED'.
unfold scheduled_task_other_than; apply/andP; split.
{
- move: SCHED' => /exists_inP [cpu INcpu /eqP SCHED'].
- apply/exists_inP; exists cpu; first by done.
- by unfold schedules_job_of_tsk; rewrite SCHED' eq_refl.
+ move: SCHED' => /existsP [cpu /eqP SCHED'].
+ by apply/existsP; exists cpu; rewrite /task_scheduled_on SCHED' eq_refl.
}
{
apply/eqP; red; intro SAMEtsk; symmetry in SAMEtsk.
diff --git a/model/jitter/platform_fp.v b/model/jitter/platform_fp.v
index d35884fd4..1df61ffee 100644
--- a/model/jitter/platform_fp.v
+++ b/model/jitter/platform_fp.v
@@ -7,7 +7,7 @@ Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module PlatformFP.
- Import Job SporadicTaskset ScheduleWithJitter ScheduleOfSporadicTask SporadicTaskset
+ Import Job SporadicTaskset ScheduleOfSporadicTaskWithJitter SporadicTaskset
SporadicTaskArrival Interference Priority Platform.
Section Lemmas.
@@ -217,7 +217,6 @@ Module PlatformFP.
apply count_exists; first by done.
{
intros cpu x1 x2 SCHED1 SCHED2.
- unfold schedules_job_of_tsk in *.
destruct (sched cpu t); last by done.
move: SCHED1 SCHED2 => /eqP SCHED1 /eqP SCHED2.
by rewrite -SCHED1 -SCHED2.
@@ -261,9 +260,8 @@ Module PlatformFP.
rewrite mem_scheduled_jobs_eq_scheduled in SCHED'.
apply/andP; split.
{
- move: SCHED' => /exists_inP [cpu INcpu /eqP SCHED'].
- apply/exists_inP; exists cpu; first by done.
- by unfold schedules_job_of_tsk; rewrite SCHED' eq_refl.
+ move: SCHED' => /existsP [cpu /eqP SCHED'].
+ by apply/existsP; exists cpu; rewrite /task_scheduled_on SCHED' eq_refl.
}
apply/andP; split; first by rewrite -JOBtsk; apply PRIO with (t := t).
{
diff --git a/model/jitter/schedule.v b/model/jitter/schedule.v
index dd8ab5827..f75c7a62e 100644
--- a/model/jitter/schedule.v
+++ b/model/jitter/schedule.v
@@ -146,10 +146,110 @@ Module ScheduleWithJitter.
End ScheduleWithJitter.
-Module ScheduleOfSporadicTask.
+(* Specific properties of a schedule of sporadic jobs. *)
+Module ScheduleOfSporadicTaskWithJitter.
+
+ Import SporadicTask Job.
+ Export ScheduleWithJitter.
+
+ Section ScheduledJobs.
+
+ Context {sporadic_task: eqType}.
+ Context {Job: eqType}.
+ Variable job_task: Job -> sporadic_task.
+
+ (* Consider any schedule. *)
+ Context {arr_seq: arrival_sequence Job}.
+ Context {num_cpus: nat}.
+ Variable sched: schedule num_cpus arr_seq.
+
+ (* Given a task tsk, ...*)
+ Variable tsk: sporadic_task.
+
+ (* ..., we we can state that tsk is scheduled on cpu at time t as follows. *)
+ Definition task_scheduled_on (cpu: processor num_cpus) (t: time) :=
+ if (sched cpu t) is Some j then
+ (job_task j == tsk)
+ else false.
+
+ (* Likewise, we can state that tsk is scheduled on some processor. *)
+ Definition task_is_scheduled (t: time) :=
+ [exists cpu, task_scheduled_on cpu t].
+
+ (* We also define the list of jobs scheduled during [t1, t2). *)
+ Definition jobs_of_task_scheduled_between (t1 t2: time) :=
+ filter (fun (j: JobIn arr_seq) => job_task j == tsk)
+ (jobs_scheduled_between sched t1 t2).
+
+ End ScheduledJobs.
- (* The model for sporadic tasks can be safely imported. *)
- Require Import rt.model.basic.schedule.
- Export ScheduleOfSporadicTask.
+ Section ScheduleProperties.
+
+ Context {sporadic_task: eqType}.
+ Context {Job: eqType}.
+ Variable job_cost: Job -> time.
+ Variable job_jitter: Job -> time.
+ Variable job_task: Job -> sporadic_task.
+
+ (* Consider any schedule. *)
+ Context {arr_seq: arrival_sequence Job}.
+ Context {num_cpus: nat}.
+ Variable sched: schedule num_cpus arr_seq.
+
+ (* Next we define intra-task parallelism, ... *)
+ Definition jobs_of_same_task_dont_execute_in_parallel :=
+ forall (j j': JobIn arr_seq) t,
+ job_task j = job_task j' ->
+ scheduled sched j t -> scheduled sched j' t -> j = j'.
+
+ (* ... and task precedence constraints. *)
+ Definition task_precedence_constraints :=
+ forall (j j': JobIn arr_seq) t,
+ job_task j = job_task j' ->
+ job_arrival j < job_arrival j' ->
+ pending job_cost job_jitter sched j t -> ~~ scheduled sched j' t.
+
+ End ScheduleProperties.
+
+ Section BasicLemmas.
+
+ (* Assume the job cost and task are known. *)
+ Context {sporadic_task: eqType}.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+
+ Context {Job: eqType}.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
+ Variable job_task: Job -> sporadic_task.
-End ScheduleOfSporadicTask.
\ No newline at end of file
+ (* Then, in a valid schedule of sporadic tasks ...*)
+ Context {arr_seq: arrival_sequence Job}.
+ Context {num_cpus: nat}.
+ Variable sched: schedule num_cpus arr_seq.
+
+ (* ...such that jobs do not execute after completion, ...*)
+ Hypothesis jobs_dont_execute_after_completion :
+ completed_jobs_dont_execute job_cost sched.
+
+ Variable tsk: sporadic_task.
+
+ Variable j: JobIn arr_seq.
+ Hypothesis H_job_of_task: job_task j = tsk.
+ Hypothesis valid_job:
+ valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
+
+ (* Remember that for any job of tsk, service <= task_cost tsk *)
+ Lemma cumulative_service_le_task_cost :
+ forall t t',
+ service_during sched j t t' <= task_cost tsk.
+ Proof.
+ rename valid_job into VALID; unfold valid_sporadic_job in *; ins; des.
+ apply leq_trans with (n := job_cost j);
+ last by rewrite -H_job_of_task; apply VALID0.
+ by apply cumulative_service_le_job_cost.
+ Qed.
+
+ End BasicLemmas.
+
+End ScheduleOfSporadicTaskWithJitter.
\ No newline at end of file
--
GitLab