From 8c2409148a7aa5ac51d79e705deb51c042c2ef56 Mon Sep 17 00:00:00 2001
From: kimaya <f20171026@goa.bits-pilani.ac.in>
Date: Thu, 7 Oct 2021 15:27:18 +0200
Subject: [PATCH] properly describe [IBF_other]
---
results/edf/rta/bounded_pi.v | 5 +++--
results/fixed_priority/rta/bounded_pi.v | 3 ++-
2 files changed, 5 insertions(+), 3 deletions(-)
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 0ef944e27..37cfb8f64 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -200,8 +200,9 @@ 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 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 *)
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index f336a702a..13d5c4670 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -171,7 +171,8 @@ Section AbstractRTAforFPwithArrivalCurves.
Let interfering_workload (j : Job) (t : instant) :=
ideal_jlfp_rta.interfering_workload arr_seq sched j t.
- (** Finally, we define the interference bound function as the sum of the priority
+ (** 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 FP, we define IBF_other as the sum of the priority
interference bound and the higher-or-equal-priority workload. *)
Let IBF_other (R : duration) := priority_inversion_bound + total_ohep_rbf R.
--
GitLab