From 44f3b130deadad6970b97c85bfef2a527e5e2e22 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Mon, 8 Apr 2024 12:06:15 +0200
Subject: [PATCH] prove that FIFO has no service inversion
---
analysis/facts/priority/fifo.v | 10 ++++++++++
1 file changed, 10 insertions(+)
diff --git a/analysis/facts/priority/fifo.v b/analysis/facts/priority/fifo.v
index 54a2ecde6..9a5f23061 100644
--- a/analysis/facts/priority/fifo.v
+++ b/analysis/facts/priority/fifo.v
@@ -8,6 +8,7 @@ Require Export prosa.analysis.facts.readiness.basic.
Require Export prosa.analysis.facts.busy_interval.all.
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
Require Export prosa.analysis.facts.priority.inversion.
+Require Export prosa.analysis.facts.busy_interval.service_inversion.
(** We first make some trivial observations about the FIFO priority policy to
avoid having to re-reason these steps repeatedly in the subsequent
@@ -165,6 +166,15 @@ Section BasicLemmas.
by apply: leq_trans. }
Qed.
+ (** As a corollary, FIFO implies the absence of service inversion. *)
+ Corollary FIFO_implies_no_service_inversion :
+ service_inversion_is_bounded_by arr_seq sched tsk (constant 0).
+ Proof.
+ move=> j ARR TSK POS t1 t2 PREF.
+ rewrite (leqRW (cumul_service_inv_le_cumul_priority_inv _ _ _ _ _ _ _ _ _ _)) //=.
+ by apply FIFO_implies_no_pi.
+ Qed.
+
End PriorityInversionBounded.
--
GitLab