diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 43cd7c314575d4c198cd36540635f9cebcca7506..c20649a01ec1a7157ef33bd4e155c00970b6854d 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -186,7 +186,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
R >= F + (task_cost tsk - task_rtct tsk).
(** To use the theorem uniprocessor_response_time_bound_seq from the Abstract RTA module,
- we need to specify functions of interference, interfering workload and IBF. *)
+ we need to specify functions of interference, interfering workload and [IBF_other]. *)
(** Instantiation of Interference *)
(** We say that job j incurs interference at time t iff it cannot execute due to
@@ -200,9 +200,10 @@ Section AbstractRTAforEDFwithArrivalCurves.
Let interfering_workload (j : Job) (t : instant) :=
ideal_jlfp_rta.interfering_workload arr_seq sched j t.
- (** Finally, we define the interference bound function ([IBF_other]). [IBF_other] 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 [IBF_other] as the sum of the priority
- interference bound and the higher-or-equal-priority workload. *)
+ (** Finally, we define the interference bound function ([IBF_other]). [IBF_other] 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 [IBF_other] as
+ the sum of the priority interference bound and the higher-or-equal-priority workload. *)
Let IBF_other (A R : duration) := priority_inversion_bound + bound_on_total_hep_workload A R.
(** ** Filling Out Hypothesis Of Abstract RTA Theorem *)
@@ -292,14 +293,14 @@ Section AbstractRTAforEDFwithArrivalCurves.
by eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2 with basic_facts.
Qed.
- (** Next, we prove that IBF is indeed an interference bound. *)
- Section TaskInterferenceIsBoundedByIBF.
+ (** Next, we prove that [IBF_other] is indeed an interference bound. *)
+ Section TaskInterferenceIsBoundedByIBF_other.
- (** We show that task_interference_is_bounded_by is bounded by IBF by
+ (** We show that task_interference_is_bounded_by is bounded by [IBF_other] by
constructing a sequence of inequalities. *)
Section Inequalities.
- (* Consider an arbitrary job j of [tsk]. *)
+ (** 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_task j = tsk.
@@ -330,7 +331,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
such that [job_deadline jo <= job_deadline j] and [job_task jo ≠tsk]. *)
Let EDF_not_from (tsk : Task) := fun (jo : Job) => EDF jo j && (job_task jo != tsk).
- (** Recall that [IBF(A, R) := priority_inversion_bound +
+ (** Recall that [IBF_other(A, R) := priority_inversion_bound +
bound_on_total_hep_workload(A, R)]. The fact that
[priority_inversion_bound] bounds cumulative priority inversion
follows from assumption [H_priority_inversion_is_bounded]. *)
@@ -563,9 +564,9 @@ Section AbstractRTAforEDFwithArrivalCurves.
However, in this module we analyze only one task -- [tsk],
therefore it is “hard-coded†inside the interference bound
- function IBF. Therefore, in order for the IBF signature to
+ function [IBF_other]. Therefore, in order for the [IBF_other] signature to
match the required signature in module abstract_seq_RTA, we
- wrap the IBF function in a function that accepts, but simply
+ wrap the [IBF_other] function in a function that accepts, but simply
ignores the task. *)
Corollary instantiated_task_interference_is_bounded:
task_interference_is_bounded_by
@@ -590,7 +591,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
by done.
Qed.
- End TaskInterferenceIsBoundedByIBF.
+ End TaskInterferenceIsBoundedByIBF_other.
(** Finally, we show that there exists a solution for the response-time recurrence. *)
Section SolutionOfResponseTimeReccurenceExists.
@@ -603,7 +604,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
(** Given any job j of task [tsk] that arrives exactly A units after the beginning of
the busy interval, the bound of the total interference incurred by j within an
- interval of length Δ is equal to [task_rbf (A + ε) - task_cost tsk + IBF(A, Δ)]. *)
+ interval of length Δ is equal to [task_rbf (A + ε) - task_cost tsk + IBF_other(A, Δ)]. *)
Let total_interference_bound tsk (A Δ : duration) :=
task_rbf (A + ε) - task_cost tsk + IBF_other A Δ.
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 3099f1223b171b2c8157651b5da6bace22b7211c..1e79c835fc50ad9b4dd73354db31e1a9a2bfa523 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -250,7 +250,7 @@ Section AbstractRTAforFPwithArrivalCurves.
by eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2 with basic_facts.
Qed.
- (** Next, we prove that IBF is indeed an interference bound.
+ (** Next, we prove that [IBF_other] is indeed an interference bound.
Recall that in module abstract_seq_RTA hypothesis task_interference_is_bounded_by expects
to receive a function that maps some task t, the relative arrival time of a job j of task t,
@@ -258,10 +258,10 @@ Section AbstractRTAforFPwithArrivalCurves.
files limited.abstract_RTA.definitions and limited.abstract_RTA.abstract_seq_rta).
However, in this module we analyze only one task -- [tsk], therefore it is “hard-codedâ€
- inside the interference bound function IBF. Moreover, in case of a model with fixed
+ inside the interference bound function [IBF_other]. Moreover, in case of a model with fixed
priorities, interference that some job j incurs from higher-or-equal priority jobs does not
- depend on the relative arrival time of job j. Therefore, in order for the IBF signature to
- match the required signature in module abstract_seq_RTA, we wrap the IBF function in a
+ depend on the relative arrival time of job j. Therefore, in order for the [IBF_other] signature to
+ match the required signature in module abstract_seq_RTA, we wrap the [IBF_other] function in a
function that accepts, but simply ignores, the task and the relative arrival time. *)
Lemma instantiated_task_interference_is_bounded:
task_interference_is_bounded_by
@@ -310,7 +310,7 @@ Section AbstractRTAforFPwithArrivalCurves.
(** Given any job j of task [tsk] that arrives exactly A units after the beginning of
the busy interval, the bound of the total interference incurred by j within an
- interval of length Δ is equal to [task_rbf (A + ε) - task_cost tsk + IBF Δ]. *)
+ interval of length Δ is equal to [task_rbf (A + ε) - task_cost tsk + IBF_other Δ]. *)
Let total_interference_bound tsk A Δ :=
task_rbf (A + ε) - task_cost tsk + IBF_other Δ.