Skip to content
Snippets Groups Projects
Commit d5cf8f9d authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Keep only the definition of parallel interference

parent 7ac7144a
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 1544 additions and 1293 deletions
analysis/basic/bertogna_edf_theory.v
+ 231
− 124
View file @ d5cf8f9d
This diff is collapsed.
analysis/basic/bertogna_fp_theory.v
+ 247
− 119
View file @ d5cf8f9d
This diff is collapsed.
analysis/basic/interference_bound_edf.v
+ 44
− 33
View file @ d5cf8f9d
......@@ -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.
......
analysis/jitter/bertogna_edf_theory.v
+ 260
− 133
View file @ d5cf8f9d
This diff is collapsed.
analysis/jitter/bertogna_fp_theory.v
+ 511
− 355
View file @ d5cf8f9d
This diff is collapsed.
analysis/jitter/interference_bound_edf.v
+ 23
− 17
View file @ d5cf8f9d
......@@ -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.
......
analysis/parallel/bertogna_edf_theory.v
+ 3
− 3
View file @ d5cf8f9d
......@@ -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.
......
analysis/parallel/bertogna_fp_theory.v
+ 5
− 5
View file @ d5cf8f9d
......@@ -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).
......
analysis/parallel/interference_bound_edf.v
+ 2
− 2
View file @ d5cf8f9d
......@@ -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.
{
......
implementation/basic/schedule.v
+ 3
− 3
View file @ d5cf8f9d
......@@ -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.
{
......
implementation/jitter/schedule.v
+ 3
− 4
View file @ d5cf8f9d
......@@ -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.
{
......
model/basic/interference.v
+ 67
− 193
View file @ d5cf8f9d
......@@ -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
model/basic/interference_edf.v
+ 8
− 36
View file @ d5cf8f9d
......@@ -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
model/basic/platform.v
+ 3
− 4
View file @ d5cf8f9d
......@@ -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.
......
model/basic/platform_fp.v
+ 3
− 4
View file @ d5cf8f9d
......@@ -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).
{
......
model/basic/schedule.v
+ 36
− 33
View file @ d5cf8f9d
......@@ -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.
......
model/jitter/interference.v
+ 70
− 206
View file @ d5cf8f9d
......@@ -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
model/jitter/interference_edf.v
+ 19
− 9
View file @ d5cf8f9d
......@@ -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.
......
model/jitter/platform.v
+ 3
− 5
View file @ d5cf8f9d
......@@ -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.
......
model/jitter/platform_fp.v
+ 3
− 5
View file @ d5cf8f9d
......@@ -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).
{
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment