Skip to content

GitLab

P
PROSA - Formally Proven Schedulability Analysis
Commit 179ca8e4 authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files
Options

Fix name of parallel interference

parent b71f34f7
Hide whitespace changes
Inline Side-by-side
Showing with 107 additions and 171 deletions
analysis/basic/bertogna_edf_theory.v
View file @ 179ca8e4
......@@ -125,7 +125,7 @@ Module ResponseTimeAnalysisEDF.
(* Let's call x the interference incurred by job j due to tsk_other, ...*)
Let x (tsk_other: sporadic_task) :=
task_interference job_cost job_task sched j
task_interference_sequential 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. *)
......@@ -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_le_workload.
first by apply task_interference_seq_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
......
analysis/basic/bertogna_fp_theory.v
View file @ 179ca8e4
......@@ -136,7 +136,7 @@ Module ResponseTimeAnalysisFP.
(* Let's call x the interference incurred by job j due to tsk_other, ...*)
Let x (tsk_other: sporadic_task) :=
task_interference job_cost job_task sched j
task_interference_sequential 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. *)
......@@ -198,7 +198,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_le_workload.
first by apply task_interference_seq_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;
......
analysis/basic/interference_bound_edf.v
View file @ 179ca8e4
......@@ -195,7 +195,7 @@ Module InterferenceBoundEDF.
(* Let's call x the task interference incurred by job j due to tsk_k. *)
Let x :=
task_interference job_cost job_task sched j_i
task_interference_sequential 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. *)
......@@ -212,7 +212,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 job_cost sched j_i.
Let interference_caused_by := job_interference_sequential job_cost sched j_i.
(* Identify the subset of jobs that actually cause interference *)
Let interfering_jobs :=
......@@ -302,7 +302,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_le_service.
first by apply job_interference_seq_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).
......@@ -396,7 +396,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_le_service.
first by apply job_interference_seq_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.
......@@ -438,20 +438,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 job_cost sched j_i j_fst t1 t2 <= D_i - (D_k - R_k).
job_interference_sequential 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_under_edf_implies_shorter_deadlines with
apply interference_seq_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 job_cost sched j_i j_fst
apply leq_trans with (n := job_interference_sequential job_cost sched j_i j_fst
(a_fst + R_k) t2).
{
apply extend_sum; last by apply leqnn.
......@@ -463,7 +463,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_le_service.
first by apply job_interference_seq_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.
......@@ -476,7 +476,7 @@ Module InterferenceBoundEDF.
rewrite addnC -subnBA; last by apply leq_addr.
by rewrite addnC -addnBA // subnn addn0.
}
apply leq_trans with (n := job_interference job_cost sched j_i j_fst t1
apply leq_trans with (n := job_interference_sequential job_cost sched j_i j_fst t1
(a_fst + D_k) + (D_k - R_k)).
{
rewrite leq_add2r.
......@@ -487,15 +487,15 @@ Module InterferenceBoundEDF.
by rewrite leq_add2l; apply H_R_k_le_deadline.
}
{
unfold job_interference.
unfold job_interference_sequential.
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 job_cost sched j_i j_fst t1
apply leq_trans with (n := job_interference_sequential 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_le_service.
by apply job_interference_seq_le_service.
}
unfold service_during.
rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost)
......@@ -506,14 +506,14 @@ Module InterferenceBoundEDF.
}
}
unfold job_interference.
unfold job_interference_sequential.
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 job_cost sched j_i j_fst t1
apply leq_trans with (n := job_interference_sequential 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_le_service.
by apply job_interference_seq_le_service.
}
unfold service_during.
rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R:=R_k);
......@@ -523,7 +523,7 @@ Module InterferenceBoundEDF.
\sum_(a_fst + 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.
by unfold job_interference_sequential; apply leq_sum; ins; apply leq_b1.
}
rewrite -big_cat_nat;
[simpl | by apply AFTERt1 | by rewrite leq_add2l; apply H_R_k_le_deadline ].
......@@ -569,7 +569,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_under_edf_implies_shorter_deadlines with
apply interference_seq_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.
......@@ -587,7 +587,7 @@ 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 job_cost sched j_i j_fst t1
apply leq_trans with (n := job_interference_sequential 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 +
......@@ -608,7 +608,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_under_edf_implies_shorter_deadlines with
by apply interference_seq_under_edf_implies_shorter_deadlines with
(job_deadline0 := job_deadline) in LEdl.
Qed.
......@@ -707,7 +707,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_le_service.
first by apply job_interference_seq_le_service.
rewrite leqn0; apply/eqP; unfold service_during.
by apply cumulative_service_before_job_arrival_zero.
Qed.
......@@ -731,7 +731,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_le_service.
first by apply job_interference_seq_le_service.
rewrite leqn0; apply/eqP.
by apply cumulative_service_before_job_arrival_zero.
}
......@@ -830,7 +830,7 @@ Module InterferenceBoundEDF.
}
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [_ [ LEdl _]].
apply interference_under_edf_implies_shorter_deadlines with
apply interference_seq_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.
......@@ -916,7 +916,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_under_edf_implies_shorter_deadlines with
by apply interference_seq_under_edf_implies_shorter_deadlines with
(job_deadline0 := job_deadline) in LSTserv.
Qed.
......@@ -943,19 +943,19 @@ Module InterferenceBoundEDF.
}
destruct (leqP t2 (a_fst + R_k)) as [LEt2 | GTt2].
{
apply leq_trans with (n := job_interference job_cost sched j_i j_fst t1
apply leq_trans with (n := job_interference_sequential 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.
}
{
unfold interference_caused_by, job_interference.
unfold interference_caused_by, job_interference_sequential.
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.
apply leq_trans with (n := service_during sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service.
first by apply job_interference_seq_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].
......@@ -1034,7 +1034,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_under_edf_implies_shorter_deadlines
by apply interference_seq_under_edf_implies_shorter_deadlines
with (job_deadline0 := job_deadline) in LSTserv.
Qed.
......
analysis/parallel/bertogna_edf_theory.v
View file @ 179ca8e4
......@@ -122,7 +122,7 @@ Module ResponseTimeAnalysisEDF.
(* Let's call x the interference incurred by job j due to tsk_other, ...*)
Let x (tsk_other: sporadic_task) :=
task_interference_with_parallelism job_cost job_task sched j
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. *)
......@@ -180,7 +180,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 apply task_interference_with_parallelism_le_workload.
first apply task_interference_le_workload.
apply workload_bounded_by_W with (task_deadline0 := task_deadline)
(job_cost0 := job_cost) (job_deadline0 := job_deadline); try (by ins).
......@@ -269,7 +269,7 @@ Module ResponseTimeAnalysisEDF.
H_rt_bounds_contains_all_tasks into UNZIP,
H_restricted_deadlines into RESTR.
unfold sporadic_task_model in *.
unfold x, X, total_interference, task_interference_with_parallelism.
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 /andP [GEt LTt].
......@@ -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_tsk SCHED;apply/eqP;rewrite eqb0 eq_sym.
last by intros i DIFF; rewrite /schedules_job_of_task 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_tsk; rewrite SCHED.
by unfold schedules_job_of_task; rewrite SCHED.
}
rewrite mem_filter; apply/andP; split; last by apply FROMTS.
unfold jldp_can_interfere_with.
......
analysis/parallel/bertogna_fp_theory.v
View file @ 179ca8e4
......@@ -122,7 +122,7 @@ Module ResponseTimeAnalysisFP.
(* Let's call x the interference incurred by job j due to tsk_other, ...*)
Let x (tsk_other: sporadic_task) :=
task_interference_with_parallelism job_cost job_task sched j
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. *)
......@@ -180,7 +180,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_with_parallelism_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);
......@@ -260,7 +260,7 @@ Module ResponseTimeAnalysisFP.
H_response_time_no_larger_than_deadline into NOMISS.
unfold sporadic_task_model, enforces_FP_policy,
enforces_JLDP_policy, FP_to_JLDP in *.
unfold x, X, total_interference, task_interference_with_parallelism.
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 /andP [GEt LTt].
......@@ -281,9 +281,9 @@ 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_tsk SCHED;apply/eqP;rewrite eqb0 eq_sym.
last by intros i DIFF; rewrite /schedules_job_of_task 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_tsk; rewrite SCHED.
by unfold schedules_job_of_task; rewrite SCHED.
}
rewrite mem_filter; apply/andP; split; last by apply FROMTS.
unfold can_interfere_with_tsk, fp_can_interfere_with.
......
analysis/parallel/interference_bound_edf.v
View file @ 179ca8e4
......@@ -191,7 +191,7 @@ Module InterferenceBoundEDF.
(* Let's call x the task interference incurred by job j due to tsk_k. *)
Let x :=
task_interference_with_parallelism job_cost job_task sched j_i
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. *)
......@@ -208,7 +208,7 @@ Module InterferenceBoundEDF.
Let n_k := div_ceil (D_i + R_k - D_k + 1) p_k.
(* Let's give a simpler name to job interference. *)
Let interference_caused_by := job_interference_with_parallelism 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 :=
......@@ -230,7 +230,7 @@ Module InterferenceBoundEDF.
x <= \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
interference_caused_by j t1 t2.
Proof.
unfold x, task_interference_with_parallelism, interference_caused_by, job_interference_with_parallelism.
unfold x, task_interference, interference_caused_by, job_interference.
rewrite [\sum_(_ <- _ sched _ _ | _) _]exchange_big /=.
rewrite big_nat_cond [\sum_(_ <= _ < _ | true) _]big_nat_cond.
apply leq_sum. move => t /andP [LEt _].
......@@ -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_tsk job_task sched tsk_k cpu t) eqn:SCHED;
destruct (schedules_job_of_task job_task sched tsk_k cpu t) eqn:SCHED;
last by done.
unfold schedules_job_of_tsk in *.
unfold schedules_job_of_task in *.
destruct (sched cpu t) eqn:SOME; last by done.
rewrite big_mkcond /= (bigD1_seq j) /=; last by apply undup_uniq.
{
......@@ -324,7 +324,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_with_parallelism_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).
......@@ -421,7 +421,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_with_parallelism_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.
......@@ -524,7 +524,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_with_parallelism_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.
......@@ -548,7 +548,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_with_parallelism_le_service.
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
by apply cumulative_service_before_job_arrival_zero.
}
......@@ -635,12 +635,12 @@ Module InterferenceBoundEDF.
last by rewrite leq_add2l.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [_ [ LEdl _]].
apply interference_with_parallelism_under_edf_implies_shorter_deadlines with
apply interference_under_edf_implies_shorter_deadlines with
(job_deadline0 := job_deadline) in LEdl; try (by done).
rewrite addnC [D_i + _]addnC.
unfold D_k, D_i.
by rewrite -interference_bound_edf_j_fst_deadline
-interference_bound_edf_j_i_deadline.
-interference_bound_edf_j_i_deadline.
Qed.
(* Using the lemma above, we prove that the ratio n_k is at least the number of
......@@ -688,7 +688,7 @@ Module InterferenceBoundEDF.
last by rewrite leq_add2r.
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [_ [ LEdl _]].
apply interference_with_parallelism_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.
......
model/basic/interference.v
View file @ 179ca8e4
......@@ -76,29 +76,30 @@ Module Interference.
(* The interference caused by job_other is defined as follows. *)
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.
Section JobInterferenceParallelism.
Section JobInterferenceSequential.
(* 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. *)
Definition job_interference_with_parallelism (t1 t2: time) :=
(* 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)
\sum_(cpu < num_cpus)
(job_is_backlogged t && scheduled_on sched job_other cpu t).
(job_is_backlogged t && scheduled sched job_other t).
End JobInterferenceParallelism.
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_tsk (cpu: processor num_cpus) (t: time) :=
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
......@@ -107,36 +108,37 @@ Module Interference.
(* 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].
[exists cpu in processor num_cpus, schedules_job_of_task cpu t].
(* We define the total interference incurred by tsk during [t1, t2)
as the cumulative time in which tsk is scheduled. *)
as the cumulative time while tsk is scheduled. *)
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 && schedules_job_of_task cpu t).
End TaskInterference.
Section TaskInterferenceParallelism.
Section TaskInterferenceSequential.
(* In order to define task interference, consider any interfering task tsk_other. *)
Variable tsk_other: sporadic_task.
(* We define the total interference incurred by tsk during [t1, t2)
as the cumulative time in which tsk is scheduled. *)
Definition task_interference_with_parallelism (t1 t2: time) :=
(* If jobs are sequential, we define the total interference incurred by tsk
during [t1, t2) as the cumulative time in which tsk is scheduled. *)
Definition task_interference_sequential (t1 t2: time) :=
\sum_(t1 <= t < t2)
\sum_(cpu < num_cpus)
(job_is_backlogged t && schedules_job_of_tsk tsk_other cpu t).
(job_is_backlogged t && task_is_scheduled tsk_other t).
End TaskInterferenceParallelism.
End TaskInterferenceSequential.
Section TaskInterferenceJobList.
Variable tsk_other: sporadic_task.
Definition task_interference_joblist (t1 t2: time) :=
Definition task_interference_sequential_joblist (t1 t2: time) :=
\sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_other)
job_interference j t1 t2.
job_interference_sequential j t1 t2.
End TaskInterferenceJobList.
......@@ -153,9 +155,9 @@ Module Interference.
by rewrite big_const_nat iter_addn mul1n addn0 leqnn.
Qed.
Lemma job_interference_le_delta :
Lemma job_interference_seq_le_delta :
forall j_other t1 delta,
job_interference j_other t1 (t1 + delta) <= 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);
......@@ -163,11 +165,11 @@ Module Interference.
by rewrite big_const_nat iter_addn mul1n addn0 addKn leqnn.
Qed.
Lemma job_interference_le_service :
Lemma job_interference_seq_le_service :
forall j_other t1 t2,
job_interference j_other t1 t2 <= service_during sched 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, service_during.
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 _.
......@@ -177,11 +179,11 @@ Module Interference.
by apply leq_trans with (n := 1).
Qed.
Lemma job_interference_with_parallelism_le_service :
Lemma job_interference_le_service :
forall j_other t1 t2,
job_interference_with_parallelism j_other t1 t2 <= service_during sched 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_with_parallelism, service_during.
intros j_other t1 t2; unfold job_interference, service_during.
apply leq_sum; intros t _.
unfold service_at; rewrite [\sum_(_ < _ | scheduled_on _ _ _ _)_]big_mkcond.
apply leq_sum; intros cpu _.
......@@ -189,9 +191,9 @@ Module Interference.
by destruct (scheduled_on sched j_other cpu t).
Qed.
Lemma task_interference_le_workload :
Lemma task_interference_seq_le_workload :
forall tsk t1 t2,
task_interference tsk t1 t2 <= workload job_task sched 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 _.
......@@ -202,99 +204,33 @@ Module Interference.
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 *.
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_with_parallelism_le_workload :
Lemma task_interference_le_workload :
forall tsk t1 t2,
task_interference_with_parallelism tsk t1 t2 <= workload job_task sched tsk t1 t2.
task_interference tsk t1 t2 <= workload job_task sched tsk t1 t2.
Proof.