From fedef925a2cd628a21e38d945370b0761d3354e1 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Wed, 11 Mar 2020 13:22:26 +0100
Subject: [PATCH] Delete duplications of search space
---
results/edf/rta/bounded_nps.v | 14 ++++++--------
results/edf/rta/bounded_pi.v | 2 +-
results/edf/rta/floating_nonpreemptive.v | 10 ++--------
results/edf/rta/fully_nonpreemptive.v | 8 +-------
results/edf/rta/fully_preemptive.v | 16 ++++++----------
results/edf/rta/limited_preemptive.v | 10 ++--------
results/fixed_priority/rta/bounded_nps.v | 2 +-
results/fixed_priority/rta/bounded_pi.v | 2 +-
.../fixed_priority/rta/floating_nonpreemptive.v | 4 ++--
results/fixed_priority/rta/fully_nonpreemptive.v | 4 ++--
results/fixed_priority/rta/fully_preemptive.v | 2 +-
results/fixed_priority/rta/limited_preemptive.v | 4 ++--
12 files changed, 27 insertions(+), 51 deletions(-)
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index a92e599eb..1c048c5ca 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -139,7 +139,8 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Let bound_on_total_hep_workload_changes_at :=
bound_on_total_hep_workload_changes_at ts tsk.
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
-
+ Let is_in_search_space := is_in_search_space ts tsk.
+
(** We also define a bound for the priority inversion caused by jobs with lower priority. *)
Definition blocking_bound :=
\max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk < D tsk_o))
@@ -257,16 +258,13 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Hypothesis H_L_positive : L > 0.
Hypothesis H_fixed_point : L = total_rbf L.
- (** To reduce the time complexity of the analysis, recall the notion of search space. *)
- Let is_in_search_space A :=
- (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
-
- (** Consider any value R, and assume that for any given arrival offset A in the search space,
- there is a solution of the response-time bound recurrence which is bounded by R. *)
+ (** Consider any value [R], and assume that for any given arrival
+ offset [A] in the search space, there is a solution of the
+ response-time bound recurrence which is bounded by [R]. *)
Variable R : duration.
Hypothesis H_R_is_maximum:
forall (A : duration),
- is_in_search_space A ->
+ is_in_search_space L A ->
exists (F : duration),
A + F = blocking_bound
+ (task_rbf (A + ε) - (task_cost tsk - task_run_to_completion_threshold tsk))
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index db70e08a2..b79368c00 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -171,7 +171,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
(** The final search space for EDF is a set of offsets that are less than [L]
and where [task_rbf] or [bound_on_total_hep_workload] changes. *)
- Let is_in_search_space (A : duration) :=
+ Definition is_in_search_space (A : duration) :=
(A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
(** Let R be a value that upper-bounds the solution of each response-time recurrence,
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index c6cb73963..b0b3bd0d3 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -123,13 +123,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
(** ** Response-Time Bound *)
(** To reduce the time complexity of the analysis, recall the notion of search space. *)
-
- Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
- Let bound_on_total_hep_workload_changes_at :=
- bound_on_total_hep_workload_changes_at ts tsk.
-
- Let is_in_search_space (A : duration) :=
- (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
+ Let is_in_search_space := is_in_search_space ts tsk L.
(** Consider any value R, and assume that for any given arrival offset A in the search space,
there is a solution of the response-time bound recurrence which is bounded by R. *)
@@ -164,4 +158,4 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
}
Qed.
-End RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
\ No newline at end of file
+End RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index 85de469f6..4d5521e51 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -114,13 +114,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
(** ** Response-Time Bound *)
(** To reduce the time complexity of the analysis, recall the notion of search space. *)
-
- Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
- Let bound_on_total_hep_workload_changes_at :=
- bound_on_total_hep_workload_changes_at ts tsk.
-
- Let is_in_search_space A :=
- (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
+ Let is_in_search_space := is_in_search_space ts tsk L.
(** Consider any value R, and assume that for any given arrival offset A in the search space,
there is a solution of the response-time bound recurrence which is bounded by R. *)
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index faaac1592..4e706669e 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -105,14 +105,8 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
(** ** Response-Time Bound *)
- (** To reduce the time complexity of the analysis, recall the notion of search space. *)
-
- Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
- Let bound_on_total_hep_workload_changes_at :=
- bound_on_total_hep_workload_changes_at ts tsk.
-
- Let is_in_search_space A :=
- (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
+ (** To reduce the time complexity of the analysis, recall the notion of search space. *)
+ Let is_in_search_space := is_in_search_space ts tsk L.
(** Consider any value R, and assume that for any given arrival offset A in the search space,
there is a solution of the response-time bound recurrence which is bounded by R. *)
@@ -124,8 +118,10 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
A + F = task_rbf (A + ε) + bound_on_total_hep_workload A (A + F) /\
F <= R.
- (** Now, we can leverage the results for the abstract model with bounded non-preemptive segments
- to establish a response-time bound for the more concrete model of fully preemptive scheduling. *)
+ (** Now, we can leverage the results for the abstract model with
+ bounded non-preemptive segments to establish a response-time
+ bound for the more concrete model of fully preemptive
+ scheduling. *)
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index f0a67d2d0..dca7b119f 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -123,13 +123,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
(** ** Response-Time Bound *)
(** To reduce the time complexity of the analysis, recall the notion of search space. *)
-
- Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
- Let bound_on_total_hep_workload_changes_at :=
- bound_on_total_hep_workload_changes_at ts tsk.
-
- Let is_in_search_space A :=
- (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
+ Let is_in_search_space := is_in_search_space ts tsk L.
(** Consider any value R, and assume that for any given arrival offset A in the search space,
there is a solution of the response-time bound recurrence which is bounded by R. *)
@@ -180,4 +174,4 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
}
Qed.
-End RTAforFixedPreemptionPointsModelwithArrivalCurves.
\ No newline at end of file
+End RTAforFixedPreemptionPointsModelwithArrivalCurves.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 325b493d5..88fb239df 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -218,7 +218,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Hypothesis H_fixed_point : L = blocking_bound + total_hep_rbf L.
(** To reduce the time complexity of the analysis, recall the notion of search space. *)
- Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+ Let is_in_search_space := is_in_search_space tsk L.
(** Next, consider any value R, and assume that for any given arrival offset A from the search
space there is a solution of the response-time bound recurrence that is bounded by R. *)
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 5f9f41962..fa895bdf3 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -144,7 +144,7 @@ Section AbstractRTAforFPwithArrivalCurves.
(** To reduce the time complexity of the analysis, recall the notion of search space.
Intuitively, this corresponds to all "interesting" arrival offsets that the job under
analysis might have with regard to the beginning of its busy-window. *)
- Let is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
+ Definition is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
(** Let R be a value that upper-bounds the solution of each response-time recurrence,
i.e., for any relative arrival time A in the search space, there exists a corresponding
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index ca36e3af9..ae0faec39 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -126,7 +126,7 @@ Section RTAforFloatingModelwithArrivalCurves.
(** ** Response-Time Bound *)
(** To reduce the time complexity of the analysis, recall the notion of search space. *)
- Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+ Let is_in_search_space := is_in_search_space tsk L.
(** Next, consider any value R, and assume that for any given
arrival A from search space there is a solution of the
@@ -159,4 +159,4 @@ Section RTAforFloatingModelwithArrivalCurves.
by exists F; rewrite addn0; split.
Qed.
-End RTAforFloatingModelwithArrivalCurves.
\ No newline at end of file
+End RTAforFloatingModelwithArrivalCurves.
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index a3b95d652..dad64281f 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -118,7 +118,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
(** ** Response-Time Bound *)
(** To reduce the time complexity of the analysis, recall the notion of search space. *)
- Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+ Let is_in_search_space := is_in_search_space tsk L.
(** Next, consider any value R, and assume that for any given arrival A from search space
there is a solution of the response-time bound recurrence which is bounded by R. *)
@@ -156,4 +156,4 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
all: eauto 2 with basic_facts.
Qed.
-End RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
\ No newline at end of file
+End RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 8144eb552..ba0fed172 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -111,7 +111,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
(** ** Response-Time Bound *)
(** To reduce the time complexity of the analysis, recall the notion of search space. *)
- Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+ Let is_in_search_space := is_in_search_space tsk L.
(** Next, consider any value R, and assume that for any given
arrival A from search space there is a solution of the
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 37576d9c5..e41780125 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -126,8 +126,8 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
(** ** Response-Time Bound *)
(** To reduce the time complexity of the analysis, recall the notion of search space. *)
- Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
-
+ Let is_in_search_space := is_in_search_space tsk L.
+
(** Next, consider any value R, and assume that for any given arrival A from search space
there is a solution of the response-time bound recurrence which is bounded by R. *)
Variable R: nat.
--
GitLab