From 0844b5aa77616fbb3005204e9f5c9a43302a7c1c Mon Sep 17 00:00:00 2001
From: Sergey Bozhko <sbozhko@mpi-sws.org>
Date: Thu, 12 Oct 2023 10:25:04 +0200
Subject: [PATCH] remove [sequential_tasks] assumption in one proof
---
analysis/abstract/ideal/iw_instantiation.v | 29 +++++++---------------
results/edf/rta/bounded_pi.v | 2 +-
results/elf/rta/bounded_pi.v | 2 +-
results/fixed_priority/rta/bounded_pi.v | 2 +-
results/gel/rta/bounded_pi.v | 2 +-
5 files changed, 13 insertions(+), 24 deletions(-)
diff --git a/analysis/abstract/ideal/iw_instantiation.v b/analysis/abstract/ideal/iw_instantiation.v
index 5fc35c632..739915943 100644
--- a/analysis/abstract/ideal/iw_instantiation.v
+++ b/analysis/abstract/ideal/iw_instantiation.v
@@ -54,10 +54,6 @@ Section JLFPInstantiation.
(** Let [tsk] be any task. *)
Variable tsk : Task.
- (** Assume we have sequential tasks, i.e., jobs of the same task
- execute in the order of their arrival. *)
- Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
-
(** We also assume that the policy respects sequential tasks,
meaning that later-arrived jobs of a task don't have higher
priority than earlier-arrived jobs of the same task. *)
@@ -486,25 +482,24 @@ Section JLFPInstantiation.
by rewrite /receives_service_at service_at_is_scheduled_at lt0b.
Qed.
- (** Let [j] be any job of task [tsk], and let [upper_bound] be any
- time instant after job [j]'s arrival. Then for any time
- interval lying before [upper_bound], the cumulative
- interference received by [tsk] is equal to the sum of the
+ (** Let [j] be any job of task [tsk]. Then the cumulative task
+ interference received by job [j] is bounded to the sum of the
cumulative priority inversion of job [j] and the cumulative
- interference incurred by task [tsk] due to other tasks. *)
+ interference incurred by job [j] due to higher-or-equal
+ priority jobs from other tasks. *)
Lemma cumulative_task_interference_split :
forall j t1 t2,
arrives_in arr_seq j ->
job_of_task tsk j ->
~~ completed_by sched j t2 ->
- cumul_task_interference arr_seq sched j t1 t2 =
- cumulative_priority_inversion arr_seq sched j t1 t2
+ cumul_task_interference arr_seq sched j t1 t2
+ <= cumulative_priority_inversion arr_seq sched j t1 t2
+ cumulative_another_task_hep_job_interference arr_seq sched j t1 t2.
Proof.
move=> j t1 R ARR TSK NCOMPL.
rewrite /cumul_task_interference /cumul_cond_interference.
- rewrite -big_split //= big_seq_cond [RHS]big_seq_cond.
- apply eq_bigr; move => t /andP [IN _].
+ rewrite -big_split //= big_seq_cond [leqRHS]big_seq_cond.
+ apply leq_sum; move => t /andP [IN _].
rewrite /cond_interference /non_self /interference /ideal_jlfp_interference.
have [IDLE|[s SCHEDs]] := ideal_proc_model_sched_case_analysis sched t.
{ move: (IDLE) => IIDLE; erewrite <-is_idle_def in IDLE => //.
@@ -525,13 +520,7 @@ Section JLFPInstantiation.
{ by subst; rewrite /job_of_task eq_refl H_priority_is_reflexive. }
have [/eqP EQt|NEQt] := eqVneq (job_task s) (job_task j).
{ apply/eqP; move: (EQt) => /eqP <-.
- rewrite /job_of_task eq_refl //= andbF addn0 eq_sym eqb0; apply/negP => LPs.
- have ARRj': job_arrival j < job_arrival s
- by move: LPs; rewrite ltnNge; apply contra, H_JLFP_respects_sequential_tasks; rewrite EQt.
- eapply H_sequential_tasks in ARRj' => //; last by rewrite /same_task eq_sym.
- apply ARRj' in SCHEDs; clear ARRj'; move: NCOMPL => /negP NCOMPL; apply: NCOMPL.
- apply completion_monotonic with t => //.
- by move: IN; rewrite mem_iota; clear; lia. }
+ by rewrite /job_of_task eq_refl //= andbF addn0 eq_sym eqb0; apply/negP => LPs. }
{ by rewrite /job_of_task NEQt //= andbT; case: hep_job. }
}
Qed.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 32c61a1e3..9b0bc644d 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -334,7 +334,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
- exfalso; move: NCOMPL => /negP COMPL; apply: COMPL.
by rewrite /completed_by /completed_by ZERO.
- rewrite -/(cumul_task_interference _ _ _ _ _).
- rewrite (cumulative_task_interference_split _ _ _ _ _ _ tsk) //=; last exact: EDF_implies_sequential_tasks.
+ rewrite (leqRW (cumulative_task_interference_split _ _ _ _ _ _ _ _ _ _ _ _ _ )) //=.
rewrite /I leq_add //; first exact: cumulative_priority_inversion_is_bounded.
eapply leq_trans; first exact: cumulative_interference_is_bounded_by_total_service.
eapply leq_trans; first exact: service_of_jobs_le_workload.
diff --git a/results/elf/rta/bounded_pi.v b/results/elf/rta/bounded_pi.v
index 7b1a456f6..805e7b7e5 100644
--- a/results/elf/rta/bounded_pi.v
+++ b/results/elf/rta/bounded_pi.v
@@ -510,7 +510,7 @@ Section AbstractRTAforELFwithArrivalCurves.
- exfalso; move: NCOMPL => /negP COMPL; apply: COMPL.
by rewrite /completed_by /completed_by ZERO.
- rewrite -/(cumul_task_interference _ _ _ _ _).
- rewrite (cumulative_task_interference_split _ _ _ _ _ _ tsk) //=.
+ rewrite (leqRW (cumulative_task_interference_split _ _ _ _ _ _ _ _ _ _ _ _ _ )) //=.
rewrite /IBF_other -addnA.
apply: leq_add;
first by apply: cumulative_priority_inversion_is_bounded priority_inversion_is_bounded =>//.
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 3768d56fe..3fe55992e 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -239,7 +239,7 @@ Section AbstractRTAforFPwithArrivalCurves.
move: (posnP (@job_cost _ Cost j)) => [ZERO|POS].
{ by exfalso; rewrite /completed_by ZERO in NCOMPL. }
rewrite -/(cumul_task_interference _ _ _ _ _).
- rewrite (cumulative_task_interference_split _ _ _ _ _ _ tsk) //=.
+ rewrite (leqRW (cumulative_task_interference_split _ _ _ _ _ _ _ _ _ _ _ _ _)) //=.
rewrite /IBF_other leq_add//.
{ apply leq_trans with (cumulative_priority_inversion arr_seq sched j t1 (t1 + Δ)); first by done.
apply leq_trans with (cumulative_priority_inversion arr_seq sched j t1 t2);
diff --git a/results/gel/rta/bounded_pi.v b/results/gel/rta/bounded_pi.v
index ab37c6821..81366f9e2 100644
--- a/results/gel/rta/bounded_pi.v
+++ b/results/gel/rta/bounded_pi.v
@@ -235,7 +235,7 @@ Section AbstractRTAforGELwithArrivalCurves.
- exfalso; move: NCOMPL => /negP COMPL; apply: COMPL.
by rewrite /completed_by /completed_by ZERO.
- rewrite -/(cumul_task_interference _ _ _ _ _).
- rewrite (cumulative_task_interference_split _ _ _ _ _ _ tsk) //=; last by exact: GEL_implies_sequential_tasks.
+ rewrite (leqRW (cumulative_task_interference_split _ _ _ _ _ _ _ _ _ _ _ _ _)) //=.
rewrite /I leq_add //.
+ exact: cumulative_priority_inversion_is_bounded.
+ eapply leq_trans; first exact: cumulative_interference_is_bounded_by_total_service.
--
GitLab