From e1f5e262336f56fc0a22e2b16d8ee4ca150e94a0 Mon Sep 17 00:00:00 2001
From: mariamvardishvili <mariamvardishvili@gmail.com>
Date: Wed, 6 Oct 2021 18:14:24 +0400
Subject: [PATCH] improve comments in bounded PI arguments
---
results/edf/rta/bounded_pi.v | 14 +++++++-------
results/fixed_priority/rta/bounded_pi.v | 4 ++--
2 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 37cfb8f64..9f04bb62a 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -200,8 +200,8 @@ 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
+ (** 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.
@@ -382,11 +382,11 @@ Section AbstractRTAforEDFwithArrivalCurves.
by apply service_of_jobs_le_workload; eauto 2 with basic_facts.
Qed.
- (** Next, we reorder summation. So the total workload of jobs
- with higher-or-equal priority from other tasks is equal to
- the sum over all tasks [tsk_o] that are to equal to task
- [tsk] of workload of jobs with higher-or-equal priority
- task [tsk_o]. *)
+ (** Next, we prove that the total workload of jobs
+ with higher-or-equal priority from other tasks is bounded by
+ the sum over all tasks [tsk_o] that are not equal to task
+ [tsk] of workload of jobs with higher-or-equal priority from
+ task [tsk_o].*)
Lemma reorder_summation:
workload_of_jobs (EDF_not_from tsk) jobs
<= \sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (EDF_from tsk_o) jobs.
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 13d5c4670..402a95200 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -171,8 +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 (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
+ (** 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