Commit 3869c2a7 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Port development to Coq 8.5

parent d5cf8f9d
......@@ -2,3 +2,4 @@
*.glob
*.vo
*.html
*.aux
This diff is collapsed.
-R . rt
\ No newline at end of file
Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.analysis.basic.bertogna_edf_theory.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationEDF.
......@@ -238,7 +237,7 @@ Module ResponseTimeIterationEDF.
Proof.
intros l; unfold all_le; rewrite eq_refl andTb.
destruct l; first by done.
by apply/(zipP (fun x y => snd x <= snd y)).
by apply/(zipP t (fun x y => snd x <= snd y)).
Qed.
(* ... and transitive. *)
......@@ -247,8 +246,8 @@ Module ResponseTimeIterationEDF.
unfold transitive, all_le.
move => y x z /andP [/eqP ZIPxy LExy] /andP [/eqP ZIPyz LEyz].
apply/andP; split; first by rewrite ZIPxy -ZIPyz.
move: LExy => /(zipP (fun x y => snd x <= snd y)) LExy.
move: LEyz => /(zipP (fun x y => snd x <= snd y)) LEyz.
move: LExy => /(zipP _ (fun x y => snd x <= snd y)) LExy.
move: LEyz => /(zipP _ (fun x y => snd x <= snd y)) LEyz.
assert (SIZExy: size (unzip1 x) = size (unzip1 y)).
by rewrite ZIPxy.
assert (SIZEyz: size (unzip1 y) = size (unzip1 z)).
......@@ -259,21 +258,22 @@ Module ResponseTimeIterationEDF.
apply size0nil in SIZExy; symmetry in SIZEyz.
by apply size0nil in SIZEyz; subst.
}
apply/(zipP (fun x y => snd x <= snd y));
[by apply (t, 0) | by rewrite SIZExy -SIZEyz|].
rewrite -SIZExy in SIZEyz.
have ZIP := zipP t (fun x y => snd x <= snd y) _ _ SIZEyz.
apply/ZIP.
intros i LTi.
specialize (LExy t); specialize (LEyz t).
exploit LExy; first by rewrite SIZExy.
{
rewrite size_zip -SIZEyz -SIZExy minnn in LTi.
by rewrite size_zip -SIZExy minnn; apply LTi.
rewrite size_zip -SIZExy minnn.
rewrite size_zip -SIZEyz minnn in LTi; apply LTi.
}
instantiate (1 := t); intro LE.
exploit LEyz; first by apply SIZEyz.
intro LE.
exploit LEyz; first by rewrite -SIZExy.
{
rewrite size_zip SIZExy SIZEyz minnn in LTi.
by rewrite size_zip SIZEyz minnn; apply LTi.
by rewrite size_zip -SIZExy -size_zip; apply LTi.
}
by instantiate (1 := t); intro LE'; apply (leq_trans LE).
by intro LE'; apply (leq_trans LE).
Qed.
(* At any step of the iteration, the corresponding list
......@@ -294,8 +294,8 @@ Module ResponseTimeIterationEDF.
by rewrite iterSr IHstep.
}
apply/(zipP (fun x y => snd x <= snd y));
[by apply (tsk0,0)|by rewrite edf_claimed_bounds_size size_map |].
apply/(zipP (tsk0,0) (fun x y => snd x <= snd y));
first by rewrite edf_claimed_bounds_size size_map.
intros i LTi; rewrite iterS; unfold edf_rta_iteration at 1.
have MAP := @nth_map _ (tsk0,0) _ (tsk0,0).
......@@ -349,10 +349,9 @@ Module ResponseTimeIterationEDF.
apply f_equal with (B := nat) (f := fun x => size x) in UNZIP'.
rename UNZIP' into SIZE.
rewrite size_map [size (unzip1 _)]size_map in SIZE.
move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
move: LE => /(zipP _ (fun x y => snd x <= snd y)) LE.
destruct x1 as [| p0 x1'], x2 as [| p0' x2']; try (by ins).
apply/(zipP (fun x y => snd x <= snd y));
[by apply (p0,0) | by done |].
apply/(zipP p0 (fun x y => snd x <= snd y)); first by done.
intros i LTi.
exploit LE; first by rewrite 2!size_map in SIZE.
......@@ -420,7 +419,7 @@ Module ResponseTimeIterationEDF.
assert (GE_COST: all (fun p => task_cost (fst p) <= snd p) ((tsk0, R0) :: x1')).
{
clear LE; move: LEinit => /andP [/eqP UNZIP' LE].
move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
move: LE => /(zipP _ (fun x y => snd x <= snd y)) LE.
specialize (LE (tsk0, R0)).
apply/(all_nthP (tsk0,R0)).
intros j LTj; generalize UNZIP'; simpl; intro SIZE'.
......@@ -614,6 +613,8 @@ Module ResponseTimeIterationEDF.
k <= max_steps ts ->
\sum_((tsk, R) <- f k) (R - task_cost tsk) + 1 > k.
Proof.
have INC := bertogna_edf_comp_f_increases.
have MONO := bertogna_edf_comp_iteration_monotonic.
rename H_at_least_one_task into NONEMPTY.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
rename H_valid_task_parameters into VALID.
......@@ -661,12 +662,12 @@ Module ResponseTimeIterationEDF.
}
rewrite -2!big_seq_cond.
have LT := bertogna_edf_comp_f_increases step (ltnW LE).
have MONO := bertogna_edf_comp_iteration_monotonic step.
have LT := INC step (ltnW LE).
specialize (MONO step).
move: LT => /andP [_ LT]; move: LT => /hasP LT.
destruct LT as [[x1 x2] INzip LT]; simpl in *.
move: MONO => /andP [_ /(zipP (fun x y => snd x <= snd y)) MONO].
move: MONO => /andP [_ /(zipP _ (fun x y => snd x <= snd y)) MONO].
rewrite 2!(big_nth (elem, 0)).
apply mem_zip_exists with (elem := (elem, 0)) (elem' := (elem, 0)) in INzip; des;
last by rewrite size_map.
......@@ -940,6 +941,9 @@ Module ResponseTimeIterationEDF.
Theorem taskset_schedulable_by_edf_rta :
forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
Proof.
have RLIST := (edf_analysis_yields_response_time_bounds).
have DL := (edf_claimed_bounds_le_deadline ts).
have HAS := (edf_claimed_bounds_has_R_for_every_task ts).
unfold no_deadline_missed_by_task, task_misses_no_deadline,
job_misses_no_deadline, completed,
edf_schedulable,
......@@ -953,10 +957,6 @@ Module ResponseTimeIterationEDF.
H_test_succeeds into TEST.
move => tsk INtsk j JOBtsk.
have RLIST := (edf_analysis_yields_response_time_bounds).
have DL := (edf_claimed_bounds_le_deadline ts).
have HAS := (edf_claimed_bounds_has_R_for_every_task ts).
destruct (edf_claimed_bounds ts) as [rt_bounds |] eqn:SOME; last by ins.
exploit (HAS rt_bounds tsk); [by ins | by ins | clear HAS; intro HAS; des].
have COMPLETED := RLIST tsk R HAS j JOBtsk.
......
Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.interference
rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
rt.model.basic.platform rt.model.basic.response_time.
Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_edf.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisEDF.
......@@ -284,8 +283,8 @@ Module ResponseTimeAnalysisEDF.
| by apply JOBtsk | by apply BACK | ].
{
intros j0 tsk0 TSK0 LE.
cut (tsk0 \in unzip1 rt_bounds); [intro IN | by rewrite UNZIP -TSK0 FROMTS].
move: IN => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
cut (tsk0 \in unzip1 rt_bounds = true); last by rewrite UNZIP -TSK0 FROMTS.
move => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
apply completion_monotonic with (t0 := job_arrival j0 + R0); try (by done).
{
rewrite leq_add2l TSK0.
......@@ -362,6 +361,7 @@ Module ResponseTimeAnalysisEDF.
Lemma bertogna_edf_all_cpus_busy :
\sum_(tsk_k <- ts_interf) x tsk_k = X * num_cpus.
Proof.
have DIFFTASK := bertogna_edf_interference_by_different_tasks.
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,
......@@ -397,7 +397,7 @@ Module ResponseTimeAnalysisEDF.
}
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 |].
apply DIFFTASK with (t := t); [by auto | by done |].
by apply/existsP; exists cpu; apply/eqP.
Qed.
......@@ -416,8 +416,8 @@ Module ResponseTimeAnalysisEDF.
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'.
cut ((job_task j0) \in unzip1 rt_bounds = true); last by rewrite UNZIP FROMTS.
move => /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));
......@@ -442,6 +442,8 @@ Module ResponseTimeAnalysisEDF.
0 < cardGE delta < num_cpus ->
\sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
Proof.
have COMP := bertogna_edf_all_previous_jobs_complete_by_their_period.
have INV := bertogna_edf_scheduling_invariant.
rename H_all_jobs_from_taskset into FROMTS,
H_valid_task_parameters into PARAMS,
H_job_of_tsk into JOBtsk,
......@@ -515,7 +517,7 @@ Module ResponseTimeAnalysisEDF.
(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 apply (COMP t); rewrite ?TSK0.
}
by subst j2; apply SEQ with (j := j1) (t := t).
}
......@@ -549,9 +551,8 @@ Module ResponseTimeAnalysisEDF.
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.
by apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
[by rewrite INV | by rewrite count_filter].
}
{
unfold x at 2, total_interference_B.
......@@ -624,9 +625,12 @@ Module ResponseTimeAnalysisEDF.
\sum_((tsk_other, R_other) <- rt_bounds | jldp_can_interfere_with tsk tsk_other)
minn (x tsk_other) (R - task_cost tsk + 1) > I tsk R.
Proof.
have GE_COST := bertogna_edf_R_other_ge_cost.
have EXCEEDS := bertogna_edf_minimum_exceeds_interference.
have ALLBUSY := bertogna_edf_all_cpus_busy.
have TOOMUCH := bertogna_edf_too_much_interference.
rename H_rt_bounds_contains_all_tasks into UNZIP,
H_response_time_is_fixed_point into REC.
have GE_COST := bertogna_edf_R_other_ge_cost.
apply leq_trans with (n := \sum_(tsk_other <- ts_interf) minn (x tsk_other) (R - task_cost tsk + 1));
last first.
{
......@@ -654,11 +658,10 @@ Module ResponseTimeAnalysisEDF.
rewrite -addn1 -leq_subLR.
rewrite -[R + 1 - _]subh1; last by apply GE_COST.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
apply bertogna_edf_minimum_exceeds_interference.
apply EXCEEDS.
apply leq_trans with (n := X * num_cpus);
last by rewrite bertogna_edf_all_cpus_busy.
rewrite leq_mul2r; apply/orP; right.
by apply bertogna_edf_too_much_interference.
last by rewrite ALLBUSY.
by rewrite leq_mul2r; apply/orP; right; apply TOOMUCH.
Qed.
(* 8) After concluding that the sum of the minimum exceeds (R - e_i + 1),
......@@ -669,6 +672,9 @@ Module ResponseTimeAnalysisEDF.
(tsk_other, R_other) \in rt_bounds /\
(minn (x tsk_other) (R - task_cost tsk + 1) > interference_bound tsk_other R_other).
Proof.
have SUM := bertogna_edf_sum_exceeds_total_interference.
have BOUND := bertogna_edf_workload_bounds_interference.
have EDFBOUND := bertogna_edf_specific_bound_holds.
rename H_rt_bounds_contains_all_tasks into UNZIP.
assert (HAS: has (fun tup : task_with_response_time =>
let (tsk_other, R_other) := tup in
......@@ -679,7 +685,6 @@ Module ResponseTimeAnalysisEDF.
{
apply/negP; unfold not; intro NOTHAS.
move: NOTHAS => /negP /hasPn ALL.
have SUM := bertogna_edf_sum_exceeds_total_interference.
rewrite -[_ < _]negbK in SUM.
move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
unfold I, total_interference_bound_edf.
......@@ -692,11 +697,11 @@ Module ResponseTimeAnalysisEDF.
unfold interference_bound; rewrite leq_min; apply/andP; split;
last by rewrite geq_minr.
apply leq_trans with (n := x tsk_k); first by rewrite geq_minl.
by apply bertogna_edf_workload_bounds_interference.
by apply BOUND.
}
{
apply leq_trans with (n := x tsk_k); first by rewrite geq_minl.
by apply bertogna_edf_specific_bound_holds.
by apply EDFBOUND.
}
}
move: HAS => /hasP HAS; destruct HAS as [[tsk_k R_k] HPk MIN].
......
Add LoadPath "../../" as rt.
Require Import rt.util.all.
Require Import rt.analysis.basic.bertogna_fp_theory.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationFP.
......@@ -444,6 +443,7 @@ Module ResponseTimeIterationFP.
k <= max_steps tsk ->
f k > k + task_cost tsk - 1.
Proof.
have INC := bertogna_fp_comp_f_increases.
rename H_valid_task_parameters into TASK_PARAMS.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *; des.
exploit (TASK_PARAMS tsk);
......@@ -457,15 +457,12 @@ Module ResponseTimeIterationFP.
{
intros LT.
specialize (IHk (ltnW LT)).
apply leq_ltn_trans with (n := f k);
last by apply bertogna_fp_comp_f_increases, ltnW.
apply leq_ltn_trans with (n := f k); last by apply INC, ltnW.
rewrite -addn1 -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite -(ltn_add2r 1) in IHk.
rewrite subh1 in IHk; last first.
{
apply leq_trans with (n := task_cost tsk); last by apply leq_addl.
by apply PARAMS.
}
rewrite subh1 in IHk;
last by apply leq_trans with (n := task_cost tsk);
[by apply PARAMS | by apply leq_addl].
by rewrite -addnBA // subnn addn0 addn1 ltnS in IHk.
}
Qed.
......@@ -476,6 +473,8 @@ Module ResponseTimeIterationFP.
Lemma per_task_rta_converges:
f (max_steps tsk) = f (max_steps tsk).+1.
Proof.
have TOOMUCH := bertogna_fp_comp_rt_grows_too_much.
have INC := bertogna_fp_comp_f_increases.
rename H_no_larger_than_deadline into LE,
H_valid_task_parameters into TASK_PARAMS.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *; des.
......@@ -493,18 +492,19 @@ Module ResponseTimeIterationFP.
move: EX => /forall_inP EX.
rewrite leqNgt in LE; move: LE => /negP LE.
exfalso; apply LE.
have TOOMUCH := bertogna_fp_comp_rt_grows_too_much _ (max_steps tsk).
exploit TOOMUCH; [| by apply leqnn |].
assert (DIFF: forall k : nat, k <= max_steps tsk -> f k != f k.+1).
{
intros k LEk; rewrite -ltnS in LEk.
by exploit (EX (Ordinal LEk)); [by done | intro DIFF].
}
unfold max_steps at 1.
by exploit (EX (Ordinal LEk)); [by done | intro DIFF; apply DIFF].
}
exploit TOOMUCH; [by apply DIFF | by apply leq_addr |].
exploit (TASK_PARAMS tsk);
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
rewrite -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite subh1; last by apply PARAMS2.
by rewrite -addnBA // subnn addn0.
rewrite -addnBA // subnn addn0 subn1 prednK //.
intros LT; apply (leq_ltn_trans LT).
by rewrite /max_steps [_ - _ + 1]addn1; apply INC, leq_addr.
Qed.
End Convergence.
......@@ -657,7 +657,7 @@ Module ResponseTimeIterationFP.
(job_task0 := job_task) (ts0 := ts) (hp_bounds0 := take idx hp_bounds)
(higher_eq_priority := higher_priority); try (by done).
{
cut (NTH idx \in hp_bounds); [intros IN | by apply mem_nth].
cut (NTH idx \in hp_bounds = true); [intros IN | by apply mem_nth].
by rewrite -UNZIP; apply/mapP; exists (TASK idx, RESP idx); rewrite PAIR.
}
{
......@@ -688,15 +688,15 @@ Module ResponseTimeIterationFP.
Theorem taskset_schedulable_by_fp_rta :
forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
Proof.
have RLIST := (fp_analysis_yields_response_time_bounds).
have UNZIP := (fp_claimed_bounds_unzip ts).
have DL := (fp_claimed_bounds_le_deadline ts).
unfold no_deadline_missed_by_task, task_misses_no_deadline,
job_misses_no_deadline, completed,
fp_schedulable, valid_sporadic_job in *.
rename H_valid_job_parameters into JOBPARAMS.
move => tsk INtsk j JOBtsk.
have RLIST := (fp_analysis_yields_response_time_bounds).
have UNZIP := (fp_claimed_bounds_unzip ts).
have DL := (fp_claimed_bounds_le_deadline ts).
destruct (fp_claimed_bounds ts) as [rt_bounds |]; last by ins.
feed (UNZIP rt_bounds); first by done.
assert (EX: exists R, (tsk, R) \in rt_bounds).
......
Add LoadPath "../.." as rt.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.platform_fp
rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
rt.model.basic.response_time rt.model.basic.interference.
Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_fp.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisFP.
......@@ -159,7 +158,7 @@ Module ResponseTimeAnalysisFP.
rename H_hp_bounds_has_interfering_tasks into UNZIP,
H_response_time_of_tsk_other into INbounds.
move: UNZIP => UNZIP.
cut (tsk_other \in ts_interf);
cut (tsk_other \in ts_interf = true);
first by rewrite mem_filter; move => /andP [_ IN].
unfold ts_interf; rewrite UNZIP.
by apply/mapP; exists (tsk_other, R_other).
......@@ -171,7 +170,7 @@ Module ResponseTimeAnalysisFP.
rename H_hp_bounds_has_interfering_tasks into UNZIP,
H_response_time_of_tsk_other into INbounds.
move: UNZIP => UNZIP.
cut (tsk_other \in ts_interf);
cut (tsk_other \in ts_interf = true);
first by rewrite mem_filter; move => /andP [INTERF _].
unfold ts_interf; rewrite UNZIP.
by apply/mapP; exists (tsk_other, R_other).
......@@ -289,7 +288,7 @@ Module ResponseTimeAnalysisFP.
{
intros j_other tsk_other JOBother INTERF.
move: UNZIP => UNZIP.
cut (tsk_other \in unzip1 hp_bounds); last first.
cut (tsk_other \in unzip1 hp_bounds = true); last first.
{
rewrite -UNZIP mem_filter; apply/andP; split; first by done.
by rewrite -JOBother; apply FROMTS.
......@@ -301,7 +300,8 @@ Module ResponseTimeAnalysisFP.
rewrite leq_add2l.
apply leq_trans with (n := task_deadline tsk_other); first by apply NOMISS.
apply RESTR.
cut (tsk_other \in unzip1 hp_bounds); last by apply/mapP; exists (tsk_other, R').
cut (tsk_other \in unzip1 hp_bounds = true);
last by apply/mapP; exists (tsk_other, R').
by rewrite -UNZIP mem_filter; move => /andP [_ IN'].
}
}
......@@ -372,6 +372,7 @@ Module ResponseTimeAnalysisFP.
Lemma bertogna_fp_all_cpus_busy :
\sum_(tsk_k <- ts_interf) x tsk_k = X * num_cpus.
Proof.
have DIFFTASK := bertogna_fp_interference_by_different_tasks.
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 *.
......@@ -399,7 +400,7 @@ Module ResponseTimeAnalysisFP.
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 |].
apply DIFFTASK with (t := t); [by auto | by done |].
by apply/existsP; exists cpu; apply/eqP.
Qed.
......@@ -414,7 +415,8 @@ Module ResponseTimeAnalysisFP.
forall delta,
0 < cardGE delta < num_cpus ->
\sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
Proof.
Proof.
have INV := bertogna_fp_scheduling_invariant.
rename H_all_jobs_from_taskset into FROMTS,
H_valid_task_parameters into PARAMS,
H_job_of_tsk into JOBtsk,
......@@ -563,9 +565,8 @@ Module ResponseTimeAnalysisFP.
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.
by apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
[by rewrite INV | by rewrite count_filter].
}
{
unfold x at 2, total_interference_B.
......@@ -640,6 +641,9 @@ Module ResponseTimeAnalysisFP.
total_interference_bound_fp task_cost task_period tsk hp_bounds
R higher_eq_priority.
Proof.
have EXCEEDS := bertogna_fp_minimum_exceeds_interference.
have ALLBUSY := bertogna_fp_all_cpus_busy.
have TOOMUCH := bertogna_fp_too_much_interference.
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));
......@@ -657,11 +661,9 @@ Module ResponseTimeAnalysisFP.
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.
apply EXCEEDS.
apply leq_trans with (n := X * num_cpus); last by rewrite ALLBUSY.
by rewrite leq_mul2r; apply/orP; right; apply TOOMUCH.
Qed.
(* 6) After concluding that the sum of the minimum exceeds (R - e_i + 1),
......@@ -673,6 +675,8 @@ Module ResponseTimeAnalysisFP.
(minn (x tsk_k) (R - task_cost tsk + 1) >
minn (workload_bound tsk_k R_k) (R - task_cost tsk + 1)).
Proof.
have SUM := bertogna_fp_sum_exceeds_total_interference.
have INTERFk := bertogna_fp_tsk_other_interferes.
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
......@@ -682,7 +686,6 @@ Module ResponseTimeAnalysisFP.
{
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.
......@@ -691,7 +694,7 @@ Module ResponseTimeAnalysisFP.
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.
specialize (INTERFk tsk_k R_k HPk).
fold (can_interfere_with_tsk); rewrite INTERFk.
by apply ALL.
}
......@@ -707,6 +710,8 @@ Module ResponseTimeAnalysisFP.
Theorem bertogna_cirinei_response_time_bound_fp :
response_time_bounded_by tsk R.
Proof.
have WORKLOAD := bertogna_fp_workload_bounds_interference.
have EX := bertogna_fp_exists_task_that_exceeds_bound.
rename H_response_time_bounds_ge_cost into GE_COST,
H_interfering_tasks_miss_no_deadlines into NOMISS,
H_response_time_recurrence_holds into REC,
......@@ -743,10 +748,10 @@ Module ResponseTimeAnalysisFP.
apply negbT in NOTCOMP; exfalso.
(* We derive a contradiction using the previous lemmas. *)
have EX := bertogna_fp_exists_task_that_exceeds_bound j JOBtsk NOTCOMP BEFOREok.
specialize (EX j JOBtsk NOTCOMP BEFOREok).
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.
specialize (WORKLOAD j tsk_k R_k HPk).
destruct (W task_cost task_period tsk_k R_k R < R - task_cost tsk + 1); rewrite leq_min in LTmin;
last