Commit fedef925 authored by Sergey Bozhko's avatar Sergey Bozhko

Delete duplications of search space

parent aae570d0
Pipeline #25832 passed with stages
in 24 minutes and 52 seconds
......@@ -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))
......
......@@ -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,
......
......@@ -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.
......@@ -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. *)
......
......@@ -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.
......
......@@ -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.
......@@ -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. *)
......
......@@ -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
......
......@@ -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.
......@@ -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.
......@@ -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
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment