diff --git a/analysis/facts/job_index.v b/analysis/facts/job_index.v
index 0d2354c6181fce55a7bfcdf34d13ab14d42ba1e8..c03967b93d2d208fda05ae3260b6474f0593b6f4 100644
--- a/analysis/facts/job_index.v
+++ b/analysis/facts/job_index.v
@@ -46,8 +46,10 @@ Section JobIndexLemmas.
Proof.
move => ARR_LT.
move: H_equal_index => IND.
+ try ( apply task_arrivals_up_to_prefix_cat with (arr_seq0 := arr_seq) in ARR_LT => // ) ||
apply task_arrivals_up_to_prefix_cat with (arr_seq := arr_seq) in ARR_LT => //.
move : ARR_LT => [xs ARR_CAT].
+ try ( apply eq_ind_in_seq with (xs0 := task_arrivals_up_to_job_arrival arr_seq j2) => // ) ||
apply eq_ind_in_seq with (xs := task_arrivals_up_to_job_arrival arr_seq j2) => //.
- now rewrite -/(job_index _ _) -IND -ARR_CAT index_cat ifT;
try apply arrives_in_task_arrivals_up_to.
diff --git a/analysis/facts/sporadic.v b/analysis/facts/sporadic.v
index 79fd0e7565ded9e399c7d0fabd5af8b83b37ee6b..24afade5787d4f9eb926c353c02ab61cb0216362 100644
--- a/analysis/facts/sporadic.v
+++ b/analysis/facts/sporadic.v
@@ -97,7 +97,8 @@ Section DifferentJobsImplyDifferentArrivalTimes.
intros UNEQ EQ_ARR.
rewrite -> diff_jobs_iff_diff_indices in UNEQ => //; eauto; last by rewrite H_j1_task.
move /neqP: UNEQ; rewrite neq_ltn => /orP [LT|LT].
- all: now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; ssrlia.
+ all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; ssrlia ) ||
+ now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; ssrlia.
Qed.
(** We prove a stronger version of the above lemma by showing
@@ -112,7 +113,7 @@ Section DifferentJobsImplyDifferentArrivalTimes.
case: (boolP (j1 == j2)) => [/eqP EQ | /eqP NEQ]; first by auto.
rewrite -> diff_jobs_iff_diff_indices in NEQ => //; eauto; last by rewrite H_j1_task.
move /neqP: NEQ; rewrite neq_ltn => /orP [LT|LT].
- all: now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; ssrlia.
+ all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; ssrlia ) || now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; ssrlia.
Qed.
End DifferentJobsImplyDifferentArrivalTimes.
@@ -172,6 +173,7 @@ Section SporadicArrivals.
apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
have EQ_ARR_A : (job_arrival a = job_arrival j) by apply H_consistent_arrivals.
have EQ_ARR_B : (job_arrival b = job_arrival j) by apply H_consistent_arrivals.
+ try ( apply uneq_job_uneq_arr with (arr_seq0 := arr_seq) (tsk0 := job_task j) in NEQ => // ) ||
apply uneq_job_uneq_arr with (arr_seq := arr_seq) (tsk := job_task j) in NEQ => //.
now rewrite EQ_ARR_A EQ_ARR_B in NEQ.
Qed.
@@ -231,6 +233,7 @@ Section SporadicArrivals.
have PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1 by apply prev_job_arr_lte => //.
rewrite ltn_neqAle; apply /andP.
split => //; apply /eqP.
+ try ( apply uneq_job_uneq_arr with (arr_seq0 := arr_seq) (tsk0 := job_task j1) => //; try by rewrite H_j1_task ) ||
apply uneq_job_uneq_arr with (arr_seq := arr_seq) (tsk := job_task j1) => //; try by rewrite H_j1_task.
- now apply prev_job_arr.
- now apply prev_job_task.
diff --git a/analysis/facts/transform/edf_opt.v b/analysis/facts/transform/edf_opt.v
index f4c43a6957a0fac01b7efa41e42fa0dcc1eb6451..1f335140902a0c53b4e2f08935aefae3dc0b1464 100644
--- a/analysis/facts/transform/edf_opt.v
+++ b/analysis/facts/transform/edf_opt.v
@@ -256,6 +256,7 @@ Section MakeEDFAtFacts.
now apply scheduled_job_in_sched_has_later_deadline.
- have EX: (exists t', scheduled_at sched j t').
{
+ try ( apply swap_job_scheduled with (t1 := t_edf) (t2 := find_swap_candidate sched t_edf j_orig) (t0 := t) ) ||
apply swap_job_scheduled with (t1 := t_edf) (t2 := find_swap_candidate sched t_edf j_orig) (t := t).
now move: SCHED; rewrite /sched' /make_edf_at SCHED_orig.
}
@@ -419,6 +420,7 @@ Section MakeEDFAtFacts.
+ by rewrite -EQ; apply fsc_range1.
- case (boolP(t_edf == t)) => [/eqP EQ'| /eqP NEQ'].
+ move=> SCHED_j.
+ try ( have ARR_j: job_arrival j <= t_edf by apply fsc_found_job_arrival with (sched0 := sched) (j1 := j_orig) => //; rewrite scheduled_at_def ) ||
have ARR_j: job_arrival j <= t_edf by apply fsc_found_job_arrival with (sched := sched) (j1 := j_orig) => //; rewrite scheduled_at_def.
now rewrite -EQ'.
+ move=> SCHED_j.
@@ -703,7 +705,7 @@ Section EDFPrefixInclusion.
by rewrite scheduled_at_def /edf_transform_prefix; apply /eqP.
apply fsc_range1 => //.
- by apply edf_prefix_jobs_must_arrive.
- - apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := h2) => //.
+ - try ( apply edf_prefix_scheduled_job_has_later_deadline with (sched0 := sched) (horizon := h2) => // ) || apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := h2) => //.
Qed.
End EDFPrefixInclusion.
@@ -798,7 +800,7 @@ Section EDFTransformFacts.
H_completed_jobs_dont_execute H_no_deadline_misses t_dl.+1) => [_ [_ DL]].
now apply (DL j t).
- by apply (identical_prefix_inclusion _ _ t_dl.+1) => //; apply edf_finite_prefix.
- - by apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := t.+1).
+ - try ( by apply edf_prefix_scheduled_job_has_later_deadline with (sched0 := sched) (horizon := t.+1) ) || by apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := t.+1).
Qed.
(** We observe that no new jobs are introduced: any job scheduled in the EDF
@@ -817,12 +819,15 @@ Section EDFTransformFacts.
forall j t, scheduled_at sched j t -> exists t', scheduled_at sched_edf j t'.
Proof.
move=> j t SCHED_j.
+ try ( have EX: exists t', scheduled_at (edf_transform_prefix sched (job_deadline j)) j t'
+ by apply edf_prefix_job_scheduled' with (t0 := t) ) ||
have EX: exists t', scheduled_at (edf_transform_prefix sched (job_deadline j)) j t'
by apply edf_prefix_job_scheduled' with (t := t).
move: EX => [t' SCHED'].
exists t'.
rewrite /sched_edf /edf_transform scheduled_at_def.
rewrite (edf_prefix_inclusion _ _ _ _ t'.+1 (job_deadline j)) -?scheduled_at_def=> //.
+ try ( now apply edf_prefix_scheduled_job_has_later_deadline with (sched0 := sched) (horizon := job_deadline j) ) ||
now apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := job_deadline j).
Qed.
diff --git a/analysis/facts/transform/swaps.v b/analysis/facts/transform/swaps.v
index 84e1d082bf146c3d467e8551f87599422483c1a2..b4d43fc47cf8d5782a3414d8f17c917e8d12dc28 100644
--- a/analysis/facts/transform/swaps.v
+++ b/analysis/facts/transform/swaps.v
@@ -435,6 +435,7 @@ Section EDFSwap.
move=> AT_t2.
rewrite -service_invariant_implies_deadline_met; first by exact H_deadline_met.
apply service_after_swap_invariant => //.
+ try ( by apply scheduled_at_implies_later_deadline with (sched0 := sched) => // ) ||
by apply scheduled_at_implies_later_deadline with (sched := sched) => //.
Qed.
diff --git a/classic/analysis/apa/bertogna_edf_theory.v b/classic/analysis/apa/bertogna_edf_theory.v
index b6c04b21d181c9f69e43d570a160e662c6b9b212..47da1d50962402f0ca7eec2f8b084136179ba63a 100644
--- a/classic/analysis/apa/bertogna_edf_theory.v
+++ b/classic/analysis/apa/bertogna_edf_theory.v
@@ -206,23 +206,29 @@ Module ResponseTimeAnalysisEDF.
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.
- by apply workload_bounded_by_W with (task_deadline := task_deadline)
+ by ((try ( apply workload_bounded_by_W with (task_deadline0 := task_deadline)
+ (job_arrival0 := job_arrival) (arr_seq0 := arr_seq)
+ (job_cost0 := job_cost) (job_deadline0 := job_deadline)) ||
+ apply workload_bounded_by_W with (task_deadline := task_deadline)
(job_arrival := job_arrival) (arr_seq := arr_seq)
- (job_cost := job_cost) (job_deadline := job_deadline); try (by ins); last 2 first;
+ (job_cost := job_cost) (job_deadline := job_deadline)); try (by ins); last 2 first;
[ by apply bertogna_edf_R_other_ge_cost
| by ins; apply NOMISS
| by ins; apply TASK_PARAMS
| by ins; apply RESTR
- | by ins; apply BEFOREok with (tsk_other := tsk_other)].
+ | by ins; apply BEFOREok with (tsk_other := tsk_other)]).
Qed.
(* Recall that the edf-specific interference bound also holds for tsk_other. *)
Lemma bertogna_edf_specific_bound_holds :
x tsk_other <= edf_specific_bound tsk_other R_other.
Proof.
+ (try ( apply interference_bound_edf_bounds_interference with
+ (job_deadline0 := job_deadline)
+ (arr_seq0 := arr_seq) (ts0 := ts) ) ||
apply interference_bound_edf_bounds_interference with
(job_deadline := job_deadline)
- (arr_seq := arr_seq) (ts := ts); try (by done);
+ (arr_seq := arr_seq) (ts := ts)); try (by done);
[ by apply bertogna_edf_tsk_other_in_ts |
by apply H_tasks_miss_no_deadlines | ].
by ins; apply H_all_previous_jobs_completed_on_time with (tsk_other := tsk_other).
@@ -300,14 +306,17 @@ Module ResponseTimeAnalysisEDF.
by apply/existsP; exists cpu.
clear SCHED; rename SCHED' into SCHED.
move: (SCHED) => PENDING.
+ (try ( apply scheduled_implies_pending with (job_arrival0 := job_arrival) (job_cost0 := job_cost)
+ in PENDING ) ||
apply scheduled_implies_pending with (job_arrival := job_arrival) (job_cost := job_cost)
- in PENDING; try (by done).
+ in PENDING); try (by done).
destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
{
move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
specialize (BEFOREok j_other tsk R ARRother SAMEtsk INbounds LT).
move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
- apply completion_monotonic with (t := job_arrival j_other + R); try (by done).
+ (try ( apply completion_monotonic with (t0 := job_arrival j_other + R)) ||
+ apply completion_monotonic with (t := job_arrival j_other + R)); try (by done).
apply leq_trans with (n := job_arrival j); last by done.
apply leq_trans with (n := job_arrival j_other + task_deadline tsk);
first by rewrite leq_add2l; apply NOMISS.
@@ -352,6 +361,7 @@ Module ResponseTimeAnalysisEDF.
intros t j0 ARR0 LEt LE.
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'.
+ try ( apply completion_monotonic with (t0 := job_arrival j0 + R0) ) ||
apply completion_monotonic with (t := job_arrival j0 + R0).
{
rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
@@ -556,10 +566,14 @@ Module ResponseTimeAnalysisEDF.
apply scheduled_implies_pending; try by done.
by apply/existsP; exists cpu2; rewrite /scheduled_on -SCHED2.
}
+ ( try ( apply platform_at_most_one_pending_job_of_each_task with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (tsk0 := tsk)
+ (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) (j0 := j) (t0 := t)
+ (job_arrival0 := job_arrival) (arr_seq0 := arr_seq) ) ||
apply platform_at_most_one_pending_job_of_each_task with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline) (tsk := tsk)
(job_cost := job_cost) (job_task := job_task) (sched := sched) (j := j) (t := t)
- (job_arrival := job_arrival) (arr_seq := arr_seq);
+ (job_arrival := job_arrival) (arr_seq := arr_seq) );
rewrite ?JOBtsk ?SAMEtsk //; first by apply PARAMS; rewrite -JOBtsk FROMTS.
intros j0 tsk0 ARR0 TSK0 LE.
by apply (COMP t); rewrite ?TSK0.
@@ -592,14 +606,20 @@ Module ResponseTimeAnalysisEDF.
by apply/existsP; exists cpu; rewrite /scheduled_on -SCHED'.
}
move: (SCHEDULED') => PENDING'.
+ ( try ( apply scheduled_implies_pending with (job_cost0 := job_cost) (job_arrival0:=job_arrival)
+ in PENDING' ) ||
apply scheduled_implies_pending with (job_cost := job_cost) (job_arrival:=job_arrival)
- in PENDING'; try by done.
+ in PENDING' ); try by done.
assert (BUG: j = j').
{
+ (try ( apply platform_at_most_one_pending_job_of_each_task with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (tsk0 := tsk)
+ (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) (j0 := j) (t0 := t)
+ (job_arrival0 := job_arrival) (arr_seq0 := arr_seq) ) ||
apply platform_at_most_one_pending_job_of_each_task with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline) (tsk := tsk)
(job_cost := job_cost) (job_task := job_task) (sched := sched) (j := j) (t := t)
- (job_arrival := job_arrival) (arr_seq := arr_seq);
+ (job_arrival := job_arrival) (arr_seq := arr_seq));
rewrite ?JOBtsk ?SAMEtsk //; first by apply PARAMS; rewrite -JOBtsk FROMTS.
intros j0 tsk0 ARR0 TSK0 LE.
by apply (COMP t); rewrite ?TSK0.
@@ -702,11 +722,16 @@ Module ResponseTimeAnalysisEDF.
apply scheduled_implies_pending; try by done.
by apply/existsP; exists cpu'; rewrite /scheduled_on -SCHED2.
}
+ ( try ( apply platform_at_most_one_pending_job_of_each_task with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (tsk0 := tsk)
+ (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) (j0 := j) (t0 := t)
+ (job_arrival0 := job_arrival) (arr_seq0 := arr_seq);
+ rewrite ?JOBtsk ?SAMEtsk // ) ||
apply platform_at_most_one_pending_job_of_each_task with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline) (tsk := tsk)
(job_cost := job_cost) (job_task := job_task) (sched := sched) (j := j) (t := t)
(job_arrival := job_arrival) (arr_seq := arr_seq);
- rewrite ?JOBtsk ?SAMEtsk //; first by apply PARAMS; rewrite -JOBtsk FROMTS.
+ rewrite ?JOBtsk ?SAMEtsk //); first by apply PARAMS; rewrite -JOBtsk FROMTS.
intros j0 tsk0 ARR0 TSK0 LE.
by apply (COMP t); rewrite ?TSK0.
}
diff --git a/classic/analysis/apa/bertogna_fp_comp.v b/classic/analysis/apa/bertogna_fp_comp.v
index 8be71da92438fa9123b757546d7a2284ba1e5352..39e694dd803be0f8c14a9857a9710d5b242fb4d0 100644
--- a/classic/analysis/apa/bertogna_fp_comp.v
+++ b/classic/analysis/apa/bertogna_fp_comp.v
@@ -613,12 +613,18 @@ Module ResponseTimeIterationFP.
}
intros [_ [_ [REC DL]]].
+ (try ( apply bertogna_cirinei_response_time_bound_fp with
+ (alpha0 := alpha) (alpha'0 := alpha')
+ (task_cost0 := task_cost) (task_period0 := task_period)
+ (task_deadline0 := task_deadline) (job_deadline0 := job_deadline) (tsk0 := (TASK idx))
+ (job_task0 := job_task) (ts0 := ts) (hp_bounds0 := take idx hp_bounds)
+ (higher_eq_priority := higher_priority) ) ||
apply bertogna_cirinei_response_time_bound_fp with
(alpha := alpha) (alpha' := alpha')
(task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (job_deadline := job_deadline) (tsk := (TASK idx))
(job_task := job_task) (ts := ts) (hp_bounds := take idx hp_bounds)
- (higher_eq_priority := higher_priority); try (by ins).
+ (higher_eq_priority := higher_priority)); try (by ins).
{
cut (NTH idx \in hp_bounds = true); [intros IN | by apply mem_nth].
by rewrite set_mem -UNZIP; apply/mapP; exists (TASK idx, RESP idx); rewrite PAIR.
diff --git a/classic/analysis/apa/bertogna_fp_theory.v b/classic/analysis/apa/bertogna_fp_theory.v
index f3ae2bcbca64abee757784a4419b723e1680fdf2..63b395a8f533543856fb85ac7723f90eebd9180f 100644
--- a/classic/analysis/apa/bertogna_fp_theory.v
+++ b/classic/analysis/apa/bertogna_fp_theory.v
@@ -229,8 +229,10 @@ Module ResponseTimeAnalysisFP.
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.
- by apply workload_bounded_by_W with (task_deadline := task_deadline) (arr_seq := arr_seq)
- (job_arrival := job_arrival) (job_cost := job_cost) (job_deadline := job_deadline);
+ by ( try ( apply workload_bounded_by_W with (task_deadline0 := task_deadline) (arr_seq0 := arr_seq)
+ (job_arrival0 := job_arrival) (job_cost0 := job_cost) (job_deadline0 := job_deadline) ) ||
+ apply workload_bounded_by_W with (task_deadline := task_deadline) (arr_seq := arr_seq)
+ (job_arrival := job_arrival) (job_cost := job_cost) (job_deadline := job_deadline));
try (by ins); last 2 first;
[ by ins; apply GE_COST
| by ins; apply NOMISS
@@ -311,14 +313,17 @@ Module ResponseTimeAnalysisFP.
by apply/existsP; exists cpu.
clear SCHED; rename SCHED' into SCHED.
move: (SCHED) => PENDING.
+ ( try ( apply scheduled_implies_pending with (job_arrival0 := job_arrival)
+ (job_cost0 := job_cost) in PENDING ) ||
apply scheduled_implies_pending with (job_arrival := job_arrival)
- (job_cost := job_cost) in PENDING; try (by done).
+ (job_cost := job_cost) in PENDING); try (by done).
destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
{
move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
specialize (BEFOREok j_other ARRother SAMEtsk BEFOREother).
move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
- apply completion_monotonic with (t := job_arrival j_other + R); try (by done).
+ ( try ( apply completion_monotonic with (t0 := job_arrival j_other + R) ) ||
+ apply completion_monotonic with (t := job_arrival j_other + R)); try (by done).
apply leq_trans with (n := job_arrival j); last by done.
apply leq_trans with (n := job_arrival j_other + task_deadline tsk);
first by rewrite leq_add2l; apply NOMISS.
@@ -571,10 +576,14 @@ Module ResponseTimeAnalysisFP.
by apply/existsP; exists cpu2; rewrite /scheduled_on -SCHED2.
}
+ ( try ( apply platform_fp_no_multiple_jobs_of_interfering_tasks with
+ (arr_seq0 := arr_seq) (task_period0 := task_period) (tsk0 := tsk) (alpha0 := alpha)
+ (job_arrival0 := job_arrival) (higher_eq_priority0 := higher_eq_priority) (t0 := t)
+ (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) ) ||
apply platform_fp_no_multiple_jobs_of_interfering_tasks with
(arr_seq := arr_seq) (task_period := task_period) (tsk := tsk) (alpha := alpha)
(job_arrival := job_arrival) (higher_eq_priority := higher_eq_priority) (t := t)
- (job_cost := job_cost) (job_task := job_task) (sched := sched);
+ (job_cost := job_cost) (job_task := job_task) (sched := sched));
rewrite ?JOBtsk ?SAMEtsk //.
{
by intros j0 tsk0 TSK0 LE; subst tsk0; apply COMP.
@@ -630,14 +639,20 @@ Module ResponseTimeAnalysisFP.
by apply/existsP; exists cpu; rewrite /scheduled_on -SCHED'.
}
move: (SCHEDULED') => PENDING'.
+ ( try ( apply scheduled_implies_pending with (job_cost0 := job_cost)
+ (job_arrival0 := job_arrival) in PENDING' ) ||
apply scheduled_implies_pending with (job_cost := job_cost)
- (job_arrival := job_arrival) in PENDING'; try by done.
+ (job_arrival := job_arrival) in PENDING'); try by done.
assert (BUG: j' = j).
{
+ ( try ( apply platform_fp_no_multiple_jobs_of_tsk with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline)
+ (job_arrival0 := job_arrival) (job_cost0 := job_cost) (job_task0 := job_task)
+ (arr_seq0 := arr_seq) (sched0 := sched) (tsk0 := tsk) (t0 := t) ) ||
apply platform_fp_no_multiple_jobs_of_tsk with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline)
(job_arrival := job_arrival) (job_cost := job_cost) (job_task := job_task)
- (arr_seq := arr_seq) (sched := sched) (tsk := tsk) (t := t);
+ (arr_seq := arr_seq) (sched := sched) (tsk := tsk) (t := t) );
try (by done);
[by apply PARAMS | by apply/andP; split | |].
{
@@ -647,7 +662,8 @@ Module ResponseTimeAnalysisFP.
}
{
intros j0 JOB0 ARR0 LT0.
- apply completion_monotonic with (t := job_arrival j0 + R); [| by apply BEFOREok].
+ ( try ( apply completion_monotonic with (t0 := job_arrival j0 + R) ) ||
+ apply completion_monotonic with (t := job_arrival j0 + R)); [| by apply BEFOREok].
by rewrite leq_add2l; apply leq_trans with (n := task_deadline tsk);
last by apply CONSTR; rewrite -JOBtsk FROMTS.
}
@@ -748,10 +764,14 @@ Module ResponseTimeAnalysisFP.
apply scheduled_implies_pending; try by done.
by apply/existsP; exists cpu'; rewrite /scheduled_on -SCHED2.
}
+ ( try ( apply platform_fp_no_multiple_jobs_of_interfering_tasks with
+ (arr_seq0 := arr_seq) (task_period0 := task_period) (tsk0 := tsk) (alpha0 := alpha)
+ (job_arrival0 := job_arrival) (higher_eq_priority0 := higher_eq_priority) (t0 := t)
+ (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) ) ||
apply platform_fp_no_multiple_jobs_of_interfering_tasks with
(arr_seq := arr_seq) (task_period := task_period) (tsk := tsk) (alpha := alpha)
(job_arrival := job_arrival) (higher_eq_priority := higher_eq_priority) (t := t)
- (job_cost := job_cost) (job_task := job_task) (sched := sched); try (by done);
+ (job_cost := job_cost) (job_task := job_task) (sched := sched)); try (by done);
rewrite ?JOBtsk ?SAMEtsk //.
{
by intros j0 tsk0 TSK0 LE; subst tsk0; apply COMP.
@@ -1047,3 +1067,4 @@ Module ResponseTimeAnalysisFP.
End ResponseTimeBound.
End ResponseTimeAnalysisFP.
+
diff --git a/classic/analysis/apa/interference_bound_edf.v b/classic/analysis/apa/interference_bound_edf.v
index 0d1e1d77908f6a6c34d6da9cfaebea69da57dfc0..8b10fba0ed7471d16cb9347e8afff3dd7f7305cc 100644
--- a/classic/analysis/apa/interference_bound_edf.v
+++ b/classic/analysis/apa/interference_bound_edf.v
@@ -329,6 +329,9 @@ Module InterferenceBoundEDF.
specialize (PARAMS j ARRj); des.
apply leq_trans with (n := service_during sched j t1 t2);
first by apply job_interference_le_service.
+ try ( by apply cumulative_service_le_task_cost with (job_task0 := job_task)
+ (task_deadline0 := task_deadline) (job_cost0 := job_cost)
+ (job_deadline0 := job_deadline) ) ||
by apply cumulative_service_le_task_cost with (job_task := job_task)
(task_deadline := task_deadline) (job_cost := job_cost)
(job_deadline := job_deadline).
@@ -425,6 +428,8 @@ Module InterferenceBoundEDF.
rewrite -leqn0; apply leq_trans with (n := service_during sched j_fst t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
+ try ( by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k)
+ (job_arrival0 := job_arrival); try (by done); apply ltnW ) ||
by apply cumulative_service_after_job_rt_zero with (job_cost := job_cost) (R := R_k)
(job_arrival := job_arrival); try (by done); apply ltnW.
Qed.
@@ -473,6 +478,8 @@ Module InterferenceBoundEDF.
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 [FSTarr [_ [ LEdl _]]].
+ try ( apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl; try (by done).
destruct (D_k - R_k <= D_i) eqn:LEdk; last first.
@@ -493,6 +500,8 @@ Module InterferenceBoundEDF.
apply leq_trans with (n := service_during sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service.
unfold service_during; rewrite leqn0; apply/eqP.
+ try ( by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k)
+ (job_arrival0 := job_arrival); try (by done); apply leqnn ) ||
by apply cumulative_service_after_job_rt_zero with (job_cost := job_cost) (R := R_k)
(job_arrival := job_arrival); try (by done); apply leqnn.
}
@@ -592,6 +601,8 @@ 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.
+ try ( apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in BUG; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in BUG; try (by done).
rewrite interference_bound_edf_j_fst_deadline
@@ -636,6 +647,8 @@ 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.
+ try ( by apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl ) ||
by apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl.
Qed.
@@ -739,6 +752,7 @@ Module InterferenceBoundEDF.
apply leq_trans with (n := service_during sched j_lst t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP; unfold service_during.
+ try ( by apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival) ) ||
by apply cumulative_service_before_job_arrival_zero with (job_arrival := job_arrival).
Qed.
@@ -763,6 +777,7 @@ Module InterferenceBoundEDF.
sched j_snd t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
+ try ( by apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival) ) ||
by apply cumulative_service_before_job_arrival_zero with (job_arrival := job_arrival).
}
apply leq_trans with (n := a_fst + p_k).
@@ -859,6 +874,8 @@ Module InterferenceBoundEDF.
}
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [LSTarr [_ [ LEdl _]]].
+ try ( apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl; try (by done).
unfold D_i, D_k in DIST; rewrite interference_bound_edf_j_lst_deadline
@@ -944,6 +961,8 @@ Module InterferenceBoundEDF.
destruct LST as [LSTarr [_ [ LSTserv _]]].
unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
-interference_bound_edf_j_i_deadline.
+ try ( by apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LSTserv ) ||
by apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LSTserv.
Qed.
@@ -989,8 +1008,10 @@ Module InterferenceBoundEDF.
apply leq_trans with (n := service_during sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
+ (try ( apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k)
+ (job_arrival0 := job_arrival) ) ||
apply cumulative_service_after_job_rt_zero with (job_cost := job_cost) (R := R_k)
- (job_arrival := job_arrival); [ by done | | by apply leqnn].
+ (job_arrival := job_arrival)); [ by done | | by apply leqnn].
by apply interference_bound_edf_j_fst_completed_on_time.
}
Qed.
@@ -1066,6 +1087,8 @@ Module InterferenceBoundEDF.
destruct LST as [LSTarr [_ [ LSTserv _]]].
unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
-interference_bound_edf_j_i_deadline.
+ try ( by apply interference_under_edf_implies_shorter_deadlines
+ with (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LSTserv ) ||
by apply interference_under_edf_implies_shorter_deadlines
with (arr_seq := arr_seq) (job_deadline := job_deadline) in LSTserv.
Qed.
diff --git a/classic/analysis/apa/workload_bound.v b/classic/analysis/apa/workload_bound.v
index d6db90a79b310771b1a684a0f3b4a63e11003f89..9bd2aef4cb190275588b05be16c0aece6ce641fc 100644
--- a/classic/analysis/apa/workload_bound.v
+++ b/classic/analysis/apa/workload_bound.v
@@ -416,6 +416,7 @@ Module WorkloadBound.
}
instantiate (1 := elem); move => [LSTarr [LSTtsk [/eqP LSTserv LSTin]]].
unfold service_during; apply LSTserv.
+ try ( by apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival) ) ||
by apply cumulative_service_before_job_arrival_zero with (job_arrival := job_arrival).
Qed.
@@ -656,6 +657,9 @@ Module WorkloadBound.
have INlst := workload_bound_j_lst_is_job_of_tsk; des.
have PARAMSfst := JOBPARAMS j_fst INfst; des.
have PARAMSlst := JOBPARAMS j_lst INlst; des.
+ try ( by apply leq_add; apply cumulative_service_le_task_cost with
+ (task_deadline0 := task_deadline)
+ (job_cost0 := job_cost) (job_deadline0 := job_deadline) (job_task0 := job_task) ) ||
by apply leq_add; apply cumulative_service_le_task_cost with
(task_deadline := task_deadline)
(job_cost := job_cost) (job_deadline := job_deadline) (job_task := job_task).
diff --git a/classic/analysis/global/basic/bertogna_edf_theory.v b/classic/analysis/global/basic/bertogna_edf_theory.v
index d31bb7f9e29ffa64382e57471ce6eb7db49f719e..b3a6b86786b0f88d519ae7962fedf45de3d4f72f 100644
--- a/classic/analysis/global/basic/bertogna_edf_theory.v
+++ b/classic/analysis/global/basic/bertogna_edf_theory.v
@@ -194,8 +194,10 @@ Module ResponseTimeAnalysisEDF.
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.
- by apply workload_bounded_by_W with (task_deadline := task_deadline) (arr_seq := arr_seq)
- (job_arrival := job_arrival) (job_cost := job_cost) (job_deadline := job_deadline);
+ by ( try ( apply workload_bounded_by_W with (task_deadline0 := task_deadline) (arr_seq0 := arr_seq)
+ (job_arrival0 := job_arrival) (job_cost0 := job_cost) (job_deadline0 := job_deadline) ) ||
+ apply workload_bounded_by_W with (task_deadline := task_deadline) (arr_seq := arr_seq)
+ (job_arrival := job_arrival) (job_cost := job_cost) (job_deadline := job_deadline));
try (by ins); last 2 first;
[ by apply bertogna_edf_R_other_ge_cost
| by ins; apply NOMISS
@@ -208,8 +210,10 @@ Module ResponseTimeAnalysisEDF.
Lemma bertogna_edf_specific_bound_holds :
x tsk_other <= edf_specific_bound tsk_other R_other.
Proof.
+ ( try ( apply interference_bound_edf_bounds_interference with (job_deadline0 := job_deadline)
+ (arr_seq0 := arr_seq) (ts0 := ts); try (by done) ) ||
apply interference_bound_edf_bounds_interference with (job_deadline := job_deadline)
- (arr_seq := arr_seq) (ts := ts); try (by done);
+ (arr_seq := arr_seq) (ts := ts); try (by done));
[ by apply bertogna_edf_tsk_other_in_ts
| by apply H_tasks_miss_no_deadlines
| ].
@@ -288,6 +292,8 @@ Module ResponseTimeAnalysisEDF.
by apply/existsP; exists cpu.
clear SCHED; rename SCHED' into SCHED.
move: (SCHED) => PENDING.
+ try ( apply scheduled_implies_pending with (job_cost0 := job_cost) (job_arrival0 := job_arrival)
+ in PENDING; try (by done) ) ||
apply scheduled_implies_pending with (job_cost := job_cost) (job_arrival := job_arrival)
in PENDING; try (by done).
destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
@@ -295,6 +301,7 @@ Module ResponseTimeAnalysisEDF.
move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
specialize (BEFOREok j_other tsk R ARRother SAMEtsk INbounds LT).
move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
+ try ( apply completion_monotonic with (t0 := job_arrival j_other + R); try (by done) ) ||
apply completion_monotonic with (t := job_arrival j_other + R); try (by done).
apply leq_trans with (n := job_arrival j); last by done.
apply leq_trans with (n := job_arrival j_other + task_deadline tsk);
@@ -340,6 +347,7 @@ Module ResponseTimeAnalysisEDF.
intros t j0 ARR0 LEt LE.
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'.
+ try ( apply completion_monotonic with (t0 := job_arrival j0 + R0) ) ||
apply completion_monotonic with (t := job_arrival j0 + R0).
{
rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
@@ -385,6 +393,7 @@ Module ResponseTimeAnalysisEDF.
intros j0 tsk0 ARR0 TSK0 LE.
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'.
+ try ( apply completion_monotonic with (t0 := job_arrival j0 + R0); try (by done) ) ||
apply completion_monotonic with (t := job_arrival j0 + R0); try (by done).
{
rewrite leq_add2l TSK0.
@@ -536,10 +545,14 @@ Module ResponseTimeAnalysisEDF.
}
assert (BUG: j1 = j2).
{
+ ( try ( apply platform_at_most_one_pending_job_of_each_task with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (tsk0 := tsk)
+ (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) (j0 := j) (t0 := t)
+ (job_arrival0 := job_arrival) (arr_seq0 := arr_seq) ) ||
apply platform_at_most_one_pending_job_of_each_task with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline) (tsk := tsk)
(job_cost := job_cost) (job_task := job_task) (sched := sched) (j := j) (t := t)
- (job_arrival := job_arrival) (arr_seq := arr_seq);
+ (job_arrival := job_arrival) (arr_seq := arr_seq));
rewrite ?JOBtsk ?SAMEtsk //; first by apply PARAMS; rewrite -JOBtsk FROMTS.
intros j0 tsk0 ARR0 TSK0 LE.
by apply (COMP t); rewrite ?TSK0.
diff --git a/classic/analysis/global/basic/bertogna_fp_comp.v b/classic/analysis/global/basic/bertogna_fp_comp.v
index 5d6497f181c6366ba819c7d9ae65d3262d1c6ea1..c2cd7bc75761f6bd5ba4c1c5dee7605d8e2f39ec 100644
--- a/classic/analysis/global/basic/bertogna_fp_comp.v
+++ b/classic/analysis/global/basic/bertogna_fp_comp.v
@@ -598,11 +598,16 @@ Module ResponseTimeIterationFP.
}
intros [_ [_ [REC DL]]].
+ ( try ( apply bertogna_cirinei_response_time_bound_fp with
+ (task_cost0 := task_cost) (task_period0 := task_period)
+ (task_deadline0 := task_deadline) (job_deadline0 := job_deadline) (tsk0 := (TASK idx))
+ (job_task0 := job_task) (ts0 := ts) (hp_bounds0 := take idx hp_bounds)
+ (higher_eq_priority := higher_priority) ) ||
apply bertogna_cirinei_response_time_bound_fp with
(task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (job_deadline := job_deadline) (tsk := (TASK idx))
(job_task := job_task) (ts := ts) (hp_bounds := take idx hp_bounds)
- (higher_eq_priority := higher_priority); try (by done).
+ (higher_eq_priority := higher_priority) ); try (by done).
{
cut (NTH idx \in hp_bounds = true); [intros IN | by apply mem_nth].
by rewrite set_mem -UNZIP; apply/mapP; exists (TASK idx, RESP idx); rewrite PAIR.
diff --git a/classic/analysis/global/basic/bertogna_fp_theory.v b/classic/analysis/global/basic/bertogna_fp_theory.v
index cd2a14bf667ced006170179b297f7094539e97a0..226c0fec894f68eb264dccf2114f59097b2bfb91 100644
--- a/classic/analysis/global/basic/bertogna_fp_theory.v
+++ b/classic/analysis/global/basic/bertogna_fp_theory.v
@@ -213,8 +213,10 @@ Module ResponseTimeAnalysisFP.
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.
- by apply workload_bounded_by_W with (task_deadline := task_deadline) (arr_seq := arr_seq)
- (job_arrival := job_arrival) (job_cost := job_cost) (job_deadline := job_deadline);
+ by ( try ( apply workload_bounded_by_W with (task_deadline0 := task_deadline) (arr_seq0 := arr_seq)
+ (job_arrival0 := job_arrival) (job_cost0 := job_cost) (job_deadline0 := job_deadline) ) ||
+ apply workload_bounded_by_W with (task_deadline := task_deadline) (arr_seq := arr_seq)
+ (job_arrival := job_arrival) (job_cost := job_cost) (job_deadline := job_deadline));
try (by ins); last 2 first;
[ by ins; apply GE_COST
| by ins; apply NOMISS
@@ -295,6 +297,8 @@ Module ResponseTimeAnalysisFP.
by apply/existsP; exists cpu.
clear SCHED; rename SCHED' into SCHED.
move: (SCHED) => PENDING.
+ try ( apply scheduled_implies_pending with (job_arrival0 := job_arrival)
+ (job_cost0 := job_cost) in PENDING; try (by done) ) ||
apply scheduled_implies_pending with (job_arrival := job_arrival)
(job_cost := job_cost) in PENDING; try (by done).
destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
@@ -302,6 +306,7 @@ Module ResponseTimeAnalysisFP.
move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
specialize (PREV j_other ARRother SAMEtsk BEFOREother).
move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
+ try ( apply completion_monotonic with (t0 := job_arrival j_other + R); try (by done) ) ||
apply completion_monotonic with (t := job_arrival j_other + R); try (by done).
apply leq_trans with (n := job_arrival j); last by done.
apply leq_trans with (n := job_arrival j_other + task_deadline tsk);
@@ -350,10 +355,14 @@ Module ResponseTimeAnalysisFP.
H_response_time_of_interfering_tasks_is_known into PREV.
unfold sporadic_task_model, is_response_time_bound_of_task in *.
move => t /andP [LEt LTt] BACK.
+ (try ( apply platform_fp_cpus_busy_with_interfering_tasks with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (job_task0 := job_task)
+ (arr_seq0 := arr_seq) (ts0 := ts) (tsk0 := tsk) (higher_eq_priority0 := higher_eq_priority)
+ in BACK ) ||
apply platform_fp_cpus_busy_with_interfering_tasks with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline) (job_task := job_task)
(arr_seq := arr_seq) (ts := ts) (tsk := tsk) (higher_eq_priority := higher_eq_priority)
- in BACK; try (by done); first by apply PARAMS.
+ in BACK); try (by done); first by apply PARAMS.
{
apply leq_trans with (n := job_arrival j + R); first by done.
rewrite leq_add2l.
@@ -363,7 +372,8 @@ Module ResponseTimeAnalysisFP.
intros j_other tsk_other ARRother JOBother INTERF.
feed (HAS tsk_other); first by rewrite -JOBother FROMTS.
move: (HAS INTERF) => [R' IN].
- apply completion_monotonic with (t := job_arrival j_other + R'); try (by done);
+ ( try ( apply completion_monotonic with (t0 := job_arrival j_other + R'); try (by done) ) ||
+ apply completion_monotonic with (t := job_arrival j_other + R'); try (by done));
last by apply PREV with (hp_tsk := tsk_other).
{
rewrite leq_add2l.
@@ -372,7 +382,8 @@ Module ResponseTimeAnalysisFP.
}
}
{
- ins; apply completion_monotonic with (t := job_arrival j0 + R); try (by done);
+ ins; ( try ( apply completion_monotonic with (t0 := job_arrival j0 + R) ) ||
+ apply completion_monotonic with (t := job_arrival j0 + R)); try (by done);
last by apply H_previous_jobs_of_tsk_completed.
rewrite leq_add2l.
by apply leq_trans with (n := task_deadline tsk); last by apply RESTR.
@@ -508,9 +519,12 @@ Module ResponseTimeAnalysisFP.
{
move: SAMEtsk => /eqP SAMEtsk.
move: (PENDING1) => SAMEjob.
+ ( try ( apply platform_fp_no_multiple_jobs_of_tsk with (task_cost0 := task_cost)
+ (arr_seq0 := arr_seq) (task_period0 := task_period) (task_deadline0 := task_deadline)
+ (job_task0 := job_task) (tsk0 := tsk) (j0 := j) in SAMEjob ) ||
apply platform_fp_no_multiple_jobs_of_tsk with (task_cost := task_cost)
(arr_seq := arr_seq) (task_period := task_period) (task_deadline := task_deadline)
- (job_task := job_task) (tsk := tsk) (j := j) in SAMEjob; try (by done);
+ (job_task := job_task) (tsk := tsk) (j := j) in SAMEjob); try (by done);
[ | by apply PARAMS | |]; last 2 first.
{
apply (leq_trans LTt); rewrite leq_add2l.
@@ -518,7 +532,8 @@ Module ResponseTimeAnalysisFP.
}
{
intros j0 ARR0 JOB0 LT0.
- apply completion_monotonic with (t := job_arrival j0 + R); try (by done);
+ ( try ( apply completion_monotonic with (t0 := job_arrival j0 + R) ) ||
+ apply completion_monotonic with (t := job_arrival j0 + R)); try (by done);
last by apply BEFOREok.
rewrite leq_add2l.
by apply leq_trans with (n := task_deadline tsk); last by apply CONSTR.
@@ -533,16 +548,21 @@ Module ResponseTimeAnalysisFP.
rewrite -JOBtsk; apply FP with (t := t); try (by done).
by apply/existsP; exists cpu; apply/eqP.
}
+ ( try ( apply platform_fp_no_multiple_jobs_of_interfering_tasks with
+ (job_arrival0 := job_arrival) (arr_seq0 := arr_seq) (task_period0 := task_period)
+ (tsk0 := tsk) (higher_eq_priority0 := higher_eq_priority)
+ (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) (t0 := t) ) ||
apply platform_fp_no_multiple_jobs_of_interfering_tasks with
(job_arrival := job_arrival) (arr_seq := arr_seq) (task_period := task_period)
(tsk := tsk) (higher_eq_priority := higher_eq_priority)
- (job_cost := job_cost) (job_task := job_task) (sched := sched) (t := t);
+ (job_cost := job_cost) (job_task := job_task) (sched := sched) (t := t));
rewrite ?JOBtsk ?SAMEtsk //.
{
intros j0 tsk0 ARR0 JOB0 INTERF0.
feed (HASHP tsk0); first by rewrite -JOB0 FROMTS.
move: (HASHP INTERF0) => [R0 IN0].
- apply completion_monotonic with (t := job_arrival j0 + R0); try (by done);
+ ( try ( apply completion_monotonic with (t0 := job_arrival j0 + R0); try (by done) ) ||
+ apply completion_monotonic with (t := job_arrival j0 + R0); try (by done));
last by eapply H_response_time_of_interfering_tasks_is_known; first by apply IN0.
rewrite leq_add2l.
by apply leq_trans with (n := task_deadline tsk0);
diff --git a/classic/analysis/global/basic/interference_bound_edf.v b/classic/analysis/global/basic/interference_bound_edf.v
index dc63774995adaa098bee730aaca55e067fe9c70c..c7acc1cbabbc23946c94eb4fa7c44535afe1bbcf 100644
--- a/classic/analysis/global/basic/interference_bound_edf.v
+++ b/classic/analysis/global/basic/interference_bound_edf.v
@@ -316,8 +316,10 @@ Module InterferenceBoundEDF.
move => [ARRj [TSKj _]].
apply leq_trans with (n := service_during sched j t1 t2);
first by apply job_interference_le_service.
+ ( try ( apply cumulative_service_le_task_cost with (job_task0 := job_task)
+ (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline) ) ||
apply cumulative_service_le_task_cost with (job_task := job_task)
- (task_deadline := task_deadline) (job_cost := job_cost) (job_deadline := job_deadline);
+ (task_deadline := task_deadline) (job_cost := job_cost) (job_deadline := job_deadline));
try (by done).
by apply PARAMS.
Qed.
@@ -413,6 +415,8 @@ Module InterferenceBoundEDF.
rewrite -leqn0; apply leq_trans with (n := service_during sched j_fst t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
+ try ( by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k)
+ (job_arrival0 := job_arrival); try (by done); apply ltnW ) ||
by apply cumulative_service_after_job_rt_zero with (job_cost := job_cost) (R := R_k)
(job_arrival := job_arrival); try (by done); apply ltnW.
Qed.
@@ -460,6 +464,8 @@ Module InterferenceBoundEDF.
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 [FSTarr [_ [ LEdl _]]].
+ try ( apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl; try (by done).
destruct (D_k - R_k <= D_i) eqn:LEdk; last first.
@@ -480,6 +486,8 @@ Module InterferenceBoundEDF.
apply leq_trans with (n := service_during sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service.
unfold service_during; rewrite leqn0; apply/eqP.
+ try ( by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k)
+ (job_arrival0 := job_arrival); try (by done); apply leqnn ) ||
by apply cumulative_service_after_job_rt_zero with (job_cost := job_cost) (R := R_k)
(job_arrival := job_arrival); try (by done); apply leqnn.
}
@@ -513,6 +521,8 @@ Module InterferenceBoundEDF.
by apply job_interference_le_service.
}
unfold service_during.
+ try ( rewrite -> cumulative_service_after_job_rt_zero with
+ (job_arrival0 := job_arrival) (job_cost0 := job_cost) (R := R_k); try (by done) ) ||
rewrite -> cumulative_service_after_job_rt_zero with
(job_arrival := job_arrival) (job_cost := job_cost) (R := R_k); try (by done).
rewrite addn0; apply extend_sum; first by apply leqnn.
@@ -530,6 +540,8 @@ Module InterferenceBoundEDF.
by apply job_interference_le_service.
}
unfold service_during.
+ try ( rewrite -> cumulative_service_after_job_rt_zero with
+ (job_arrival0 := job_arrival) (job_cost0 := job_cost) (R:=R_k); try (by done) ) ||
rewrite -> cumulative_service_after_job_rt_zero with
(job_arrival := job_arrival) (job_cost := job_cost) (R:=R_k); try (by done).
rewrite addn0.
@@ -587,6 +599,8 @@ Module InterferenceBoundEDF.
apply/eqP; rewrite -[_ _ _ _ == 0]negbK; apply/negP; red; intro BUG.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [FSTarr [_ [LEdl _]]].
+ try ( apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in BUG; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in BUG; try (by done).
rewrite interference_bound_edf_j_fst_deadline
@@ -631,6 +645,8 @@ 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.
+ try ( by apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl ) ||
by apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl.
Qed.
@@ -734,6 +750,7 @@ Module InterferenceBoundEDF.
apply leq_trans with (n := service_during sched j_lst t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP; unfold service_during.
+ try ( by apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival) ) ||
by apply cumulative_service_before_job_arrival_zero with (job_arrival := job_arrival).
Qed.
@@ -758,6 +775,7 @@ Module InterferenceBoundEDF.
sched j_snd t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
+ try ( by apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival) ) ||
by apply cumulative_service_before_job_arrival_zero with (job_arrival := job_arrival).
}
apply leq_trans with (n := a_fst + p_k).
@@ -854,6 +872,8 @@ Module InterferenceBoundEDF.
}
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [LSTarr [_ [ LEdl _]]].
+ try ( apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl; try (by done).
unfold D_i, D_k in DIST; rewrite interference_bound_edf_j_lst_deadline
@@ -939,6 +959,8 @@ Module InterferenceBoundEDF.
destruct LST as [LSTarr [_ [ LSTserv _]]].
unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
-interference_bound_edf_j_i_deadline.
+ try ( by apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LSTserv ) ||
by apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LSTserv.
Qed.
@@ -984,8 +1006,10 @@ Module InterferenceBoundEDF.
apply leq_trans with (n := service_during sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
+ (try ( apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k)
+ (job_arrival0 := job_arrival) ) ||
apply cumulative_service_after_job_rt_zero with (job_cost := job_cost) (R := R_k)
- (job_arrival := job_arrival); [ by done | | by apply leqnn].
+ (job_arrival := job_arrival)); [ by done | | by apply leqnn].
by apply interference_bound_edf_j_fst_completed_on_time.
}
Qed.
@@ -1061,6 +1085,8 @@ Module InterferenceBoundEDF.
destruct LST as [LSTarr [_ [ LSTserv _]]].
unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
-interference_bound_edf_j_i_deadline.
+ try ( by apply interference_under_edf_implies_shorter_deadlines
+ with (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LSTserv ) ||
by apply interference_under_edf_implies_shorter_deadlines
with (arr_seq := arr_seq) (job_deadline := job_deadline) in LSTserv.
Qed.
diff --git a/classic/analysis/global/basic/workload_bound.v b/classic/analysis/global/basic/workload_bound.v
index 5ea1e680a27801574eaed7eafe43b8cd367dcd92..e0806cef23dc937bfc1cf9882d608f9ed848fec9 100644
--- a/classic/analysis/global/basic/workload_bound.v
+++ b/classic/analysis/global/basic/workload_bound.v
@@ -418,6 +418,7 @@ Module WorkloadBound.
}
instantiate (1 := elem); move => [LSTarr [LSTtsk [/eqP LSTserv LSTin]]].
unfold service_during; apply LSTserv.
+ try ( by apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival) ) ||
by apply cumulative_service_before_job_arrival_zero with (job_arrival := job_arrival).
Qed.
@@ -657,6 +658,9 @@ Module WorkloadBound.
by rewrite H_at_least_two_jobs.
have INfst := workload_bound_j_fst_is_job_of_tsk SIZE elem;
have INlst := workload_bound_j_lst_is_job_of_tsk; des.
+ try ( by apply leq_add; apply cumulative_service_le_task_cost with
+ (task_deadline0 := task_deadline) (job_cost0 := job_cost)
+ (job_deadline0 := job_deadline) (job_task0 := job_task); eauto 2 ) ||
by apply leq_add; apply cumulative_service_le_task_cost with
(task_deadline := task_deadline) (job_cost := job_cost)
(job_deadline := job_deadline) (job_task := job_task); eauto 2.
diff --git a/classic/analysis/global/jitter/bertogna_edf_theory.v b/classic/analysis/global/jitter/bertogna_edf_theory.v
index 91c6d1252fd33951c326b6cda5256ffc484e4e27..dcbf04c18afac9239d0473e1e91e39e4de7e08a7 100644
--- a/classic/analysis/global/jitter/bertogna_edf_theory.v
+++ b/classic/analysis/global/jitter/bertogna_edf_theory.v
@@ -225,8 +225,10 @@ Module ResponseTimeAnalysisEDFJitter.
Lemma bertogna_edf_specific_bound_holds :
x tsk_other <= edf_specific_bound tsk_other R_other.
Proof.
- by apply interference_bound_edf_bounds_interference with (job_deadline := job_deadline)
- (arr_seq := arr_seq) (ts := ts); try (by done);
+ by ( try ( apply interference_bound_edf_bounds_interference with (job_deadline0 := job_deadline)
+ (arr_seq0 := arr_seq) (ts0 := ts) ) ||
+ apply interference_bound_edf_bounds_interference with (job_deadline := job_deadline)
+ (arr_seq := arr_seq) (ts := ts)); try (by done);
[ by apply bertogna_edf_tsk_other_in_ts
| by apply H_tasks_miss_no_deadlines
| by ins; apply H_all_previous_jobs_completed_on_time with (tsk_other := tsk_other)].
@@ -307,8 +309,10 @@ Module ResponseTimeAnalysisEDFJitter.
have ARRother: arrives_in arr_seq j_other.
by apply (H_jobs_come_from_arrival_sequence j_other t).
move: (SCHED) => PENDING.
+ ( try ( apply scheduled_implies_pending with (job_cost0 := job_cost) (job_jitter0 := job_jitter)
+ (job_arrival0 := job_arrival) in PENDING ) ||
apply scheduled_implies_pending with (job_cost := job_cost) (job_jitter := job_jitter)
- (job_arrival := job_arrival) in PENDING; try (by done).
+ (job_arrival := job_arrival) in PENDING); try (by done).
destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
{
move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
@@ -319,7 +323,8 @@ Module ResponseTimeAnalysisEDFJitter.
}
intros COMP.
move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
- apply completion_monotonic with (t := job_arrival j_other + task_jitter tsk + R);
+ ( try ( apply completion_monotonic with (t0 := job_arrival j_other + task_jitter tsk + R) ) ||
+ apply completion_monotonic with (t := job_arrival j_other + task_jitter tsk + R));
try by done.
apply leq_trans with (n := job_arrival j);
last by apply leq_trans with (n := t1); [by apply leq_addr | by done].
@@ -379,6 +384,7 @@ Module ResponseTimeAnalysisEDFJitter.
intros t j0 LEt ARR0 LE.
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'.
+ try ( apply completion_monotonic with (t0 := job_arrival j0 + task_jitter (job_task j0) + R0) ) ||
apply completion_monotonic with (t := job_arrival j0 + task_jitter (job_task j0) + R0).
{
rewrite -addnA leq_add2l.
@@ -433,6 +439,7 @@ Module ResponseTimeAnalysisEDFJitter.
intros j0 tsk0 ARR0 TSK0 LE.
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'.
+ try ( apply completion_monotonic with (t0 := job_arrival j0 + task_jitter tsk0 + R0); try (by done) ) ||
apply completion_monotonic with (t := job_arrival j0 + task_jitter tsk0 + R0); try (by done).
{
rewrite -addnA leq_add2l TSK0.
@@ -577,11 +584,16 @@ Module ResponseTimeAnalysisEDFJitter.
}
assert (BUG: j1 = j2).
{
+ ( try ( apply platform_at_most_one_pending_job_of_each_task with (task_cost0 := task_cost)
+ (job_jitter0 := job_jitter) (task_period0 := task_period) (job_cost0 := job_cost)
+ (task_deadline0 := task_deadline) (tsk0 := tsk) (job_task0 := job_task)
+ (sched0 := sched) (job_arrival0 := job_arrival) (arr_seq0 := arr_seq)
+ (j0 := j) (t0 := t) ) ||
apply platform_at_most_one_pending_job_of_each_task with (task_cost := task_cost)
(job_jitter := job_jitter) (task_period := task_period) (job_cost := job_cost)
(task_deadline := task_deadline) (tsk := tsk) (job_task := job_task)
(sched := sched) (job_arrival := job_arrival) (arr_seq := arr_seq)
- (j := j) (t := t);
+ (j := j) (t := t));
rewrite ?JOBtsk ?SAMEtsk //; first by apply PARAMS; rewrite -JOBtsk FROMTS.
by intros j0 tsk0 ARR0 TSK0 LE; apply (COMP t); rewrite ?TSK0.
}
diff --git a/classic/analysis/global/jitter/bertogna_fp_comp.v b/classic/analysis/global/jitter/bertogna_fp_comp.v
index d2aeef9dc46165880847442b9cb831065b280096..3982a2438da4a15d6922afbdf58f8191bb4d0c3b 100644
--- a/classic/analysis/global/jitter/bertogna_fp_comp.v
+++ b/classic/analysis/global/jitter/bertogna_fp_comp.v
@@ -607,6 +607,11 @@ Module ResponseTimeIterationFP.
}
intros [_ [_ [REC DL]]].
+ try ( apply bertogna_cirinei_response_time_bound_fp with
+ (task_cost0 := task_cost) (task_period0 := task_period)
+ (task_deadline0 := task_deadline) (job_deadline0 := job_deadline) (tsk0 := (TASK idx))
+ (job_task0 := job_task) (ts0 := ts) (hp_bounds0 := take idx hp_bounds)
+ (job_jitter0 := job_jitter) (higher_eq_priority := higher_priority); try (by done) ) ||
apply bertogna_cirinei_response_time_bound_fp with
(task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (job_deadline := job_deadline) (tsk := (TASK idx))
diff --git a/classic/analysis/global/jitter/bertogna_fp_theory.v b/classic/analysis/global/jitter/bertogna_fp_theory.v
index 6d290d6b55de6fd486d2a98edad8dc8d675b670c..6326824745d4754c3194e55e8faf9bfc468581ad 100644
--- a/classic/analysis/global/jitter/bertogna_fp_theory.v
+++ b/classic/analysis/global/jitter/bertogna_fp_theory.v
@@ -225,6 +225,9 @@ Module ResponseTimeAnalysisFP.
}
apply leq_trans with (n := workload job_task sched tsk_other t1 (t1 + R));
first by apply task_interference_le_workload.
+ try ( apply workload_bounded_by_W with (task_deadline0 := task_deadline)
+ (job_arrival0 := job_arrival) (arr_seq0 := arr_seq)
+ (job_jitter0 := job_jitter) (job_cost0 := job_cost) (job_deadline0 := job_deadline) ) ||
apply workload_bounded_by_W with (task_deadline := task_deadline)
(job_arrival := job_arrival) (arr_seq := arr_seq)
(job_jitter := job_jitter) (job_cost := job_cost) (job_deadline := job_deadline);
@@ -310,6 +313,8 @@ Module ResponseTimeAnalysisFP.
have SCHED': scheduled sched j_other t by apply/existsP; exists cpu.
clear SCHED; rename SCHED' into SCHED.
move: (SCHED) => PENDING.
+ try ( apply scheduled_implies_pending with (job_arrival0 := job_arrival)
+ (job_cost0 := job_cost) (job_jitter0 := job_jitter) in PENDING; try (by done) ) ||
apply scheduled_implies_pending with (job_arrival := job_arrival)
(job_cost := job_cost) (job_jitter := job_jitter) in PENDING; try (by done).
destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
@@ -317,6 +322,7 @@ Module ResponseTimeAnalysisFP.
move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
specialize (PREV j_other ARRother SAMEtsk BEFOREother).
move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
+ try ( apply completion_monotonic with (t0 := job_arrival j_other + task_jitter tsk + R) ) ||
apply completion_monotonic with (t := job_arrival j_other + task_jitter tsk + R);
try by done.
apply leq_trans with (n := job_arrival j);
@@ -380,10 +386,14 @@ Module ResponseTimeAnalysisFP.
valid_sporadic_job_with_jitter in *.
move => t /andP [LEt LTt] BACK.
+ ( try ( apply platform_fp_cpus_busy_with_interfering_tasks with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (job_task0 := job_task)
+ (ts0 := ts) (tsk0 := tsk) (higher_eq_priority0 := higher_eq_priority) (arr_seq0 := arr_seq)
+ in BACK ) ||
apply platform_fp_cpus_busy_with_interfering_tasks with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline) (job_task := job_task)
(ts := ts) (tsk := tsk) (higher_eq_priority := higher_eq_priority) (arr_seq := arr_seq)
- in BACK; try (by done); first by apply PARAMS; rewrite -JOBtsk FROMTS.
+ in BACK); try (by done); first by apply PARAMS; rewrite -JOBtsk FROMTS.
{
apply leq_trans with (n := job_arrival j + job_jitter j + R); first by done.
rewrite -addnA leq_add2l.
@@ -395,13 +405,15 @@ Module ResponseTimeAnalysisFP.
intros j_other tsk_other ARRother JOBother INTERF.
feed (HAS tsk_other); first by rewrite -JOBother FROMTS.
move: (HAS INTERF) => [R' IN].
+ try ( apply completion_monotonic with (t0 := job_arrival j_other + task_jitter tsk_other + R') ) ||
apply completion_monotonic with (t := job_arrival j_other + task_jitter tsk_other + R');
try (by done); last by rewrite -addnA; apply PREV.
rewrite -addnA leq_add2l; apply leq_trans with (n := task_deadline tsk_other);
[by apply NOMISS | by apply RESTR; rewrite -JOBother; apply FROMTS].
}
{
- ins; apply completion_monotonic with (t := job_arrival j0 + task_jitter tsk + R);
+ ins; ( try ( apply completion_monotonic with (t0 := job_arrival j0 + task_jitter tsk + R) ) ||
+ apply completion_monotonic with (t := job_arrival j0 + task_jitter tsk + R));
try (by done); last by apply PREVtsk.
rewrite -addnA leq_add2l.
by apply leq_trans with (n := task_deadline tsk); [by done | by apply RESTR].
@@ -542,9 +554,12 @@ Module ResponseTimeAnalysisFP.
{
move: SAMEtsk => /eqP SAMEtsk.
move: (PENDING1) => SAMEjob.
+ ( try ( apply platform_fp_no_multiple_jobs_of_tsk with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (arr_seq0 := arr_seq)
+ (job_task0 := job_task) (tsk0 := tsk) (j0 := j) in SAMEjob) ||
apply platform_fp_no_multiple_jobs_of_tsk with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline) (arr_seq := arr_seq)
- (job_task := job_task) (tsk := tsk) (j := j) in SAMEjob; try (by done);
+ (job_task := job_task) (tsk := tsk) (j := j) in SAMEjob); try (by done);
[ | by apply PARAMS | |]; last 2 first.
{
apply (leq_trans LTt); rewrite -addnA leq_add2l.
@@ -554,7 +569,8 @@ Module ResponseTimeAnalysisFP.
}
{
intros j0 ARR0 JOB0 LT0.
- apply completion_monotonic with (t := job_arrival j0 + task_jitter tsk + R);
+ ( try ( apply completion_monotonic with (t0 := job_arrival j0 + task_jitter tsk + R) ) ||
+ apply completion_monotonic with (t := job_arrival j0 + task_jitter tsk + R));
try (by done); last by apply BEFOREok.
rewrite -addnA leq_add2l.
by apply leq_trans with (n := task_deadline tsk); last by apply CONSTR.
@@ -569,17 +585,23 @@ Module ResponseTimeAnalysisFP.
rewrite -JOBtsk; apply FP with (t := t); try (by done).
by apply/existsP; exists cpu; apply/eqP.
}
+ ( try ( apply platform_fp_no_multiple_jobs_of_interfering_tasks with
+ (task_period0 := task_period) (tsk0 := tsk) (job_arrival0 := job_arrival)
+ (higher_eq_priority0 := higher_eq_priority) (job_jitter0 := job_jitter)
+ (arr_seq0 := arr_seq)
+ (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) (t0 := t) ) ||
apply platform_fp_no_multiple_jobs_of_interfering_tasks with
(task_period := task_period) (tsk := tsk) (job_arrival := job_arrival)
(higher_eq_priority := higher_eq_priority) (job_jitter := job_jitter)
(arr_seq := arr_seq)
- (job_cost := job_cost) (job_task := job_task) (sched := sched) (t := t);
+ (job_cost := job_cost) (job_task := job_task) (sched := sched) (t := t));
rewrite ?JOBtsk ?SAMEtsk //.
{
intros j0 tsk0 ARR0 JOB0 INTERF0.
feed (HASHP tsk0); first by rewrite -JOB0 FROMTS.
move: (HASHP INTERF0) => [R0 IN0].
- apply completion_monotonic with (t := job_arrival j0 + task_jitter tsk0 + R0);
+ ( try ( apply completion_monotonic with (t0 := job_arrival j0 + task_jitter tsk0 + R0) ) ||
+ apply completion_monotonic with (t := job_arrival j0 + task_jitter tsk0 + R0));
try (by done).
{
rewrite -addnA leq_add2l.
diff --git a/classic/analysis/global/jitter/interference_bound_edf.v b/classic/analysis/global/jitter/interference_bound_edf.v
index d808bc95d2eddb3fe2b30bf80170c8103da4e053..4948f71ee887f30b0c6d769a034825934dc16ba2 100644
--- a/classic/analysis/global/jitter/interference_bound_edf.v
+++ b/classic/analysis/global/jitter/interference_bound_edf.v
@@ -327,6 +327,9 @@ Module InterferenceBoundEDFJitter.
specialize (PARAMS j ARRj); des.
apply leq_trans with (n := service_during sched j t1 t2);
first by apply job_interference_le_service.
+ try ( by apply cumulative_service_le_task_cost with (job_task0 := job_task)
+ (task_deadline0 := task_deadline) (job_cost0 := job_cost)
+ (job_deadline0 := job_deadline); try (by done) ) ||
by apply cumulative_service_le_task_cost with (job_task := job_task)
(task_deadline := task_deadline) (job_cost := job_cost)
(job_deadline := job_deadline); try (by done).
@@ -424,8 +427,10 @@ Module InterferenceBoundEDFJitter.
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
unfold service_during.
- by apply cumulative_service_after_job_rt_zero with
- (job_arrival := job_arrival) (job_cost := job_cost) (R := J_k + R_k);
+ by ( try ( apply cumulative_service_after_job_rt_zero with
+ (job_arrival0 := job_arrival) (job_cost0 := job_cost) (R := J_k + R_k) ) ||
+ apply cumulative_service_after_job_rt_zero with
+ (job_arrival := job_arrival) (job_cost := job_cost) (R := J_k + R_k) );
try (by done); rewrite addnA; last by apply ltnW.
Qed.
@@ -474,6 +479,8 @@ Module InterferenceBoundEDFJitter.
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 [ARRfst [_ [LEdl _]]].
+ try ( apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl; try (by done).
destruct (D_k - R_k - J_k <= D_i) eqn:LEdk; last first.
@@ -486,6 +493,9 @@ Module InterferenceBoundEDFJitter.
apply leq_trans with (n := service_during sched j_fst (a_fst + J_k + R_k) t2);
first by apply job_interference_le_service.
unfold service_during; rewrite leqn0; apply/eqP.
+ try ( by apply cumulative_service_after_job_rt_zero with
+ (job_arrival0 := job_arrival) (job_cost0 := job_cost) (R := J_k + R_k);
+ try (by done); rewrite addnA // leqnn ) ||
by apply cumulative_service_after_job_rt_zero with
(job_arrival := job_arrival) (job_cost := job_cost) (R := J_k + R_k);
try (by done); rewrite addnA // leqnn.
@@ -546,8 +556,10 @@ Module InterferenceBoundEDFJitter.
by apply job_interference_le_service.
}
unfold service_during.
+ ( try ( rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost)
+ (job_arrival0 := job_arrival) (R := J_k + R_k) ) ||
rewrite -> cumulative_service_after_job_rt_zero with (job_cost := job_cost)
- (job_arrival := job_arrival) (R := J_k + R_k);
+ (job_arrival := job_arrival) (R := J_k + R_k));
rewrite ?addnA //.
rewrite addn0; apply extend_sum; first by done.
rewrite -addnA leq_add2l.
@@ -572,8 +584,10 @@ Module InterferenceBoundEDFJitter.
by apply job_interference_le_service.
}
unfold service_during.
+ ( try ( rewrite -> cumulative_service_after_job_rt_zero with (job_arrival0 := job_arrival)
+ (job_cost0 := job_cost) (R:=J_k + R_k) ) ||
rewrite -> cumulative_service_after_job_rt_zero with (job_arrival := job_arrival)
- (job_cost := job_cost) (R:=J_k + R_k);
+ (job_cost := job_cost) (R:=J_k + R_k));
rewrite ?addnA //.
rewrite addn0.
apply leq_trans with (n := (\sum_(a_i <= t < a_fst + J_k + R_k) 1) +
@@ -639,6 +653,8 @@ Module InterferenceBoundEDFJitter.
by apply interference_bound_edf_response_time_bound_of_j_fst_after_interval.
}
apply/eqP; rewrite -[_ _ _ _ == 0]negbK; apply/negP; red; intro BUG.
+ try ( apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in BUG; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in BUG; try (by done).
rewrite interference_bound_edf_j_fst_deadline
@@ -707,6 +723,8 @@ Module InterferenceBoundEDFJitter.
-interference_bound_edf_j_i_deadline.
apply leq_trans with (n := a_i + job_deadline j_i);
last by rewrite leq_add2r leq_addr.
+ try ( by apply interference_under_edf_implies_shorter_deadlines with (arr_seq0 := arr_seq)
+ (job_arrival0 := job_arrival) (job_deadline0 := job_deadline) in LEdl ) ||
by apply interference_under_edf_implies_shorter_deadlines with (arr_seq := arr_seq)
(job_arrival := job_arrival) (job_deadline := job_deadline) in LEdl.
Qed.
@@ -808,6 +826,7 @@ Module InterferenceBoundEDFJitter.
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP; unfold service_during.
rewrite (cumulative_service_before_job_arrival_zero job_arrival) //.
+ try ( by apply arrival_before_jitter with (job_jitter0 := job_jitter) ) ||
by apply arrival_before_jitter with (job_jitter := job_jitter).
Qed.
@@ -839,8 +858,10 @@ Module InterferenceBoundEDFJitter.
sched j_snd t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
- apply cumulative_service_before_job_arrival_zero with (job_arrival := job_arrival);
+ ( try ( apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival) ) ||
+ apply cumulative_service_before_job_arrival_zero with (job_arrival := job_arrival));
try (by done).
+ try ( by apply arrival_before_jitter with (job_jitter0 := job_jitter) ) ||
by apply arrival_before_jitter with (job_jitter := job_jitter).
}
apply leq_trans with (n := a_fst + p_k).
@@ -951,6 +972,8 @@ Module InterferenceBoundEDFJitter.
last by rewrite leq_add2l.
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [LSTarr [_ [LEdl _]]].
+ try ( apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl; try (by done).
unfold D_i, D_k in DIST; rewrite interference_bound_edf_j_lst_deadline
@@ -1040,6 +1063,8 @@ Module InterferenceBoundEDFJitter.
destruct LST as [LSTarr [_ [ LSTserv _]]].
unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
-interference_bound_edf_j_i_deadline.
+ try ( by apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LSTserv ) ||
by apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LSTserv.
Qed.
@@ -1085,8 +1110,10 @@ Module InterferenceBoundEDFJitter.
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.
+ ( try ( apply cumulative_service_after_job_rt_zero with (job_arrival0 := job_arrival)
+ (job_cost0 := job_cost) (R := J_k + R_k) ) ||
apply cumulative_service_after_job_rt_zero with (job_arrival := job_arrival)
- (job_cost := job_cost) (R := J_k + R_k);
+ (job_cost := job_cost) (R := J_k + R_k));
[ by done | rewrite addnA | by rewrite addnA leqnn].
by apply interference_bound_edf_j_fst_completed_on_time.
}
@@ -1165,6 +1192,8 @@ Module InterferenceBoundEDFJitter.
-interference_bound_edf_j_i_deadline.
apply leq_trans with (n := a_i + job_deadline j_i);
last by rewrite -addnA leq_add2l leq_addl.
+ try ( by apply interference_under_edf_implies_shorter_deadlines
+ with (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LSTserv ) ||
by apply interference_under_edf_implies_shorter_deadlines
with (arr_seq := arr_seq) (job_deadline := job_deadline) in LSTserv.
Qed.
diff --git a/classic/analysis/global/jitter/workload_bound.v b/classic/analysis/global/jitter/workload_bound.v
index de982499420276771455d1393acb20ca434d7525..463f35ccc19bdfe3397d22357aa71cd128f2b556 100644
--- a/classic/analysis/global/jitter/workload_bound.v
+++ b/classic/analysis/global/jitter/workload_bound.v
@@ -399,8 +399,10 @@ Module WorkloadBoundJitter.
}
instantiate (1 := elem); move => [FSTARR [FSTtsk [/eqP FSTserv FSTin]]].
apply FSTserv.
+ ( try ( apply cumulative_service_after_job_rt_zero with (job_arrival0 := job_arrival)
+ (job_cost0 := job_cost) (R := task_jitter tsk + R_tsk) ) ||
apply cumulative_service_after_job_rt_zero with (job_arrival := job_arrival)
- (job_cost := job_cost) (R := task_jitter tsk + R_tsk);
+ (job_cost := job_cost) (R := task_jitter tsk + R_tsk));
[by done | | by rewrite addnA ltnW].
rewrite addnA; apply H_response_time_bound; try (by done).
by apply leq_trans with (n := t1); last by apply leq_addr.
@@ -419,6 +421,7 @@ Module WorkloadBoundJitter.
instantiate (1 := elem); move => [LSTarr [LSTtsk [/eqP LSTserv LSTin]]].
apply LSTserv.
apply (cumulative_service_before_job_arrival_zero job_arrival); last by done.
+ try ( by apply arrival_before_jitter with (job_jitter0 := job_jitter) ) ||
by apply arrival_before_jitter with (job_jitter := job_jitter).
Qed.
@@ -475,6 +478,7 @@ Module WorkloadBoundJitter.
last by apply leq_sum; ins; apply service_at_most_one.
rewrite (cumulative_service_before_job_arrival_zero job_arrival);
[by apply leqnn | | by apply leqnn].
+ try ( by apply arrival_before_jitter with (job_jitter0 := job_jitter) ) ||
by apply arrival_before_jitter with (job_jitter := job_jitter).
}
}
@@ -684,6 +688,9 @@ Module WorkloadBoundJitter.
have INlst := workload_bound_j_lst_is_job_of_tsk; des.
have PARAMSfst := JOBPARAMS j_fst INfst; des.
have PARAMSlst := JOBPARAMS j_lst INlst; des.
+ try ( by apply leq_add; apply cumulative_service_le_task_cost with
+ (task_deadline0 := task_deadline) (job_cost0 := job_cost)
+ (job_deadline0 := job_deadline) (job_task0 := job_task) ) ||
by apply leq_add; apply cumulative_service_le_task_cost with
(task_deadline := task_deadline) (job_cost := job_cost)
(job_deadline := job_deadline) (job_task := job_task).
diff --git a/classic/analysis/global/parallel/bertogna_edf_theory.v b/classic/analysis/global/parallel/bertogna_edf_theory.v
index 8031119cf6d3f1d2cc7c8fbefac7d6547e91f9a3..7d76bb6e48e8d6cc068b8820c171adc8a459b949 100644
--- a/classic/analysis/global/parallel/bertogna_edf_theory.v
+++ b/classic/analysis/global/parallel/bertogna_edf_theory.v
@@ -206,8 +206,10 @@ Module ResponseTimeAnalysisEDF.
x tsk_other <= edf_specific_bound tsk_other R_other.
Proof.
rename H_job_of_tsk into JOBtsk, H_all_jobs_from_taskset into FROMTS.
+ ( try ( apply interference_bound_edf_bounds_interference with (job_deadline0 := job_deadline)
+ (arr_seq0 := arr_seq) (ts0 := ts); try (by done) ) ||
apply interference_bound_edf_bounds_interference with (job_deadline := job_deadline)
- (arr_seq := arr_seq) (ts := ts); try (by done);
+ (arr_seq := arr_seq) (ts := ts); try (by done));
[ by rewrite -JOBtsk FROMTS
| by apply bertogna_edf_tsk_other_in_ts
| by apply H_tasks_miss_no_deadlines
@@ -315,6 +317,8 @@ Module ResponseTimeAnalysisEDF.
}
clear SCHED; rename SCHED' into SCHED.
move: (SCHED) => PENDING.
+ try ( apply scheduled_implies_pending with (job_cost0 := job_cost) (job_arrival0 := job_arrival)
+ in PENDING; try (by done) ) ||
apply scheduled_implies_pending with (job_cost := job_cost) (job_arrival := job_arrival)
in PENDING; try (by done).
destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
@@ -322,6 +326,7 @@ Module ResponseTimeAnalysisEDF.
move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
specialize (BEFOREok j_other tsk R ARRother SAMEtsk INbounds LT).
move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
+ try ( apply completion_monotonic with (t0 := job_arrival j_other + R); try (by done) ) ||
apply completion_monotonic with (t := job_arrival j_other + R); try (by done).
apply leq_trans with (n := job_arrival j); last by done.
apply leq_trans with (n := job_arrival j_other + task_deadline tsk);
diff --git a/classic/analysis/global/parallel/bertogna_fp_comp.v b/classic/analysis/global/parallel/bertogna_fp_comp.v
index 3dcd6cc038c0547337b33ef686346fe1fc9bce32..e4394284dc969456176d2f12a7c355520aaa890d 100644
--- a/classic/analysis/global/parallel/bertogna_fp_comp.v
+++ b/classic/analysis/global/parallel/bertogna_fp_comp.v
@@ -585,6 +585,11 @@ Module ResponseTimeIterationFP.
}
intros [_ [_ [REC DL]]].
+ try ( apply bertogna_cirinei_response_time_bound_fp with
+ (task_cost0 := task_cost) (task_period0 := task_period)
+ (task_deadline0 := task_deadline) (job_deadline0 := job_deadline) (tsk0 := (TASK idx))
+ (job_task0 := job_task) (ts0 := ts) (hp_bounds0 := take idx hp_bounds)
+ (higher_eq_priority := higher_priority); try (by done) ) ||
apply bertogna_cirinei_response_time_bound_fp with
(task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (job_deadline := job_deadline) (tsk := (TASK idx))
diff --git a/classic/analysis/global/parallel/bertogna_fp_theory.v b/classic/analysis/global/parallel/bertogna_fp_theory.v
index 333a3d528c663497f33ebe05df5e586cdfc048be..f1f2b7cda7dc6408f770bd58a2bb13a3134b422e 100644
--- a/classic/analysis/global/parallel/bertogna_fp_theory.v
+++ b/classic/analysis/global/parallel/bertogna_fp_theory.v
@@ -201,8 +201,10 @@ Module ResponseTimeAnalysisFP.
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.
- by apply workload_bounded_by_W with (task_deadline := task_deadline) (arr_seq := arr_seq)
- (job_arrival := job_arrival) (job_cost := job_cost) (job_deadline := job_deadline);
+ by ( try ( apply workload_bounded_by_W with (task_deadline0 := task_deadline) (arr_seq0 := arr_seq)
+ (job_arrival0 := job_arrival) (job_cost0 := job_cost) (job_deadline0 := job_deadline) ) ||
+ apply workload_bounded_by_W with (task_deadline := task_deadline) (arr_seq := arr_seq)
+ (job_arrival := job_arrival) (job_cost := job_cost) (job_deadline := job_deadline));
try (by ins);
[ by ins; apply TASK_PARAMS
| by ins; apply RESP with (hp_tsk := tsk_other)].
@@ -315,12 +317,15 @@ Module ResponseTimeAnalysisFP.
by apply/existsP; exists cpu; rewrite SCHED.
} clear SCHED; rename SCHED' into SCHED.
move: (SCHED) => PENDING.
+ try ( apply scheduled_implies_pending with (job_arrival0 := job_arrival)
+ (job_cost0 := job_cost) in PENDING; try (by done) ) ||
apply scheduled_implies_pending with (job_arrival := job_arrival)
(job_cost := job_cost) in PENDING; try (by done).
destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
{
specialize (BEFOREok j_other ARRother SAMEtsk BEFOREother).
move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
+ try ( apply completion_monotonic with (t0 := job_arrival j_other + R); try (by done) ) ||
apply completion_monotonic with (t := job_arrival j_other + R); try (by done).
apply leq_trans with (n := job_arrival j); last by done.
apply leq_trans with (n := job_arrival j_other + task_deadline tsk);
@@ -466,4 +471,4 @@ Module ResponseTimeAnalysisFP.
End ResponseTimeBound.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/analysis/global/parallel/interference_bound_edf.v b/classic/analysis/global/parallel/interference_bound_edf.v
index d3fb6f870e7aceedf3dec44937cc5cb0a1f9eca4..75187d19d69cfed98c580ea7394b893120d34607 100644
--- a/classic/analysis/global/parallel/interference_bound_edf.v
+++ b/classic/analysis/global/parallel/interference_bound_edf.v
@@ -342,6 +342,8 @@ Module InterferenceBoundEDF.
specialize (PARAMS j ARRj); des.
apply leq_trans with (n := service_during sched j t1 t2);
first by apply job_interference_le_service.
+ try ( by apply cumulative_service_le_task_cost with (job_task0 := job_task)
+ (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline) ) ||
by apply cumulative_service_le_task_cost with (job_task := job_task)
(task_deadline := task_deadline) (job_cost := job_cost) (job_deadline := job_deadline).
Qed.
@@ -440,6 +442,9 @@ Module InterferenceBoundEDF.
rewrite -leqn0; apply leq_trans with (n := service_during sched j_fst t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
+ try ( by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost)
+ (job_arrival0 := job_arrival) (R := R_k);
+ try (by done); apply ltnW ) ||
by apply cumulative_service_after_job_rt_zero with (job_cost := job_cost)
(job_arrival := job_arrival) (R := R_k);
try (by done); apply ltnW.
@@ -545,6 +550,7 @@ Module InterferenceBoundEDF.
apply leq_trans with (n := service_during sched j_lst t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP; unfold service_during.
+ try ( by apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival) ) ||
by apply cumulative_service_before_job_arrival_zero with (job_arrival := job_arrival).
Qed.
@@ -569,6 +575,7 @@ Module InterferenceBoundEDF.
sched j_snd t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
+ try ( by apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival) ) ||
by apply cumulative_service_before_job_arrival_zero with (job_arrival := job_arrival).
}
apply leq_trans with (n := a_fst + p_k).
@@ -653,6 +660,8 @@ Module InterferenceBoundEDF.
last by rewrite leq_add2l.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [ARRfst [_ [ LEdl _]]].
+ try ( apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl; try (by done).
rewrite addnC [D_i + _]addnC.
@@ -706,6 +715,8 @@ Module InterferenceBoundEDF.
last by rewrite leq_add2r.
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [ARRlst [_ [ LEdl _]]].
+ try ( apply interference_under_edf_implies_shorter_deadlines with
+ (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl; try (by done).
unfold D_i, D_k in DIST; rewrite interference_bound_edf_j_lst_deadline
diff --git a/classic/analysis/uni/basic/fp_rta_comp.v b/classic/analysis/uni/basic/fp_rta_comp.v
index 206ee8cb1b14a26d2b795a34b88994dbba0cc77e..58043a5e490bec3a06bcdab032022b03704f9c68 100644
--- a/classic/analysis/uni/basic/fp_rta_comp.v
+++ b/classic/analysis/uni/basic/fp_rta_comp.v
@@ -221,6 +221,8 @@ Module ResponseTimeIterationFP.
apply total_workload_bound_fp_non_decreasing.
}
apply leq_trans with (n := task_cost tsk); first by done.
+ try ( apply iter_fixpoint_ge_bottom with (f0 := f) (max_steps := s);
+ try (by done) ) ||
apply iter_fixpoint_ge_bottom with (f := f) (max_steps := s);
try (by done).
by apply fp_claimed_bounds_computes_iteration.
@@ -323,18 +325,31 @@ Module ResponseTimeIterationFP.
valid_sporadic_taskset, is_valid_sporadic_task in *.
unfold RTA_claimed_bounds; intros tsk R.
case SOME: fp_claimed_bounds => [rt_bounds|] IN; last by done.
+ try ( apply uniprocessor_response_time_bound_fp with
+ (task_cost0 := task_cost) (task_period0 := task_period)
+ (ts0 := ts) (task_deadline0 := task_deadline)
+ (job_deadline0 := job_deadline)
+ (higher_eq_priority0 := higher_eq_priority); try (by done) ) ||
apply uniprocessor_response_time_bound_fp with
(task_cost := task_cost) (task_period := task_period)
(ts := ts) (task_deadline := task_deadline)
(job_deadline := job_deadline)
(higher_eq_priority := higher_eq_priority); try (by done).
{
+ ( try ( apply fp_claimed_bounds_gt_zero with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline)
+ (higher_eq_priority0 := higher_eq_priority) (ts0 := ts)
+ (rt_bounds0 := rt_bounds) (tsk0 := tsk) ) ||
apply fp_claimed_bounds_gt_zero with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline)
(higher_eq_priority := higher_eq_priority) (ts := ts)
- (rt_bounds := rt_bounds) (tsk := tsk); try (by done).
+ (rt_bounds := rt_bounds) (tsk := tsk)); try (by done).
{
- feed (PARAMS tsk); last by move: PARAMS => [P1 _].
+ feed (PARAMS tsk) ; last by move: PARAMS => [P1 _].
+ try ( by apply fp_claimed_bounds_from_taskset with
+ (task_cost0 := task_cost) (task_period0 := task_period)
+ (task_deadline0 := task_deadline) (rt_bounds0 := rt_bounds)
+ (higher_eq_priority0 := higher_eq_priority) (R0 := R) ) ||
by apply fp_claimed_bounds_from_taskset with
(task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (rt_bounds := rt_bounds)
@@ -342,6 +357,8 @@ Module ResponseTimeIterationFP.
}
by intros tsk0 IN0; specialize (PARAMS tsk0 IN0); des.
}
+ try ( by apply fp_claimed_bounds_yields_fixed_point with
+ (task_deadline0 := task_deadline) (rt_bounds0 := rt_bounds) ) ||
by apply fp_claimed_bounds_yields_fixed_point with
(task_deadline := task_deadline) (rt_bounds := rt_bounds).
Qed.
@@ -367,8 +384,10 @@ Module ResponseTimeIterationFP.
intros tsk IN.
move: (RESP rt_bounds TEST tsk IN) => [R INbounds].
specialize (DL rt_bounds TEST tsk R INbounds).
+ ( try ( apply task_completes_before_deadline with
+ (task_deadline0 := task_deadline) (R0 := R) ) ||
apply task_completes_before_deadline with
- (task_deadline := task_deadline) (R := R); try (by done);
+ (task_deadline := task_deadline) (R := R)); try (by done);
first by intros j ARRj; specialize (JOBPARAMS j ARRj); move: JOBPARAMS => [_ [_ EQ]].
by apply RTA; rewrite /RTA_claimed_bounds TEST.
Qed.
@@ -391,4 +410,4 @@ Module ResponseTimeIterationFP.
End ProvingCorrectness.
-End ResponseTimeIterationFP.
\ No newline at end of file
+End ResponseTimeIterationFP.
diff --git a/classic/analysis/uni/basic/fp_rta_theory.v b/classic/analysis/uni/basic/fp_rta_theory.v
index 98830276dc2dcb529070bc842a19a1c104d4fe14..1e7ad76b22b8639d69c2ddd96e4ad0f4248a00e1 100644
--- a/classic/analysis/uni/basic/fp_rta_theory.v
+++ b/classic/analysis/uni/basic/fp_rta_theory.v
@@ -101,6 +101,10 @@ Module ResponseTimeAnalysisFP.
move: (posnP (job_cost j)) => [Z|POS].
{ by rewrite /is_response_time_bound_of_job /completed_by Z. }
set prio := FP_to_JLFP job_task higher_eq_priority.
+ try ( apply busy_interval_bounds_response_time with
+ (arr_seq0 := arr_seq)
+ (higher_eq_priority0 := prio)
+ (priority_inversion_bound := 0); try by done ) ||
apply busy_interval_bounds_response_time with
(arr_seq := arr_seq)
(higher_eq_priority := prio)
@@ -129,6 +133,10 @@ Module ResponseTimeAnalysisFP.
}
{ by rewrite /scheduled_at SCHED. }
}
+ try ( apply fp_workload_bound_holds with
+ (job_arrival0 := job_arrival) (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline)
+ (job_deadline0 := job_deadline) (ts0 := ts); try (by done) ) ||
apply fp_workload_bound_holds with
(job_arrival := job_arrival) (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline)
@@ -138,4 +146,4 @@ Module ResponseTimeAnalysisFP.
End ResponseTimeBound.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/analysis/uni/basic/tdma_rta_theory.v b/classic/analysis/uni/basic/tdma_rta_theory.v
index 6c4f833072e1d939c2182f2a1bd8f67f4702128b..21fe61975f8aa59b50e44e1dafe67c9607b2cdf5 100644
--- a/classic/analysis/uni/basic/tdma_rta_theory.v
+++ b/classic/analysis/uni/basic/tdma_rta_theory.v
@@ -132,16 +132,25 @@ Module ResponseTimeAnalysisTDMA.
induction t as [ t IHt ] using (well_founded_induction lt_wf).
case t eqn:GT;intros.
- have INJ: arrives_in arr_seq j by exists 0.
- (apply completion_monotonic with (t:=job_arrival j + WCRT task_cost task_time_slot ts tsk )
- ;trivial;try by rewrite leq_add2l H); apply job_completed_by_WCRT
+ (( try ( apply completion_monotonic with (t0:=job_arrival j + WCRT task_cost task_time_slot ts tsk ) ) || apply completion_monotonic with (t:=job_arrival j + WCRT task_cost task_time_slot ts tsk ) )
+ ;trivial;try by rewrite leq_add2l H); ( try ( apply job_completed_by_WCRT
+ with (task_deadline0:=task_deadline)
+ (arr_seq0:=arr_seq)(job_deadline0:=job_deadline)
+ (job_task0:=job_task)(slot_order0:=slot_order) ) || apply job_completed_by_WCRT
with (task_deadline:=task_deadline)
(arr_seq:=arr_seq)(job_deadline:=job_deadline)
- (job_task:=job_task)(slot_order:=slot_order);eauto 2.
+ (job_task:=job_task)(slot_order:=slot_order) );eauto 2.
intros. apply H_arrival_times_are_consistent in ARR. ssrlia.
- have INJ: arrives_in arr_seq j by exists n.+1.
+ try ( apply completion_monotonic
+ with (t0:=job_arrival j + WCRT task_cost task_time_slot ts tsk);auto ) ||
apply completion_monotonic
with (t:=job_arrival j + WCRT task_cost task_time_slot ts tsk);auto.
- by rewrite leq_add2l H. apply job_completed_by_WCRT
+ by rewrite leq_add2l H. try ( apply job_completed_by_WCRT
+ with (task_deadline0:=task_deadline)
+ (arr_seq0:=arr_seq)(job_deadline0:=job_deadline)
+ (job_task0:=job_task)(slot_order0:=slot_order);auto ) ||
+ apply job_completed_by_WCRT
with (task_deadline:=task_deadline)
(arr_seq:=arr_seq)(job_deadline:=job_deadline)
(job_task:=job_task)(slot_order:=slot_order);auto.
@@ -149,6 +158,8 @@ Module ResponseTimeAnalysisTDMA.
have PERIOD: job_arrival j_other + task_period (job_task j_other)<= job_arrival j.
apply H_sporadic_tasks;auto. case (j==j_other)eqn: JJ;move/eqP in JJ;last auto.
have JO:job_arrival j_other = job_arrival j by f_equal. ssrlia.
+ try ( apply completion_monotonic with (t0:= job_arrival j_other +
+ task_period (job_task j_other)); auto ) ||
apply completion_monotonic with (t:= job_arrival j_other +
task_period (job_task j_other)); auto.
have ARRJ: job_arrival j = n.+1 by auto.
@@ -189,21 +200,35 @@ Module ResponseTimeAnalysisTDMA.
intros j arr_seq_j JobTsk.
apply completion_monotonic with (t:=job_arrival j + RT j); try done.
- rewrite leq_add2l /BOUND.
+ (try ( apply (response_time_le_WCRT)
+ with (task_cost0:=task_cost) (task_deadline0:=task_deadline)(sched0:=sched)
+ (job_arrival0:=job_arrival)(job_cost0:=job_cost)(job_deadline0:=job_deadline)
+ (job_task0:=job_task)(ts0:=ts)(arr_seq0:=arr_seq)
+ (slot_order0:=slot_order)(Job0:=Job)(tsk0:=tsk) ) ||
apply (response_time_le_WCRT)
with (task_cost:=task_cost) (task_deadline:=task_deadline)(sched:=sched)
(job_arrival:=job_arrival)(job_cost:=job_cost)(job_deadline:=job_deadline)
(job_task:=job_task)(ts:=ts)(arr_seq:=arr_seq)
- (slot_order:=slot_order)(Job:=Job)(tsk:=tsk); try done;auto;try (intros;
+ (slot_order:=slot_order)(Job:=Job)(tsk:=tsk)); try done;auto;try (intros;
by apply all_previous_jobs_of_same_task_completed).
- - apply completed_by_end_time
+ - ( try ( apply completed_by_end_time
+ with (sched0:=sched)(job_arrival0:=job_arrival)
+ (job_cost0:=job_cost) ) ||
+ apply completed_by_end_time
with (sched:=sched)(job_arrival:=job_arrival)
- (job_cost:=job_cost); first exact.
+ (job_cost:=job_cost)); first exact.
+ ( try ( apply completes_at_end_time
+ with
+ (job_arrival0:=job_arrival)(task_cost0:=task_cost)(arr_seq0:=arr_seq)
+ (job_task0:=job_task)(job_deadline0:=job_deadline)(task_deadline0:=task_deadline)
+ (sched0:=sched)(ts0:=ts)(slot_order0:=slot_order)
+ (tsk0:=tsk) (j0:=j) ) ||
apply completes_at_end_time
with
(job_arrival:=job_arrival)(task_cost:=task_cost)(arr_seq:=arr_seq)
(job_task:=job_task)(job_deadline:=job_deadline)(task_deadline:=task_deadline)
(sched:=sched)(ts:=ts)(slot_order:=slot_order)
- (tsk:=tsk) (j:=j); try auto;try (intros;
+ (tsk:=tsk) (j:=j)); try auto;try (intros;
by apply all_previous_jobs_of_same_task_completed).
Qed.
@@ -218,7 +243,8 @@ Module ResponseTimeAnalysisTDMA.
(* We can prove the theorem: there is no deadline miss of task tsk *)
Theorem taskset_schedulable_by_tdma : no_deadline_missed_by_task tsk.
Proof.
- apply task_completes_before_deadline with (task_deadline:=task_deadline) (R:=BOUND)
+ ( try ( apply task_completes_before_deadline with (task_deadline0:=task_deadline) (R:=BOUND) ) ||
+ apply task_completes_before_deadline with (task_deadline:=task_deadline) (R:=BOUND) )
;try done.
move => j arr_seqJ.
- by apply H_valid_job_parameters.
@@ -241,6 +267,3 @@ Module ResponseTimeAnalysisTDMA.
End ResponseTimeBound.
End ResponseTimeAnalysisTDMA.
-
-
-
diff --git a/classic/analysis/uni/basic/tdma_wcrt_analysis.v b/classic/analysis/uni/basic/tdma_wcrt_analysis.v
index 76d7a36047b3227d1874899a165d930a5b941a58..0075cfbf39a274bf2aa765a10af569ac1933e3a4 100644
--- a/classic/analysis/uni/basic/tdma_wcrt_analysis.v
+++ b/classic/analysis/uni/basic/tdma_wcrt_analysis.v
@@ -185,6 +185,8 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
apply /andP. split.
- rewrite /has_arrived. auto.
- rewrite /completed_by /service /service_during.
+ try ( rewrite ->cumulative_service_before_job_arrival_zero
+ with (job_arrival0:=job_arrival)) ||
rewrite ->cumulative_service_before_job_arrival_zero
with (job_arrival:=job_arrival). rewrite -ltnNge.
apply H_valid_job. apply H_jobs_must_arrive_to_execute. auto.
@@ -710,6 +712,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
apply completes_at_end_time_pre.
by apply pendingArrival.
rewrite /service /service_during.
+ try ( by rewrite ->cumulative_service_before_job_arrival_zero with (job_arrival0:=job_arrival) ) ||
by rewrite ->cumulative_service_before_job_arrival_zero with (job_arrival:=job_arrival).
Qed.
@@ -826,6 +829,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
apply completion_monotonic with (t:= job_arrival j + job_response_time_tdma_in_at_most_one_job_is_pending);auto.
rewrite leq_add2l.
apply response_time_le_WCRT.
+ try ( apply completed_by_end_time with (job_arrival0:=job_arrival);auto ) ||
apply completed_by_end_time with (job_arrival:=job_arrival);auto.
apply completes_at_end_time.
Qed.
diff --git a/classic/analysis/uni/jitter/fp_rta_comp.v b/classic/analysis/uni/jitter/fp_rta_comp.v
index cbafbe9b443ccd4fc7e93f9b01ceb1a23c12ef30..4317091000217dbe704d42076611acd0e7cb3020 100644
--- a/classic/analysis/uni/jitter/fp_rta_comp.v
+++ b/classic/analysis/uni/jitter/fp_rta_comp.v
@@ -344,11 +344,19 @@ Module ResponseTimeIterationFP.
valid_sporadic_taskset, is_valid_sporadic_task in *.
unfold RTA_claimed_bounds; intros tsk R.
case SOME: fp_claimed_bounds => [rt_bounds|] IN; last by done.
+ try ( apply uniprocessor_response_time_bound_fp with
+ (task_cost0 := task_cost) (task_period0 := task_period)
+ (ts0 := ts) (job_jitter0 := job_jitter)
+ (higher_eq_priority0 := higher_eq_priority); try (by done) ) ||
apply uniprocessor_response_time_bound_fp with
(task_cost := task_cost) (task_period := task_period)
(ts := ts) (job_jitter := job_jitter)
(higher_eq_priority := higher_eq_priority); try (by done).
{
+ try ( apply fp_claimed_bounds_gt_zero with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_deadline0 := task_deadline)
+ (higher_eq_priority0 := higher_eq_priority) (ts0 := ts) (task_jitter0 := task_jitter)
+ (rt_bounds0 := rt_bounds) (tsk0 := tsk); try (by done) ) ||
apply fp_claimed_bounds_gt_zero with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline)
(higher_eq_priority := higher_eq_priority) (ts := ts) (task_jitter := task_jitter)
@@ -356,6 +364,8 @@ Module ResponseTimeIterationFP.
apply H_positive_costs.
by eapply fp_claimed_bounds_from_taskset; eauto 1.
}
+ try ( by apply fp_claimed_bounds_yields_fixed_point with
+ (task_deadline0 := task_deadline) (rt_bounds0 := rt_bounds) ) ||
by apply fp_claimed_bounds_yields_fixed_point with
(task_deadline := task_deadline) (rt_bounds := rt_bounds).
Qed.
@@ -381,6 +391,8 @@ Module ResponseTimeIterationFP.
intros tsk IN.
move: (RESP rt_bounds TEST tsk IN) => [R INbounds].
specialize (DL rt_bounds TEST tsk R INbounds).
+ try ( apply task_completes_before_deadline with
+ (task_deadline0 := task_deadline) (R0 := task_jitter tsk + R); try (by done) ) ||
apply task_completes_before_deadline with
(task_deadline := task_deadline) (R := task_jitter tsk + R); try (by done).
by apply BOUND; rewrite /RTA_claimed_bounds TEST.
@@ -404,4 +416,4 @@ Module ResponseTimeIterationFP.
End ProvingCorrectness.
-End ResponseTimeIterationFP.
\ No newline at end of file
+End ResponseTimeIterationFP.
diff --git a/classic/analysis/uni/jitter/fp_rta_theory.v b/classic/analysis/uni/jitter/fp_rta_theory.v
index 35656284076d0d9ed9e3e45ddb35d5ea4b9e88e9..3296e94cee72233b9862670e3775c577f77469dd 100644
--- a/classic/analysis/uni/jitter/fp_rta_theory.v
+++ b/classic/analysis/uni/jitter/fp_rta_theory.v
@@ -119,11 +119,15 @@ Module ResponseTimeAnalysisFP.
by rewrite -JOBtsk; apply H_job_jitter_le_task_jitter.
}
set prio := FP_to_JLFP job_task higher_eq_priority.
+ try ( apply busy_interval_bounds_response_time with (arr_seq0 := arr_seq)
+ (higher_eq_priority0 := prio); try (by done) ) ||
apply busy_interval_bounds_response_time with (arr_seq := arr_seq)
(higher_eq_priority := prio); try (by done).
- by intros x; apply H_priority_is_reflexive.
- by intros x z y; apply H_priority_is_transitive.
intros t.
+ try ( apply fp_workload_bound_holds with (task_cost0 := task_cost)
+ (task_period0 := task_period) (task_jitter0 := task_jitter) (ts0 := ts); try (by done) ) ||
apply fp_workload_bound_holds with (task_cost := task_cost)
(task_period := task_period) (task_jitter := task_jitter) (ts := ts); try (by done).
by rewrite JOBtsk.
@@ -131,4 +135,4 @@ Module ResponseTimeAnalysisFP.
End ResponseTimeBound.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v b/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
index 25b938f3ea54f3ccf7014bfa70e5dc6a427a6917..b145a9948ec3a34e3e267c64170b74a69e586860 100644
--- a/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
+++ b/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
@@ -254,6 +254,7 @@ Module JitterScheduleService.
rewrite big_mkcond [X in _ <= X]big_mkcond.
apply leq_sum_sub_uniq; first by apply actual_arrivals_uniq.
intros j0 IN0.
+ try ( by apply actual_arrivals_between_sub with (t3 := 0) (t4 := t) ) ||
by apply actual_arrivals_between_sub with (t1 := 0) (t2 := t).
}
apply leq_sum_seq; rewrite /act /actual_arrivals; intros j0 IN0 HP0.
@@ -313,6 +314,8 @@ Module JitterScheduleService.
rewrite HP0 SCHED0 /=.
have ARRin0: arrives_in arr_seq j0 by apply FROMarr in SCHED0.
have ARR0: job_arrival j0 <= t' by apply MUSTARRs.
+ try ( apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival);
+ try (by done) ) ||
apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival);
try (by done).
by apply: (leq_ltn_trans _ LT').
@@ -996,6 +999,8 @@ Module JitterScheduleService.
have ARRin2: arrives_in arr_seq j2.
{
rewrite /sched_j in SCHED2.
+ try ( by apply reduction_prop.sched_jitter_jobs_come_from_arrival_sequence with
+ (sched_susp0 := sched_susp) in SCHED2 ) ||
by apply reduction_prop.sched_jitter_jobs_come_from_arrival_sequence with
(sched_susp := sched_susp) in SCHED2.
}
@@ -1193,6 +1198,8 @@ Module JitterScheduleService.
rewrite (big_rem j_hp) /other_higher_eq_priority_job /=; last first.
{
have IN: arrives_in arr_seq j_hp by apply FROM in SCHEDhp.
+ try ( apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival);
+ try (by done) ) ||
apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival);
try (by done).
by apply: (leq_trans _ LTi); apply ARRIVE.
@@ -1238,6 +1245,7 @@ Module JitterScheduleService.
apply leq_ltn_trans with (n := service_during sched_jitter j arr_j (arr_j + R_j)).
{ rewrite /service /service_during.
rewrite (ignore_service_before_arrival job_arrival) ?leq_addr //.
+ try ( apply jobs_with_jitter_must_arrive_to_execute with (job_jitter0 := job_jitter) ) ||
apply jobs_with_jitter_must_arrive_to_execute with (job_jitter := job_jitter).
by apply reduction_prop.sched_jitter_jobs_execute_after_jitter.
}
diff --git a/classic/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v b/classic/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
index 18b2321e2ca7afb8b7c3aab641cb488e78976987..65fc824fa14f78073006b6da04551d88bf06ff75 100644
--- a/classic/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
+++ b/classic/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
@@ -180,6 +180,10 @@ Module RTAByReduction.
H_valid_response_time_bound_of_hp_tasks into RESPhp,
H_valid_response_time_bound_in_sched_jitter into RESPj.
rewrite -H_job_of_tsk /job_response_time_in_sched_susp_bounded_by.
+ try ( apply reduction_serv.jitter_reduction_job_j_completes_no_later with (job_task0 := job_task)
+ (ts0 := ts) (arr_seq0 := arr_seq) (higher_eq_priority0 := higher_eq_priority)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (job_deadline0 := job_deadline)
+ (job_suspension_duration0 := job_suspension_duration) (R_hp := actual_response_time) ) ||
apply reduction_serv.jitter_reduction_job_j_completes_no_later with (job_task := job_task)
(ts := ts) (arr_seq := arr_seq) (higher_eq_priority := higher_eq_priority)
(task_period := task_period) (task_deadline := task_deadline) (job_deadline := job_deadline)
@@ -199,4 +203,4 @@ Module RTAByReduction.
End ComparingResponseTimeBounds.
-End RTAByReduction.
\ No newline at end of file
+End RTAByReduction.
diff --git a/classic/analysis/uni/susp/dynamic/jitter/taskset_membership.v b/classic/analysis/uni/susp/dynamic/jitter/taskset_membership.v
index a6d8f3cea4b783b7b47e5ca7043d719532bf29d4..353f00aa08a6a51bcaa35a8df7048744751832de 100644
--- a/classic/analysis/uni/susp/dynamic/jitter/taskset_membership.v
+++ b/classic/analysis/uni/susp/dynamic/jitter/taskset_membership.v
@@ -313,6 +313,10 @@ Module TaskSetMembership.
split_conj VALIDSCHED.
apply leq_trans with (n := R (job_task any_j) - higher_cost_wcet any_j);
last by apply leq_sub2l; rewrite /higher_cost_wcet eq_refl.
+ try ( apply sust_prop.sched_susp_highercost_incurs_more_interference with
+ (job_arrival0 := job_arrival) (arr_seq0 := arr_seq) (sched_susp0 := sched_susp)
+ (higher_eq_priority0:=job_higher_eq_priority)
+ (job_suspension_duration0 := job_suspension_duration); try (by done) ) ||
apply sust_prop.sched_susp_highercost_incurs_more_interference with
(job_arrival := job_arrival) (arr_seq := arr_seq) (sched_susp := sched_susp)
(higher_eq_priority:=job_higher_eq_priority)
@@ -347,4 +351,4 @@ Module TaskSetMembership.
End ProvingMembership.
-End TaskSetMembership.
\ No newline at end of file
+End TaskSetMembership.
diff --git a/classic/analysis/uni/susp/dynamic/jitter/taskset_rta.v b/classic/analysis/uni/susp/dynamic/jitter/taskset_rta.v
index 1c22803393980641484299b9acb44eb732993ff5..3dcf1a9a8498d5c9e2e2d4a042122a96c3b1a6de 100644
--- a/classic/analysis/uni/susp/dynamic/jitter/taskset_rta.v
+++ b/classic/analysis/uni/susp/dynamic/jitter/taskset_rta.v
@@ -205,6 +205,11 @@ Module TaskSetRTA.
reduction.inflated_job_cost job_cost job_suspension_duration.
set job_jitter := reduction.job_jitter job_arrival job_task
higher_eq_priority job_cost j actual_response_time.
+ try ( apply valid_response_time_bound_in_sched_susp with
+ (task_period0 := task_period) (task_deadline0 := task_deadline)
+ (job_deadline0 := job_deadline) (job_task0 := job_task) (ts0 := ts)
+ (arr_seq0 := arr_seq) (higher_eq_priority0 := higher_eq_priority)
+ (job_suspension_duration0:=job_suspension_duration); try (by done) ) ||
apply valid_response_time_bound_in_sched_susp with
(task_period := task_period) (task_deadline := task_deadline)
(job_deadline := job_deadline) (job_task := job_task) (ts := ts)
@@ -230,4 +235,4 @@ Module TaskSetRTA.
End PerTaskAnalysis.
-End TaskSetRTA.
\ No newline at end of file
+End TaskSetRTA.
diff --git a/classic/analysis/uni/susp/dynamic/oblivious/fp_rta.v b/classic/analysis/uni/susp/dynamic/oblivious/fp_rta.v
index b5dc915f54bb9dd4f89e70bbe1ac4a9d1a28f62b..4102429d90cda7d22a73318fb964948a2414ddff 100644
--- a/classic/analysis/uni/susp/dynamic/oblivious/fp_rta.v
+++ b/classic/analysis/uni/susp/dynamic/oblivious/fp_rta.v
@@ -132,16 +132,24 @@ Module SuspensionObliviousFP.
rename H_claimed_schedulable_by_suspension_oblivious_RTA into SCHED,
H_jobs_from_taskset into FROMTS, H_inflated_cost_le_deadline_and_period into LEdl.
intros tsk INts j ARRj JOBtsk.
+ try ( apply suspension_oblivious_preserves_schedulability with
+ (higher_eq_priority0 := (FP_to_JLDP job_task higher_eq_priority))
+ (arr_seq0 := arr_seq) (next_suspension0 := next_suspension); try (by done) ) ||
apply suspension_oblivious_preserves_schedulability with
(higher_eq_priority := (FP_to_JLDP job_task higher_eq_priority))
(arr_seq := arr_seq) (next_suspension := next_suspension); try (by done).
- by intros t y x z; apply H_priority_is_transitive.
- by intros j1 j2 t ARR1 ARR2; apply/orP; apply H_priority_is_total; apply FROMTS.
+ try ( apply jobs_schedulable_by_fp_rta with (task_cost0 := inflated_cost) (ts0 := ts)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (job_task0 := job_task)
+ (higher_eq_priority0 := higher_eq_priority); try (by done) ) ||
apply jobs_schedulable_by_fp_rta with (task_cost := inflated_cost) (ts := ts)
(task_period := task_period) (task_deadline := task_deadline) (job_task := job_task)
(higher_eq_priority := higher_eq_priority); try (by done).
- by apply suspension_oblivious_task_parameters_remain_valid.
- - by apply suspension_oblivious_job_parameters_remain_valid with (ts := ts)
+ - try ( by apply suspension_oblivious_job_parameters_remain_valid with (ts0 := ts)
+ (task_period0 := task_period) ) ||
+ by apply suspension_oblivious_job_parameters_remain_valid with (ts := ts)
(task_period := task_period).
- by apply sched_newjobs_come_from_arrival_sequence.
- by apply sched_new_jobs_must_arrive_to_execute.
@@ -158,4 +166,4 @@ Module SuspensionObliviousFP.
End ReductionToBasicAnalysis.
-End SuspensionObliviousFP.
\ No newline at end of file
+End SuspensionObliviousFP.
diff --git a/classic/analysis/uni/susp/dynamic/oblivious/reduction.v b/classic/analysis/uni/susp/dynamic/oblivious/reduction.v
index 2d60c451c68d16cbbda4d2795e607200abe8098e..c628567ccb3971e8020035d33a2b3f3c6bb6d0b1 100644
--- a/classic/analysis/uni/susp/dynamic/oblivious/reduction.v
+++ b/classic/analysis/uni/susp/dynamic/oblivious/reduction.v
@@ -494,7 +494,8 @@ Module ReductionToBasicSchedule.
first apply cumulative_service_le_job_cost,
sched_new_completed_jobs_dont_execute.
}
- rewrite leq_add //; first by apply completion_monotonic with (t := t).
+ rewrite leq_add //; first by ( try ( apply completion_monotonic with (t0 := t) ) ||
+ apply completion_monotonic with (t := t)).
apply completion_monotonic with (t' := t.+1) in COMP; try done.
rewrite /job_cumulative_suspension.
by rewrite -> cumulative_suspension_eq_total_suspension with
@@ -593,8 +594,10 @@ Module ReductionToBasicSchedule.
Proof.
rename H_j_not_scheduled_in_susp into NOTSCHEDs, H_j_scheduled_in_new into SCHEDn.
move: H_j_hp_is_scheduled (H_j_hp_is_scheduled) => SCHEDhp PENDhp.
+ ( try ( apply scheduled_implies_pending with (job_arrival0 := job_arrival)
+ (job_cost := original_job_cost) in PENDhp) ||
apply scheduled_implies_pending with (job_arrival := job_arrival)
- (job_cost := original_job_cost) in PENDhp; try (by done).
+ (job_cost := original_job_cost) in PENDhp); try (by done).
move: PENDhp => /andP [ARRhp _].
apply contraT; intro NOTCOMPhp.
have PENDhp: pending job_arrival inflated_job_cost sched_new j_hp t
@@ -739,4 +742,4 @@ Module ReductionToBasicSchedule.
End Reduction.
-End ReductionToBasicSchedule.
\ No newline at end of file
+End ReductionToBasicSchedule.
diff --git a/classic/analysis/uni/susp/sustainability/allcosts/main_claim.v b/classic/analysis/uni/susp/sustainability/allcosts/main_claim.v
index 4c4808ba90f7598405bc79be27e9c8c85307df29..676199b7f390c434e1c5cb277a8c772741c365bb 100644
--- a/classic/analysis/uni/susp/sustainability/allcosts/main_claim.v
+++ b/classic/analysis/uni/susp/sustainability/allcosts/main_claim.v
@@ -122,6 +122,9 @@ Module SustainabilityAllCostsProperty.
good_arr_seq higher_eq_priority good_sched good_suspension bad_cost good_j R.
set bad_params := [:: param JOB_ARRIVAL job_arrival; param JOB_COST bad_cost;
param JOB_SUSPENSION reduced_suspension_duration].
+ try ( apply reduction_prop.sched_new_response_time_of_job_j with (arr_seq := good_arr_seq)
+ (higher_eq_priority0 := higher_eq_priority) (inflated_job_cost := bad_cost);
+ try done ) ||
apply reduction_prop.sched_new_response_time_of_job_j with (arr_seq := good_arr_seq)
(higher_eq_priority := higher_eq_priority) (inflated_job_cost := bad_cost);
try done.
@@ -162,4 +165,4 @@ Module SustainabilityAllCostsProperty.
End SustainabilityProperty.
-End SustainabilityAllCostsProperty.
\ No newline at end of file
+End SustainabilityAllCostsProperty.
diff --git a/classic/analysis/uni/susp/sustainability/allcosts/reduction_properties.v b/classic/analysis/uni/susp/sustainability/allcosts/reduction_properties.v
index d4f6215409f9910b6a61874d861c99004cca3566..5f9290dc016626a797918debcfcc0bfd62d3b210 100644
--- a/classic/analysis/uni/susp/sustainability/allcosts/reduction_properties.v
+++ b/classic/analysis/uni/susp/sustainability/allcosts/reduction_properties.v
@@ -568,11 +568,13 @@ Module SustainabilityAllCostsProperties.
by apply NOSERV; rewrite ?SUSPn ?LTr ?SUSPt ?GE ?LT.
}
apply/andP; split; first by apply: (ltn_trans _ LTr).
+ try ( apply suspended_in_suspension_interval with (t0 := t); try done ) ||
apply suspended_in_suspension_interval with (t := t); try done.
{
apply/negP; intro COMPmid.
apply suspended_implies_not_completed in SUSPt.
suff BUG: completed_by job_cost sched_susp j0 t by rewrite BUG in SUSPt.
+ try ( by apply completion_monotonic with (t0 := k); [ apply ltnW |] ) ||
by apply completion_monotonic with (t := k); [ apply ltnW |].
}
apply/andP; split;
diff --git a/classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v b/classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v
index 0aab584fc54c313d961c0dbd75a7747a3021a777..4bd116bdd8931da4468f3c1c276f2861a64ce5bf 100644
--- a/classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v
+++ b/classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v
@@ -413,7 +413,8 @@ Module SustainabilitySingleCostProperties.
case (boolP (any_j == j)) => [/eqP EQ | NEQ]; subst.
{ unfold completed_jobs_dont_execute in *.
have BUG: service sched_susp j t >= job_cost j.
- { apply completion_monotonic with (t := k); try (by done); apply ltnW. }
+ { try ( apply completion_monotonic with (t0 := k); try (by done); apply ltnW ) ||
+ apply completion_monotonic with (t := k); try (by done); apply ltnW. }
by exfalso; move: BUG; rewrite leqNgt; move => /negP BUG; apply: BUG.
}
rewrite COSTother //.
@@ -589,6 +590,7 @@ Module SustainabilitySingleCostProperties.
intros k any_j LT; apply IHtmp; first by done.
apply/negP; intro COMPk.
suff COMPt: completed_in_sched_susp j t by rewrite COMPt in NOTCOMP.
+ try ( by apply completion_monotonic with (t0 := k);[apply ltnW|] ) ||
by apply completion_monotonic with (t := k);[apply ltnW|].
Qed.
diff --git a/classic/implementation/apa/bertogna_edf_example.v b/classic/implementation/apa/bertogna_edf_example.v
index eb4a3df69feeb4d31bbbf9bf9d10b99aa626a601..b4c29d2f80a6e5f328f7832a7e53481f320ead96 100644
--- a/classic/implementation/apa/bertogna_edf_example.v
+++ b/classic/implementation/apa/bertogna_edf_example.v
@@ -151,6 +151,9 @@ Module ResponseTimeAnalysisEDF.
have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
have VALIDTS := ts_has_valid_parameters.
unfold valid_sporadic_job, valid_realtime_job in *; des.
+ try ( apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period)
+ (task_deadline := task_deadline) (alpha := task_affinity) (alpha' := task_affinity)
+ (ts0 := ts); try (by done) ) ||
apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (alpha := task_affinity) (alpha' := task_affinity)
(ts := ts); try (by done).
@@ -183,4 +186,4 @@ Module ResponseTimeAnalysisEDF.
End ExampleRTA.
-End ResponseTimeAnalysisEDF.
\ No newline at end of file
+End ResponseTimeAnalysisEDF.
diff --git a/classic/implementation/apa/bertogna_fp_example.v b/classic/implementation/apa/bertogna_fp_example.v
index 65ba91363bcaa4eca7c932ed445d4acbd6faf05a..fe65e131bb730515c67a6bf34943a1e5cdc015d1 100644
--- a/classic/implementation/apa/bertogna_fp_example.v
+++ b/classic/implementation/apa/bertogna_fp_example.v
@@ -233,6 +233,10 @@ Module ResponseTimeAnalysisFP.
have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
have TSVALID := ts_has_valid_parameters.
unfold valid_sporadic_job, valid_realtime_job in *; des.
+ try ( apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
+ (task_period := task_period) (task_deadline := task_deadline)
+ (ts0 := ts) (higher_priority0 := RM task_period)
+ (alpha := task_affinity) (alpha' := task_affinity); try (by done) ) ||
apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline)
(ts := ts) (higher_priority := RM task_period)
@@ -269,4 +273,4 @@ Module ResponseTimeAnalysisFP.
End ExampleRTA.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/implementation/apa/schedule.v b/classic/implementation/apa/schedule.v
index 9a53a6420378916eac613643645e0e97ebf9ed21..4c864dd311cb4aafb2969ccaf9973576385b6e0e 100644
--- a/classic/implementation/apa/schedule.v
+++ b/classic/implementation/apa/schedule.v
@@ -444,6 +444,7 @@ Module ConcreteScheduler.
{
rewrite mem_sort mem_filter PENDING andTb.
move: PENDING => /andP [ARR IN]; rewrite /has_arrived in ARR.
+ try ( by apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival) ) ||
by apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival).
}
have INhp: j_hp \in l by apply scheduler_job_in_mapping in SCHED.
@@ -628,6 +629,7 @@ Module ConcreteScheduler.
{
rewrite mem_sort mem_filter PENDING andTb.
move: PENDING => /andP [ARR _].
+ try ( by apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival) ) ||
by apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival).
}
have WORK := scheduler_mapping_is_work_conserving j cpu t l IN SORT UNIQ.
@@ -662,4 +664,4 @@ Module ConcreteScheduler.
End Proofs.
-End ConcreteScheduler.
\ No newline at end of file
+End ConcreteScheduler.
diff --git a/classic/implementation/global/basic/bertogna_edf_example.v b/classic/implementation/global/basic/bertogna_edf_example.v
index 42f5fce837b32aecf6f6fa7bc589e7e0c65f4721..ff0179db376e8509666c9d24175c9295b6d13b71 100644
--- a/classic/implementation/global/basic/bertogna_edf_example.v
+++ b/classic/implementation/global/basic/bertogna_edf_example.v
@@ -106,6 +106,8 @@ Module ResponseTimeAnalysisEDF.
have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
have TSVALID := ts_has_valid_parameters.
unfold valid_sporadic_job, valid_realtime_job in *; des.
+ try ( apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period)
+ (task_deadline := task_deadline) (ts0 := ts); try (by done) ) ||
apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (ts := ts); try (by done).
- by apply ts_has_constrained_deadlines.
@@ -129,4 +131,4 @@ Module ResponseTimeAnalysisEDF.
End ExampleRTA.
-End ResponseTimeAnalysisEDF.
\ No newline at end of file
+End ResponseTimeAnalysisEDF.
diff --git a/classic/implementation/global/basic/bertogna_fp_example.v b/classic/implementation/global/basic/bertogna_fp_example.v
index dab8caeefc2ed4f5aa3b26c91b53c93fdd79a96f..81562051b42fda9d22e79689cfa421217690602c 100644
--- a/classic/implementation/global/basic/bertogna_fp_example.v
+++ b/classic/implementation/global/basic/bertogna_fp_example.v
@@ -144,6 +144,9 @@ Module ResponseTimeAnalysisFP.
have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
have TSVALID := ts_has_valid_parameters.
unfold valid_sporadic_job, valid_realtime_job in *; des.
+ try ( apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
+ (task_period := task_period) (task_deadline := task_deadline)
+ (ts0 := ts) (higher_priority0 := RM task_period); try (by done) ) ||
apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline)
(ts := ts) (higher_priority := RM task_period); try (by done).
@@ -171,4 +174,4 @@ Module ResponseTimeAnalysisFP.
End ExampleRTA.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/implementation/global/basic/schedule.v b/classic/implementation/global/basic/schedule.v
index 8f9aa1442a4114af19f3d854d0dcecdbe1fd0c38..9bf0d619699838ea38bc89c101c5da9bd3262c34 100644
--- a/classic/implementation/global/basic/schedule.v
+++ b/classic/implementation/global/basic/schedule.v
@@ -138,6 +138,7 @@ Module ConcreteScheduler.
{
rewrite mem_sort mem_filter PENDING andTb.
move: PENDING => /andP [ARRIVED _].
+ try ( by apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival) ) ||
by apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival).
}
apply nth_or_none_mem_exists in IN; des.
@@ -180,6 +181,7 @@ Module ConcreteScheduler.
intros j t cpu1 cpu2 SCHED1 SCHED2.
rewrite 2!scheduler_nth_or_none_mapping in SCHED1 SCHED2.
set l := sorted_pending_jobs _ _ _ _ _ _ _ in SCHED1 SCHED2.
+ try ( apply ord_inj, nth_or_none_uniq with (l0 := l) (x := j); try (by done) ) ||
apply ord_inj, nth_or_none_uniq with (l := l) (x := j); try (by done).
by rewrite sort_uniq filter_uniq //; eapply arrivals_uniq; eauto 1.
Qed.
@@ -211,6 +213,7 @@ Module ConcreteScheduler.
move: SCHED SCHED' => /eqP SCHED /eqP SCHED'.
rewrite 2!scheduler_nth_or_none_mapping in SCHED SCHED'.
set l := sorted_pending_jobs _ _ _ _ _ _ _ in SCHED SCHED'.
+ try ( apply nth_or_none_uniq with (l0 := l) (x := j); try (by done) ) ||
apply nth_or_none_uniq with (l := l) (x := j); try (by done).
by rewrite sort_uniq filter_uniq //; eapply arrivals_uniq; eauto 1.
}
diff --git a/classic/implementation/global/jitter/bertogna_edf_example.v b/classic/implementation/global/jitter/bertogna_edf_example.v
index 49c748d91f421c01f306a0292fe7730d753bdbf0..b2e25bd31c152dd063ce48c24bd0a458b55f53f1 100644
--- a/classic/implementation/global/jitter/bertogna_edf_example.v
+++ b/classic/implementation/global/jitter/bertogna_edf_example.v
@@ -110,6 +110,9 @@ Module ResponseTimeAnalysisEDF.
have VALIDTS := ts_has_valid_parameters.
unfold valid_sporadic_job_with_jitter,
valid_sporadic_job, valid_realtime_job in *; des.
+ try ( apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period)
+ (task_deadline := task_deadline) (ts0 := ts) (task_jitter := task_jitter)
+ (job_jitter := job_jitter); try (by done) ) ||
apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (ts := ts) (task_jitter := task_jitter)
(job_jitter := job_jitter); try (by done).
@@ -134,4 +137,4 @@ Module ResponseTimeAnalysisEDF.
End ExampleRTA.
-End ResponseTimeAnalysisEDF.
\ No newline at end of file
+End ResponseTimeAnalysisEDF.
diff --git a/classic/implementation/global/jitter/bertogna_fp_example.v b/classic/implementation/global/jitter/bertogna_fp_example.v
index 00a3ed257ab9727deb8fbfb0a4c5898f91a9d9b3..7f907041fb359891c5f150b088c0d1352befb427 100644
--- a/classic/implementation/global/jitter/bertogna_fp_example.v
+++ b/classic/implementation/global/jitter/bertogna_fp_example.v
@@ -147,6 +147,10 @@ Module ResponseTimeAnalysisFP.
have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
have TSVALID := ts_has_valid_parameters.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job, valid_realtime_job in *; des.
+ try ( apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
+ (task_period := task_period) (task_deadline := task_deadline)
+ (task_jitter := task_jitter) (job_jitter := job_jitter)
+ (ts0 := ts) (higher_priority0 := RM task_period); try (by done) ) ||
apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline)
(task_jitter := task_jitter) (job_jitter := job_jitter)
@@ -175,4 +179,4 @@ Module ResponseTimeAnalysisFP.
End ExampleRTA.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/implementation/global/jitter/schedule.v b/classic/implementation/global/jitter/schedule.v
index 885cb48b303d6a9cffb4c5c694459eeaca5783d3..bfb5c1ba58027d6f8fea86c65bea9f7c25716649 100644
--- a/classic/implementation/global/jitter/schedule.v
+++ b/classic/implementation/global/jitter/schedule.v
@@ -141,6 +141,7 @@ Module ConcreteScheduler.
{
rewrite mem_sort mem_filter PENDING andTb.
move: PENDING => /andP [ARRIVED _].
+ try ( by apply arrived_between_implies_in_actual_arrivals with (job_arrival0 := job_arrival) ) ||
by apply arrived_between_implies_in_actual_arrivals with (job_arrival := job_arrival).
}
apply nth_or_none_mem_exists in IN; des.
@@ -185,6 +186,7 @@ Module ConcreteScheduler.
intros j t cpu1 cpu2 SCHED1 SCHED2.
rewrite 2!scheduler_nth_or_none_mapping in SCHED1 SCHED2.
set l := sorted_pending_jobs _ _ _ _ _ _ _ _ in SCHED1 SCHED2.
+ try ( apply ord_inj, nth_or_none_uniq with (l0 := l) (x := j); try (by done) ) ||
apply ord_inj, nth_or_none_uniq with (l := l) (x := j); try (by done).
by rewrite sort_uniq filter_uniq // /actual_arrivals_up_to; apply actual_arrivals_uniq.
Qed.
@@ -216,6 +218,7 @@ Module ConcreteScheduler.
move: SCHED SCHED' => /eqP SCHED /eqP SCHED'.
rewrite 2!scheduler_nth_or_none_mapping in SCHED SCHED'.
set l := sorted_pending_jobs _ _ _ _ _ _ _ _ in SCHED SCHED'.
+ try ( apply nth_or_none_uniq with (l0 := l) (x := j); try (by done) ) ||
apply nth_or_none_uniq with (l := l) (x := j); try (by done).
by rewrite sort_uniq filter_uniq //; apply actual_arrivals_uniq.
}
diff --git a/classic/implementation/global/parallel/bertogna_edf_example.v b/classic/implementation/global/parallel/bertogna_edf_example.v
index 4252b579a5dd88fbefc9b480a6fd61599ab301ff..80f9fb7f164e98a78d7d65d61910b7bf53b61454 100644
--- a/classic/implementation/global/parallel/bertogna_edf_example.v
+++ b/classic/implementation/global/parallel/bertogna_edf_example.v
@@ -113,6 +113,8 @@ Module ResponseTimeAnalysisEDF.
have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
have TSVALID := ts_has_valid_parameters.
unfold valid_sporadic_job, valid_realtime_job in *; des.
+ try ( apply taskset_schedulable_by_edf_rta with (task_cost := task_cost)
+ (task_period := task_period) (task_deadline := task_deadline) (ts0 := ts); try (by done) ) ||
apply taskset_schedulable_by_edf_rta with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline) (ts := ts); try (by done).
- by apply ts_has_constrained_deadlines.
@@ -133,4 +135,4 @@ Module ResponseTimeAnalysisEDF.
End ExampleRTA.
-End ResponseTimeAnalysisEDF.
\ No newline at end of file
+End ResponseTimeAnalysisEDF.
diff --git a/classic/implementation/global/parallel/bertogna_fp_example.v b/classic/implementation/global/parallel/bertogna_fp_example.v
index f1c7175bc0f88fc57128bfa4eaa3a6739a8fd55c..39b37c91256b0b469ed690693a387101f6ae1c91 100644
--- a/classic/implementation/global/parallel/bertogna_fp_example.v
+++ b/classic/implementation/global/parallel/bertogna_fp_example.v
@@ -166,6 +166,9 @@ Module ResponseTimeAnalysisFP.
have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
have TSVALID := ts_has_valid_parameters.
unfold valid_sporadic_job, valid_realtime_job in *; des.
+ try ( apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
+ (task_period := task_period) (task_deadline := task_deadline)
+ (ts0 := ts) (higher_priority0 := RM task_period); try (by done) ) ||
apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline)
(ts := ts) (higher_priority := RM task_period); try (by done).
@@ -190,4 +193,4 @@ Module ResponseTimeAnalysisFP.
End ExampleRTA.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/implementation/uni/basic/fp_rta_example.v b/classic/implementation/uni/basic/fp_rta_example.v
index 363b126bca6af5776c167f0dd3dc2f77fa13b185..f7c662d21052a7f3f264e4fb6681a579d82adfbe 100644
--- a/classic/implementation/uni/basic/fp_rta_example.v
+++ b/classic/implementation/uni/basic/fp_rta_example.v
@@ -136,6 +136,9 @@ Module ResponseTimeAnalysisFP.
have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
have TSVALID := ts_has_valid_parameters.
unfold valid_sporadic_job, valid_realtime_job in *; des.
+ try ( apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
+ (task_period := task_period) (task_deadline := task_deadline)
+ (ts0 := ts) (higher_eq_priority0 := RM task_period); try (by done) ) ||
apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline)
(ts := ts) (higher_eq_priority := RM task_period); try (by done).
@@ -157,4 +160,4 @@ Module ResponseTimeAnalysisFP.
End ExampleRTA.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/implementation/uni/basic/schedule.v b/classic/implementation/uni/basic/schedule.v
index 3f3f448d5a340b942cc955d295805b5f0ddf3d39..28e99a4d58f509f3f7166e51dd725e251677535a 100644
--- a/classic/implementation/uni/basic/schedule.v
+++ b/classic/implementation/uni/basic/schedule.v
@@ -62,7 +62,8 @@ Module ConcreteScheduler.
suff SAME: pending_jobs sched1 t = pending_jobs sched2 t by rewrite SAME.
apply eq_in_filter.
intros j ARR.
- apply in_arrivals_implies_arrived_before with (job_arrival := job_arrival) in ARR;
+ ( try ( apply in_arrivals_implies_arrived_before with (job_arrival0 := job_arrival) in ARR ) ||
+ apply in_arrivals_implies_arrived_before with (job_arrival := job_arrival) in ARR);
last by done.
rewrite /arrived_before ltnS in ARR.
rewrite /pending /has_arrived ARR 2!andTb; f_equal.
@@ -188,4 +189,4 @@ Module ConcreteScheduler.
End Proofs.
-End ConcreteScheduler.
\ No newline at end of file
+End ConcreteScheduler.
diff --git a/classic/implementation/uni/basic/schedule_tdma.v b/classic/implementation/uni/basic/schedule_tdma.v
index 9f85d159ce2e3896503c514ae7d733cbe1de0884..6f82352bfb344179294ed7643e3e23187ae70006 100644
--- a/classic/implementation/uni/basic/schedule_tdma.v
+++ b/classic/implementation/uni/basic/schedule_tdma.v
@@ -66,6 +66,8 @@ Module ConcreteSchedulerTDMA.
Lemma pending_jobs_uniq:
uniq pending_jobs.
Proof.
+ try ( apply filter_uniq
+ , arrivals_uniq with (job_arrival0:=job_arrival);auto ) ||
apply filter_uniq
, arrivals_uniq with (job_arrival:=job_arrival);auto.
Qed.
@@ -132,6 +134,7 @@ Module ConcreteSchedulerTDMA.
intros* ARRJ PEN.
rewrite mem_filter. apply /andP. split.
apply PEN. rewrite /jobs_arrived_up_to.
+ try ( apply arrived_between_implies_in_arrivals with (job_arrival0:=job_arrival) ) ||
apply arrived_between_implies_in_arrivals with (job_arrival:=job_arrival).
apply H_arrival_times_are_consistent. auto.
rewrite /arrived_between. simpl.
@@ -169,6 +172,8 @@ Module ConcreteSchedulerTDMA.
rewrite /job_to_schedule. f_equal.
apply eq_in_filter.
intros j ARR.
+ try ( apply in_arrivals_implies_arrived_before
+ with (job_arrival0 := job_arrival) in ARR ) ||
apply in_arrivals_implies_arrived_before
with (job_arrival := job_arrival) in ARR.
rewrite /arrived_before ltnS in ARR.
@@ -226,4 +231,4 @@ Module ConcreteSchedulerTDMA.
End ImplementationTDMA.
-End ConcreteSchedulerTDMA.
\ No newline at end of file
+End ConcreteSchedulerTDMA.
diff --git a/classic/implementation/uni/basic/tdma_rta_example.v b/classic/implementation/uni/basic/tdma_rta_example.v
index 433541a299aced501fe700f0ad9a156b61c3e730..403c393bf0508cfb478f208b60eeaae71fecf9e8 100644
--- a/classic/implementation/uni/basic/tdma_rta_example.v
+++ b/classic/implementation/uni/basic/tdma_rta_example.v
@@ -126,6 +126,7 @@ Module ResponseTimeAnalysisExemple.
have SAMETSK: job_task j = job_task y.
have EQ:Task_in_time_slot ts slot_order (job_task y) time_slot t =
Task_in_time_slot ts slot_order (job_task j) time_slot t by rewrite INSLOT.
+ try ( apply task_in_time_slot_uniq with (ts0:= ts) (t0:=t) (slot_order:=slot_order) (task_time_slot:=time_slot);auto ) ||
apply task_in_time_slot_uniq with (ts:= ts) (t:=t) (slot_order:=slot_order) (task_time_slot:=time_slot);auto.
intros;by apply slot_order_total.
by apply slot_order_antisymmetric.
@@ -136,9 +137,11 @@ Module ResponseTimeAnalysisExemple.
by apply valid_time_slots ,periodic_arrivals_all_jobs_from_taskset.
split;auto.
* split;case (y==j)eqn:YJ;move/eqP in YJ;try by rewrite FIND YJ in NSJ;move/eqP in NSJ;auto.
- apply pending_job_in_penging_list with (arr_seq:=arr_seq) in PEN;auto
+ ( try ( apply pending_job_in_penging_list with (arr_seq0:=arr_seq) in PEN ) ||
+ apply pending_job_in_penging_list with (arr_seq:=arr_seq) in PEN);auto
;last apply job_arrival_times_are_consistent.
- apply findP_FIFO with (y:=j) in FIND;auto. fold sched in FIND.
+ ( try ( apply findP_FIFO with (y0:=j) in FIND ) ||
+ apply findP_FIFO with (y:=j) in FIND);auto. fold sched in FIND.
apply (respects_FIFO ) in FIND;auto.
apply periodic_arrivals_are_sporadic with (ts:=ts) in FIND;auto.
have PERIODY:task_period (job_task y)>0 by
@@ -196,6 +199,10 @@ Module ResponseTimeAnalysisExemple.
Proof.
intros tsk tskIN.
have VALID_JOB := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
+ try ( apply taskset_schedulable_by_tdma with (task_deadline:=task_deadline)(task_period:=task_period)
+ (tsk0:=tsk)(ts0:=ts)(task_cost:=task_cost)
+ (task_time_slot:=time_slot) (slot_order:= slot_order)
+ (arr_seq0:=arr_seq) ) ||
apply taskset_schedulable_by_tdma with (task_deadline:=task_deadline)(task_period:=task_period)
(tsk:=tsk)(ts:=ts)(task_cost:=task_cost)
(task_time_slot:=time_slot) (slot_order:= slot_order)
@@ -218,7 +225,3 @@ Module ResponseTimeAnalysisExemple.
End ExampleTDMA.
End ResponseTimeAnalysisExemple.
-
-
-
-
diff --git a/classic/implementation/uni/jitter/fp_rta_example.v b/classic/implementation/uni/jitter/fp_rta_example.v
index 6b6e1e6dbe66a10d3511b8d8dd8e49cef7d0e3ab..9ff1556ab460ca1d2f5400c7c71ef657d4adb158 100644
--- a/classic/implementation/uni/jitter/fp_rta_example.v
+++ b/classic/implementation/uni/jitter/fp_rta_example.v
@@ -153,6 +153,10 @@ Module ResponseTimeAnalysisFP.
rename H_jitter_is_bounded into JIT.
intros tsk IN.
unfold valid_sporadic_job, valid_realtime_job in *; des.
+ try ( apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
+ (task_period := task_period) (task_deadline := task_deadline) (ts0 := ts)
+ (higher_eq_priority0 := RM task_period) (job_jitter0 := job_jitter)
+ (task_jitter := task_jitter); try (by done) ) ||
apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline) (ts := ts)
(higher_eq_priority := RM task_period) (job_jitter := job_jitter)
@@ -179,4 +183,4 @@ Module ResponseTimeAnalysisFP.
End ExampleRTA.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v b/classic/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
index 594c18eb3968de6fd115a005346146f963cb8d06..fb35791f9b07cef859c181786ac2b6bbf08a1152 100644
--- a/classic/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
+++ b/classic/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
@@ -156,6 +156,10 @@ Module ResponseTimeAnalysisFP.
have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
have TSVALID := ts_has_valid_parameters.
unfold valid_sporadic_job, valid_realtime_job in *; des.
+ try ( apply suspension_oblivious_fp_rta_implies_schedulability with (task_cost := task_cost)
+ (task_period := task_period) (task_deadline := task_deadline) (ts0 := ts)
+ (higher_eq_priority0 := RM task_period) (next_suspension0 := next_suspension)
+ (task_suspension_bound := task_suspension_bound); try (by done) ) ||
apply suspension_oblivious_fp_rta_implies_schedulability with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline) (ts := ts)
(higher_eq_priority := RM task_period) (next_suspension := next_suspension)
@@ -181,4 +185,4 @@ Module ResponseTimeAnalysisFP.
End ExampleRTA.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/implementation/uni/susp/schedule.v b/classic/implementation/uni/susp/schedule.v
index 8484195e9e20e3c574af2fd7951bdc3bc569eab0..4d191d8087341b55214a9e59bcff1d7db3be4d01 100644
--- a/classic/implementation/uni/susp/schedule.v
+++ b/classic/implementation/uni/susp/schedule.v
@@ -68,7 +68,8 @@ Module ConcreteScheduler.
suff SAME: pending_jobs sched1 t = pending_jobs sched2 t by rewrite SAME.
apply eq_in_filter.
rewrite /jobs_arrived_up_to; intros j IN.
- apply in_arrivals_implies_arrived_before with (job_arrival := job_arrival) in IN;
+ ( try ( apply in_arrivals_implies_arrived_before with (job_arrival0 := job_arrival) in IN ) ||
+ apply in_arrivals_implies_arrived_before with (job_arrival := job_arrival) in IN);
last by done.
rewrite /arrived_before ltnS in IN.
rewrite /pending /has_arrived IN 2!andTb.
@@ -248,4 +249,4 @@ Module ConcreteScheduler.
End Proofs.
-End ConcreteScheduler.
\ No newline at end of file
+End ConcreteScheduler.
diff --git a/classic/model/arrival/basic/arrival_bounds.v b/classic/model/arrival/basic/arrival_bounds.v
index 094b5acc2e7dfc5674e5e6457bf30b5563a7a005..33e8e7da83f026bcd4bb56f72b4266c4b0b3abf4 100644
--- a/classic/model/arrival/basic/arrival_bounds.v
+++ b/classic/model/arrival/basic/arrival_bounds.v
@@ -73,7 +73,8 @@ Module ArrivalBounds.
destruct arriving_jobs as [| j l] eqn:EQ; first by done.
have IN: j \in arriving_jobs by rewrite EQ in_cons eq_refl orTb.
rewrite mem_filter in IN; move: IN => /andP [_ ARR].
- apply in_arrivals_implies_arrived_between with (job_arrival := job_arrival) in ARR;
+ ( try ( apply in_arrivals_implies_arrived_between with (job_arrival0 := job_arrival) in ARR ) ||
+ apply in_arrivals_implies_arrived_between with (job_arrival := job_arrival) in ARR);
last by done.
move: ARR => /andP [GE LT].
by apply: (leq_ltn_trans GE).
@@ -223,4 +224,4 @@ Module ArrivalBounds.
End Lemmas.
-End ArrivalBounds.
\ No newline at end of file
+End ArrivalBounds.
diff --git a/classic/model/arrival/jitter/arrival_sequence.v b/classic/model/arrival/jitter/arrival_sequence.v
index 0bbb20ebb5262436205e2884870413b1960102b3..fcfcd0bbfaae83f97936d5e39422bd0973572d9b 100644
--- a/classic/model/arrival/jitter/arrival_sequence.v
+++ b/classic/model/arrival/jitter/arrival_sequence.v
@@ -84,6 +84,8 @@ Module ArrivalSequenceWithJitter.
case (ltnP (actual_job_arrival j) t) => [BEFORE | AFTER]; last by right; rewrite LT2.
left; rewrite GE1 /=.
have INarr: arrives_in arr_seq j by apply in_arrivals_implies_arrived in IN.
+ try ( apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival);
+ try (by done) ) ||
apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival);
try (by done).
by apply: (leq_ltn_trans _ BEFORE); apply leq_addr.
@@ -95,6 +97,8 @@ Module ArrivalSequenceWithJitter.
rewrite mem_filter GE0 /=.
apply/andP; split; first by apply: (leq_trans _ LE).
have INarr: arrives_in arr_seq j by apply in_arrivals_implies_arrived in IN0.
+ try ( apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival);
+ try (by done) ) ||
apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival);
try (by done).
rewrite /arrived_between /=.
@@ -105,6 +109,8 @@ Module ArrivalSequenceWithJitter.
rewrite mem_filter LT0 /= andbT.
apply/andP; split; first by apply: (leq_trans GE).
have INarr: arrives_in arr_seq j by apply in_arrivals_implies_arrived in IN0.
+ try ( apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival);
+ try (by done) ) ||
apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival);
try (by done).
by apply: (leq_ltn_trans _ LT0); apply leq_addr.
@@ -220,4 +226,4 @@ Module ArrivalSequenceWithJitter.
End ArrivingJobs.
-End ArrivalSequenceWithJitter.
\ No newline at end of file
+End ArrivalSequenceWithJitter.
diff --git a/classic/model/schedule/apa/constrained_deadlines.v b/classic/model/schedule/apa/constrained_deadlines.v
index 542e448f63630078f579a5e2d2e162acb93ffe44..e201d732a98f4ddee3a37828f45b5670ecaee131 100644
--- a/classic/model/schedule/apa/constrained_deadlines.v
+++ b/classic/model/schedule/apa/constrained_deadlines.v
@@ -117,6 +117,7 @@ Module ConstrainedDeadlines.
}
exploit (PREV j1 (job_task j1)); try (by done).
intros COMP1; apply NOTCOMP1.
+ try ( by apply completion_monotonic with (t0 := job_arrival j1 + task_period (job_task j1)) ) ||
by apply completion_monotonic with (t := job_arrival j1 + task_period (job_task j1)).
}
{
@@ -128,6 +129,7 @@ Module ConstrainedDeadlines.
}
exploit (PREV j2 (job_task j2)); try (by done).
intros COMP2; apply NOTCOMP2.
+ try ( by apply completion_monotonic with (t0 := job_arrival j2 + task_period (job_task j2)) ) ||
by apply completion_monotonic with (t := job_arrival j2 + task_period (job_task j2)).
}
Qed.
@@ -228,6 +230,7 @@ Module ConstrainedDeadlines.
by apply leq_trans with (n := job_arrival j2).
exploit (PREV j1 (job_task j1) ARR1); [by done | by apply INTERF | intros COMP1].
apply NOTCOMP1.
+ try ( by apply completion_monotonic with (t0 := job_arrival j1 + task_period (job_task j1)) ) ||
by apply completion_monotonic with (t := job_arrival j1 + task_period (job_task j1)).
}
{
@@ -238,6 +241,7 @@ Module ConstrainedDeadlines.
exploit (PREV j2 (job_task j2) ARR2);
[by done | by rewrite -SAMEtsk | intro COMP2 ].
apply NOTCOMP2.
+ try ( by apply completion_monotonic with (t0 := job_arrival j2 + task_period (job_task j2)) ) ||
by apply completion_monotonic with (t := job_arrival j2 + task_period (job_task j2)).
}
Qed.
@@ -266,7 +270,8 @@ Module ConstrainedDeadlines.
assert (LEt: job_arrival j' + task_period tsk <= t).
by apply leq_trans with (n := job_arrival j); first by rewrite -SAMEtsk.
apply NOTCOMP'.
- apply completion_monotonic with (t := job_arrival j' + task_period tsk); [by done |].
+ (try ( apply completion_monotonic with (t0 := job_arrival j' + task_period tsk) ) ||
+ apply completion_monotonic with (t := job_arrival j' + task_period tsk)); [by done |].
apply PREVtsk; try (by done).
apply leq_trans with (n := job_arrival j' + task_period tsk); last by rewrite -SAMEtsk.
rewrite -addn1; apply leq_add; first by done.
@@ -285,4 +290,4 @@ Module ConstrainedDeadlines.
End Lemmas.
-End ConstrainedDeadlines.
\ No newline at end of file
+End ConstrainedDeadlines.
diff --git a/classic/model/schedule/global/basic/constrained_deadlines.v b/classic/model/schedule/global/basic/constrained_deadlines.v
index c52c2609e9201389668ccab902c8cc293a1ec305..6879906301527a6ed7820c4a75a1ba6b72df435f 100644
--- a/classic/model/schedule/global/basic/constrained_deadlines.v
+++ b/classic/model/schedule/global/basic/constrained_deadlines.v
@@ -112,7 +112,8 @@ Module ConstrainedDeadlines.
exploit (PREV j1 (job_task j1) ARR1);
[by done | by apply leq_trans with (n := job_arrival j2) | intros COMP1].
apply NOTCOMP1.
- apply completion_monotonic with (t := job_arrival j1 + task_period (job_task j1));
+ ( try ( apply completion_monotonic with (t0 := job_arrival j1 + task_period (job_task j1)) ) ||
+ apply completion_monotonic with (t := job_arrival j1 + task_period (job_task j1)));
try (by done).
by apply leq_trans with (n := job_arrival j2).
}
@@ -122,7 +123,8 @@ Module ConstrainedDeadlines.
exploit (PREV j2 (job_task j2) ARR2);
[by done | by apply leq_trans with (n := job_arrival j1) | intros COMP2].
apply NOTCOMP2.
- apply completion_monotonic with (t := job_arrival j2 + task_period (job_task j2));
+ ( try ( apply completion_monotonic with (t0 := job_arrival j2 + task_period (job_task j2)) ) ||
+ apply completion_monotonic with (t := job_arrival j2 + task_period (job_task j2)));
try (by done).
by apply leq_trans with (n := job_arrival j1).
}
@@ -292,7 +294,8 @@ Module ConstrainedDeadlines.
specialize (SPO j1 j2 DIFF ARR1 ARR2 SAMEtsk BEFORE1).
exploit (PREV j1 (job_task j1) ARR1); [by done | by apply INTERF | intros COMP1].
apply NOTCOMP1.
- apply completion_monotonic with (t := job_arrival j1 + task_period (job_task j1));
+ ( try ( apply completion_monotonic with (t0 := job_arrival j1 + task_period (job_task j1)) ) ||
+ apply completion_monotonic with (t := job_arrival j1 + task_period (job_task j1)));
try (by done).
by apply leq_trans with (n := job_arrival j2).
}
@@ -302,7 +305,8 @@ Module ConstrainedDeadlines.
exploit (PREV j2 (job_task j2) ARR2);
[by done | by rewrite -SAMEtsk | intro COMP2 ].
apply NOTCOMP2.
- apply completion_monotonic with (t := job_arrival j2 + task_period (job_task j2));
+ ( try ( apply completion_monotonic with (t0 := job_arrival j2 + task_period (job_task j2)) ) ||
+ apply completion_monotonic with (t := job_arrival j2 + task_period (job_task j2)));
try (by done).
by apply leq_trans with (n := job_arrival j1).
}
@@ -330,7 +334,8 @@ Module ConstrainedDeadlines.
{
exploit (SPO j' j DIFF ARR' H_j_arrives); [by rewrite JOBtsk | by done | intro SPO'].
apply NOTCOMP'.
- apply completion_monotonic with (t := job_arrival j' + task_period tsk); try (by done);
+ ( try ( apply completion_monotonic with (t0 := job_arrival j' + task_period tsk) ) ||
+ apply completion_monotonic with (t := job_arrival j' + task_period tsk)); try (by done);
first by apply leq_trans with (n := job_arrival j); [by rewrite -SAMEtsk | by done].
{
apply PREVtsk; try (by done).
@@ -427,8 +432,10 @@ Module ConstrainedDeadlines.
apply/eqP; red; intro SAMEtsk.
generalize SCHED'; intro PENDING'.
have ARRin': arrives_in arr_seq j' by apply (FROMarr j' t).
+ ( try ( apply scheduled_implies_pending with (job_arrival0 := job_arrival)
+ (job_cost0 := job_cost) in PENDING' ) ||
apply scheduled_implies_pending with (job_arrival := job_arrival)
- (job_cost := job_cost) in PENDING'; try (by done).
+ (job_cost := job_cost) in PENDING'); try (by done).
specialize (UNIQ' j' ARRin' PENDING' SAMEtsk); subst j'.
by move: BACK => /andP [_ NOTSCHED]; rewrite SCHED' in NOTSCHED.
}
@@ -440,4 +447,4 @@ Module ConstrainedDeadlines.
End Lemmas.
-End ConstrainedDeadlines.
\ No newline at end of file
+End ConstrainedDeadlines.
diff --git a/classic/model/schedule/global/jitter/constrained_deadlines.v b/classic/model/schedule/global/jitter/constrained_deadlines.v
index 187b0332535f69742839182ef6c7bcc2999027b1..42f7772e40968fe257256c16850021cd63d8725f 100644
--- a/classic/model/schedule/global/jitter/constrained_deadlines.v
+++ b/classic/model/schedule/global/jitter/constrained_deadlines.v
@@ -124,6 +124,7 @@ Module ConstrainedDeadlines.
}
exploit (PREV j1 (job_task j1)); try (by done).
intros COMP1; apply NOTCOMP1.
+ try ( by apply completion_monotonic with (t0 := job_arrival j1 + task_period (job_task j1)) ) ||
by apply completion_monotonic with (t := job_arrival j1 + task_period (job_task j1)).
}
{
@@ -136,6 +137,7 @@ Module ConstrainedDeadlines.
}
exploit (PREV j2 (job_task j2)); try (by done).
intros COMP2; apply NOTCOMP2.
+ try ( by apply completion_monotonic with (t0 := job_arrival j2 + task_period (job_task j2)) ) ||
by apply completion_monotonic with (t := job_arrival j2 + task_period (job_task j2)).
}
Qed.
@@ -310,6 +312,7 @@ Module ConstrainedDeadlines.
}
exploit (PREV j1 (job_task j1) ARRin1); [by done | by apply INTERF | intros COMP1].
apply NOTCOMP1.
+ try ( by apply completion_monotonic with (t0 := job_arrival j1 + task_period (job_task j1)) ) ||
by apply completion_monotonic with (t := job_arrival j1 + task_period (job_task j1)).
}
{
@@ -325,6 +328,7 @@ Module ConstrainedDeadlines.
exploit (PREV j2 (job_task j2) ARRin2);
[by done | by rewrite -SAMEtsk | intro COMP2 ].
apply NOTCOMP2.
+ try ( by apply completion_monotonic with (t0 := job_arrival j2 + task_period (job_task j2)) ) ||
by apply completion_monotonic with (t := job_arrival j2 + task_period (job_task j2)).
}
Qed.
@@ -356,6 +360,7 @@ Module ConstrainedDeadlines.
by apply leq_trans with (n := job_arrival j + job_jitter j); first by apply leq_addr.
}
apply NOTCOMP'.
+ try ( apply completion_monotonic with (t0 := job_arrival j' + task_period tsk); try (by done) ) ||
apply completion_monotonic with (t := job_arrival j' + task_period tsk); try (by done).
apply PREVtsk; try (by done).
apply leq_trans with (n := job_arrival j' + task_period tsk); last by rewrite -SAMEtsk.
@@ -454,6 +459,8 @@ Module ConstrainedDeadlines.
apply/eqP; red; intro SAMEtsk.
generalize SCHED'; intro PENDING'.
have ARRin': arrives_in arr_seq j' by apply (FROMarr j' t).
+ try ( apply scheduled_implies_pending with (job_arrival0 := job_arrival)
+ (job_cost0 := job_cost) (job_jitter0 := job_jitter) in PENDING'; try (by done) ) ||
apply scheduled_implies_pending with (job_arrival := job_arrival)
(job_cost := job_cost) (job_jitter := job_jitter) in PENDING'; try (by done).
specialize (UNIQ' j' ARRin' PENDING' SAMEtsk); subst j'.
@@ -467,4 +474,4 @@ Module ConstrainedDeadlines.
End Lemmas.
-End ConstrainedDeadlines.
\ No newline at end of file
+End ConstrainedDeadlines.
diff --git a/classic/model/schedule/uni/jitter/busy_interval.v b/classic/model/schedule/uni/jitter/busy_interval.v
index 47a6b0ab98e84b83a4ef69da2128967b51ba36de..913a8964f913628e95f934f631bd9c4150e0f94e 100644
--- a/classic/model/schedule/uni/jitter/busy_interval.v
+++ b/classic/model/schedule/uni/jitter/busy_interval.v
@@ -127,6 +127,7 @@ Module BusyInterval.
move: PEND => /andP [_ /negP NOTCOMP].
move: INT => /andP [LE _].
exfalso; apply NOTCOMP.
+ try ( apply completion_monotonic with (t0 := t1); try (by done) ) ||
apply completion_monotonic with (t := t1); try (by done).
by apply QUIET; [by done | by apply REFL |].
Qed.
@@ -284,6 +285,7 @@ Module BusyInterval.
}
apply/andP; split; first by done.
apply/negP; intro COMP; apply NOTCOMP'.
+ try ( by apply completion_monotonic with (t0 := t) ) ||
by apply completion_monotonic with (t := t).
}
feed (PRIO j_hp' j_hp t IN BACK); first by done.
@@ -292,6 +294,8 @@ Module BusyInterval.
repeat split; [| by done | by done].
{
move: (SCHED) => PENDING.
+ try ( apply scheduled_implies_pending with (job_arrival0 := job_arrival)
+ (job_cost0 := job_cost) (job_jitter0 := job_jitter) in PENDING; try (by done) ) ||
apply scheduled_implies_pending with (job_arrival := job_arrival)
(job_cost := job_cost) (job_jitter := job_jitter) in PENDING; try (by done).
apply/andP; split;
@@ -299,6 +303,7 @@ Module BusyInterval.
apply contraT; rewrite -ltnNge; intro LT; exfalso.
feed (QUIET j_hp); first by eapply FROM, SCHED.
specialize (QUIET HP LT).
+ try ( have COMP: job_completed_by j_hp t by apply completion_monotonic with (t0 := t1) ) ||
have COMP: job_completed_by j_hp t by apply completion_monotonic with (t := t1).
apply completed_implies_not_scheduled in COMP; last by done.
by move: COMP => /negP COMP; apply COMP.
@@ -491,6 +496,7 @@ Module BusyInterval.
intros j' NEQ; destruct (higher_eq_priority j' j); last by done.
apply/eqP; rewrite eqb0; apply/negP; move => SCHED'.
move: NEQ => /eqP NEQ; apply NEQ.
+ try ( by apply only_one_job_scheduled with (sched0 := sched) (t0 := t) ) ||
by apply only_one_job_scheduled with (sched := sched) (t := t).
}
{
@@ -539,7 +545,8 @@ Module BusyInterval.
unfold service_during.
rewrite (ignore_service_before_jitter job_arrival job_jitter) //;
last by apply/andP; split; last by apply ltnW.
- rewrite <- ignore_service_before_jitter with (t1:=0); rewrite //; [|by apply ltnW].
+ ( try ( rewrite <- ignore_service_before_jitter with (t2:=0)) ||
+ rewrite <- ignore_service_before_jitter with (t1:=0)); rewrite //; [|by apply ltnW].
by rewrite ltnNge; apply/negP.
Qed.
diff --git a/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v b/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
index b3bcc0a1a18b892df759bbc8f5fd2b2f4f8ac5ca..59f720fd69b820e319acbc852aa8e6b6dec6acf4 100644
--- a/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
+++ b/classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
@@ -612,6 +612,9 @@ Module AbstractSeqRTA.
response_time_bounded_by tsk R.
Proof.
intros j ARR TSK.
+ try ( eapply uniprocessor_response_time_bound with
+ (interference_bound_function := fun tsk A R => task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A R)
+ (interfering_workload0 := interfering_workload); eauto 2 ) ||
eapply uniprocessor_response_time_bound with
(interference_bound_function := fun tsk A R => task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A R)
(interfering_workload := interfering_workload); eauto 2.
@@ -636,4 +639,3 @@ Module AbstractSeqRTA.
End Sequential_Abstract_RTA.
End AbstractSeqRTA.
-
diff --git a/classic/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v b/classic/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
index ea257da89c944b4996cd7fde5ce7ceda723a7dd3..0c985ecd4c5abede7fa53d3e432a9abaca0400a0 100644
--- a/classic/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
+++ b/classic/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
@@ -211,6 +211,7 @@ Module AbstractRTALockInService.
rewrite subnKC //.
apply/negP; intros COMPL.
move: CONTR => /negP Temp; apply: Temp.
+ try ( apply completion_monotonic with (t0 := t'); try done ) ||
apply completion_monotonic with (t := t'); try done.
}
have SERV: job_last + 1 <= \sum_(t <= t' < t + (job_last + 1)) service_at sched j t'.
@@ -239,4 +240,3 @@ Module AbstractRTALockInService.
End LockInService.
End AbstractRTALockInService.
-
diff --git a/classic/model/schedule/uni/limited/busy_interval.v b/classic/model/schedule/uni/limited/busy_interval.v
index 3dc5b47bab38ba492adbb6d3c52a7f386d1f303e..18817801ccdd6b300f9267ad8802a1e0ddb794fe 100644
--- a/classic/model/schedule/uni/limited/busy_interval.v
+++ b/classic/model/schedule/uni/limited/busy_interval.v
@@ -236,7 +236,8 @@ Module BusyIntervalJLFP.
{
move: COMP => /hasP [j_hp ARR /andP [NOTCOMP HP]].
move: (ARR) => INarr.
- apply in_arrivals_implies_arrived_between with (job_arrival := job_arrival) in ARR;
+ ( try ( apply in_arrivals_implies_arrived_between with (job_arrival0 := job_arrival) in ARR ) ||
+ apply in_arrivals_implies_arrived_between with (job_arrival := job_arrival) in ARR);
last by done.
apply in_arrivals_implies_arrived in INarr.
by exists j_hp; repeat split; last by apply/negP.
@@ -327,6 +328,7 @@ Module BusyIntervalJLFP.
{ move: H => [ARR [PEN HP]].
rewrite mem_filter.
apply/andP; split; first (apply/andP; split); try done.
+ try ( apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival); try done ) ||
apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival); try done.
apply/andP; split; first by done.
rewrite ltnS.
@@ -740,7 +742,7 @@ Module BusyIntervalJLFP.
}
unfold service_during.
rewrite (ignore_service_before_arrival job_arrival); rewrite //; [| by apply ltnW].
- rewrite <- ignore_service_before_arrival with (t1:=0); rewrite //; [|by apply ltnW].
+ ( try ( rewrite <- ignore_service_before_arrival with (t2:=0)) || rewrite <- ignore_service_before_arrival with (t1:=0)); rewrite //; [|by apply ltnW].
by rewrite ltnNge; apply/negP.
Qed.
@@ -1215,4 +1217,3 @@ Module BusyIntervalJLFP.
End Definitions.
End BusyIntervalJLFP.
-
diff --git a/classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v b/classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
index e0367babc249b747d692b2b370d4906184a98e22..e8904850ce1830d68f945229fe29f9b484b2364f 100644
--- a/classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
@@ -236,6 +236,12 @@ Module RTAforConcreteModels.
}
by rewrite /is_response_time_bound_of_job /completed_by ZEROj.
}
+ try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with
+ (job_max_nps := fun j => job_cost j)
+ (task_max_nps := fun tsk => task_cost tsk)
+ (job_lock_in_service := fun j => ε)
+ (task_lock_in_service := fun tsk => ε)
+ (L0 := L); eauto 2 ) ||
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with
(job_max_nps := fun j => job_cost j)
(task_max_nps := fun tsk => task_cost tsk)
@@ -358,6 +364,11 @@ Module RTAforConcreteModels.
by rewrite -(leq_add2r 1) !addn1 prednK //.
}
}
+ try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments
+ with (task_lock_in_service := fun tsk => (task_cost tsk - (task_last_nps tsk - ε)))
+ (job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
+ (L0 := L)(job_cost0 := job_cost) (task_max_nps0 := task_max_nps)
+ ; eauto 2 ) ||
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments
with (task_lock_in_service := fun tsk => (task_cost tsk - (task_last_nps tsk - ε)))
(job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
@@ -417,7 +428,9 @@ Module RTAforConcreteModels.
apply/andP; split; first by done.
rewrite prednK; first by done.
rewrite -(leq_add2r 1) !addn1 prednK.
+ try ( eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2 ) ||
eapply number_of_preemption_points_at_least_two with (job_cost := job_cost); eauto 2.
+ try ( eapply list_of_preemption_point_is_not_empty with (job_cost0 := job_cost); eauto 2 ) ||
eapply list_of_preemption_point_is_not_empty with (job_cost := job_cost); eauto 2.
}
by done.
@@ -462,6 +475,7 @@ Module RTAforConcreteModels.
rewrite leq_add2r.
apply domination_of_distances_implies_domination_of_seq; try done; eauto 2.
rewrite BEG // BEGj //.
+ try ( eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2 ) ||
eapply number_of_preemption_points_at_least_two with (job_cost := job_cost); eauto 2.
rewrite -TSK; apply HYP1; try done.
intros. rewrite -TSK; eauto 2.
@@ -545,11 +559,16 @@ Module RTAforConcreteModels.
Proof.
move: (H_task_model_with_floating_nonpreemptive_regions) => [LIMJ JMLETM].
move: (LIMJ) => [ZERO [LSMj [BEG [END HH]]]].
+ ( try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments
+ with (task_lock_in_service := fun tsk => task_cost tsk)
+ (job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
+ (L0 := L) (job_max_nps0 := job_max_nps)
+ (job_cost0 := job_cost ) ) ||
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments
with (task_lock_in_service := fun tsk => task_cost tsk)
(job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
(L := L) (job_max_nps := job_max_nps)
- (job_cost := job_cost )
+ (job_cost := job_cost ) )
; eauto 2.
{ by apply model_with_fixed_preemption_points_is_correct. }
{ by eapply model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions; eauto 2. }
@@ -598,7 +617,9 @@ Module RTAforConcreteModels.
apply/andP; split; first by done.
rewrite prednK; first by done.
rewrite -(leq_add2r 1) !addn1 prednK.
+ try ( eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2 ) ||
eapply number_of_preemption_points_at_least_two with (job_cost := job_cost); eauto 2.
+ try ( eapply list_of_preemption_point_is_not_empty with (job_cost0 := job_cost); eauto 2 ) ||
eapply list_of_preemption_point_is_not_empty with (job_cost := job_cost); eauto 2.
}
by done.
@@ -630,4 +651,4 @@ Module RTAforConcreteModels.
End Analysis.
-End RTAforConcreteModels.
\ No newline at end of file
+End RTAforConcreteModels.
diff --git a/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v b/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
index a89b53eee865d6735f8b1709a2c3998870e0eaac..4cb4c88081c823295c361d3cbcc435d51d954686 100644
--- a/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
@@ -275,7 +275,8 @@ Module RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
move: SCHEDHP => [j_hp [ARRB [HP SCHEDHP]]].
apply/eqP; rewrite eqb0 Bool.negb_involutive.
have EQ: s = j_hp.
- { by apply only_one_job_scheduled with (sched := sched) (t := t); [apply/eqP | ]. }
+ { by ( try ( apply only_one_job_scheduled with (sched0 := sched) (t0 := t) ) ||
+ apply only_one_job_scheduled with (sched := sched) (t := t) ); [apply/eqP | ]. }
by rewrite EQ.
rewrite ltn_subRL in NEQ.
apply leq_trans with (t1 + blocking_bound); last by apply ltnW.
diff --git a/classic/model/schedule/uni/limited/edf/response_time_bound.v b/classic/model/schedule/uni/limited/edf/response_time_bound.v
index 4f12c262251a3531e7d3617221ed771478e98a6f..ec3ae03b9a8f9a1af0ccc27cf7f3d1297f0f4bb4 100644
--- a/classic/model/schedule/uni/limited/edf/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/edf/response_time_bound.v
@@ -636,6 +636,9 @@ Module AbstractRTAforEDFwithArrivalCurves.
intros js ARRs TSKs.
move: (posnP (job_cost js)) => [ZERO|POS].
{ by rewrite /is_response_time_bound_of_job /completed_by ZERO. }
+ try ( eapply AbstractSeqRTA.uniprocessor_response_time_bound_seq with
+ (interference0 := interference) (interfering_workload0 := interfering_workload)
+ (task_interference_bound_function := fun tsk A R => IBF A R) (L0 := L); eauto 3 ) ||
eapply AbstractSeqRTA.uniprocessor_response_time_bound_seq with
(interference := interference) (interfering_workload := interfering_workload)
(task_interference_bound_function := fun tsk A R => IBF A R) (L := L); eauto 3.
@@ -648,4 +651,4 @@ Module AbstractRTAforEDFwithArrivalCurves.
End AbstractResponseTimeAnalysisForEDF.
-End AbstractRTAforEDFwithArrivalCurves.
\ No newline at end of file
+End AbstractRTAforEDFwithArrivalCurves.
diff --git a/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v b/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
index 75bc2a0e46ac2dc5293a8e73469dc5154330f85b..52d1fd6d794e553d3810895db68eb51b72cbf347 100644
--- a/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
@@ -212,6 +212,12 @@ Module RTAforConcreteModels.
}
by rewrite /is_response_time_bound_of_job /completed_by ZEROj.
}
+ try ( eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
+ (job_max_nps := fun j => job_cost j)
+ (task_max_nps := fun tsk => task_cost tsk)
+ (job_lock_in_service := fun j => ε)
+ (task_lock_in_service := fun tsk => ε)
+ (L0 := L); eauto 2 ) ||
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
(job_max_nps := fun j => job_cost j)
(task_max_nps := fun tsk => task_cost tsk)
@@ -333,11 +339,16 @@ Module RTAforConcreteModels.
by rewrite -(leq_add2r 1) !addn1 prednK //.
}
}
+ ( try ( eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
+ with (task_lock_in_service := fun tsk => (task_cost tsk - (task_last_nps tsk - ε)))
+ (job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
+ (L0 := L) (job_max_nps0 := job_max_nps)
+ (job_cost0 := job_cost ) ) ||
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
with (task_lock_in_service := fun tsk => (task_cost tsk - (task_last_nps tsk - ε)))
(job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
(L := L) (job_max_nps := job_max_nps)
- (job_cost := job_cost )
+ (job_cost := job_cost ))
; eauto 2.
{ by apply model_with_fixed_preemption_points_is_correct. }
{
@@ -393,7 +404,9 @@ Module RTAforConcreteModels.
apply/andP; split; first by done.
rewrite prednK; first by done.
rewrite -(leq_add2r 1) !addn1 prednK.
+ try ( eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2 ) ||
eapply number_of_preemption_points_at_least_two with (job_cost := job_cost); eauto 2.
+ try ( eapply list_of_preemption_point_is_not_empty with (job_cost0 := job_cost); eauto 2 ) ||
eapply list_of_preemption_point_is_not_empty with (job_cost := job_cost); eauto 2.
}
by done.
@@ -439,6 +452,7 @@ Module RTAforConcreteModels.
rewrite leq_add2r.
apply domination_of_distances_implies_domination_of_seq; try done; eauto 2.
rewrite BEG // BEGj //.
+ try ( eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2 ) ||
eapply number_of_preemption_points_at_least_two with (job_cost := job_cost); eauto 2.
rewrite -TSK; apply HYP1; try done.
intros. rewrite -TSK; eauto 2.
@@ -521,6 +535,11 @@ Module RTAforConcreteModels.
Proof.
move: (H_task_model_with_floating_nonpreemptive_regions) => [LIMJ JMLETM].
move: (LIMJ) => [ZERO [LSMj [BEG [END HH]]]].
+ try ( eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
+ with (task_lock_in_service := fun tsk => task_cost tsk)
+ (job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
+ (L0 := L) (job_max_nps0 := job_max_nps)
+ (job_cost0 := job_cost ) ) ||
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
with (task_lock_in_service := fun tsk => task_cost tsk)
(job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
@@ -573,7 +592,9 @@ Module RTAforConcreteModels.
apply/andP; split; first by done.
rewrite prednK; first by done.
rewrite -(leq_add2r 1) !addn1 prednK.
+ try ( eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2 ) ||
eapply number_of_preemption_points_at_least_two with (job_cost := job_cost); eauto 2.
+ try ( eapply list_of_preemption_point_is_not_empty with (job_cost0 := job_cost); eauto 2 ) ||
eapply list_of_preemption_point_is_not_empty with (job_cost := job_cost); eauto 2.
}
by done.
@@ -606,4 +627,4 @@ Module RTAforConcreteModels.
End Analysis.
-End RTAforConcreteModels.
\ No newline at end of file
+End RTAforConcreteModels.
diff --git a/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v b/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
index 1aedd6fd7c7144a16c91ebb8ff2ba170bc5f8ec2..8e32ca77c23bf5de8dce6e95ee76e13496d9346b 100644
--- a/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
@@ -229,7 +229,8 @@ Module RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
move: SCHEDHP => [j_hp [ARRB [HP SCHEDHP]]].
apply/eqP; rewrite eqb0 Bool.negb_involutive.
have EQ: s = j_hp.
- { by apply only_one_job_scheduled with (sched := sched) (t := t); [apply/eqP | ]. }
+ { by ( try ( apply only_one_job_scheduled with (sched0 := sched) (t0 := t) ) ||
+ apply only_one_job_scheduled with (sched := sched) (t := t)); [apply/eqP | ]. }
by rewrite EQ.
rewrite ltn_subRL in NEQ.
apply leq_trans with (t1 + blocking_bound); last by apply ltnW.
diff --git a/classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v b/classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v
index 48b84c1cd01e4e3f0e3da1f142fe975241668af0..d7648ee4a27c32883bce28e1870db2baa83d96f1 100644
--- a/classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v
@@ -421,6 +421,9 @@ Module AbstractRTAforFPwithArrivalCurves.
{ by rewrite /is_response_time_bound_of_job /completed_by ZERO. }
move: H_proper_job_lock_in_service => [T1 [T2 T3]].
move: H_proper_task_lock_in_service => [T4 T5].
+ try ( eapply AbstractSeqRTA.uniprocessor_response_time_bound_seq with
+ (interference0 := interference) (interfering_workload0 := interfering_workload)
+ (task_interference_bound_function := fun _ A R => IBF R) (L0 := L) (ts0 := ts); eauto 3 ) ||
eapply AbstractSeqRTA.uniprocessor_response_time_bound_seq with
(interference := interference) (interfering_workload := interfering_workload)
(task_interference_bound_function := fun _ A R => IBF R) (L := L) (ts := ts); eauto 3.
@@ -433,4 +436,4 @@ Module AbstractRTAforFPwithArrivalCurves.
End AbstractResponseTimeAnalysisForFP.
-End AbstractRTAforFPwithArrivalCurves.
\ No newline at end of file
+End AbstractRTAforFPwithArrivalCurves.
diff --git a/classic/model/schedule/uni/limited/jlfp_instantiation.v b/classic/model/schedule/uni/limited/jlfp_instantiation.v
index b2637679a4eb73e9eeccedc1151b4d8b5a8be037..58aee51244acef55759e133f186df3ad1499d567 100644
--- a/classic/model/schedule/uni/limited/jlfp_instantiation.v
+++ b/classic/model/schedule/uni/limited/jlfp_instantiation.v
@@ -283,6 +283,7 @@ Module JLFPInstantiation.
apply/hasP; exists j.
{ rewrite /arrivals_of_task_before /arrivals_of_task_between.
rewrite /arrivals_of_task_between mem_filter; apply/andP; split; first by rewrite /is_job_of_task.
+ try ( by unfold jobs_arrived_before in ARR; apply jobs_arrived_between_sub with (t2 := 0) (t3 := upp) ) ||
by unfold jobs_arrived_before in ARR; apply jobs_arrived_between_sub with (t1 := 0) (t2 := upp).
}
{ case HP: (higher_eq_priority s j).
@@ -430,6 +431,7 @@ Module JLFPInstantiation.
rewrite eqn_leq; apply/andP; split; last by apply service_of_jobs_le_1 with job_arrival.
rewrite (big_rem jo) //=.
rewrite PRIO /service_at /scheduled_at SCHED eq_refl add1n; by done.
+ try ( apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival); try done ) ||
apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival); try done.
unfold jobs_come_from_arrival_sequence in *.
apply H_jobs_come_from_arrival_sequence with (t1 + k). by rewrite /scheduled_at SCHED.
@@ -556,6 +558,7 @@ Module JLFPInstantiation.
rewrite PRIO /job_from_another_task_with_higher_eq_priority
/is_interference_from_another_task_with_higher_eq_priority /service_at
/scheduled_at SCHED eq_refl add1n PRIO; by done.
+ try ( apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival); try done ) ||
apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival); try done.
unfold jobs_come_from_arrival_sequence in *.
apply H_jobs_come_from_arrival_sequence with (t1 + k). by rewrite /scheduled_at SCHED.
@@ -657,6 +660,7 @@ Module JLFPInstantiation.
apply in_arrivals_implies_arrived in H0; by done.
move: H1 => /andP [H3 H4].
unfold FP_to_JLFP. by done.
+ try ( apply in_arrivals_implies_arrived_between with (job_arrival0 := job_arrival) in H0; try done ) ||
apply in_arrivals_implies_arrived_between with (job_arrival := job_arrival) in H0; try done.
}
{
@@ -694,6 +698,7 @@ Module JLFPInstantiation.
intros jo IN; apply/negP; intros EQ; move: EQ => /eqP EQ.
subst jo.
unfold arrivals_between in *.
+ try ( apply in_arrivals_implies_arrived_between with (job_arrival0:= job_arrival) in IN; try done ) ||
apply in_arrivals_implies_arrived_between with (job_arrival:= job_arrival) in IN; try done.
by move: IN => /andP [_ IN]; move: H1; rewrite leqNgt; move => /negP LT; apply: LT.
}
@@ -705,6 +710,7 @@ Module JLFPInstantiation.
{
have JIN: j \in arrivals_between 0 t.
{ eapply completed_implies_scheduled_before in H1; eauto 2.
+ try ( apply arrived_between_implies_in_arrivals with (job_arrival0:= job_arrival); try done ) ||
apply arrived_between_implies_in_arrivals with (job_arrival:= job_arrival); try done.
move: H1 => [t' [H3 _]].
apply/andP; split; first by done.
diff --git a/classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v b/classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
index b43be52f14efe390be041cd75254f04c2ce6ae3c..b346c8fcf7d2c0ceef7e26682efa4f60a11ec7f4 100644
--- a/classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
+++ b/classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
@@ -159,6 +159,7 @@ Module PriorityInversionIsBounded.
{ apply/andP; split.
- apply/andP; split. unfold arrived_before, has_arrived in *. by rewrite ltnW.
apply/negP; intro COMP; apply NOTCOMP'.
+ try ( by apply completion_monotonic with (t0 := t) ) ||
by apply completion_monotonic with (t := t).
- apply/negP; intro SCHED'.
apply only_one_job_scheduled with (j1 := j_hp) in SCHED'; last by done.
@@ -185,6 +186,7 @@ Module PriorityInversionIsBounded.
}
apply/andP; split. unfold arrived_before, has_arrived in *. by done.
apply/negP; intro COMP; apply NOTCOMP'.
+ try ( by apply completion_monotonic with (t0 := t) ) ||
by apply completion_monotonic with (t := t).
}
feed (PRIO j_hp' j_hp t PREEMPTP IN BACK); first by done.
@@ -193,11 +195,13 @@ Module PriorityInversionIsBounded.
}
repeat split; [| by done | by done].
move: (SCHED) => PENDING.
- eapply scheduled_implies_pending with (job_cost := job_cost) in PENDING; [| by eauto | by done].
+ ( try ( eapply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING ) ||
+ eapply scheduled_implies_pending with (job_cost := job_cost) in PENDING ); [| by eauto | by done].
apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING => /andP [ARR _].
apply contraT; rewrite -ltnNge; intro LT; exfalso.
feed (QUIET j_hp); first by eapply CONS, SCHED.
specialize (QUIET HP LT).
+ try ( have COMP: job_completed_by j_hp t by apply completion_monotonic with (t0 := t1) ) ||
have COMP: job_completed_by j_hp t by apply completion_monotonic with (t := t1).
apply completed_implies_not_scheduled in COMP; last by done.
by move: COMP => /negP COMP; apply COMP.
@@ -248,7 +252,8 @@ Module PriorityInversionIsBounded.
rewrite !subnKC; last rewrite ltnW; by done.
by rewrite ltnn in MIN. }
have PP: preemption_time mpt.+1.
- { apply first_moment_is_pt with (arr_seq := arr_seq) (j := s); eauto 2. }
+ { (try ( apply first_moment_is_pt with (arr_seq0 := arr_seq) (j0 := s) ) ||
+ apply first_moment_is_pt with (arr_seq := arr_seq) (j := s) ); eauto 2. }
exists mpt.+1; repeat split; try done.
- apply/andP; split; last by done.
by apply H_jobs_must_arrive_to_execute in SCHEDsmpt.
@@ -315,7 +320,8 @@ Module PriorityInversionIsBounded.
repeat split; [| by done | by done].
move: (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET EXj]]].
move: (SCHED) => PENDING.
- eapply scheduled_implies_pending with (job_cost := job_cost) in PENDING;
+ ( try ( eapply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING ) ||
+ eapply scheduled_implies_pending with (job_cost := job_cost) in PENDING );
[| by eauto | by done].
apply/andP; split;
last by apply leq_ltn_trans with (n := t); first by move: PENDING => /andP [ARR _].
@@ -323,7 +329,8 @@ Module PriorityInversionIsBounded.
feed (QUIET j_hp); first by eapply CONS, SCHED.
specialize (QUIET HP LT).
have COMP: job_completed_by j_hp t.
- { by apply completion_monotonic with (t := t1); [ apply leq_trans with tp | ]. }
+ { by ( try ( apply completion_monotonic with (t0 := t1) ) ||
+ apply completion_monotonic with (t := t1)); [ apply leq_trans with tp | ]. }
apply completed_implies_not_scheduled in COMP; last by done.
by move: COMP => /negP COMP; apply COMP.
Qed.
@@ -476,6 +483,7 @@ Module PriorityInversionIsBounded.
destruct t1.
{ eapply zero_is_pt; [eauto 2 | apply H_jobs_come_from_arrival_sequence]. }
eapply hp_job_not_scheduled_before_quiet_time in QT1; eauto 2.
+ try ( eapply first_moment_is_pt with (j0 := s); eauto 2 ) ||
eapply first_moment_is_pt with (j := s); eauto 2.
}
{ move: (SCHED) => ARRs; apply H_jobs_come_from_arrival_sequence in ARRs.
@@ -585,4 +593,4 @@ Module PriorityInversionIsBounded.
End PriorityInversionIsBounded.
-End PriorityInversionIsBounded.
\ No newline at end of file
+End PriorityInversionIsBounded.
diff --git a/classic/model/schedule/uni/nonpreemptive/schedule.v b/classic/model/schedule/uni/nonpreemptive/schedule.v
index dbd44c9865a1570c20c36fde6df647d48fb86ccb..3273fbe3f98d86cec52f8932ce978e27c9ff6c35 100644
--- a/classic/model/schedule/uni/nonpreemptive/schedule.v
+++ b/classic/model/schedule/uni/nonpreemptive/schedule.v
@@ -113,7 +113,8 @@ Module NonpreemptiveSchedule.
apply job_doesnt_complete_before_remaining_cost in NOTCOMP; last by done.
apply contraT; rewrite negbK; intros COMP.
exfalso; move: NOTCOMP => /negP NOTCOMP; apply: NOTCOMP.
- apply completion_monotonic with (t := i); try ( by done).
+ ( try ( apply completion_monotonic with (t0 := i) ) ||
+ apply completion_monotonic with (t := i)); try ( by done).
by apply leq_subRL_impl; first rewrite addn1.
Qed.
@@ -241,7 +242,8 @@ Module NonpreemptiveSchedule.
have COMPL: completed_by job_cost sched j (t + job_remaining_cost j t - 1).
{
- apply completion_monotonic with (t := t' + job_remaining_cost j t');
+ ( try ( apply completion_monotonic with (t0 := t' + job_remaining_cost j t') ) ||
+ apply completion_monotonic with (t := t' + job_remaining_cost j t'));
[| by apply job_completes_after_remaining_cost].
unfold remaining_cost.
have LLF: t' < t - service sched j t.
diff --git a/classic/model/schedule/uni/susp/suspension_intervals.v b/classic/model/schedule/uni/susp/suspension_intervals.v
index 155b7b04e74d45a34ec9c05c6cd4a1ec6f447db8..2acf86b8c1d6af1aecbed0650795e09556520069 100644
--- a/classic/model/schedule/uni/susp/suspension_intervals.v
+++ b/classic/model/schedule/uni/susp/suspension_intervals.v
@@ -445,6 +445,7 @@ Module SuspensionIntervals.
apply contraT; rewrite -leqNgt; intro LE.
apply suspended_implies_not_completed in SUSPi.
exfalso; move: SUSPi => /negP COMPi; apply COMPi.
+ try ( apply completion_monotonic with (t0 := t); try (by done) ) ||
apply completion_monotonic with (t := t); try (by done).
by apply/eqP.
}
@@ -502,6 +503,7 @@ Module SuspensionIntervals.
{
apply contraT; rewrite negbK; intro COMP.
suff COMP': completed_by job_cost sched j t.+1 by rewrite COMP' in NOTCOMP'.
+ try ( by apply completion_monotonic with (t0 := t) ) ||
by apply completion_monotonic with (t := t).
}
apply/andP; split; last by apply: (leq_ltn_trans _ LT).
diff --git a/classic/util/minmax.v b/classic/util/minmax.v
index 8c7c2d4196ce816afb51c2d94cdb6e9adb956ce9..6261fe835ab475ce638cd180349fdf15ed3bbd11 100644
--- a/classic/util/minmax.v
+++ b/classic/util/minmax.v
@@ -321,6 +321,7 @@ Section MinMaxSeq.
F x <= F y.
Proof.
intros l x y SOME IN.
+ try ( apply seq_argmin_computes_min with (l0 := l); try (by done) ) ||
apply seq_argmin_computes_min with (l := l); try (by done).
- by intros x1 x2 x3; apply leq_trans.
- by intros x1 x2 IN1 IN2; apply leq_total.
@@ -333,6 +334,7 @@ Section MinMaxSeq.
F x >= F y.
Proof.
intros l x y SOME IN.
+ try ( apply seq_argmax_computes_max with (l0 := l); try (by done) ) ||
apply seq_argmax_computes_max with (l := l); try (by done).
- by intros x1 x2 x3; apply leq_trans.
- by intros x1 x2 IN1 IN2; apply leq_total.
@@ -392,6 +394,7 @@ Section MinMaxSeq.
x <= y.
Proof.
intros l x y SOME IN.
+ try ( apply seq_min_computes_min with (l0 := l); try (by done) ) ||
apply seq_min_computes_min with (l := l); try (by done).
- by intros x1 x2 x3; apply leq_trans.
- by intros x1 x2 IN1 IN2; apply leq_total.
@@ -404,6 +407,7 @@ Section MinMaxSeq.
x >= y.
Proof.
intros l x y SOME IN.
+ try ( apply seq_max_computes_max with (l0 := l); try (by done) ) ||
apply seq_max_computes_max with (l := l); try (by done).
- by intros x1 x2 x3; apply leq_trans.
- by intros x1 x2 IN1 IN2; apply leq_total.
@@ -452,6 +456,7 @@ Section MinMaxSeq.
min_nat_cond P a b != None.
Proof.
intros P a b x LE HOLDS.
+ try ( apply seq_argmin_exists with (x0 := x) ) ||
apply seq_argmin_exists with (x := x).
by rewrite mem_filter mem_values_between HOLDS LE.
Qed.
@@ -484,6 +489,7 @@ Section MinMaxSeq.
max_nat_cond P a b != None.
Proof.
intros P a b x LE HOLDS.
+ try ( apply seq_argmax_exists with (x0 := x) ) ||
apply seq_argmax_exists with (x := x).
by rewrite mem_filter mem_values_between HOLDS LE.
Qed.
@@ -538,6 +544,7 @@ Section Kmin.
move => l x _ IN /=.
destruct (seq_argmin rel F l) as [|] eqn:MIN; first by done.
suff NOTNONE: seq_argmin rel F l != None by rewrite MIN in NOTNONE.
+ try ( by apply seq_argmin_exists with (x0 := x) ) ||
by apply seq_argmin_exists with (x := x).
Qed.
diff --git a/results/edf/optimality.v b/results/edf/optimality.v
index 9fe6fbb49ebc2dfb632579967abe2a4634cfb56f..4450724d00251ed78bf508f6b022d276d7a1e68c 100644
--- a/results/edf/optimality.v
+++ b/results/edf/optimality.v
@@ -161,8 +161,8 @@ Section WeakOptimality.
- by apply edf_transform_completed_jobs_dont_execute.
- by apply edf_transform_deadlines_met.
- by apply edf_transform_ensures_edf.
- - by move=> [t SCHED_j]; apply edf_transform_job_scheduled' with (t := t).
- - by move=> [t SCHED_j]; apply edf_transform_job_scheduled with (t := t).
+ - by move=> [t SCHED_j]; try ( apply edf_transform_job_scheduled' with (t0 := t) ) || apply edf_transform_job_scheduled' with (t := t).
+ - by move=> [t SCHED_j]; try ( apply edf_transform_job_scheduled with (t0 := t) ) || apply edf_transform_job_scheduled with (t := t).
Qed.
End WeakOptimality.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index c96c4386014dd9a2febe4b5b90a1b3b265aae83a..793083c42afcbf8f3d72b90bfe793fdaf31e8e30 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -678,9 +678,12 @@ Section AbstractRTAforEDFwithArrivalCurves.
move: H_sched_valid => [CARR MBR].
move: (posnP (@job_cost _ Cost js)) => [ZERO|POS].
{ by rewrite /job_response_time_bound /completed_by ZERO. }
+ ( try ( eapply uniprocessor_response_time_bound_seq with
+ (interference0 := interference) (interfering_workload0 := interfering_workload)
+ (task_interference_bound_function := fun tsk A R => IBF_other A R) (L0 := L) ) ||
eapply uniprocessor_response_time_bound_seq with
(interference := interference) (interfering_workload := interfering_workload)
- (task_interference_bound_function := fun tsk A R => IBF_other A R) (L := L); eauto 2 with basic_facts.
+ (task_interference_bound_function := fun tsk A R => IBF_other A R) (L := L)); eauto 2 with basic_facts.
- by apply instantiated_i_and_w_are_coherent_with_schedule.
- by apply instantiated_interference_and_workload_consistent_with_sequential_tasks.
- by apply instantiated_busy_intervals_are_bounded.
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index 1e90c04adb01531693b5d272e0c495b8ac2d3991..5b752d5c8a64838ed5d8b82c51fbe8228622d7b1 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -141,6 +141,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
Proof.
move: (H_valid_task_model_with_floating_nonpreemptive_regions) => [LIMJ JMLETM].
move: (LIMJ) => [BEG [END _]].
+ try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L).
all: eauto 2 with basic_facts.
rewrite subnn.
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index 98a3e67349a3cce8ade94229124cbf960241de95..a828bdffa324fd6feea834da4c66602d58cb207c 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -139,6 +139,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
}
by rewrite /job_response_time_bound /completed_by ZEROj.
}
+ try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L).
all: eauto 3 with basic_facts.
Qed.
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index 123eac0e3a58c88dde30cf054be0dee9263e5d3c..9be9531432810283262d483e1b96b393b523874d 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -127,6 +127,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
have BLOCK: blocking_bound ts tsk = 0.
{ by rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
/fully_preemptive.fully_preemptive_model subnn big1_eq. }
+ try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L) .
all: eauto 2 with basic_facts.
- move => A /andP [LT NEQ].
@@ -139,4 +140,3 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
Qed.
End RTAforFullyPreemptiveEDFModelwithArrivalCurves.
-
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index 95ad8fc559b0dfe76399d2ccc743ecd2f5fdb975..061fab7368c193fe24b7a7c7e67b718523ad658a 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -148,6 +148,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
move: TSK => /eqP TSK; move: POSt; rewrite /valid_job_cost TSK ZERO leqn0; move => /eqP Z.
by rewrite /job_response_time_bound /completed_by Z.
}
+ try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L).
all: eauto 2 with basic_facts.
rewrite subKn; first by done.
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index 998e00383a27e06e3c064b12fe129ef771a99589..f59b44bb98c7b57893fc47d955200ab94e2ee718 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -291,7 +291,8 @@ Section AbstractRTAforFIFOwithArrivalCurves.
{ rewrite /workload_of_jobs /IBF (big_rem tsk) //= (addnC (rbf tsk (job_arrival j - t1 + ε))).
rewrite -addnBA; last first.
{ apply leq_trans with (task_rbf ε).
- apply (task_rbf_1_ge_task_cost arr_seq) with (j := j) => //=; first by auto.
+ ( try ( apply (task_rbf_1_ge_task_cost arr_seq) with (j0 := j) => //= ) ||
+ apply (task_rbf_1_ge_task_cost arr_seq) with (j := j) => //=); first by auto.
by apply task_rbf_monotone; [apply H_valid_arrival_curve | ssrlia]. }
{ eapply leq_trans; last first.
by erewrite leq_add2l; eapply task_rbf_excl_tsk_bounds_task_workload_excl_j; eauto 1.
@@ -406,9 +407,12 @@ Section AbstractRTAforFIFOwithArrivalCurves.
intros js ARRs TSKs.
move: (posnP (@job_cost _ Cost js)) => [ZERO|POS].
{ by rewrite /job_response_time_bound /completed_by ZERO. }
+ ( try ( eapply uniprocessor_response_time_bound with
+ (interference0 := interference) (interfering_workload0 := interfering_workload)
+ (interference_bound_function := fun tsk A R => IBF tsk A R) (L0 := L) ) ||
eapply uniprocessor_response_time_bound with
(interference := interference) (interfering_workload := interfering_workload)
- (interference_bound_function := fun tsk A R => IBF tsk A R) (L := L); eauto 2 with basic_facts.
+ (interference_bound_function := fun tsk A R => IBF tsk A R) (L := L)); eauto 2 with basic_facts.
- by apply instantiated_i_and_w_are_coherent_with_schedule.
- by apply instantiated_busy_intervals_are_bounded.
- by apply instantiated_interference_is_bounded.
@@ -419,6 +423,3 @@ Section AbstractRTAforFIFOwithArrivalCurves.
Qed.
End AbstractRTAforFIFOwithArrivalCurves.
-
-
-
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index 04652878a042dc802655afb10f77a1d4f9cb179f..925ad4882d48201d14416e369aef05c32387e8c2 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -150,6 +150,8 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
}
by rewrite /job_response_time_bound /completed_by ZEROj.
}
+ try ( eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
+ (L0 := L) ) ||
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
(L := L).
all: eauto 3 with basic_facts.
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 98b2a7c969440e16a4ce883f3dc6761ca8a51965..1dadfd26cc56c782cc2375c1d3575ea0789eeb7d 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -154,6 +154,8 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
move: TSK => /eqP TSK; move: POSt; rewrite /valid_job_cost TSK ZERO leqn0; move => /eqP Z.
by rewrite /job_response_time_bound /completed_by Z.
}
+ try ( eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
+ with (L0 := L) ) ||
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
with (L := L).
all: eauto 2 with basic_facts.
diff --git a/scripts/known-long-proofs.json b/scripts/known-long-proofs.json
index c479bade585cbe5f027536dcffa72fd127aa9305..a5e0cc60aae214f74c4e17c8b2f669ba42da80be 100644
--- a/scripts/known-long-proofs.json
+++ b/scripts/known-long-proofs.json
@@ -12,26 +12,26 @@
"bertogna_cirinei_response_time_bound_edf": 49,
"bertogna_edf_all_cpus_in_affinity_busy": 52,
"bertogna_edf_all_cpus_in_subaffinity_busy": 51,
- "bertogna_edf_alpha'_is_full": 106,
- "bertogna_edf_interference_by_different_tasks": 43,
- "bertogna_edf_interference_in_non_full_processors": 133,
+ "bertogna_edf_alpha'_is_full": 116,
+ "bertogna_edf_interference_by_different_tasks": 46,
+ "bertogna_edf_interference_in_non_full_processors": 138,
"bertogna_edf_sum_exceeds_total_interference": 43
},
"./classic/analysis/apa/bertogna_fp_comp.v": {
- "fp_analysis_yields_response_time_bounds": 107
+ "fp_analysis_yields_response_time_bounds": 113
},
"./classic/analysis/apa/bertogna_fp_theory.v": {
"bertogna_cirinei_response_time_bound_fp": 47,
"bertogna_fp_all_cpus_in_affinity_busy": 54,
"bertogna_fp_all_cpus_in_subaffinity_busy": 53,
- "bertogna_fp_alpha'_is_full": 143,
- "bertogna_fp_interference_by_different_tasks": 42,
- "bertogna_fp_interference_in_non_full_processors": 149,
+ "bertogna_fp_alpha'_is_full": 154,
+ "bertogna_fp_interference_by_different_tasks": 45,
+ "bertogna_fp_interference_in_non_full_processors": 153,
"bertogna_fp_sum_exceeds_total_interference": 42,
- "bertogna_fp_workload_bounds_interference": 44
+ "bertogna_fp_workload_bounds_interference": 46
},
"./classic/analysis/apa/interference_bound_edf.v": {
- "interference_bound_edf_holds_for_single_job_that_completes_on_time": 86,
+ "interference_bound_edf_holds_for_single_job_that_completes_on_time": 90,
"interference_bound_edf_many_periods_in_between": 40
},
"./classic/analysis/apa/workload_bound.v": {
@@ -47,20 +47,21 @@
},
"./classic/analysis/global/basic/bertogna_edf_theory.v": {
"bertogna_cirinei_response_time_bound_edf": 50,
- "bertogna_edf_interference_by_different_tasks": 43,
- "bertogna_edf_interference_in_non_full_processors": 129
+ "bertogna_edf_interference_by_different_tasks": 46,
+ "bertogna_edf_interference_in_non_full_processors": 133
},
"./classic/analysis/global/basic/bertogna_fp_comp.v": {
- "fp_analysis_yields_response_time_bounds": 105
+ "fp_analysis_yields_response_time_bounds": 110
},
"./classic/analysis/global/basic/bertogna_fp_theory.v": {
"bertogna_cirinei_response_time_bound_fp": 48,
- "bertogna_fp_interference_by_different_tasks": 42,
- "bertogna_fp_interference_in_non_full_processors": 164,
- "bertogna_fp_workload_bounds_interference": 45
+ "bertogna_fp_all_cpus_are_busy": 44,
+ "bertogna_fp_interference_by_different_tasks": 45,
+ "bertogna_fp_interference_in_non_full_processors": 173,
+ "bertogna_fp_workload_bounds_interference": 47
},
"./classic/analysis/global/basic/interference_bound_edf.v": {
- "interference_bound_edf_holds_for_single_job_that_completes_on_time": 92,
+ "interference_bound_edf_holds_for_single_job_that_completes_on_time": 100,
"interference_bound_edf_many_periods_in_between": 40
},
"./classic/analysis/global/basic/workload_bound.v": {
@@ -76,30 +77,31 @@
},
"./classic/analysis/global/jitter/bertogna_edf_theory.v": {
"bertogna_cirinei_response_time_bound_edf": 60,
- "bertogna_edf_interference_by_different_tasks": 63,
- "bertogna_edf_interference_in_non_full_processors": 125
+ "bertogna_edf_interference_by_different_tasks": 66,
+ "bertogna_edf_interference_in_non_full_processors": 130
},
"./classic/analysis/global/jitter/bertogna_fp_comp.v": {
- "fp_analysis_yields_response_time_bounds": 120
+ "fp_analysis_yields_response_time_bounds": 125
},
"./classic/analysis/global/jitter/bertogna_fp_theory.v": {
"bertogna_cirinei_response_time_bound_fp": 49,
- "bertogna_fp_all_cpus_are_busy": 40,
- "bertogna_fp_interference_by_different_tasks": 54,
- "bertogna_fp_interference_in_non_full_processors": 173,
- "bertogna_fp_workload_bounds_interference": 46
+ "bertogna_fp_all_cpus_are_busy": 46,
+ "bertogna_fp_interference_by_different_tasks": 57,
+ "bertogna_fp_interference_in_non_full_processors": 183,
+ "bertogna_fp_workload_bounds_interference": 49
},
"./classic/analysis/global/jitter/interference_bound_edf.v": {
- "interference_bound_edf_holds_for_single_job_that_completes_on_time": 123,
- "interference_bound_edf_holds_for_single_job_with_small_slack": 55,
- "interference_bound_edf_j_fst_completed_on_time": 46,
+ "interference_bound_edf_holds_for_single_job_that_completes_on_time": 132,
+ "interference_bound_edf_holds_for_single_job_with_small_slack": 57,
+ "interference_bound_edf_j_fst_completed_on_time": 48,
"interference_bound_edf_many_periods_in_between": 49
},
"./classic/analysis/global/jitter/workload_bound.v": {
"W_monotonic": 51,
"workload_bound_many_periods_in_between": 41,
"workload_bound_n_k_covers_middle_jobs": 40,
- "workload_bound_service_of_first_and_last_jobs": 50,
+ "workload_bound_n_k_equals_num_mid_jobs_plus_1": 42,
+ "workload_bound_service_of_first_and_last_jobs": 51,
"workload_bounded_by_W": 48
},
"./classic/analysis/global/parallel/bertogna_edf_comp.v": {
@@ -110,24 +112,30 @@
},
"./classic/analysis/global/parallel/bertogna_edf_theory.v": {
"bertogna_cirinei_response_time_bound_edf": 49,
- "bertogna_edf_interference_on_all_cpus": 75
+ "bertogna_edf_interference_on_all_cpus": 78
},
"./classic/analysis/global/parallel/bertogna_fp_comp.v": {
- "fp_analysis_yields_response_time_bounds": 98
+ "fp_analysis_yields_response_time_bounds": 103
},
"./classic/analysis/global/parallel/bertogna_fp_theory.v": {
"bertogna_cirinei_response_time_bound_fp": 41,
- "bertogna_fp_all_cpus_are_busy": 78
+ "bertogna_fp_all_cpus_are_busy": 81
},
"./classic/analysis/global/parallel/interference_bound_edf.v": {
"interference_bound_edf_many_periods_in_between": 40,
- "interference_bound_edf_n_k_covers_all_jobs": 45
+ "interference_bound_edf_n_k_covers_all_jobs": 47
},
"./classic/analysis/uni/arrival_curves/workload_bound.v": {
"total_workload_le_total_rbf": 45,
"total_workload_le_total_rbf'": 41,
"total_workload_le_total_rbf''": 41
},
+ "./classic/analysis/uni/basic/fp_rta_comp.v": {
+ "fp_analysis_yields_response_time_bounds": 42
+ },
+ "./classic/analysis/uni/basic/fp_rta_theory.v": {
+ "uniprocessor_response_time_bound_fp": 46
+ },
"./classic/analysis/uni/basic/tdma_wcrt_analysis.v": {
"formula_not_sched_St": 45,
"formula_sched_St": 100,
@@ -138,18 +146,18 @@
"sched_jitter_respects_policy": 77
},
"./classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v": {
- "jitter_reduction_inductive_step_case2": 96,
+ "jitter_reduction_inductive_step_case2": 98,
"jitter_reduction_less_job_service_before_interval_case5": 44,
"jitter_reduction_service_jitter": 51
},
"./classic/analysis/uni/susp/dynamic/jitter/taskset_rta.v": {
- "valid_response_time_bound_of_tsk_i": 52
+ "valid_response_time_bound_of_tsk_i": 57
},
"./classic/analysis/uni/susp/dynamic/oblivious/reduction.v": {
"sched_new_completed_jobs_dont_execute": 42
},
"./classic/analysis/uni/susp/sustainability/allcosts/main_claim.v": {
- "policy_is_weakly_sustainable": 63
+ "policy_is_weakly_sustainable": 66
},
"./classic/analysis/uni/susp/sustainability/allcosts/reduction_properties.v": {
"executes_before_suspension_in_sched_new": 42,
@@ -169,7 +177,7 @@
"./classic/implementation/apa/schedule.v": {
"scheduler_has_no_duplicate_jobs": 55,
"scheduler_mapping_is_work_conserving": 46,
- "scheduler_priority": 113
+ "scheduler_priority": 114
},
"./classic/implementation/global/basic/bertogna_fp_example.v": {
"schedulability_test_succeeds": 40
@@ -187,7 +195,7 @@
"respects_FIFO": 45
},
"./classic/implementation/uni/basic/tdma_rta_example.v": {
- "respects_TDMA_policy": 43
+ "respects_TDMA_policy": 46
},
"./classic/implementation/uni/jitter/fp_rta_example.v": {
"RTA_yields_these_bounds": 52
@@ -196,18 +204,21 @@
"RTA_yields_these_bounds": 51
},
"./classic/implementation/uni/susp/schedule.v": {
- "scheduler_depends_only_on_prefix": 52
+ "scheduler_depends_only_on_prefix": 53
+ },
+ "./classic/model/arrival/jitter/arrival_sequence.v": {
+ "actual_arrivals_between_mem_cat": 42
},
"./classic/model/schedule/global/basic/constrained_deadlines.v": {
"platform_cpus_busy_with_interfering_tasks": 65,
- "platform_fp_cpus_busy_with_interfering_tasks": 82
+ "platform_fp_cpus_busy_with_interfering_tasks": 84
},
"./classic/model/schedule/global/basic/platform.v": {
"work_conserving_eq_work_conserving_count": 67
},
"./classic/model/schedule/global/jitter/constrained_deadlines.v": {
"platform_cpus_busy_with_interfering_tasks": 65,
- "platform_fp_cpus_busy_with_interfering_tasks": 85
+ "platform_fp_cpus_busy_with_interfering_tasks": 87
},
"./classic/model/schedule/global/jitter/platform.v": {
"work_conserving_eq_work_conserving_count": 68
@@ -215,7 +226,7 @@
"./classic/model/schedule/uni/jitter/busy_interval.v": {
"busy_interval_is_bounded": 59,
"exists_busy_interval_prefix": 68,
- "not_quiet_implies_exists_scheduled_hp_job": 46
+ "not_quiet_implies_exists_scheduled_hp_job": 50
},
"./classic/model/schedule/uni/limited/abstract_RTA/abstract_rta.v": {
"in": 115
@@ -225,59 +236,49 @@
"task_rbf_excl_tsk_bounds_task_workload_excl_j": 69
},
"./classic/model/schedule/uni/limited/busy_interval.v": {
- "busy_interval_has_uninterrupted_service": 84,
- "busy_interval_is_bounded": 81,
- "exists_busy_interval_prefix": 75,
- "no_idle_time_within_non_quiet_time_interval": 76,
- "pending_hp_job_exists": 73
+ "busy_interval_is_bounded": 75,
+ "exists_busy_interval_prefix": 62,
+ "pending_hp_job_exists": 74
},
"./classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v": {
- "uniprocessor_response_time_bound_edf_with_fixed_preemption_points": 168,
- "uniprocessor_response_time_bound_edf_with_floating_nonpreemptive_regions": 81
+ "uniprocessor_response_time_bound_edf_with_fixed_preemption_points": 174,
+ "uniprocessor_response_time_bound_edf_with_floating_nonpreemptive_regions": 88
},
"./classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v": {
- "priority_inversion_is_bounded": 56,
- "priority_inversion_is_bounded_by_blocking": 58
+ "priority_inversion_is_bounded": 57,
+ "priority_inversion_is_bounded_by_blocking": 56
},
"./classic/model/schedule/uni/limited/edf/response_time_bound.v": {
"A_is_in_concrete_search_space": 85,
"instantiated_task_interference_is_bounded": 163
},
"./classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v": {
- "uniprocessor_response_time_bound_fp_with_fixed_preemption_points": 168,
- "uniprocessor_response_time_bound_fp_with_floating_nonpreemptive_regions": 81
+ "uniprocessor_response_time_bound_fp_with_fixed_preemption_points": 176,
+ "uniprocessor_response_time_bound_fp_with_floating_nonpreemptive_regions": 88
},
"./classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v": {
- "priority_inversion_is_bounded": 52
+ "priority_inversion_is_bounded": 53
},
"./classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v": {
"instantiated_task_interference_is_bounded": 47
},
"./classic/model/schedule/uni/limited/jlfp_instantiation.v": {
- "cumulative_task_interference_split": 62,
- "instantiated_cumulative_interference_of_hep_jobs_equal_total_interference_of_hep_jobs": 114,
- "instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks": 127,
- "instantiated_quiet_time_equivalent_edf_quiet_time": 102
+ "cumulative_task_interference_split": 63,
+ "instantiated_cumulative_interference_of_hep_jobs_equal_total_interference_of_hep_jobs": 115,
+ "instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks": 128,
+ "instantiated_quiet_time_equivalent_edf_quiet_time": 105
},
"./classic/model/schedule/uni/limited/platform/limited.v": {
"model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions": 83
},
"./classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v": {
- "=>": 119,
- "not_quiet_implies_exists_scheduled_hp_job_after_preemption_point": 55,
- "not_quiet_implies_exists_scheduled_hp_job_at_preemption_point": 90,
- "scheduling_of_any_segment_starts_with_preemption_time": 44
- },
- "./classic/model/schedule/uni/limited/platform/util.v": {
- "belonging_to_segment_of_seq_is_total": 46,
- "distance_between_neighboring_elements_le_max_distance_in_seq": 43,
- "domination_of_distances_implies_domination_of_seq": 58,
- "max_distance_in_nontrivial_seq_is_positive": 127,
- "max_distance_in_seq_le_last_element_of_seq": 47,
- "max_of_dominating_seq": 47
+ "=>": 120,
+ "not_quiet_implies_exists_scheduled_hp_job_after_preemption_point": 57,
+ "not_quiet_implies_exists_scheduled_hp_job_at_preemption_point": 94,
+ "scheduling_of_any_segment_starts_with_preemption_time": 45
},
"./classic/model/schedule/uni/nonpreemptive/schedule.v": {
- "j_is_not_scheduled_at_t_minus_service_minus_one": 54,
+ "j_is_not_scheduled_at_t_minus_service_minus_one": 55,
"j_is_scheduled_at_t_minus_service": 74
},
"./classic/model/schedule/uni/service.v": {
@@ -292,7 +293,7 @@
"same_service_implies_same_last_execution": 49
},
"./classic/model/schedule/uni/susp/suspension_intervals.v": {
- "cumulative_suspension_eq_total_suspension": 86,
+ "cumulative_suspension_eq_total_suspension": 87,
"cumulative_suspension_le_total_suspension": 57
},
"./classic/model/schedule/uni/sustainability.v": {