Commit f7aaa70c authored by Xiaojie Guo's avatar Xiaojie Guo

Merge remote-tracking branch 'upstream/master'

parents cc5093e8 3b689961
Pipeline #18212 passed with stages
in 5 minutes and 57 seconds
# Configuration file for the 'ack' search utility
# See https://beyondgrep.com/ for details.
# Ignore misc files generated by the build process
--ignore-file=ext:glob,aux
--ignore-dir=html
\ No newline at end of file
*.v gitlab-language=coq
...@@ -2,6 +2,7 @@ ...@@ -2,6 +2,7 @@
*.glob *.glob
*.vo *.vo
*.html *.html
/html
*.aux *.aux
Makefile* Makefile*
_CoqProject _CoqProject
...@@ -10,3 +11,7 @@ _CoqProject ...@@ -10,3 +11,7 @@ _CoqProject
*.cache *.cache
*~ *~
*.orig *.orig
*/.#*
#*#
.#*
*.DS_Store
\ No newline at end of file
stages:
- build
- process
.build:
stage: build
image: mathcomp/mathcomp:${CI_JOB_NAME}
script:
- ./create_makefile.sh
- make -j ${NJOBS}
1.8.0-coq-8.8:
extends: .build
1.9.0-coq-dev:
extends: .build
# it's ok to fail with an unreleased version of Coq
allow_failure: true
1.9.0-coq-8.9:
extends: .build
# Keep track of all compiled output and the build infrastructure
artifacts:
name: prosa-build-files
paths:
- _CoqProject
- Makefile
- Makefile.conf
# Ugly hack around https://gitlab.com/gitlab-org/gitlab-runner/issues/2620
- "*/*.vo"
- "*/*/*.vo"
- "*/*/*/*.vo"
- "*/*/*/*/*.vo"
- "*/*/*/*/*/*.vo"
- "*/*/*/*/*/*/*.vo"
- "*/*/*/*/*/*/*/*.vo"
- "*/*/*/*/*/*/*/*/*.vo"
- "*/*/*/*/*/*/*/*/*/*.vo"
- "*/*.glob"
- "*/*/*.glob"
- "*/*/*/*.glob"
- "*/*/*/*/*.glob"
- "*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*/*/*/*.glob"
expire_in: 1 week
validate:
stage: process
image: mathcomp/mathcomp:1.9.0-coq-8.9
dependencies:
- 1.9.0-coq-8.9
script: make validate
doc:
stage: process
image: mathcomp/mathcomp:1.9.0-coq-8.9
dependencies:
- 1.9.0-coq-8.9
script:
- make html
- mv html with-proofs
- make gallinahtml
- mv html without-proofs
artifacts:
name: "prosa-spec-$CI_COMMIT_REF_NAME"
paths:
- "with-proofs/"
- "without-proofs/"
expire_in: 1 week
proof-length:
stage: process
image: python:3-alpine
script:
- scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
...@@ -972,8 +972,6 @@ Module ResponseTimeIterationEDF. ...@@ -972,8 +972,6 @@ Module ResponseTimeIterationEDF.
have COMPLETED := RLIST tsk R HAS j ARRj JOBtsk. have COMPLETED := RLIST tsk R HAS j ARRj JOBtsk.
exploit (DL rt_bounds tsk R); exploit (DL rt_bounds tsk R);
[by ins | by ins | clear DL; intro DL]. [by ins | by ins | clear DL; intro DL].
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
apply leq_trans with (n := service sched j (job_arrival j + R)); last first. apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
{ {
unfold valid_sporadic_taskset, is_valid_sporadic_task in *. unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
...@@ -981,8 +979,7 @@ Module ResponseTimeIterationEDF. ...@@ -981,8 +979,7 @@ Module ResponseTimeIterationEDF.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1. specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk. by rewrite JOBtsk.
} }
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym. by done.
by apply COMPLETED.
Qed. Qed.
(* For completeness, since all jobs of the arrival sequence (* For completeness, since all jobs of the arrival sequence
......
...@@ -220,12 +220,12 @@ Module ResponseTimeAnalysisEDF. ...@@ -220,12 +220,12 @@ Module ResponseTimeAnalysisEDF.
Lemma bertogna_edf_specific_bound_holds : Lemma bertogna_edf_specific_bound_holds :
x tsk_other <= edf_specific_bound tsk_other R_other. x tsk_other <= edf_specific_bound tsk_other R_other.
Proof. Proof.
apply interference_bound_edf_bounds_interference with (job_deadline0 := job_deadline) apply interference_bound_edf_bounds_interference with
(arr_seq0 := arr_seq) (ts0 := ts); try (by done); (job_deadline0 := job_deadline)
[ by apply bertogna_edf_tsk_other_in_ts (arr_seq0 := arr_seq) (ts0 := ts); try (by done);
| by apply H_tasks_miss_no_deadlines [ by apply bertogna_edf_tsk_other_in_ts |
| by apply H_tasks_miss_no_deadlines | ]. by apply H_tasks_miss_no_deadlines | ].
by ins; apply H_all_previous_jobs_completed_on_time with (tsk_other := tsk_other). by ins; apply H_all_previous_jobs_completed_on_time with (tsk_other := tsk_other).
Qed. Qed.
End LemmasAboutInterferingTasks. End LemmasAboutInterferingTasks.
...@@ -246,12 +246,7 @@ Module ResponseTimeAnalysisEDF. ...@@ -246,12 +246,7 @@ Module ResponseTimeAnalysisEDF.
rewrite subh1; last by rewrite [R](REC tsk) // leq_addr. rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
rewrite -addnBA // subnn addn0. rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'. move: (NOTCOMP) => /negP NOTCOMP'.
rewrite neq_ltn in NOTCOMP. rewrite -ltnNge in NOTCOMP.
move: NOTCOMP => /orP [LT | BUG]; last first.
{
exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
by apply cumulative_service_le_job_cost.
}
apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R) apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
backlogged job_arrival job_cost sched j t) + backlogged job_arrival job_cost sched j t) +
service sched j (job_arrival j + R)); last first. service sched j (job_arrival j + R)); last first.
...@@ -357,7 +352,7 @@ Module ResponseTimeAnalysisEDF. ...@@ -357,7 +352,7 @@ Module ResponseTimeAnalysisEDF.
intros t j0 ARR0 LEt LE. intros t j0 ARR0 LEt LE.
cut ((job_task j0) \in unzip1 rt_bounds = true); last by rewrite UNZIP FROMTS. 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'. move => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
apply completion_monotonic with (t0 := job_arrival j0 + R0); first by done. apply completion_monotonic with (t0 := job_arrival j0 + R0).
{ {
rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0)); rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
[by apply NOMISS | by apply CONSTR; rewrite FROMTS]. [by apply NOMISS | by apply CONSTR; rewrite FROMTS].
...@@ -976,7 +971,7 @@ Module ResponseTimeAnalysisEDF. ...@@ -976,7 +971,7 @@ Module ResponseTimeAnalysisEDF.
job_task j0 = tsk -> job_task j0 = tsk ->
(tsk, R0) \in rt_bounds -> (tsk, R0) \in rt_bounds ->
job_arrival j0 + R0 < job_arrival j + R' -> job_arrival j0 + R0 < job_arrival j + R' ->
service sched j0 (job_arrival j0 + R0) == job_cost j0). service sched j0 (job_arrival j0 + R0) >= job_cost j0).
{ {
by ins; apply IH with (tsk := tsk0) (R := R0). by ins; apply IH with (tsk := tsk0) (R := R0).
} }
...@@ -998,7 +993,7 @@ Module ResponseTimeAnalysisEDF. ...@@ -998,7 +993,7 @@ Module ResponseTimeAnalysisEDF.
unfold interference_bound_edf, interference_bound_generic in LTmin. unfold interference_bound_edf, interference_bound_generic in LTmin.
rewrite minnAC in LTmin; apply min_lt_same in LTmin. rewrite minnAC in LTmin; apply min_lt_same in LTmin.
have BASICBOUND := bertogna_edf_workload_bounds_interference R' j BEFOREok tsk_other R_other HP. have BASICBOUND := bertogna_edf_workload_bounds_interference R' j BEFOREok tsk_other R_other HP.
have EDFBOUND := (bertogna_edf_specific_bound_holds tsk' R' INbounds j ARRj JOBtsk BEFOREok tsk_other R_other HP). have EDFBOUND := (bertogna_edf_specific_bound_holds tsk' R' j ARRj JOBtsk BEFOREok tsk_other R_other HP).
unfold minn in LTmin; clear -LTmin HP BASICBOUND EDFBOUND tsk; desf. unfold minn in LTmin; clear -LTmin HP BASICBOUND EDFBOUND tsk; desf.
{ {
by apply (leq_ltn_trans BASICBOUND) in LTmin; rewrite ltnn in LTmin. by apply (leq_ltn_trans BASICBOUND) in LTmin; rewrite ltnn in LTmin.
......
...@@ -310,7 +310,7 @@ Module ResponseTimeIterationFP. ...@@ -310,7 +310,7 @@ Module ResponseTimeIterationFP.
rename ts into ts'; destruct ts' as [ts UNIQ]; simpl in *. rename ts into ts'; destruct ts' as [ts UNIQ]; simpl in *.
intros hp_idx idx LThp LT NEQ HP. intros hp_idx idx LThp LT NEQ HP.
rewrite ltn_neqAle; apply/andP; split; first by done. rewrite ltn_neqAle; apply/andP; split; first by done.
by apply sorted_rel_implies_le_idx with (leT := higher_priority) (s := ts) (x0 := elem). by apply sorted_rel_implies_le_idx with (leT := higher_priority) (xs := ts) (default := elem).
Qed. Qed.
End HighPriorityTasks. End HighPriorityTasks.
...@@ -696,7 +696,6 @@ Module ResponseTimeIterationFP. ...@@ -696,7 +696,6 @@ Module ResponseTimeIterationFP.
} des. } des.
exploit (RLIST tsk R EX j ARRj); [by apply JOBtsk | intro COMPLETED]. exploit (RLIST tsk R EX j ARRj); [by apply JOBtsk | intro COMPLETED].
exploit (DL rt_bounds tsk R); [by ins | by ins | clear DL; intro DL]. exploit (DL rt_bounds tsk R); [by ins | by ins | clear DL; intro DL].
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
apply leq_trans with (n := service sched j (job_arrival j + R)); last first. apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
{ {
unfold valid_sporadic_taskset, is_valid_sporadic_task in *. unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
...@@ -704,8 +703,7 @@ Module ResponseTimeIterationFP. ...@@ -704,8 +703,7 @@ Module ResponseTimeIterationFP.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1. specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk. by rewrite JOBtsk.
} }
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym. by done.
by apply COMPLETED.
Qed. Qed.
(* For completeness, since all jobs of the arrival sequence (* For completeness, since all jobs of the arrival sequence
......
...@@ -258,12 +258,7 @@ Module ResponseTimeAnalysisFP. ...@@ -258,12 +258,7 @@ Module ResponseTimeAnalysisFP.
rewrite subh1; last by rewrite [R]REC // leq_addr. rewrite subh1; last by rewrite [R]REC // leq_addr.
rewrite -addnBA // subnn addn0. rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'. move: (NOTCOMP) => /negP NOTCOMP'.
rewrite neq_ltn in NOTCOMP. rewrite -ltnNge in NOTCOMP.
move: NOTCOMP => /orP [LT | BUG]; last first.
{
exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
by apply cumulative_service_le_job_cost.
}
apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R) apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
backlogged job_arrival job_cost sched j t) + backlogged job_arrival job_cost sched j t) +
service sched j (job_arrival j + R)); last first. service sched j (job_arrival j + R)); last first.
...@@ -369,14 +364,10 @@ Module ResponseTimeAnalysisFP. ...@@ -369,14 +364,10 @@ Module ResponseTimeAnalysisFP.
intros j0 ARR0 INTERF. intros j0 ARR0 INTERF.
exploit (HAS (job_task j0)); exploit (HAS (job_task j0));
[by rewrite FROMTS | by done | move => [R0 INbounds]]. [by rewrite FROMTS | by done | move => [R0 INbounds]].
apply completion_monotonic with (t := job_arrival j0 + R0); first by done. apply completion_monotonic with (t := job_arrival j0 + R0).
{ - rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
[by apply NOMISS' | by apply CONSTR; rewrite FROMTS]. [by apply NOMISS' | by apply CONSTR; rewrite FROMTS].
} - by apply (RESP (job_task j0)).
{
by apply (RESP (job_task j0)).
}
Qed. Qed.
(* 3) Next, we prove that the sum of the interference of each task is equal to the (* 3) Next, we prove that the sum of the interference of each task is equal to the
...@@ -656,8 +647,7 @@ Module ResponseTimeAnalysisFP. ...@@ -656,8 +647,7 @@ Module ResponseTimeAnalysisFP.
} }
{ {
intros j0 JOB0 ARR0 LT0. intros j0 JOB0 ARR0 LT0.
apply completion_monotonic with (t0 := job_arrival j0 + R); apply completion_monotonic with (t0 := job_arrival j0 + R); [| by apply BEFOREok].
[by done | | by apply BEFOREok].
by rewrite leq_add2l; apply leq_trans with (n := task_deadline tsk); by rewrite leq_add2l; apply leq_trans with (n := task_deadline tsk);
last by apply CONSTR; rewrite -JOBtsk FROMTS. last by apply CONSTR; rewrite -JOBtsk FROMTS.
} }
...@@ -1028,7 +1018,7 @@ Module ResponseTimeAnalysisFP. ...@@ -1028,7 +1018,7 @@ Module ResponseTimeAnalysisFP.
arrives_in arr_seq j0 -> arrives_in arr_seq j0 ->
job_task j0 = tsk -> job_task j0 = tsk ->
job_arrival j0 < job_arrival j -> job_arrival j0 < job_arrival j ->
service sched j0 (job_arrival j0 + R) == job_cost j0). service sched j0 (job_arrival j0 + R) >= job_cost j0).
{ {
by ins; apply IH; try (by done); rewrite ltn_add2r. by ins; apply IH; try (by done); rewrite ltn_add2r.
} clear IH. } clear IH.
......
...@@ -609,7 +609,7 @@ Module InterferenceBoundEDF. ...@@ -609,7 +609,7 @@ Module InterferenceBoundEDF.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k. have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [FSTarr [FSTtask [LEdl _]]]. destruct FST as [FSTarr [FSTtask [LEdl _]]].
have LTr := interference_bound_edf_response_time_bound_of_j_fst_after_interval. have LTr := interference_bound_edf_response_time_bound_of_j_fst_after_interval.
apply subh3; last by apply LEdk. apply subh3.
apply leq_trans with (n := job_interference job_arrival job_cost job_task sched alpha j_i j_fst t1 apply leq_trans with (n := job_interference job_arrival job_cost job_task sched alpha j_i j_fst t1
(job_arrival j_fst + R_k) + (D_k - R_k)); (job_arrival j_fst + R_k) + (D_k - R_k));
first by rewrite leq_add2r; apply extend_sum; [by apply leqnn|]. first by rewrite leq_add2r; apply extend_sum; [by apply leqnn|].
...@@ -955,8 +955,8 @@ Module InterferenceBoundEDF. ...@@ -955,8 +955,8 @@ Module InterferenceBoundEDF.
interference_caused_by j_fst t1 t2 <= D_i %% p_k - (D_k - R_k). interference_caused_by j_fst t1 t2 <= D_i %% p_k - (D_k - R_k).
Proof. Proof.
intro LE. intro LE.
apply subh3; last by apply interference_bound_edf_remainder_ge_slack. apply subh3.
by rewrite -subndiv_eq_mod; apply subh3; last by apply leq_trunc_div. by rewrite -subndiv_eq_mod; apply subh3.
Qed. Qed.
(* Next, we prove that interference caused by j_fst is bounded by the length (* Next, we prove that interference caused by j_fst is bounded by the length
......
...@@ -960,8 +960,6 @@ Module ResponseTimeIterationEDF. ...@@ -960,8 +960,6 @@ Module ResponseTimeIterationEDF.
exploit (HAS rt_bounds tsk); [by ins | by ins | clear HAS; intro HAS; des]. exploit (HAS rt_bounds tsk); [by ins | by ins | clear HAS; intro HAS; des].
have COMPLETED := RLIST tsk R HAS j ARRj JOBtsk. have COMPLETED := RLIST tsk R HAS j ARRj JOBtsk.
exploit (DL rt_bounds tsk R); try (by done); clear DL; intro DL. exploit (DL rt_bounds tsk R); try (by done); clear DL; intro DL.
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
apply leq_trans with (n := service sched j (job_arrival j + R)); last first. apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
{ {
unfold valid_sporadic_taskset, is_valid_sporadic_task in *. unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
...@@ -969,8 +967,7 @@ Module ResponseTimeIterationEDF. ...@@ -969,8 +967,7 @@ Module ResponseTimeIterationEDF.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1. specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk. by rewrite JOBtsk.
} }
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym. by done.
by apply COMPLETED.
Qed. Qed.
(* For completeness, since all jobs of the arrival sequence (* For completeness, since all jobs of the arrival sequence
......
...@@ -212,7 +212,7 @@ Module ResponseTimeAnalysisEDF. ...@@ -212,7 +212,7 @@ Module ResponseTimeAnalysisEDF.
(arr_seq0 := arr_seq) (ts0 := ts); try (by done); (arr_seq0 := arr_seq) (ts0 := ts); try (by done);
[ by apply bertogna_edf_tsk_other_in_ts [ by apply bertogna_edf_tsk_other_in_ts
| by apply H_tasks_miss_no_deadlines | by apply H_tasks_miss_no_deadlines
| by apply H_tasks_miss_no_deadlines | ]. | ].
by ins; apply H_all_previous_jobs_completed_on_time with (tsk_other := tsk_other). by ins; apply H_all_previous_jobs_completed_on_time with (tsk_other := tsk_other).
Qed. Qed.
...@@ -234,12 +234,7 @@ Module ResponseTimeAnalysisEDF. ...@@ -234,12 +234,7 @@ Module ResponseTimeAnalysisEDF.
rewrite subh1; last by rewrite [R](REC tsk) // leq_addr. rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
rewrite -addnBA // subnn addn0. rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'. move: (NOTCOMP) => /negP NOTCOMP'.
rewrite neq_ltn in NOTCOMP. rewrite -ltnNge in NOTCOMP.
move: NOTCOMP => /orP [LT | BUG]; last first.
{
exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
by apply cumulative_service_le_job_cost.
}
apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R) apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
backlogged job_arrival job_cost sched j t) + backlogged job_arrival job_cost sched j t) +
service sched j (job_arrival j + R)); last first. service sched j (job_arrival j + R)); last first.
...@@ -345,7 +340,7 @@ Module ResponseTimeAnalysisEDF. ...@@ -345,7 +340,7 @@ Module ResponseTimeAnalysisEDF.
intros t j0 ARR0 LEt LE. intros t j0 ARR0 LEt LE.
cut ((job_task j0) \in unzip1 rt_bounds = true); last by rewrite UNZIP FROMTS. 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'. move => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
apply completion_monotonic with (t0 := job_arrival j0 + R0); first by done. apply completion_monotonic with (t0 := job_arrival j0 + R0).
{ {
rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0)); rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
[by apply NOMISS | by apply CONSTR; rewrite FROMTS]. [by apply NOMISS | by apply CONSTR; rewrite FROMTS].
...@@ -774,7 +769,7 @@ Module ResponseTimeAnalysisEDF. ...@@ -774,7 +769,7 @@ Module ResponseTimeAnalysisEDF.
job_task j0 = tsk -> job_task j0 = tsk ->
(tsk, R0) \in rt_bounds -> (tsk, R0) \in rt_bounds ->
job_arrival j0 + R0 < job_arrival j + R' -> job_arrival j0 + R0 < job_arrival j + R' ->
service sched j0 (job_arrival j0 + R0) == job_cost j0). service sched j0 (job_arrival j0 + R0) >= job_cost j0).
{ {
by ins; apply IH with (tsk := tsk0) (R := R0). by ins; apply IH with (tsk := tsk0) (R := R0).
} }
...@@ -796,7 +791,7 @@ Module ResponseTimeAnalysisEDF. ...@@ -796,7 +791,7 @@ Module ResponseTimeAnalysisEDF.
unfold interference_bound_edf, interference_bound_generic in LTmin. unfold interference_bound_edf, interference_bound_generic in LTmin.
rewrite minnAC in LTmin; apply min_lt_same in LTmin. rewrite minnAC in LTmin; apply min_lt_same in LTmin.
have BASICBOUND := bertogna_edf_workload_bounds_interference R' j BEFOREok tsk_other R_other HP. have BASICBOUND := bertogna_edf_workload_bounds_interference R' j BEFOREok tsk_other R_other HP.
have EDFBOUND := (bertogna_edf_specific_bound_holds tsk' R' INbounds j ARRj have EDFBOUND := (bertogna_edf_specific_bound_holds tsk' R' j ARRj
JOBtsk BEFOREok tsk_other R_other HP). JOBtsk BEFOREok tsk_other R_other HP).
unfold minn in LTmin; clear -LTmin HP BASICBOUND EDFBOUND tsk; desf. unfold minn in LTmin; clear -LTmin HP BASICBOUND EDFBOUND tsk; desf.
{ {
......
...@@ -304,7 +304,7 @@ Module ResponseTimeIterationFP. ...@@ -304,7 +304,7 @@ Module ResponseTimeIterationFP.
rename ts into ts'; destruct ts' as [ts UNIQ]; simpl in *. rename ts into ts'; destruct ts' as [ts UNIQ]; simpl in *.
intros hp_idx idx LThp LT NEQ HP. intros hp_idx idx LThp LT NEQ HP.
rewrite ltn_neqAle; apply/andP; split; first by done. rewrite ltn_neqAle; apply/andP; split; first by done.
by apply sorted_rel_implies_le_idx with (leT := higher_priority) (s := ts) (x0 := elem). by apply sorted_rel_implies_le_idx with (leT := higher_priority) (xs := ts) (default := elem).
Qed. Qed.
End HighPriorityTasks. End HighPriorityTasks.
...@@ -679,16 +679,11 @@ Module ResponseTimeIterationFP. ...@@ -679,16 +679,11 @@ Module ResponseTimeIterationFP.
} des. } des.
exploit (RLIST tsk R EX j ARRj); [by done | intro COMPLETED]. exploit (RLIST tsk R EX j ARRj); [by done | intro COMPLETED].
exploit (DL rt_bounds tsk R); [by ins | by ins | clear DL; intro DL]. exploit (DL rt_bounds tsk R); [by ins | by ins | clear DL; intro DL].
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost. apply leq_trans with (n := service sched j (job_arrival j + R)); first by done.
apply leq_trans with (n := service sched j (job_arrival j + R)); last first. unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
{ apply extend_sum; rewrite // leq_add2l.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *. specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
apply extend_sum; rewrite // leq_add2l.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk. by rewrite JOBtsk.
}
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
by apply COMPLETED.
Qed. Qed.
(* For completeness, since all jobs of the arrival sequence (* For completeness, since all jobs of the arrival sequence
......
...@@ -242,12 +242,7 @@ Module ResponseTimeAnalysisFP. ...@@ -242,12 +242,7 @@ Module ResponseTimeAnalysisFP.
rewrite subh1; last by rewrite [R](REC) // leq_addr. rewrite subh1; last by rewrite [R](REC) // leq_addr.
rewrite -addnBA // subnn addn0. rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'. move: (NOTCOMP) => /negP NOTCOMP'.
rewrite neq_ltn in NOTCOMP. rewrite -ltnNge in NOTCOMP.
move: NOTCOMP => /orP [LT | BUG]; last first.
{
exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
by apply cumulative_service_le_job_cost.
}
apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R) apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
backlogged job_arrival job_cost sched j t) + backlogged job_arrival job_cost sched j t) +
service sched j (job_arrival j + R)); last first. service sched j (job_arrival j + R)); last first.
...@@ -761,7 +756,7 @@ Module ResponseTimeAnalysisFP. ...@@ -761,7 +756,7 @@ Module ResponseTimeAnalysisFP.
arrives_in arr_seq j0 -> arrives_in arr_seq j0 ->
job_task j0 = tsk -> job_task j0 = tsk ->
job_arrival j0 < job_arrival j -> job_arrival j0 < job_arrival j ->
service sched j0 (job_arrival j0 + R) == job_cost j0). service sched j0 (job_arrival j0 + R) >= job_cost j0).
{ {
by ins; apply IH; try (by done); rewrite ltn_add2r. by ins; apply IH; try (by done); rewrite ltn_add2r.
} clear IH. } clear IH.
......
...@@ -604,7 +604,7 @@ Module InterferenceBoundEDF. ...@@ -604,7 +604,7 @@ Module InterferenceBoundEDF.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k. have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [FSTarr [FSTtask [LEdl _]]]. destruct FST as [FSTarr [FSTtask [LEdl _]]].
have LTr := interference_bound_edf_response_time_bound_of_j_fst_after_interval. have LTr := interference_bound_edf_response_time_bound_of_j_fst_after_interval.
apply subh3; last by apply LEdk. apply subh3.
apply leq_trans with (n := job_interference job_arrival job_cost sched j_i j_fst t1 apply leq_trans with (n := job_interference job_arrival job_cost sched j_i j_fst t1
(job_arrival j_fst + R_k) + (D_k - R_k)); (job_arrival j_fst + R_k) + (D_k - R_k));
first by rewrite leq_add2r; apply extend_sum; [by apply leqnn|].