From 109324ac399ee33ebb19bb531f778bd728f6be2a Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Fri, 11 Sep 2020 18:56:26 +0200
Subject: [PATCH] generalize definition of busy interval
The definition of busy interval can be generalized
to an arbitrary processor state model without
affecting other parts of the project.
---
analysis/definitions/busy_interval.v | 12 ++++++++----
1 file changed, 8 insertions(+), 4 deletions(-)
diff --git a/analysis/definitions/busy_interval.v b/analysis/definitions/busy_interval.v
index 137ac75a4..8e1a8db9e 100644
--- a/analysis/definitions/busy_interval.v
+++ b/analysis/definitions/busy_interval.v
@@ -13,12 +13,16 @@ Section BusyIntervalJLFP.
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (** Consider any arrival sequence with consistent arrivals. *)
+ (** Consider any kind of processor state model. *)
+ Context {PState : Type}.
+ Context `{ProcessorState Job PState}.
+
+ (** Consider any arrival sequence with consistent arrivals ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
- (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
- Variable sched : schedule (ideal.processor_state Job).
+ (** ... and a schedule of this arrival sequence. *)
+ Variable sched : schedule PState.
(** Assume a given JLFP policy. *)
Context `{JLFP_policy Job}.
@@ -89,4 +93,4 @@ Section BusyIntervalJLFP.
End DecidableQuietTime.
-End BusyIntervalJLFP.
\ No newline at end of file
+End BusyIntervalJLFP.
--
GitLab