From 3eb2a96bbd55ed6f6bb7949c8cbcba8a94cfd27d Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Mon, 19 Feb 2024 14:26:53 +0100
Subject: [PATCH] de-duplicate EDF hep-workload bound definition
---
.../definitions/workload/edf_athep_bound.v | 37 ++++
analysis/facts/workload/edf_athep_bound.v | 158 +++++++++++++++++
results/edf/rta/bounded_nps.v | 9 +-
results/edf/rta/bounded_pi.v | 159 ++++--------------
results/edf/rta/floating_nonpreemptive.v | 8 +-
results/edf/rta/fully_nonpreemptive.v | 8 +-
results/edf/rta/fully_preemptive.v | 8 +-
results/edf/rta/limited_preemptive.v | 8 +-
8 files changed, 237 insertions(+), 158 deletions(-)
create mode 100644 analysis/definitions/workload/edf_athep_bound.v
create mode 100644 analysis/facts/workload/edf_athep_bound.v
diff --git a/analysis/definitions/workload/edf_athep_bound.v b/analysis/definitions/workload/edf_athep_bound.v
new file mode 100644
index 000000000..f60441079
--- /dev/null
+++ b/analysis/definitions/workload/edf_athep_bound.v
@@ -0,0 +1,37 @@
+Require Export prosa.analysis.definitions.request_bound_function.
+
+(** * Bound on Higher-or-Equal Priority Workload under EDF Scheduling *)
+
+(** In this file, we define an upper bound on workload incurred by a
+ job from jobs with higher-or-equal priority that come from other
+ tasks under EDF scheduling. *)
+Section EDFWorkloadBound.
+
+ (** Consider any type of tasks, each characterized by a WCET
+ [task_cost], and an arrival curve [max_arrivals]. *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+ Context `{TaskDeadline Task}.
+ Context `{MaxArrivals Task}.
+
+ (** Consider an arbitrary task set [ts] ... *)
+ Variable ts : seq Task.
+
+ (** ... and a task [tsk]. *)
+ Variable tsk : Task.
+
+ (** For brevity, let's denote the relative deadline of a task as [D] ... *)
+ Let D tsk := task_deadline tsk.
+
+ (** ... and let's use the abbreviation [rbf] for the task
+ request-bound function. *)
+ Let rbf := task_request_bound_function.
+
+ (** Finally, we define an upper bound on workload received from jobs
+ with higher-than-or-equal priority that come from other
+ tasks. *)
+ Definition bound_on_athep_workload A Δ :=
+ \sum_(tsk_o <- ts | tsk_o != tsk)
+ rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
+
+End EDFWorkloadBound.
diff --git a/analysis/facts/workload/edf_athep_bound.v b/analysis/facts/workload/edf_athep_bound.v
new file mode 100644
index 000000000..1cdc19b5a
--- /dev/null
+++ b/analysis/facts/workload/edf_athep_bound.v
@@ -0,0 +1,158 @@
+Require Export prosa.model.priority.edf.
+Require Export prosa.model.task.absolute_deadline.
+Require Export prosa.analysis.definitions.workload.bounded.
+Require Export prosa.analysis.facts.model.workload.
+Require Export prosa.analysis.definitions.workload.edf_athep_bound.
+
+
+(** * Bound on Higher-or-Equal Priority Workload under EDF Scheduling is Valid *)
+
+(** In this file, we prove that the upper bound on interference
+ incurred by a job from jobs with higher-or-equal priority that
+ come from other tasks under EDF scheduling (defined in
+ [prosa.analysis.definitions.workload.edf_athep_bound]) is
+ valid. *)
+Section ATHEPWorkloadBoundIsValidForEDF.
+
+ (** Consider any type of tasks, each characterized by a WCET
+ [task_cost], a relative deadline [task_deadline], and an arrival
+ curve [max_arrivals], ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+ Context `{TaskDeadline Task}.
+ Context `{MaxArrivals 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 `{JobArrival Job}.
+ Context `{JobCost Job}.
+
+ (** Consider any kind of processor model. *)
+ Context `{PState : ProcessorState Job}.
+
+ (** For brevity, let's denote the relative deadline of a task as [D]. *)
+ Let D tsk := task_deadline tsk.
+
+ (** Consider any valid arrival sequence [arr_seq] ... *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+ (** ... with valid job costs. *)
+ Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+ (** We consider an arbitrary task set [ts] ... *)
+ Variable ts : seq Task.
+
+ (** ... and assume that all jobs stem from tasks in this task set. *)
+ Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+ (** We assume that [max_arrivals] is a family of valid arrival
+ curves that constrains the arrival sequence [arr_seq], i.e., for
+ any task [tsk] in [ts], [max_arrival tsk] is an arrival bound of
+ [tsk]. *)
+ Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+ (** Let [tsk] be any task to be analyzed. *)
+ Variable tsk : Task.
+
+ (** Consider any schedule. *)
+ Variable sched : schedule PState.
+
+ (** Before we prove the main result, we establish some auxiliary lemmas. *)
+ Section HepWorkloadBound.
+
+ (** Consider an arbitrary job [j] of [tsk]. *)
+ Variable j : Job.
+ Hypothesis H_j_arrives : arrives_in arr_seq j.
+ Hypothesis H_job_of_tsk : job_of_task tsk j.
+ Hypothesis H_job_cost_positive: job_cost_positive j.
+
+ (** Consider the busy interval <<[t1, t2)>> of job [j]. *)
+ Variable t1 t2 : duration.
+ Hypothesis H_busy_interval : busy_interval arr_seq sched j t1 t2.
+
+ (** Let's define [A] as a relative arrival time of job [j] (with
+ respect to time [t1]). *)
+ Let A := job_arrival j - t1.
+
+ (** Consider an arbitrary shift [Δ] inside the busy interval ... *)
+ Variable Δ : duration.
+ Hypothesis H_Δ_in_busy : t1 + Δ < t2.
+
+ (** ... and the set of all arrivals between [t1] and [t1 + Δ]. *)
+ Let jobs := arrivals_between arr_seq t1 (t1 + Δ).
+
+ (** We define a predicate [EDF_from tsk]. Predicate [EDF_from tsk]
+ holds true for any job [jo] of task [tsk] such that
+ [job_deadline jo <= job_deadline j]. *)
+ Let EDF_from (tsk : Task) (jo : Job) := EDF Job jo j && (job_task jo == tsk).
+
+ (** Now, consider the case where [A + ε + D tsk - D tsk_o ≤ Δ]. *)
+ Section ShortenRange.
+
+ (** Consider an arbitrary task [tsk_o ≠tsk] from [ts]. *)
+ Variable tsk_o : Task.
+ Hypothesis H_tsko_in_ts: tsk_o \in ts.
+ Hypothesis H_neq: tsk_o != tsk.
+
+ (** And assume that [A + ε + D tsk - D tsk_o ≤ Δ]. *)
+ Hypothesis H_Δ_ge : A + ε + D tsk - D tsk_o <= Δ.
+
+ (** Then we prove that the total workload of jobs with
+ higher-or-equal priority from task [tsk_o] over the interval
+ [[t1, t1 + Δ]] is bounded by workload over the interval
+ [[t1, t1 + A + ε + D tsk - D tsk_o]]. The intuition behind
+ this inequality is that jobs that arrive after time instant
+ [t1 + A + ε + D tsk - D tsk_o] have lower priority than job
+ [j] due to the term [D tsk - D tsk_o]. *)
+ Lemma total_workload_shorten_range :
+ workload_of_jobs (EDF_from tsk_o) (arrivals_between arr_seq t1 (t1 + Δ))
+ <= workload_of_jobs (EDF_from tsk_o) (arrivals_between arr_seq t1 (t1 + (A + ε + D tsk - D tsk_o))).
+ Proof.
+ have BOUNDED: t1 + (A + ε + D tsk - D tsk_o) <= t1 + Δ by lia.
+ rewrite (workload_of_jobs_nil_tail _ _ BOUNDED) // => j' IN'.
+ rewrite /EDF_from => ARR'.
+ case: (eqVneq (job_task j') tsk_o) => TSK';
+ last by rewrite andbF.
+ rewrite andbT; apply: contraT => /negPn.
+ rewrite /EDF/edf.EDF/job_deadline/job_deadline_from_task_deadline.
+ move: H_job_of_tsk; rewrite TSK' /job_of_task => /eqP -> HEP.
+ have LATEST: job_arrival j' <= t1 + A + D tsk - D tsk_o by rewrite /D/A; lia.
+ have EARLIEST: t1 <= job_arrival j' by apply: job_arrival_between_ge.
+ by case: (leqP (A + 1 + D tsk) (D tsk_o)); [rewrite /D/A|]; lia.
+ Qed.
+
+ End ShortenRange.
+
+ (** Using the above lemma, we prove that the total workload of the
+ tasks is at most [bound_on_total_hep_workload(A, Δ)]. *)
+ Corollary sum_of_workloads_is_at_most_bound_on_total_hep_workload :
+ \sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (EDF_from tsk_o) jobs
+ <= bound_on_athep_workload ts tsk A Δ.
+ Proof.
+ apply leq_sum_seq => tsko INtsko NEQT; fold (D tsk) (D tsko).
+ edestruct (leqP Δ (A + ε + D tsk - D tsko)) as [NEQ|NEQ]; [ | apply ltnW in NEQ].
+ - exact: (workload_le_rbf' arr_seq tsko).
+ - eapply leq_trans; first by eapply total_workload_shorten_range; eauto 2.
+ exact: workload_le_rbf'.
+ Qed.
+
+ End HepWorkloadBound.
+
+ (** The validity of [bound_on_athep_workload] then easily follows
+ from lemma [sum_of_workloads_is_at_most_bound_on_total_hep_workload]. *)
+ Corollary bound_on_athep_workload_is_valid :
+ athep_workload_is_bounded arr_seq sched tsk (bound_on_athep_workload ts tsk).
+ Proof.
+ move=> j t1 Δ POS TSK QT.
+ eapply leq_trans.
+ + eapply reorder_summation => j' IN _.
+ by apply H_all_jobs_from_taskset; eapply in_arrivals_implies_arrived; exact IN.
+ + move : TSK => /eqP TSK; rewrite TSK.
+ by apply: sum_of_workloads_is_at_most_bound_on_total_hep_workload => //; apply /eqP.
+ Qed.
+
+End ATHEPWorkloadBoundIsValidForEDF.
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index 1c2f83691..ee4a228ad 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -6,6 +6,7 @@ Require Export prosa.results.edf.rta.bounded_pi.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.analysis.definitions.busy_interval.classical.
Require Export prosa.analysis.facts.blocking_bound.edf.
+Require Export prosa.analysis.facts.workload.edf_athep_bound.
(** * RTA for EDF with Bounded Non-Preemptive Segments *)
@@ -115,12 +116,6 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
function of all tasks (total request bound function). *)
Let total_rbf := total_request_bound_function ts.
- (** Next, we define an upper bound on interfering workload received from jobs
- of other tasks with higher-than-or-equal priority. *)
- Let bound_on_total_hep_workload A Δ :=
- \sum_(tsk_o <- ts | tsk_o != tsk)
- rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
-
(** Let's define some local names for clarity. *)
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
@@ -219,7 +214,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
exists (F : duration),
A + F >= blocking_bound ts tsk A
+ (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
- + bound_on_total_hep_workload A (A + F) /\
+ + bound_on_athep_workload ts tsk A (A + F) /\
R >= F + (task_cost tsk - task_rtct tsk).
(** Then, using the results for the general RTA for EDF-schedulers, we establish a
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index b3feda83d..b6b5f4796 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -8,6 +8,7 @@ Require Import prosa.analysis.facts.busy_interval.carry_in.
Require Import prosa.analysis.facts.readiness.basic.
Require Export prosa.analysis.abstract.ideal.abstract_seq_rta.
Require Export prosa.analysis.facts.model.task_cost.
+Require Export prosa.analysis.facts.workload.edf_athep_bound.
(** * Abstract RTA for EDF-schedulers with Bounded Priority Inversion *)
(** In this module we instantiate the Abstract Response-Time analysis
@@ -35,7 +36,6 @@ Section AbstractRTAforEDFwithArrivalCurves.
Context `{TaskRunToCompletionThreshold Task}.
Context `{TaskMaxNonpreemptiveSegment Task}.
-
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
@@ -159,12 +159,6 @@ Section AbstractRTAforEDFwithArrivalCurves.
Hypothesis H_L_positive : L > 0.
Hypothesis H_fixed_point : L = total_rbf L.
- (** Next, we define an upper bound on interfering workload received
- from jobs of other tasks with higher-than-or-equal priority. *)
- Let bound_on_total_hep_workload (A Δ : duration) :=
- \sum_(tsk_o <- ts | tsk_o != tsk)
- rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
-
(** To reduce the time complexity of the analysis, we introduce the
notion of search space for EDF. Intuitively, this corresponds to
all "interesting" arrival offsets that the job under analysis
@@ -211,134 +205,52 @@ Section AbstractRTAforEDFwithArrivalCurves.
exists (F : duration),
A + F >= priority_inversion_bound A
+ (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
- + bound_on_total_hep_workload A (A + F) /\
+ + bound_on_athep_workload ts tsk A (A + F) /\
R >= F + (task_cost tsk - task_rtct tsk).
-
+
(** Finally, we define the interference bound function
([task_IBF]). [task_IBF] bounds the interference if tasks are
sequential. Since tasks are sequential, we exclude interference
from other jobs of the same task. For EDF, we define [task_IBF]
as the sum of the priority interference bound and the
higher-or-equal-priority workload. *)
- Let task_IBF (A R : duration) := priority_inversion_bound A + bound_on_total_hep_workload A R.
+ Let task_IBF (A R : duration) :=
+ priority_inversion_bound A + bound_on_athep_workload ts tsk A R.
(** ** Filling Out Hypothesis Of Abstract RTA Theorem *)
(** In this section we prove that all hypotheses necessary to use
the abstract theorem are satisfied. *)
Section FillingOutHypothesesOfAbstractRTATheorem.
- (** First, we prove that [task_IBF] is indeed an interference bound. *)
- Section TaskInterferenceIsBoundedBytask_IBF.
-
- Section HepWorkloadBound.
-
- (** Consider an arbitrary job [j] of [tsk]. *)
- Variable j : Job.
- Hypothesis H_j_arrives : arrives_in arr_seq j.
- Hypothesis H_job_of_tsk : job_of_task tsk j.
- Hypothesis H_job_cost_positive: job_cost_positive j.
-
- (** Consider any busy interval <<[t1, t2)>> of job [j]. *)
- Variable t1 t2 : duration.
- Hypothesis H_busy_interval : definitions.busy_interval sched j t1 t2.
-
- (** Let's define A as a relative arrival time of job j (with respect to time t1). *)
- Let A := job_arrival j - t1.
-
- (** Consider an arbitrary shift Δ inside the busy interval ... *)
- Variable Δ : duration.
- Hypothesis H_Δ_in_busy : t1 + Δ < t2.
-
- (** ... and the set of all arrivals between [t1] and [t1 + Δ]. *)
- Let jobs := arrivals_between arr_seq t1 (t1 + Δ).
-
- (** We define a predicate [EDF_from tsk]. Predicate [EDF_from
- tsk] holds true for any job [jo] of task [tsk] such that
- [job_deadline jo <= job_deadline j]. *)
- Let EDF_from (tsk : Task) := fun (jo : Job) => EDF jo j && (job_task jo == tsk).
-
- (** Now, consider the case where [A + ε + D tsk - D tsk_o ≤ Δ]. *)
- Section ShortenRange.
-
- (** Consider an arbitrary task [tsk_o ≠tsk] from [ts]. *)
- Variable tsk_o : Task.
- Hypothesis H_tsko_in_ts: tsk_o \in ts.
- Hypothesis H_neq: tsk_o != tsk.
-
- (** And assume that [A + ε + D tsk - D tsk_o ≤ Δ]. *)
- Hypothesis H_Δ_ge : A + ε + D tsk - D tsk_o <= Δ.
-
- (** Then we prove that the total workload of jobs with
- higher-or-equal priority from task [tsk_o] over time
- interval [t1, t1 + Δ] is bounded by workload over time
- interval [t1, t1 + A + ε + D tsk - D tsk_o]. The
- intuition behind this inequality is that jobs which
- arrive after time instant [t1 + A + ε + D tsk - D tsk_o]
- have lower priority than job [j] due to the term [D tsk
- - D tsk_o]. *)
- Lemma total_workload_shorten_range:
- workload_of_jobs (EDF_from tsk_o) (arrivals_between arr_seq t1 (t1 + Δ))
- <= workload_of_jobs (EDF_from tsk_o) (arrivals_between arr_seq t1 (t1 + (A + ε + D tsk - D tsk_o))).
- Proof.
- have BOUNDED: t1 + (A + ε + D tsk - D tsk_o) <= t1 + Δ by lia.
- rewrite (workload_of_jobs_nil_tail _ _ BOUNDED) // => j' IN'.
- rewrite /EDF_from => ARR'.
- case: (eqVneq (job_task j') tsk_o) => TSK';
- last by rewrite andbF.
- rewrite andbT; apply: contraT => /negPn.
- rewrite /EDF/edf.EDF/job_deadline/job_deadline_from_task_deadline.
- move: H_job_of_tsk; rewrite TSK' /job_of_task => /eqP -> HEP.
- have LATEST: job_arrival j' <= t1 + A + D tsk - D tsk_o by rewrite /D/A; lia.
- have EARLIEST: t1 <= job_arrival j' by apply: job_arrival_between_ge.
- by case: (leqP (A + 1 + D tsk) (D tsk_o)); [rewrite /D/A|]; lia.
- Qed.
-
- End ShortenRange.
-
- (** Using the above lemma, we prove that the total workload of the
- tasks is at most [bound_on_total_hep_workload(A, Δ)]. *)
- Corollary sum_of_workloads_is_at_most_bound_on_total_hep_workload :
- \sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (EDF_from tsk_o) jobs
- <= bound_on_total_hep_workload A Δ.
- Proof.
- apply leq_sum_seq => tsko INtsko NEQT.
- edestruct (leqP Δ (A + ε + D tsk - D tsko)) as [NEQ|NEQ]; [ | apply ltnW in NEQ].
- - exact: (workload_le_rbf' arr_seq tsko).
- - eapply leq_trans; first by eapply total_workload_shorten_range; eauto 2.
- exact: workload_le_rbf'.
- Qed.
-
- End HepWorkloadBound.
-
- (** The above lemma, in turn, implies that [task_IBF] is a valid
- bound on the cumulative task interference. *)
- Corollary instantiated_task_interference_is_bounded :
- task_interference_is_bounded_by arr_seq sched tsk task_IBF.
- Proof.
- move => t1 t2 R2 j ARR TSK BUSY LT NCOMPL A OFF.
- move: (OFF _ _ BUSY) => EQA; subst A.
- move: (posnP (@job_cost _ Cost j)) => [ZERO|POS].
- - exfalso; move: NCOMPL => /negP COMPL; apply: COMPL.
- by rewrite /completed_by /completed_by ZERO.
- - rewrite -/(cumul_task_interference _ _ _ _ _).
- 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.
- eapply leq_trans.
- + eapply reorder_summation.
- move => j' IN _.
- apply H_all_jobs_from_taskset. eapply in_arrivals_implies_arrived. exact IN.
- + move : TSK => /eqP TSK.
- rewrite TSK.
- apply: sum_of_workloads_is_at_most_bound_on_total_hep_workload => //.
- by apply /eqP.
- Qed.
-
- End TaskInterferenceIsBoundedBytask_IBF.
-
- (** Finally, we show that there exists a solution for the response-time recurrence. *)
+ (** First, we prove that [task_IBF] is indeed a valid bound on the
+ cumulative task interference. *)
+ Lemma instantiated_task_interference_is_bounded :
+ task_interference_is_bounded_by arr_seq sched tsk task_IBF.
+ Proof.
+ move => t1 t2 R2 j ARR TSK BUSY LT NCOMPL A OFF.
+ move: (OFF _ _ BUSY) => EQA; subst A.
+ move: (posnP (@job_cost _ Cost j)) => [ZERO|POS].
+ - exfalso; move: NCOMPL => /negP COMPL; apply: COMPL.
+ by rewrite /completed_by /completed_by ZERO.
+ - rewrite -/(cumul_task_interference _ _ _ _ _).
+ 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.
+ eapply leq_trans.
+ + eapply reorder_summation.
+ move => j' IN _.
+ apply H_all_jobs_from_taskset.
+ eapply in_arrivals_implies_arrived.
+ exact IN.
+ + move : TSK => /eqP TSK.
+ rewrite TSK.
+ apply: sum_of_workloads_is_at_most_bound_on_total_hep_workload => //.
+ by apply /eqP.
+ Qed.
+
+ (** Finally, we show that there exists a solution for the response-time recurrence. *)
Section SolutionOfResponseTimeReccurenceExists.
(** To rule out pathological cases with the concrete search
@@ -373,9 +285,10 @@ Section AbstractRTAforEDFwithArrivalCurves.
exfalso; apply INSP2.
rewrite /total_interference_bound subnK // RBF.
apply /eqP; rewrite eqn_add2l /task_IBF PI eqn_add2l.
- rewrite /bound_on_total_hep_workload subnK //.
+ rewrite /bound_on_athep_workload subnK //.
apply /eqP; rewrite big_seq_cond [RHS]big_seq_cond.
apply eq_big => // tsk_i /andP [TS OTHER].
+ fold (D tsk) (D tsk_i).
move: WL; rewrite /bound_on_total_hep_workload_changes_at => /hasPn WL.
move: {WL} (WL tsk_i TS) => /nandP [/negPn/eqP EQ|/negPn/eqP WL];
first by move: OTHER; rewrite EQ => /neqP.
@@ -384,7 +297,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
{ rewrite ifF //.
by move: gtn_x; rewrite leq_eqVlt => /orP [/eqP EQ|LEQ]; lia. }
{ case: (A + D tsk - D tsk_i < x).
- - by rewrite WL.
+ - by rewrite -/(rbf _) WL.
- by rewrite eq_x. } }
Qed.
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index fd4ae79c9..811a56243 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -93,12 +93,6 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
function of all tasks (total request bound function). *)
Let total_rbf := total_request_bound_function ts.
- (** Next, we define an upper bound on interfering workload received from jobs
- of other tasks with higher-than-or-equal priority. *)
- Let bound_on_total_hep_workload A Δ :=
- \sum_(tsk_o <- ts | tsk_o != tsk)
- rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).
-
(** Let L be any positive fixed point of the busy interval recurrence. *)
Variable L : duration.
Hypothesis H_L_positive : L > 0.
@@ -117,7 +111,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
forall (A : duration),
is_in_search_space A ->
exists (F : duration),
- A + F >= blocking_bound ts tsk A + task_rbf (A + ε) + bound_on_total_hep_workload A (A + F) /\
+ A + F >= blocking_bound ts tsk A + task_rbf (A + ε) + bound_on_athep_workload ts tsk A (A + F) /\
R >= F.
(** Now, we can leverage the results for the abstract model with
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index b8fecdff0..f4a06399c 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -91,12 +91,6 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
&& (task_deadline tsk_o > task_deadline tsk + A))
(task_cost tsk_o - ε).
- (** Next, we define an upper bound on interfering workload received from jobs
- of other tasks with higher-than-or-equal priority. *)
- Let bound_on_total_hep_workload A Δ :=
- \sum_(tsk_o <- ts | tsk_o != tsk)
- rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).
-
(** Let L be any positive fixed point of the busy interval recurrence. *)
Variable L : duration.
Hypothesis H_L_positive : L > 0.
@@ -116,7 +110,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
is_in_search_space A ->
exists F,
A + F >= blocking_bound A + (task_rbf (A + ε) - (task_cost tsk - ε))
- + bound_on_total_hep_workload A (A + F) /\
+ + bound_on_athep_workload ts tsk A (A + F) /\
R >= F + (task_cost tsk - ε).
(** Now, we can leverage the results for the abstract model with bounded nonpreemptive segments
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index 91dd7788c..eb28c3bfe 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -90,12 +90,6 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
Hence, the blocking bound is always 0 for any [A]. *)
Let blocking_bound (A : duration) := 0.
- (** Next, we define an upper bound on interfering workload received from jobs
- of other tasks with higher-than-or-equal priority. *)
- Let bound_on_total_hep_workload A Δ :=
- \sum_(tsk_o <- ts | tsk_o != tsk)
- rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).
-
(** Let L be any positive fixed point of the busy interval recurrence. *)
Variable L : duration.
Hypothesis H_L_positive : L > 0.
@@ -114,7 +108,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
forall (A : duration),
is_in_search_space A ->
exists (F : duration),
- A + F >= task_rbf (A + ε) + bound_on_total_hep_workload A (A + F) /\
+ A + F >= task_rbf (A + ε) + bound_on_athep_workload ts tsk A (A + F) /\
R >= F.
(** Now, we can leverage the results for the abstract model with
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index 26819293c..19c06d9a8 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -94,12 +94,6 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
function of all tasks (total request bound function). *)
Let total_rbf := total_request_bound_function ts.
- (** Next, we define an upper bound on interfering workload received from jobs
- of other tasks with higher-than-or-equal priority. *)
- Let bound_on_total_hep_workload A Δ :=
- \sum_(tsk_o <- ts | tsk_o != tsk)
- rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).
-
(** Let L be any positive fixed point of the busy interval recurrence. *)
Variable L : duration.
Hypothesis H_L_positive : L > 0.
@@ -120,7 +114,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
exists (F : duration),
A + F >= blocking_bound ts tsk A
+ (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε))
- + bound_on_total_hep_workload A (A + F) /\
+ + bound_on_athep_workload ts tsk A (A + F) /\
R >= F + (task_last_nonpr_segment tsk - ε).
(** Now, we can leverage the results for the abstract model with bounded non-preemptive segments
--
GitLab