From cbd73a7ebf40fb2e984d24e260eea45ca3a39cce Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Fri, 12 Apr 2024 10:42:03 +0200
Subject: [PATCH] add corollary about only one job causing pi
---
analysis/facts/busy_interval/pi.v | 43 ++++++++++++++++++++++++++++++-
1 file changed, 42 insertions(+), 1 deletion(-)
diff --git a/analysis/facts/busy_interval/pi.v b/analysis/facts/busy_interval/pi.v
index 44b5e1abd..04c673d41 100644
--- a/analysis/facts/busy_interval/pi.v
+++ b/analysis/facts/busy_interval/pi.v
@@ -153,7 +153,7 @@ Section PriorityInversionIsBounded.
(** In this section, we prove that priority inversion only
occurs at the start of the busy window and occurs due to only
- one job. *)
+ one job. *)
Section SingleJob.
(** Suppose job [j] incurs priority inversion at a time [t_pi] in its busy window. *)
@@ -206,6 +206,47 @@ Section PriorityInversionIsBounded.
End SingleJob.
+ (** As a simple corollary to the lemmas proved in the previous
+ section, we show that for any two jobs [j1] and [j2] that cause
+ priority inversion to job [j], it is the case that [j1 = j2]. *)
+ Section SingleJobEq.
+
+ (** Consider a time instant [ts1] in <<[t1, t2)>> ... *)
+ Variable ts1 : instant.
+ Hypothesis H_ts1_in_busy_prefix : t1 <= ts1 < t2.
+
+ (** ... and a lower-priority (w.r.t. job [j]) job [j1] that is
+ scheduled at time [ts1]. *)
+ Variable j1 : Job.
+ Hypothesis H_j1_sched : scheduled_at sched j1 ts1.
+ Hypothesis H_j1_lower_prio : ~~ hep_job j1 j.
+
+ (** Similarly, consider a time instant [ts2] in <<[t1, t2)>> ... *)
+ Variable ts2 : instant.
+ Hypothesis H_ts2_in_busy_prefix : t1 <= ts2 < t2.
+
+ (** ... and a lower-priority job [j2] that is scheduled at time [ts2]. *)
+ Variable j2 : Job.
+ Hypothesis H_j2_sched : scheduled_at sched j2 ts2.
+ Hypothesis H_j2_lower_prio : ~~ hep_job j2 j.
+
+ (** Then, [j1] is equal to [j2]. *)
+ Corollary only_one_pi_job :
+ j1 = j2.
+ Proof.
+ have [NEQ|NEQ] := leqP ts1 ts2.
+ { apply: H_uni; first by apply H_j1_sched.
+ apply: pi_job_remains_scheduled; try apply H_j2_sched; try lia.
+ by erewrite priority_inversion_hep_job.
+ }
+ { apply: H_uni; last by apply H_j2_sched.
+ apply: pi_job_remains_scheduled; try apply H_j1_sched; try lia.
+ by erewrite priority_inversion_hep_job; try apply H_j1_sched.
+ }
+ Qed.
+
+ End SingleJobEq.
+
(** From the above lemmas, it follows that either job [j] incurs no priority
inversion at all or certainly at time [t1], i.e., the beginning of its
busy interval. *)
--
GitLab