diff --git a/bertogna_edf_theory.v b/bertogna_edf_theory.v
index bec683cd67df47e02f4873a836d5fc0cf2d6d6cc..90eb0c29e68fab09824cffabcaf70fb807681a3f 100644
--- a/bertogna_edf_theory.v
+++ b/bertogna_edf_theory.v
@@ -250,18 +250,13 @@ 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.
- apply workload_bounded_by_W with (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline); try (by ins); last 2 first;
+ by apply workload_bounded_by_W with (task_deadline0 := task_deadline)
+ (job_cost0 := job_cost) (job_deadline0 := job_deadline); try (by ins); last 2 first;
[ by apply bertogna_edf_R_other_ge_cost
- | by ins; apply BEFOREok with (tsk_other := tsk_other)
+ | by ins; apply NOMISS
| by ins; apply TASK_PARAMS
- | by ins; apply RESTR |].
- red; move => j' JOBtsk' LEdl; unfold job_misses_no_deadline.
- assert (PARAMS' := PARAMS j'); des; rewrite PARAMS'1 JOBtsk'.
- apply completion_monotonic with (t := job_arrival j' + (R_other)); ins;
- first by rewrite leq_add2l; apply NOMISS.
- apply BEFOREok with (tsk_other := tsk_other); ins.
- apply leq_ltn_trans with (n := job_arrival j' + job_deadline j'); last by done.
- by specialize (PARAMS j'); des; rewrite leq_add2l PARAMS1 JOBtsk'; apply NOMISS.
+ | by ins; apply RESTR
+ | by ins; apply BEFOREok with (tsk_other := tsk_other)].
Qed.
(* Recall that the edf-specific interference bound also holds. *)
diff --git a/bertogna_fp_theory.v b/bertogna_fp_theory.v
index 6959795294eeeb087b86969b805ddf9bd83bbef3..5ddae8efae4e7513c095f40a98cb2e50ec15f000 100644
--- a/bertogna_fp_theory.v
+++ b/bertogna_fp_theory.v
@@ -237,18 +237,14 @@ 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.
- apply workload_bounded_by_W with (task_deadline0 := task_deadline)
+ by apply workload_bounded_by_W with (task_deadline0 := task_deadline)
(job_cost0 := job_cost) (job_deadline0 := job_deadline);
try (by ins); last 2 first;
[ by ins; apply GE_COST
- | by ins; apply RESP with (hp_tsk := tsk_other)
+ | by ins; apply NOMISS
| by ins; apply TASK_PARAMS
- | by ins; apply RESTR |].
- red; red; move => j' JOBtsk' _; unfold job_misses_no_deadline.
- specialize (PARAMS j'); des.
- rewrite PARAMS1 JOBtsk'.
- by apply completion_monotonic with (t := job_arrival j' + R_other); ins;
- [by rewrite leq_add2l; apply NOMISS | by apply (RESP tsk_other)].
+ | by ins; apply RESTR
+ | by ins; apply RESP with (hp_tsk := tsk_other)].
Qed.
End LemmasAboutInterferingTasks.
diff --git a/workload_bound.v b/workload_bound.v
index 3e63f8b9516eb18b533b10d8b1ef43b5a30ab0bf..5dd34515383ab42eed1fcb4cfbb93d350db59142 100644
--- a/workload_bound.v
+++ b/workload_bound.v
@@ -154,9 +154,7 @@ Module WorkloadBound.
(* Before starting the proof, let's give simpler names to the definitions. *)
Let job_has_completed_by := completed job_cost sched.
- Let no_deadline_misses_by (tsk: sporadic_task) (t: time) :=
- task_misses_no_deadline_before job_cost job_deadline job_task
- sched tsk t.
+
Let workload_of (tsk: sporadic_task) (t1 t2: time) :=
workload job_task sched tsk t1 t2.
@@ -180,22 +178,22 @@ Module WorkloadBound.
middle jobs (i.e., number of jobs - 2 in the worst case). *)
Hypothesis H_restricted_deadline: task_deadline tsk <= task_period tsk.
- (* Consider an interval [t1, t1 + delta), with no deadline misses. *)
+ (* Consider an interval [t1, t1 + delta). *)
Variable t1 delta: time.
- Hypothesis H_no_deadline_misses_during_interval: no_deadline_misses_by tsk (t1 + delta).
(* Assume that a response-time bound R_tsk for that task in any
- schedule of this processor platform is also given,
- such that R_tsk >= task_cost tsk. *)
+ schedule of this processor platform is also given, ... *)
Variable R_tsk: time.
- Hypothesis H_response_time_ge_cost: R_tsk >= task_cost tsk.
-
Hypothesis H_response_time_bound :
forall (j: JobIn arr_seq),
job_task j = tsk ->
job_arrival j + R_tsk < t1 + delta ->
job_has_completed_by j (job_arrival j + R_tsk).
+
+ (* ... such that R_tsk >= task_cost tsk and R_tsk <= task_deadline tsk. *)
+ Hypothesis H_response_time_ge_cost: R_tsk >= task_cost tsk.
+ Hypothesis H_no_deadline_miss: R_tsk <= task_deadline tsk.
Section MainProof.
@@ -546,55 +544,6 @@ Module WorkloadBound.
by rewrite subh3 // addnC; move: INnth => /eqP INnth; rewrite -INnth.
Qed.
- (* Now, we prove an auxiliary lemma for the next result.
- The statement is not meaningful, since it's part of a proof
- by contradiction. *)
- Lemma workload_bound_helper_lemma :
- job_arrival j_fst + task_period tsk + delta <= job_arrival j_lst ->
- t1 <= job_arrival j_fst + task_deadline tsk.
- Proof.
- intros LE.
- rename H_jobs_have_valid_parameters into PARAMS,
- H_completed_jobs_dont_execute into EXEC,
- H_no_deadline_misses_during_interval into NOMISS.
- unfold task_misses_no_deadline_before, valid_sporadic_job,
- job_misses_no_deadline, completed in *; des.
- exploit workload_bound_all_jobs_from_tsk.
- {
- apply mem_nth; instantiate (1 := 0).
- apply ltn_trans with (n := 1); [by done | by rewrite H_at_least_two_jobs].
- }
- instantiate (1 := elem); move => [FSTtsk [/eqP FSTserv FSTin]].
- exploit (NOMISS j_fst FSTtsk); last intros COMP.
- {
- (* Prove that arr_fst + d_k <= t2 *)
- apply leq_ltn_trans with (n := job_arrival j_lst);
- last by apply workload_bound_last_job_arrives_before_end_of_interval.
- apply leq_trans with (n := job_arrival j_fst + task_period tsk + delta); last by done.
- rewrite -addnA leq_add2l -[job_deadline _]addn0.
- apply leq_add; last by ins.
- specialize (PARAMS j_fst); des.
- by rewrite PARAMS1 FSTtsk H_restricted_deadline.
- }
- rewrite leqNgt; apply/negP; unfold not; intro LTt1.
- (* Now we assume that (job_arrival j_fst + d_k < t1) and reach a contradiction.
- Since j_fst doesn't miss deadlines, then the service it receives between t1 and t2
- equals 0, which contradicts the previous assumption that j_fst interferes in
- the scheduling window. *)
- apply FSTserv.
- {
- unfold service_during; apply/eqP; rewrite -leqn0.
- rewrite <- leq_add2l with (p := job_cost j_fst); rewrite addn0.
- move: COMP => /eqP COMP; unfold service in COMP; rewrite -{1}COMP.
- apply leq_trans with (n := service sched j_fst t2); last by apply EXEC.
- unfold service; rewrite -> big_cat_nat with (m := 0) (p := t2) (n := t1);
- [rewrite leq_add2r /= | by ins | by apply leq_addr].
- rewrite -> big_cat_nat with (p := t1) (n := job_arrival j_fst + job_deadline j_fst);
- [by rewrite /= -{1}[\sum_(_ <= _ < _) _]addn0 leq_add2l | by ins | ].
- by apply ltnW; specialize (PARAMS j_fst); des; rewrite PARAMS1 FSTtsk.
- }
- Qed.
-
(* Prove that n_k is at least the number of the middle jobs *)
Lemma workload_bound_n_k_covers_middle_jobs :
n_k >= num_mid_jobs.
@@ -631,7 +580,9 @@ Module WorkloadBound.
last by apply leq_trans with (n := job_arrival j_fst + task_period tsk + delta);
[rewrite leq_add2r leq_add2l; apply H_restricted_deadline | apply DISTmax].
unfold t2; rewrite leq_add2r.
- by apply workload_bound_helper_lemma.
+ apply leq_trans with (n := job_arrival j_fst + R_tsk);
+ last by rewrite leq_add2l.
+ by apply workload_bound_response_time_of_first_job_inside_interval.
Qed.
(* If n_k = num_mid_jobs, then the workload bound holds. *)
@@ -719,12 +670,7 @@ Module WorkloadBound.
Theorem workload_bounded_by_W :
workload_of tsk t1 (t1 + delta) <= workload_bound.
Proof.
- rename H_jobs_have_valid_parameters into job_properties,
- H_no_deadline_misses_during_interval into no_dl_misses,
- H_valid_task_parameters into task_properties.
- unfold valid_sporadic_job, valid_realtime_job, restricted_deadline_model,
- valid_sporadic_taskset, is_valid_sporadic_task, sporadic_task_model,
- workload_of, no_deadline_misses_by, workload_bound, W in *; ins; des.
+ unfold workload_of, workload_bound, W in *; ins; des.
fold n_k.
(* Use the definition of workload based on list of jobs. *)