From 1b8501dc7349387b4aceb66a8840ce0236daaf0d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 30 Mar 2023 13:11:16 +0200
Subject: [PATCH] move misplaced code out of `prosa.analysis.facts.busy_window`
- The busy_window.v file still depends on the ideal uniprocessor
assumption, so move it to the ideal submodule.
- The priority_inversion.v file has nothing to do with busy windows,
so move it to the prosa.analysis.facts.priority module.
- Move a trivial quiet-time lemma from carry_in.v to quiet_time.v.
Much cleanup of the ideal submodule remains to be done...
See also: https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/112
---
analysis/facts/busy_interval/carry_in.v | 17 ++++-------------
.../busy_interval/{ => ideal}/busy_interval.v | 0
analysis/facts/busy_interval/ideal/carry_in.v | 1 +
.../busy_interval/ideal/hep_job_scheduled.v | 2 +-
.../busy_interval/ideal/priority_inversion.v | 2 +-
analysis/facts/busy_interval/quiet_time.v | 18 +++++++++++++-----
analysis/facts/priority/edf.v | 2 +-
.../inversion.v} | 0
results/fixed_priority/rta/bounded_pi.v | 2 +-
9 files changed, 22 insertions(+), 22 deletions(-)
rename analysis/facts/busy_interval/{ => ideal}/busy_interval.v (100%)
rename analysis/facts/{busy_interval/priority_inversion.v => priority/inversion.v} (100%)
diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index 7e24459df..c4ff57326 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -1,8 +1,8 @@
Require Export prosa.analysis.facts.model.workload.
-Require Export prosa.analysis.definitions.carry_in.
-Require Export prosa.analysis.facts.busy_interval.busy_interval.
Require Export prosa.analysis.facts.model.ideal.service_of_jobs.
-
+Require Export prosa.analysis.facts.busy_interval.quiet_time.
+Require Export prosa.analysis.definitions.work_bearing_readiness.
+Require Export prosa.model.schedule.work_conserving.
(** * Existence of No Carry-In Instant *)
@@ -60,14 +60,6 @@ Section ExistsNoCarryIn.
(** ... and assume that the schedule is work-conserving. *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
- (** The fact that there is no carry-in at time instant [t] trivially
- implies that [t] is a quiet time. *)
- Lemma no_carry_in_implies_quiet_time :
- forall j t,
- no_carry_in t ->
- quiet_time j t.
- Proof. by move=> j t + j_hp ARR HP BEF; apply. Qed.
-
(** Conversely, the presence of a pending job implies that the processor isn't
idle due to work-conservation. *)
Lemma pending_job_implies_not_idle :
@@ -230,8 +222,7 @@ Section ExistsNoCarryIn.
- eapply in_arrivals_implies_arrived_between in A; eauto 2.
}
apply/eqP; rewrite eqn_leq; apply/andP; split;
- last by apply service_of_jobs_le_workload;
- auto using ideal_proc_model_provides_unit_service.
+ last by apply service_of_jobs_le_workload.
rewrite /total_workload (workload_of_jobs_cat arr_seq t); last first.
apply/andP; split; [by done | by rewrite leq_addr].
rewrite (service_of_jobs_cat_scheduling_interval _ _ _ _ _ _ _ t); try done; first last.
diff --git a/analysis/facts/busy_interval/busy_interval.v b/analysis/facts/busy_interval/ideal/busy_interval.v
similarity index 100%
rename from analysis/facts/busy_interval/busy_interval.v
rename to analysis/facts/busy_interval/ideal/busy_interval.v
diff --git a/analysis/facts/busy_interval/ideal/carry_in.v b/analysis/facts/busy_interval/ideal/carry_in.v
index a88fb6f27..1bc826f8d 100644
--- a/analysis/facts/busy_interval/ideal/carry_in.v
+++ b/analysis/facts/busy_interval/ideal/carry_in.v
@@ -1,4 +1,5 @@
Require Export prosa.analysis.facts.busy_interval.carry_in.
+Require Export prosa.analysis.facts.busy_interval.ideal.busy_interval.
(** The following lemma conceptually belongs in
[prosa.analysis.facts.busy_interval.carry_in], but still has dependencies
diff --git a/analysis/facts/busy_interval/ideal/hep_job_scheduled.v b/analysis/facts/busy_interval/ideal/hep_job_scheduled.v
index 932556146..1d55f9e95 100644
--- a/analysis/facts/busy_interval/ideal/hep_job_scheduled.v
+++ b/analysis/facts/busy_interval/ideal/hep_job_scheduled.v
@@ -1,5 +1,5 @@
Require Export prosa.model.schedule.priority_driven.
-Require Export prosa.analysis.facts.busy_interval.busy_interval.
+Require Export prosa.analysis.facts.busy_interval.ideal.busy_interval.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.
diff --git a/analysis/facts/busy_interval/ideal/priority_inversion.v b/analysis/facts/busy_interval/ideal/priority_inversion.v
index 6409a84ba..f08013b1a 100644
--- a/analysis/facts/busy_interval/ideal/priority_inversion.v
+++ b/analysis/facts/busy_interval/ideal/priority_inversion.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.facts.busy_interval.priority_inversion.
+Require Export prosa.analysis.facts.priority.inversion.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.
diff --git a/analysis/facts/busy_interval/quiet_time.v b/analysis/facts/busy_interval/quiet_time.v
index f2b6f5655..400dc7733 100644
--- a/analysis/facts/busy_interval/quiet_time.v
+++ b/analysis/facts/busy_interval/quiet_time.v
@@ -1,5 +1,6 @@
Require Export prosa.analysis.definitions.busy_interval.
-
+Require Export prosa.analysis.definitions.carry_in.
+
(** In this module we collect some basic facts about quiet times. *)
Section Facts.
@@ -16,9 +17,16 @@ Section Facts.
Variable arr_seq : arrival_sequence Job.
(** We prove that 0 is always a quiet time. *)
- Lemma zero_is_quiet_time (j : Job) : quiet_time arr_seq sched j 0.
- Proof.
- by intros jhp ARR HP AB; move: AB; rewrite /arrived_before ltn0.
- Qed.
+ Lemma zero_is_quiet_time (j : Job) :
+ quiet_time arr_seq sched j 0.
+ Proof. by move=> jhp ARR HP; rewrite /arrived_before ltn0. Qed.
+
+ (** The fact that there is no carry-in at time instant [t] trivially
+ implies that [t] is a quiet time. *)
+ Lemma no_carry_in_implies_quiet_time :
+ forall j t,
+ no_carry_in arr_seq sched t ->
+ quiet_time arr_seq sched j t.
+ Proof. by move=> j t + j_hp ARR HP BEF; apply. Qed.
End Facts.
diff --git a/analysis/facts/priority/edf.v b/analysis/facts/priority/edf.v
index 2c1b624c5..29ba56726 100644
--- a/analysis/facts/priority/edf.v
+++ b/analysis/facts/priority/edf.v
@@ -35,7 +35,7 @@ Global Hint Resolve EDF_respects_sequential_tasks : basic_rt_facts.
Require Export prosa.model.task.sequentiality.
-Require Export prosa.analysis.facts.busy_interval.priority_inversion.
+Require Export prosa.analysis.facts.priority.inversion.
Require Export prosa.analysis.facts.priority.sequential.
(** In this section, we prove that the EDF priority policy implies that tasks
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/priority/inversion.v
similarity index 100%
rename from analysis/facts/busy_interval/priority_inversion.v
rename to analysis/facts/priority/inversion.v
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 37e456c40..436090ab3 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -1,6 +1,6 @@
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.abstract.ideal.iw_instantiation.
-Require Export prosa.analysis.facts.busy_interval.busy_interval.
+Require Export prosa.analysis.facts.busy_interval.ideal.busy_interval.
(** * Abstract RTA for FP-schedulers with Bounded Priority Inversion *)
(** In this module we instantiate the Abstract Response-Time analysis
--
GitLab