From c2267dffde5418fc58a16b31a46becddc1e02823 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Tue, 20 Feb 2024 14:35:04 +0100
Subject: [PATCH] bound max non-preemptive low-pr segment under EDF
---
.../restricted_supply/fp_bounded_bi.v | 6 +-
.../restricted_supply/search_space_fp.v | 9 +-
.../edf.v} | 0
.../fp.v} | 0
analysis/facts/blocking_bound/edf.v | 103 ++++++++++++++++++
.../fp.v} | 4 +-
results/edf/rta/bounded_nps.v | 53 +--------
results/edf/rta/floating_nonpreemptive.v | 2 +-
results/edf/rta/fully_preemptive.v | 4 +-
results/edf/rta/limited_preemptive.v | 2 +-
results/fixed_priority/rta/bounded_nps.v | 2 +-
.../rta/floating_nonpreemptive.v | 2 +-
.../fixed_priority/rta/limited_preemptive.v | 2 +-
results/rs/fp/fully_preemptive.v | 2 +-
14 files changed, 125 insertions(+), 66 deletions(-)
rename analysis/definitions/{blocking_bound_edf.v => blocking_bound/edf.v} (100%)
rename analysis/definitions/{blocking_bound_fp.v => blocking_bound/fp.v} (100%)
create mode 100644 analysis/facts/blocking_bound/edf.v
rename analysis/facts/{blocking_bound_fp.v => blocking_bound/fp.v} (96%)
diff --git a/analysis/abstract/restricted_supply/fp_bounded_bi.v b/analysis/abstract/restricted_supply/fp_bounded_bi.v
index 93d678eee..f4ebfe746 100644
--- a/analysis/abstract/restricted_supply/fp_bounded_bi.v
+++ b/analysis/abstract/restricted_supply/fp_bounded_bi.v
@@ -1,4 +1,4 @@
- Require Export prosa.analysis.facts.blocking_bound_fp.
+ Require Export prosa.analysis.facts.blocking_bound.fp.
Require Export prosa.analysis.abstract.restricted_supply.abstract_rta.
Require Export prosa.analysis.abstract.restricted_supply.iw_instantiation.
Require Export prosa.analysis.definitions.sbf.busy.
@@ -184,7 +184,7 @@ Section BoundedBusyIntervals.
rewrite -(leqRW H_fixed_point); apply leq_add.
- apply: leq_trans; first apply: service_inversion_is_bounded => //.
+ instantiate (1 := fun _ => blocking_bound ts tsk) => //=.
- by move=> jo t t' ARRo TSKo PREFo; apply: priority_inversion_is_bounded_by_blocking => //.
+ by move=> jo t t' ARRo TSKo PREFo; apply: nonpreemptive_segments_bounded_by_blocking => //.
+ by done.
- rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
by apply hep_workload_le_total_hep_rbf.
@@ -339,7 +339,7 @@ Section BoundedBusyIntervals.
- apply: leq_trans.
+ apply: service_inversion_is_bounded => //.
move => *; instantiate (1 := fun _ => blocking_bound ts tsk) => //.
- by apply: priority_inversion_is_bounded_by_blocking => //.
+ by apply: nonpreemptive_segments_bounded_by_blocking => //.
+ by done.
- by done.
- lia.
diff --git a/analysis/abstract/restricted_supply/search_space_fp.v b/analysis/abstract/restricted_supply/search_space_fp.v
index fcb0fdfd1..9459d14c7 100644
--- a/analysis/abstract/restricted_supply/search_space_fp.v
+++ b/analysis/abstract/restricted_supply/search_space_fp.v
@@ -1,6 +1,6 @@
Require Export prosa.analysis.facts.model.rbf.
Require Export prosa.analysis.abstract.search_space.
-Require Export prosa.analysis.definitions.blocking_bound_fp.
+Require Export prosa.analysis.definitions.blocking_bound.fp.
(** * Abstract Search Space is a Subset of Restricted Supply FP Search Space *)
@@ -50,9 +50,10 @@ Section SearchSpaceSubset.
Let task_rbf := task_request_bound_function tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
- (** Let [L] be any positive constant. Typically, [L] denotes an
- upper bound on the length of a busy interval of a [tsk]'s upper
- bound on the length of a busy interval of any job of [tsk]. *)
+ (** Let [L] be an arbitrary positive constant. Typically, [L]
+ denotes an upper bound on the length of a busy interval of a job
+ of [tsk]. In this file, however, [L] can be any positive
+ constant. *)
Variable L : duration.
Hypothesis H_L_positive : 0 < L.
diff --git a/analysis/definitions/blocking_bound_edf.v b/analysis/definitions/blocking_bound/edf.v
similarity index 100%
rename from analysis/definitions/blocking_bound_edf.v
rename to analysis/definitions/blocking_bound/edf.v
diff --git a/analysis/definitions/blocking_bound_fp.v b/analysis/definitions/blocking_bound/fp.v
similarity index 100%
rename from analysis/definitions/blocking_bound_fp.v
rename to analysis/definitions/blocking_bound/fp.v
diff --git a/analysis/facts/blocking_bound/edf.v b/analysis/facts/blocking_bound/edf.v
new file mode 100644
index 000000000..174781667
--- /dev/null
+++ b/analysis/facts/blocking_bound/edf.v
@@ -0,0 +1,103 @@
+Require Export prosa.analysis.definitions.blocking_bound.edf.
+Require Export prosa.analysis.facts.busy_interval.pi.
+Require Export prosa.model.priority.edf.
+Require Export prosa.model.task.absolute_deadline.
+Require Export prosa.analysis.facts.model.arrival_curves.
+
+(** * Lower-Priority Non-Preemptive Segment is Bounded *)
+(** In this file, we prove that, under the EDF scheduling policy, the
+ length of the maximum non-preemptive segment of a lower-priority
+ job (w.r.t. a job of a task [tsk]) is bounded by
+ [blocking_bound]. *)
+Section MaxNPSegmentIsBounded.
+
+ (** Consider any type of tasks, each characterized by a WCET
+ [task_cost], an arrival curve [max_arrivals], a relative
+ deadline [task_deadline], and a bound on the the task's longest
+ non-preemptive segment [task_max_nonpreemptive_segment] ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+ Context `{MaxArrivals Task}.
+ Context `{TaskDeadline Task}.
+ Context `{TaskMaxNonpreemptiveSegment Task}.
+
+ (** ... and any type of jobs associated with these tasks, where each
+ job has a task [job_task], a cost [job_cost], and an arrival
+ time [job_arrival]. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobCost Job}.
+ Context `{JobArrival Job}.
+
+ (** Consider any kind of processor state model. *)
+ Context `{PState : ProcessorState Job}.
+
+ (** Consider the EDF policy. *)
+ Let EDF := EDF Job.
+
+ (** Consider any valid arrival sequence. *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+ (** ... and any schedule of this arrival sequence. *)
+ Variable sched : schedule PState.
+
+ (** We further require that a job's cost cannot exceed its task's stated WCET ... *)
+ Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+ (** ... and assume that jobs have bounded non-preemptive segments. *)
+ Context `{JobPreemptable Job}.
+ Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
+ valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+ (** Consider an arbitrary task set [ts], ... *)
+ Variable ts : seq Task.
+
+ (** ... assume that all jobs come from the task set, ... *)
+ Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+ (** ... and let [tsk] be any task in [ts] that is to be analyzed. *)
+ Variable tsk : Task.
+ Hypothesis H_tsk_in_ts : tsk \in ts.
+
+ (** Let [max_arrivals] be a family of arrival curves. *)
+ Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+ (** Consider any job [j] of [tsk]. *)
+ Variable j : Job.
+ Hypothesis H_job_of_tsk : job_of_task tsk j.
+
+ (** Then, the maximum length of a nonpreemptive segment among all
+ lower-priority jobs (w.r.t. the given job [j]) arrived so far is
+ bounded by [blocking_bound]. *)
+ Lemma nonpreemptive_segments_bounded_by_blocking :
+ forall t1 t2,
+ busy_interval_prefix arr_seq sched j t1 t2 ->
+ max_lp_nonpreemptive_segment arr_seq j t1 <= blocking_bound ts tsk (job_arrival j - t1).
+ Proof.
+ move=> t1 t2 BUSY; rewrite /max_lp_nonpreemptive_segment /blocking_bound.
+ apply: leq_trans;first by exact: max_np_job_segment_bounded_by_max_np_task_segment.
+ apply /bigmax_leq_seqP => j' JINB NOTHEP.
+ have ARR': arrives_in arr_seq j'
+ by apply: in_arrivals_implies_arrived; exact: JINB.
+ apply leq_bigmax_cond_seq with (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1);
+ first by apply H_all_jobs_from_taskset.
+ apply in_arrivals_implies_arrived_between in JINB => [|//].
+ move: JINB; move => /andP [_ TJ'].
+ repeat (apply/andP; split); last first.
+ { rewrite /hep_job -ltnNge in NOTHEP.
+ move: H_job_of_tsk => /eqP <-.
+ have ARRLE: job_arrival j' < job_arrival j.
+ { by apply: (@leq_trans t1) => //; move: BUSY => [ _ [ _ [ _ /andP [F G]]] ]. }
+ move: NOTHEP; rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline.
+ by lia. }
+ { move: NOTHEP => /andP [_ NZ].
+ move: (H_valid_job_cost j' ARR'); rewrite /valid_job_cost.
+ by lia. }
+ { apply: non_pathological_max_arrivals; last first.
+ - exact: ARR'.
+ - by rewrite /job_of_task.
+ - by apply H_is_arrival_curve, H_all_jobs_from_taskset, ARR'. }
+ Qed.
+
+End MaxNPSegmentIsBounded.
diff --git a/analysis/facts/blocking_bound_fp.v b/analysis/facts/blocking_bound/fp.v
similarity index 96%
rename from analysis/facts/blocking_bound_fp.v
rename to analysis/facts/blocking_bound/fp.v
index 45f83b186..168efede0 100644
--- a/analysis/facts/blocking_bound_fp.v
+++ b/analysis/facts/blocking_bound/fp.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.definitions.blocking_bound_fp.
+Require Export prosa.analysis.definitions.blocking_bound.fp.
Require Export prosa.analysis.facts.busy_interval.pi.
@@ -57,7 +57,7 @@ Section MaxNPSegmentIsBounded.
(** Then, the maximum length of a nonpreemptive segment among all
lower-priority jobs (w.r.t. the given job [j]) arrived so far is
bounded by [blocking_bound]. *)
- Lemma priority_inversion_is_bounded_by_blocking :
+ Lemma nonpreemptive_segments_bounded_by_blocking :
forall t,
max_lp_nonpreemptive_segment arr_seq j t <= blocking_bound ts tsk.
Proof.
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index bb9605acf..15ac234bb 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -3,9 +3,9 @@ Require Import prosa.model.readiness.basic.
Require Export prosa.analysis.facts.busy_interval.pi_bound.
Require Export prosa.analysis.facts.busy_interval.arrival.
Require Export prosa.results.edf.rta.bounded_pi.
-Require Export model.schedule.work_conserving.
-Require Export analysis.definitions.busy_interval.
-Require Export analysis.definitions.blocking_bound_edf.
+Require Export prosa.model.schedule.work_conserving.
+Require Export prosa.analysis.definitions.busy_interval.
+Require Export prosa.analysis.facts.blocking_bound.edf.
(** * RTA for EDF with Bounded Non-Preemptive Segments *)
@@ -199,51 +199,6 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Qed.
- (** ** Priority inversion is bounded *)
- (** In this section, we prove that a priority inversion for task [tsk] is bounded by
- the maximum length of non-preemptive segments among the tasks with lower priority. *)
- Section PriorityInversionIsBounded.
-
- (** Since EDF is a JLFP policy, the maximum non-preemptive segment length of any task
- that releases a job with an earlier absolute deadline (w.r.t. a given job [j]) and
- non-zero execution cost upper-bounds the maximum possible length of priority
- inversion (experienced by said job [j]). *)
-
- (** Using this fact, we prove that the maximum length of a priority inversion of a given
- job [j] is indeed bounded by the defined blocking bound. *)
- Lemma priority_inversion_is_bounded_by_blocking:
- forall j t1 t2,
- arrives_in arr_seq j ->
- job_of_task tsk j ->
- busy_interval_prefix arr_seq sched j t1 t2 ->
- max_lp_nonpreemptive_segment arr_seq j t1 <= blocking_bound ts tsk (job_arrival j - t1).
- Proof.
- move=> j t1 t2 ARR TSK BUSY; rewrite /max_lp_nonpreemptive_segment /blocking_bound.
- apply: leq_trans;first by exact: max_np_job_segment_bounded_by_max_np_task_segment.
- apply /bigmax_leq_seqP => j' JINB NOTHEP.
- have ARR': arrives_in arr_seq j'
- by apply: in_arrivals_implies_arrived; exact: JINB.
- apply leq_bigmax_cond_seq with (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1);
- first by apply H_all_jobs_from_taskset.
- apply in_arrivals_implies_arrived_between in JINB => [|//].
- move: JINB; move => /andP [_ TJ'].
- repeat (apply/andP; split); last first.
- { rewrite /EDF -ltnNge in NOTHEP.
- move: TSK => /eqP <-.
- have ARRLE: job_arrival j' < job_arrival j by apply: (@leq_trans t1).
- move: NOTHEP; rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline /D.
- by lia. }
- { move: NOTHEP => /andP [_ NZ].
- move: (H_valid_job_cost j' ARR'); rewrite /valid_job_cost.
- by lia. }
- { apply: non_pathological_max_arrivals; last first.
- - exact: ARR'.
- - by rewrite /job_of_task.
- - by apply H_is_arrival_curve, H_all_jobs_from_taskset, ARR'. }
- Qed.
-
- End PriorityInversionIsBounded.
-
(** ** Response-Time Bound *)
(** In this section, we prove that the maximum among the solutions of the response-time
bound recurrence is a response-time bound for [tsk]. *)
@@ -278,7 +233,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Proof.
apply: uniprocessor_response_time_bound_edf; eauto 4 with basic_rt_facts.
{ apply: priority_inversion_is_bounded => //.
- apply: priority_inversion_is_bounded_by_blocking. }
+ by move=> *; apply: nonpreemptive_segments_bounded_by_blocking. }
- move=> A BPI_SP.
by apply H_R_is_maximum, search_space_inclusion.
Qed.
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index 1ca4ae122..fd4ae79c9 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -3,7 +3,7 @@ Require Export prosa.results.edf.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
Require Export prosa.analysis.facts.readiness.sequential.
Require Import prosa.model.priority.edf.
-Require Export prosa.analysis.definitions.blocking_bound_edf.
+Require Export prosa.analysis.definitions.blocking_bound.edf.
(** * RTA for EDF with Floating Non-Preemptive Regions *)
(** In this module we prove the RTA theorem for floating non-preemptive regions EDF model. *)
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index 2b1560bc7..91dd7788c 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -129,8 +129,8 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
Proof.
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L:=L) => //.
move => A /andP [LT CHANGE].
- have BLOCK: forall A', blocking_bound_edf.blocking_bound ts tsk A' = blocking_bound A'.
- { by move=> A'; rewrite /blocking_bound_edf.blocking_bound /parameters.task_max_nonpreemptive_segment
+ have BLOCK: forall A', edf.blocking_bound ts tsk A' = blocking_bound A'.
+ { by move=> A'; rewrite /edf.blocking_bound /parameters.task_max_nonpreemptive_segment
/fully_preemptive_task_model subnn big1_eq. }
specialize (H_R_is_maximum A); feed H_R_is_maximum; first by apply/andP; split; done.
move: H_R_is_maximum => [F [FIX BOUND]].
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index ae47221d5..26819293c 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -4,7 +4,7 @@ Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
Require Export prosa.analysis.facts.readiness.basic.
Require Export prosa.model.task.preemption.limited_preemptive.
Require Export prosa.model.priority.edf.
-Require Export prosa.analysis.definitions.blocking_bound_edf.
+Require Export prosa.analysis.definitions.blocking_bound.edf.
(** * RTA for EDF with Fixed Preemption Points *)
(** In this module we prove the RTA theorem for EDF-schedulers with
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 9d319066c..2f67d52b2 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -2,7 +2,7 @@ Require Export prosa.analysis.facts.busy_interval.pi_bound.
Require Export prosa.results.fixed_priority.rta.bounded_pi.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.analysis.definitions.busy_interval.
-Require Export prosa.analysis.definitions.blocking_bound_fp.
+Require Export prosa.analysis.definitions.blocking_bound.fp.
(** * RTA for FP-schedulers with Bounded Non-Preemptive Segments *)
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index 189642013..c0c19d376 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -1,7 +1,7 @@
Require Export prosa.results.fixed_priority.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
Require Export prosa.analysis.facts.readiness.sequential.
-Require Export prosa.analysis.definitions.blocking_bound_fp.
+Require Export prosa.analysis.definitions.blocking_bound.fp.
(** * RTA for Model with Floating Non-Preemptive Regions *)
(** In this module we prove the RTA theorem for floating non-preemptive regions FP model. *)
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 240853fd1..81b0c74aa 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -2,7 +2,7 @@ Require Export prosa.results.fixed_priority.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
Require Export prosa.analysis.facts.readiness.sequential.
Require Export prosa.model.task.preemption.limited_preemptive.
-Require Export prosa.analysis.definitions.blocking_bound_fp.
+Require Export prosa.analysis.definitions.blocking_bound.fp.
(** * RTA for FP-schedulers with Fixed Preemption Points *)
(** In this module we prove the RTA theorem for FP-schedulers with
diff --git a/results/rs/fp/fully_preemptive.v b/results/rs/fp/fully_preemptive.v
index 731efe96e..6c5b9deba 100644
--- a/results/rs/fp/fully_preemptive.v
+++ b/results/rs/fp/fully_preemptive.v
@@ -205,7 +205,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
- apply: instantiated_task_intra_interference_is_bounded; eauto 1 => //; first last.
+ by apply athep_workload_le_total_ohep_rbf.
+ apply: service_inversion_is_bounded => // => jo t1 t2 ARRo TSKo BUSYo.
- by unshelve rewrite (leqRW (priority_inversion_is_bounded_by_blocking _ _ _ _ _ _ _ _ _)) => //.
+ by unshelve rewrite (leqRW (nonpreemptive_segments_bounded_by_blocking _ _ _ _ _ _ _ _ _)) => //.
- move => A SP; move: (H_R_is_maximum A) => [].
+ apply: search_space_sub => //; apply: search_space_switch_IBF; last by exact: SP.
by move=> A1 Δ1; rewrite //= BLOCK.
--
GitLab