From d5871c8f5d7e2b82d1a92d84252959c8ab82dcf8 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre@roux01.fr>
Date: Mon, 14 Feb 2022 17:13:02 +0100
Subject: [PATCH] Fix some Admitted
---
analysis/abstract/ideal_jlfp_rta.v | 17 ++--
analysis/facts/busy_interval/busy_interval.v | 59 ++++++-------
.../facts/busy_interval/priority_inversion.v | 76 +++++++++--------
analysis/facts/readiness/sequential.v | 9 +-
model/task/arrival/arrival_curve_to_rbf.v | 23 +++--
model/task/arrivals.v | 2 +-
results/edf/rta/bounded_nps.v | 50 ++++++-----
results/edf/rta/bounded_pi.v | 41 +++++----
results/fixed_priority/rta/bounded_nps.v | 83 +++++++++----------
.../rta/floating_nonpreemptive.v | 13 ++-
.../fixed_priority/rta/fully_nonpreemptive.v | 5 +-
results/fixed_priority/rta/fully_preemptive.v | 19 ++---
.../fixed_priority/rta/limited_preemptive.v | 37 ++++-----
13 files changed, 209 insertions(+), 225 deletions(-)
diff --git a/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
index 5252a1c2e..8253de5ed 100644
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -261,13 +261,12 @@ Section JLFPInstantiation.
have Fact: forall b, ~~ b + b = true; first by intros b; destruct b.
rewrite Bool.andb_true_r Fact; simpl; rewrite lt0b; clear Fact.
apply/hasP; exists j.
- Admitted.
- (* * rewrite mem_filter; apply/andP; split; first by done. *)
- (* by eapply arrivals_between_sub with (t2 := 0) (t3 := upp); eauto 2. *)
- (* * destruct (hep_job s j) eqn:HP; apply/orP; [right|left]; last by done. *)
- (* by rewrite /is_interference_from_another_hep_job EQ *)
- (* /another_hep_job NEQ Bool.andb_true_r. *)
- (* Qed. *)
+ * rewrite in_fsetE inE eqxx andbT.
+ exact: (arrivals_between_sub _ _ 0 _ upp).
+ * destruct (hep_job s j) eqn:HP; apply/orP; [right|left]; last by done.
+ by rewrite /is_interference_from_another_hep_job EQ
+ /another_hep_job NEQ Bool.andb_true_r.
+ Qed.
(** In this section we prove that the (abstract) cumulative interfering workload is equivalent to
conventional workload, i.e., the one defined with concrete schedule parameters. *)
@@ -465,11 +464,11 @@ Section JLFPInstantiation.
intros; apply QT.
- by apply in_arrivals_implies_arrived in H4.
- by move: H5 => /andP [H6 H7].
+ - by apply in_arrivals_implies_arrived_between in H4.
Admitted.
- (* - by apply in_arrivals_implies_arrived_between in H4. *)
(* } *)
(* { rewrite negb_and Bool.negb_involutive; apply/orP. *)
- (* case ARR: (arrived_before j t); [right | by left]. *)
+ (* case ARR: (arrived_before j t); [right | by left]. *)
(* apply QT; try eauto 2. *)
(* } *)
(* Qed. *)
diff --git a/analysis/facts/busy_interval/busy_interval.v b/analysis/facts/busy_interval/busy_interval.v
index 48d4feccf..0078eb438 100644
--- a/analysis/facts/busy_interval/busy_interval.v
+++ b/analysis/facts/busy_interval/busy_interval.v
@@ -9,6 +9,9 @@ Require Export prosa.analysis.definitions.work_bearing_readiness.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.
+Local Open Scope fset_scope.
+Local Open Scope nat_scope.
+
(** * Existence of Busy Interval for JLFP-models *)
(** In this module we derive a sufficient condition for existence of
busy intervals for uni-processor for JLFP schedulers. *)
@@ -188,37 +191,35 @@ Section ExistsBusyIntervalJLFP.
by rewrite -REL; eapply job_pending_at_arrival; eauto 2.
+ by apply (H_priority_is_reflexive 0).
- by exfalso; move_neq_down CONTR; eapply leq_ltn_trans; eauto 2.
- - have EX: exists hp__seq: seq Job,
+ - have [hp__seq SE]: exists hp__seq: {fset Job},
forall j__hp, j__hp \in hp__seq <-> arrives_in arr_seq j__hp /\ job_pending_at j__hp t /\ hep_job j__hp j.
- { exists (filter (fun jo => (job_pending_at jo t) && (hep_job jo j)) (arrivals_between 0 t.+1)).
+ { exists [fset jo in arrivals_between 0 t.+1 | job_pending_at jo t && hep_job jo j].
intros; split; intros T.
- - move: T; rewrite mem_filter; move => /andP [/andP [PEN HP] IN].
- repeat split; eauto using in_arrivals_implies_arrived.
- Admitted.
- (* - move: T => [ARR [PEN HP]]. *)
- (* rewrite mem_filter; apply/andP; split; first (apply/andP; split); try done. *)
- (* eapply arrived_between_implies_in_arrivals; try done. *)
- (* by apply/andP; split; last rewrite ltnS; move: PEN => /andP [T _]. *)
- (* } move: EX => [hp__seq SE]; case FL: (hp__seq) => [ | jhp jhps]. *)
- (* + subst hp__seq; exfalso. *)
- (* move: GE; rewrite leq_eqVlt; move => /orP [/eqP EQ| GE]. *)
- (* * subst t. *)
- (* apply NQT with t1.+1; first by apply/andP; split. *)
- (* intros jhp ARR HP ARRB; apply negbNE; apply/negP; intros NCOMP. *)
- (* move: (SE jhp) => [_ SE2]. *)
- (* rewrite in_nil in SE2; feed SE2; [clear SE2 | by done]. *)
- (* repeat split; try done; first apply/andP; split; try done. *)
- (* apply/negP; intros COMLP. *)
- (* move: NCOMP => /negP NCOMP; apply: NCOMP. *)
- (* by apply completion_monotonic with t1. *)
- (* * apply NQT with t; first by apply/andP; split. *)
- (* intros jhp ARR HP ARRB; apply negbNE; apply/negP; intros NCOMP. *)
- (* move: (SE jhp) => [_ SE2]. *)
- (* rewrite in_nil in SE2; feed SE2; [clear SE2 | by done]. *)
- (* by repeat split; auto; apply/andP; split; first apply ltnW. *)
- (* + move: (SE jhp)=> [SE1 _]; subst; clear SE. *)
- (* by exists jhp; apply SE1; rewrite in_cons; apply/orP; left. *)
- (* Qed. *)
+ - move: T; rewrite in_fsetE inE => /andP[IN /andP[PEN HP]].
+ split=> [|//]; exact: in_arrivals_implies_arrived IN.
+ - move: T => [ARR [PEN HP]].
+ rewrite in_fsetE inE; apply/andP; split; last by apply/andP; split.
+ apply: arrived_between_implies_in_arrivals ARR _ => //.
+ by apply/andP; split; last rewrite ltnS; move: PEN => /andP [T _].
+ } case: (fset_0Vmem hp__seq) => [hp__seq0|[jhp jhpP]].
+ + subst hp__seq; exfalso.
+ move: GE; rewrite leq_eqVlt; move => /orP [/eqP EQ| GE].
+ * subst t.
+ apply NQT with t1.+1; first by apply/andP; split.
+ intros jhp ARR HP ARRB; apply negbNE; apply/negP; intros NCOMP.
+ move: (SE jhp) => [_ SE2].
+ rewrite in_nil in SE2; feed SE2; [clear SE2 | by done].
+ repeat split; try done; first apply/andP; split; try done.
+ apply/negP; intros COMLP.
+ move: NCOMP => /negP NCOMP; apply: NCOMP.
+ by apply completion_monotonic with t1.
+ * apply NQT with t; first by apply/andP; split.
+ intros jhp ARR HP ARRB; apply negbNE; apply/negP; intros NCOMP.
+ move: (SE jhp) => [_ SE2].
+ rewrite in_nil in SE2; feed SE2; [clear SE2 | by done].
+ by repeat split; auto; apply/andP; split; first apply ltnW.
+ + exists jhp; exact: (SE jhp).1.
+ Qed.
(** We prove that at any time instant [t] within <<[t1, t2)>> the processor is not idle. *)
Lemma not_quiet_implies_not_idle:
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index 0525fed87..4729e627b 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -126,9 +126,8 @@ Section PriorityInversionIsBounded.
~ is_idle sched t.
Proof.
intros IDLE.
- Admitted.
- (* by exfalso; eapply not_quiet_implies_not_idle with (t0 := t); eauto 2 with basic_facts. *)
- (* Qed. *)
+ by exfalso; eapply not_quiet_implies_not_idle with (t0 := t); eauto 2 with basic_facts.
+ Qed.
(** Next we consider two cases: (1) when [t] is less than [t2 - 1] and (2) [t] is equal to [t2 - 1]. *)
Lemma t_lt_t2_or_t_eq_t2:
@@ -308,42 +307,41 @@ Section PriorityInversionIsBounded.
move => tp t PRPOINT /andP [GEtp LTtp] /andP [LEtp LTt].
ideal_proc_model_sched_case_analysis_eq sched t jhp.
{ apply instant_t_is_not_idle in Idle; first by done.
- Admitted.
- (* by apply/andP; split; first apply leq_trans with tp. } *)
- (* exists jhp. *)
- (* have HP: hep_job jhp j. *)
- (* { intros. *)
- (* move:(H_valid_model_with_bounded_nonpreemptive_segments) => [PREE ?]. *)
- (* specialize (scheduling_of_any_segment_starts_with_preemption_time arr_seq sched H_sched_valid PREE jhp t Sched_jhp) => SOAS. *)
- (* move: SOAS => [prt [/andP [_ LE] [PR SCH]]]. *)
- (* case E:(t1 <= prt). *)
- (* - move: E => /eqP /eqP E; rewrite subn_eq0 in E. *)
- (* edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point as [jlp [_ [HEP SCHEDjhp]]]; eauto 2. *)
- (* { by apply /andP; split; last by apply leq_ltn_trans with t. } *)
- (* enough (EQ : jhp = jlp); first by subst. *)
- (* eapply ideal_proc_model_is_a_uniprocessor_model with (t0 := prt); eauto; *)
- (* by apply SCH; apply/andP; split. *)
- (* - move: E => /eqP /neqP E; rewrite -lt0n subn_gt0 in E. *)
- (* apply negbNE; apply/negP; intros LP; rename jhp into jlp. *)
- (* edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point *)
- (* as [jhp [_ [HEP SCHEDjhp]]]; [ | apply PRPOINT| ]; first by apply/andP; split. *)
- (* move: LP => /negP LP; apply: LP. *)
- (* enough (EQ : jhp = jlp); first by subst. *)
- (* eapply ideal_proc_model_is_a_uniprocessor_model with (j1 := jhp) (t0 := tp); eauto. *)
- (* by apply SCH; apply/andP; split; first apply leq_trans with t1; auto. *)
- (* } *)
- (* repeat split; try done. *)
- (* move: (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET EXj]]]; move: (Sched_jhp) => PENDING. *)
- (* eapply scheduled_implies_pending in PENDING; eauto with basic_facts. *)
- (* 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 jhp); first by eapply H_jobs_come_from_arrival_sequence, Sched_jhp. *)
- (* specialize (QUIET HP LT). *)
- (* have COMP: job_completed_by jhp t. *)
- (* { by apply completion_monotonic with (t0 := t1); [ apply leq_trans with tp | ]. } *)
- (* apply completed_implies_not_scheduled in COMP; eauto with basic_facts. *)
- (* by move : COMP => /negP COMP; apply : COMP. *)
- (* Qed. *)
+ by apply/andP; split; first apply leq_trans with tp. }
+ exists jhp.
+ have HP: hep_job jhp j.
+ { intros.
+ move:(H_valid_model_with_bounded_nonpreemptive_segments) => [PREE ?].
+ specialize (scheduling_of_any_segment_starts_with_preemption_time arr_seq sched H_sched_valid PREE jhp t Sched_jhp) => SOAS.
+ move: SOAS => [prt [/andP [_ LE] [PR SCH]]].
+ case E:(t1 <= prt).
+ - move: E => /eqP /eqP E; rewrite subn_eq0 in E.
+ edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point as [jlp [_ [HEP SCHEDjhp]]]; eauto 2.
+ { by apply /andP; split; last by apply leq_ltn_trans with t. }
+ enough (EQ : jhp = jlp); first by subst.
+ eapply ideal_proc_model_is_a_uniprocessor_model with (t0 := prt); eauto;
+ by apply SCH; apply/andP; split.
+ - move: E => /eqP /neqP E; rewrite -lt0n subn_gt0 in E.
+ apply negbNE; apply/negP; intros LP; rename jhp into jlp.
+ edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point
+ as [jhp [_ [HEP SCHEDjhp]]]; [ | apply PRPOINT| ]; first by apply/andP; split.
+ move: LP => /negP LP; apply: LP.
+ enough (EQ : jhp = jlp); first by subst.
+ eapply ideal_proc_model_is_a_uniprocessor_model with (j1 := jhp) (t0 := tp); eauto.
+ by apply SCH; apply/andP; split; first apply leq_trans with t1; auto.
+ }
+ repeat split; try done.
+ move: (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET EXj]]]; move: (Sched_jhp) => PENDING.
+ eapply scheduled_implies_pending in PENDING; eauto with basic_facts.
+ 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 jhp); first by eapply H_jobs_come_from_arrival_sequence, Sched_jhp.
+ specialize (QUIET HP LT).
+ have COMP: job_completed_by jhp t.
+ { by apply completion_monotonic with (t0 := t1); [ apply leq_trans with tp | ]. }
+ apply completed_implies_not_scheduled in COMP; eauto with basic_facts.
+ by move : COMP => /negP COMP; apply : COMP.
+ Qed.
(** Now, suppose there exists some constant K that bounds the distance to
a preemption time from the beginning of the busy interval. *)
diff --git a/analysis/facts/readiness/sequential.v b/analysis/facts/readiness/sequential.v
index 062d0ccd9..998e0c3b4 100644
--- a/analysis/facts/readiness/sequential.v
+++ b/analysis/facts/readiness/sequential.v
@@ -65,11 +65,10 @@ Section SequentialTasksReadiness.
intros j1 j2 t ARR1 ARR2 SAME LT SCHED.
destruct (boolP (job_ready sched j2 t)) as [READY | NREADY].
- move: READY => /andP [PEND /allP ALL]; apply: ALL.
- Admitted.
- (* rewrite mem_filter; apply/andP; split; first by done. *)
- (* by apply arrived_between_implies_in_arrivals => //. *)
- (* - by apply H_valid_schedule in SCHED; rewrite SCHED in NREADY. *)
- (* Qed. *)
+ rewrite in_fsetE inE -/(same_task j1 j2) SAME andbT.
+ exact: arrived_between_implies_in_arrivals.
+ - by apply H_valid_schedule in SCHED; rewrite SCHED in NREADY.
+ Qed.
(* Finally, we show that the sequential readiness model is a
work-bearing readiness model. That is, if a job [j] is pending
diff --git a/model/task/arrival/arrival_curve_to_rbf.v b/model/task/arrival/arrival_curve_to_rbf.v
index 448fac298..5e8df8c77 100644
--- a/model/task/arrival/arrival_curve_to_rbf.v
+++ b/model/task/arrival/arrival_curve_to_rbf.v
@@ -1,3 +1,4 @@
+From mathcomp Require Import ssreflect ssrnat finmap.
Require Export prosa.util.all.
Require Export prosa.model.task.arrival.request_bound_functions.
Require Export prosa.model.task.arrival.curves.
@@ -88,13 +89,11 @@ Section ArrivalCurveToRBF.
move=> TASK_COST RESPECT t1 t2 LEQ.
specialize (RESPECT t1 t2 LEQ).
apply leq_trans with (n := task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2) => //.
- - rewrite /max_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // => j.
- Admitted.
- (* rewrite mem_filter => /andP [/eqP TSK _] _. *)
- (* rewrite -TSK. *)
- (* by apply TASK_COST. *)
- (* - by destruct (task_cost tsk) eqn:C; rewrite /task_max_rbf C // leq_pmul2l. *)
- (* Qed. *)
+ - rewrite /number_of_task_arrivals.
+ rewrite -sum1_size big_distrr/= muln1 leq_sum_seq// => j.
+ rewrite in_fsetE inE => /andP[_ /eqP<- _]; exact: TASK_COST.
+ - by destruct (task_cost tsk) eqn:C; rewrite /task_max_rbf C // leq_pmul2l.
+ Qed.
(** Finally, we prove that the task respects the request-bound function also in
the lower-bounding case. This time, we assume that the cost of tasks lower-bounds
@@ -108,12 +107,10 @@ Section ArrivalCurveToRBF.
specialize (RESPECT t1 t2 LEQ).
apply leq_trans with (n := task_min_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2) => //.
- by destruct (task_min_cost tsk) eqn:C; rewrite /task_min_rbf C // leq_pmul2l.
- - rewrite /min_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // => j.
- Admitted.
- (* rewrite mem_filter => /andP [/eqP TSK _] _. *)
- (* rewrite -TSK. *)
- (* by apply TASK_COST. *)
- (* Qed. *)
+ - rewrite /number_of_task_arrivals.
+ rewrite -sum1_size big_distrr/= muln1 leq_sum_seq// => j.
+ rewrite in_fsetE inE => /andP[_ /eqP<- _]; exact: TASK_COST.
+ Qed.
End SingleTask.
diff --git a/model/task/arrivals.v b/model/task/arrivals.v
index 9e3c53500..b649a39bc 100644
--- a/model/task/arrivals.v
+++ b/model/task/arrivals.v
@@ -42,7 +42,7 @@ Section TaskArrivals.
(** ... and finally count the number of job arrivals. *)
Definition number_of_task_arrivals (t1 t2 : instant) :=
- size (task_arrivals_between t1 t2).
+ #|`task_arrivals_between t1 t2|.
(** ... and also count the cost of job arrivals. *)
Definition cost_of_task_arrivals (t1 t2 : instant) :=
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index ddd6daea6..9bc712b10 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -167,32 +167,30 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
intros j' JINB NOTHEP.
apply leq_bigmax_cond_seq with (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1).
{ apply H_all_jobs_from_taskset.
- Admitted.
- (* apply mem_bigcat_nat_exists in JINB. *)
- (* by inversion JINB as [ta' [JIN' _]]; exists ta'. } *)
- (* { have NINTSK: job_task j' != tsk. *)
- (* { apply/eqP; intros TSKj'. *)
- (* rewrite /EDF -ltnNge in NOTHEP. *)
- (* rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP. *)
- (* rewrite TSKj' TSK ltn_add2r in NOTHEP. *)
- (* move: NOTHEP; rewrite ltnNge; move => /negP T; apply: T. *)
- (* apply leq_trans with t; last by done. *)
- (* eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2. *)
- (* move: JINB; move => /andP [_ T]. *)
- (* by apply ltnW. *)
- (* } *)
- (* apply/andP; split; first by done. *)
- (* rewrite /EDF -ltnNge in NOTHEP. *)
- (* rewrite -TSK. *)
- (* have ARRLE: job_arrival j' < job_arrival j. *)
- (* { apply leq_trans with t; last by done. *)
- (* eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2. *)
- (* by move: JINB; move => /andP [_ T]. *)
- (* } *)
- (* rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP. *)
- (* rewrite /D; ssrlia. *)
- (* } *)
- (* Qed. *)
+ by move: JINB => /bigfcup_natP[ta' _ JIN']; exists ta'. }
+ { have NINTSK: job_task j' != tsk.
+ { apply/eqP; intros TSKj'.
+ rewrite /EDF -ltnNge in NOTHEP.
+ rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP.
+ rewrite TSKj' TSK ltn_add2r in NOTHEP.
+ move: NOTHEP; rewrite ltnNge; move => /negP T; apply: T.
+ apply leq_trans with t; last by done.
+ eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2.
+ move: JINB; move => /andP [_ T].
+ by apply ltnW.
+ }
+ apply/andP; split; first by done.
+ rewrite /EDF -ltnNge in NOTHEP.
+ rewrite -TSK.
+ have ARRLE: job_arrival j' < job_arrival j.
+ { apply leq_trans with t; last by done.
+ eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2.
+ by move: JINB; move => /andP [_ T].
+ }
+ rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP.
+ rewrite /D; ssrlia.
+ }
+ Qed.
(** Using the lemma above, we prove that the priority inversion of the task is bounded by
the maximum length of a nonpreemptive section of lower-priority tasks. *)
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 410ff1464..b75220ba3 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -228,27 +228,26 @@ Section AbstractRTAforEDFwithArrivalCurves.
{ exfalso; clear HYP1 HYP2.
eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto 2 with basic_facts.
move: BUSY => [PREF _].
- Admitted.
- (* by eapply not_quiet_implies_not_idle; eauto 2 with basic_facts. } *)
- (* { clear EqSched_jo; move: Sched_jo; rewrite scheduled_at_def; move => /eqP EqSched_jo. *)
- (* rewrite EqSched_jo in HYP1, HYP2. *)
- (* move: HYP1 HYP2. *)
- (* rewrite Bool.negb_involutive negb_and. *)
- (* move => HYP1 /orP [/negP HYP2| /eqP HYP2]. *)
- (* - by exfalso. *)
- (* - rewrite Bool.negb_involutive in HYP2. *)
- (* move: HYP2 => /eqP /eqP HYP2. *)
- (* by subst jo; rewrite scheduled_at_def EqSched_jo. *)
- (* } *)
- (* } *)
- (* { apply/negP; *)
- (* rewrite /interference /ideal_jlfp_rta.interference /is_priority_inversion *)
- (* /is_interference_from_another_hep_job *)
- (* HYP negb_or; apply/andP; split. *)
- (* - by rewrite Bool.negb_involutive; eapply (EDF_is_reflexive 0). *)
- (* - by rewrite negb_and Bool.negb_involutive; apply/orP; right. *)
- (* } *)
- (* Qed. *)
+ by eapply not_quiet_implies_not_idle; eauto 2 with basic_facts. }
+ { clear EqSched_jo; move: Sched_jo; rewrite scheduled_at_def; move => /eqP EqSched_jo.
+ rewrite EqSched_jo in HYP1, HYP2.
+ move: HYP1 HYP2.
+ rewrite Bool.negb_involutive negb_and.
+ move => HYP1 /orP [/negP HYP2| /eqP HYP2].
+ - by exfalso.
+ - rewrite Bool.negb_involutive in HYP2.
+ move: HYP2 => /eqP /eqP HYP2.
+ by subst jo; rewrite scheduled_at_def EqSched_jo.
+ }
+ }
+ { apply/negP;
+ rewrite /interference /ideal_jlfp_rta.interference /is_priority_inversion
+ /is_interference_from_another_hep_job
+ HYP negb_or; apply/andP; split.
+ - by rewrite Bool.negb_involutive; eapply (EDF_is_reflexive 0).
+ - by rewrite negb_and Bool.negb_involutive; apply/orP; right.
+ }
+ Qed.
(** Next, we prove that the interference and interfering workload
functions are consistent with sequential tasks. *)
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index eaa63d9b9..058ea5892 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -146,18 +146,16 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
intros j' JINB NOTHEP.
rewrite leq_sub2r //.
apply H_valid_model_with_bounded_nonpreemptive_segments.
- Admitted.
- (* by eapply in_arrivals_implies_arrived; eauto 2. *)
- (* } *)
- (* { apply /bigmax_leq_seqP. *)
- (* intros j' JINB NOTHEP. *)
- (* apply leq_bigmax_cond_seq with *)
- (* (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1); last by done. *)
- (* apply H_all_jobs_from_taskset. *)
- (* apply mem_bigcat_nat_exists in JINB. *)
- (* by inversion JINB as [ta' [JIN' _]]; exists ta'. *)
- (* } *)
- (* Qed. *)
+ exact: in_arrivals_implies_arrived JINB.
+ }
+ { apply /bigmax_leq_seqP.
+ intros j' JINB NOTHEP.
+ apply leq_bigmax_cond_seq with
+ (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1); last by done.
+ apply H_all_jobs_from_taskset.
+ by have /bigfcup_natP[i _ {}JINB] := JINB; exists i.
+ }
+ Qed.
(** Using the above lemma, we prove that the priority inversion of the task is bounded by blocking_bound. *)
Lemma priority_inversion_is_bounded:
@@ -175,37 +173,36 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
}
move: NEQ => /negP /negP; rewrite -ltnNge; move => BOUND.
edestruct (@preemption_time_exists) as [ppt [PPT NEQ]]; eauto 2 with basic_facts.
- Admitted.
- (* move: NEQ => /andP [GE LE]. *)
- (* apply leq_trans with (cumulative_priority_inversion sched j t1 ppt); *)
- (* last apply leq_trans with (ppt - t1); first last. *)
- (* - rewrite leq_subLR. *)
- (* apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done. *)
- (* by rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2. *)
- (* - rewrite /cumulative_priority_inversion /is_priority_inversion. *)
- (* rewrite -[X in _ <= X]addn0 -[ppt - t1]mul1n -iter_addn -big_const_nat. *)
- (* rewrite leq_sum //; intros t _; case: (sched t); last by done. *)
- (* by intros s; case: (hep_job s j). *)
- (* - rewrite /cumulative_priority_inversion /is_priority_inversion. *)
- (* rewrite (@big_cat_nat _ _ _ ppt) //=; last first. *)
- (* { rewrite ltn_subRL in BOUND. *)
- (* apply leq_trans with (t1 + blocking_bound); last by apply ltnW. *)
- (* apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done. *)
- (* rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2. *)
- (* } *)
- (* rewrite -[X in _ <= X]addn0 leq_add2l leqn0. *)
- (* rewrite big_nat_cond big1 //; move => t /andP [/andP [GEt LTt] _ ]. *)
- (* case SCHED: (sched t) => [s | ]; last by done. *)
- (* edestruct (@not_quiet_implies_exists_scheduled_hp_job) *)
- (* with (K := ppt - t1) (t1 := t1) (t2 := t2) (t := t) *)
- (* as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2 with basic_facts. *)
- (* { by exists ppt; split; [done | rewrite subnKC //; apply/andP]. } *)
- (* { by rewrite subnKC //; apply/andP; split. } *)
- (* apply/eqP; rewrite eqb0 Bool.negb_involutive. *)
- (* enough (EQef : s = j_hp); first by subst;auto. *)
- (* eapply ideal_proc_model_is_a_uniprocessor_model; eauto 2. *)
- (* by rewrite scheduled_at_def SCHED. *)
- (* Qed. *)
+ move: NEQ => /andP [GE LE].
+ apply leq_trans with (cumulative_priority_inversion sched j t1 ppt);
+ last apply leq_trans with (ppt - t1); first last.
+ - rewrite leq_subLR.
+ apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done.
+ by rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.
+ - rewrite /cumulative_priority_inversion /is_priority_inversion.
+ rewrite -[X in _ <= X]addn0 -[ppt - t1]mul1n -iter_addn -big_const_nat.
+ rewrite leq_sum //; intros t _; case: (sched t); last by done.
+ by intros s; case: (hep_job s j).
+ - rewrite /cumulative_priority_inversion /is_priority_inversion.
+ rewrite (@big_cat_nat _ _ _ ppt) //=; last first.
+ { rewrite ltn_subRL in BOUND.
+ apply leq_trans with (t1 + blocking_bound); last by apply ltnW.
+ apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done.
+ rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.
+ }
+ rewrite -[X in _ <= X]addn0 leq_add2l leqn0.
+ rewrite big_nat_cond big1 //; move => t /andP [/andP [GEt LTt] _ ].
+ case SCHED: (sched t) => [s | ]; last by done.
+ edestruct (@not_quiet_implies_exists_scheduled_hp_job)
+ with (K := ppt - t1) (t1 := t1) (t2 := t2) (t := t)
+ as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2 with basic_facts.
+ { by exists ppt; split; [done | rewrite subnKC //; apply/andP]. }
+ { by rewrite subnKC //; apply/andP; split. }
+ apply/eqP; rewrite eqb0 Bool.negb_involutive.
+ enough (EQef : s = j_hp); first by subst;auto.
+ eapply ideal_proc_model_is_a_uniprocessor_model; eauto 2.
+ by rewrite scheduled_at_def SCHED.
+ Qed.
End PriorityInversionIsBounded.
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index d9c587289..df337638a 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -150,12 +150,11 @@ Section RTAforFloatingModelwithArrivalCurves.
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.
all: eauto 2 with basic_facts.
- by apply sequential_readiness_implies_work_bearing_readiness.
- Admitted.
- (* - by apply sequential_readiness_implies_sequential_tasks. *)
- (* - intros A SP. *)
- (* rewrite subnn subn0. *)
- (* destruct (H_R_is_maximum _ SP) as [F [EQ LE]]. *)
- (* by exists F; rewrite addn0; split. *)
- (* Qed. *)
+ - by apply sequential_readiness_implies_sequential_tasks.
+ - intros A SP.
+ rewrite subnn subn0.
+ destruct (H_R_is_maximum _ SP) as [F [EQ LE]].
+ by exists F; rewrite addn0; split.
+ Qed.
End RTAforFloatingModelwithArrivalCurves.
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index 818cf5ae9..2d6dacf8e 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -152,8 +152,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
(L0 := L).
all: eauto 3 with basic_facts.
- by apply sequential_readiness_implies_work_bearing_readiness.
- Admitted.
- (* - by apply sequential_readiness_implies_sequential_tasks. *)
- (* Qed. *)
+ - by apply sequential_readiness_implies_sequential_tasks.
+ Qed.
End RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 9572773b0..9bc13ee17 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -139,15 +139,14 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
all: eauto 2 with basic_facts.
rewrite /work_bearing_readiness.
- by apply sequential_readiness_implies_work_bearing_readiness.
- Admitted.
- (* - by apply sequential_readiness_implies_sequential_tasks => //. *)
- (* - by rewrite BLOCK add0n. *)
- (* - move => A /andP [LT NEQ]. *)
- (* edestruct H_R_is_maximum as [F [FIX BOUND]]. *)
- (* { by apply/andP; split; eauto 2. } *)
- (* exists F; split. *)
- (* + by rewrite BLOCK add0n subnn subn0. *)
- (* + by rewrite subnn addn0. *)
- (* Qed. *)
+ - by apply sequential_readiness_implies_sequential_tasks => //.
+ - by rewrite BLOCK add0n.
+ - move => A /andP [LT NEQ].
+ edestruct H_R_is_maximum as [F [FIX BOUND]].
+ { by apply/andP; split; eauto 2. }
+ exists F; split.
+ + by rewrite BLOCK add0n subnn subn0.
+ + by rewrite subnn addn0.
+ Qed.
End RTAforFullyPreemptiveFPModelwithArrivalCurves.
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 277eb2ea0..608eb424a 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -158,24 +158,23 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
with (L0 := L).
all: eauto 2 with basic_facts.
- by apply sequential_readiness_implies_work_bearing_readiness.
- Admitted.
- (* - by apply sequential_readiness_implies_sequential_tasks. *)
- (* - intros A SP. *)
- (* destruct (H_R_is_maximum _ SP) as[FF [EQ1 EQ2]]. *)
- (* exists FF; rewrite subKn; first by done. *)
- (* rewrite /task_last_nonpr_segment -(leq_add2r 1) subn1 !addn1 prednK; last first. *)
- (* + rewrite /last0 -nth_last. *)
- (* apply HYP3; try by done. *)
- (* rewrite -(ltn_add2r 1) !addn1 prednK //. *)
- (* move: (number_of_preemption_points_in_task_at_least_two *)
- (* _ _ H_valid_model_with_fixed_preemption_points _ H_tsk_in_ts POSt) => Fact2. *)
- (* move: (Fact2) => Fact3. *)
- (* by rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2. *)
- (* + apply leq_trans with (task_max_nonpreemptive_segment tsk). *)
- (* * by apply last_of_seq_le_max_of_seq. *)
- (* * rewrite -END; last by done. *)
- (* apply ltnW; rewrite ltnS; try done. *)
- (* by apply max_distance_in_seq_le_last_element_of_seq; eauto 2. *)
- (* Qed. *)
+ - by apply sequential_readiness_implies_sequential_tasks.
+ - intros A SP.
+ destruct (H_R_is_maximum _ SP) as[FF [EQ1 EQ2]].
+ exists FF; rewrite subKn; first by done.
+ rewrite /task_last_nonpr_segment -(leq_add2r 1) subn1 !addn1 prednK; last first.
+ + rewrite /last0 -nth_last.
+ apply HYP3; try by done.
+ rewrite -(ltn_add2r 1) !addn1 prednK //.
+ move: (number_of_preemption_points_in_task_at_least_two
+ _ _ H_valid_model_with_fixed_preemption_points _ H_tsk_in_ts POSt) => Fact2.
+ move: (Fact2) => Fact3.
+ by rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2.
+ + apply leq_trans with (task_max_nonpreemptive_segment tsk).
+ * by apply last_of_seq_le_max_of_seq.
+ * rewrite -END; last by done.
+ apply ltnW; rewrite ltnS; try done.
+ by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
+ Qed.
End RTAforFixedPreemptionPointsModelwithArrivalCurves.
--
GitLab