diff --git a/analysis/definitions/busy_interval.v b/analysis/definitions/busy_interval.v
index 8e1a8db9e97be924ceb21becf47f0c2e20d88697..16e2e45896cf0a2e6b8d4130321bf23a11dd9f82 100644
--- a/analysis/definitions/busy_interval.v
+++ b/analysis/definitions/busy_interval.v
@@ -1,9 +1,6 @@
Require Export prosa.model.priority.classes.
Require Export prosa.analysis.facts.behavior.completion.
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require Import prosa.model.processor.ideal.
-
(** * Busy Interval for JLFP-models *)
(** In this file we define the notion of busy intervals for uniprocessor for JLFP schedulers. *)
Section BusyIntervalJLFP.
@@ -34,8 +31,8 @@ Section BusyIntervalJLFP.
Variable j : Job.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
- (** We say that t is a quiet time for j iff every higher-priority job from
- the arrival sequence that arrived before t has completed by that time. *)
+ (** We say that [t] is a quiet time for [j] iff every higher-priority job from
+ the arrival sequence that arrived before [t] has completed by that time. *)
Definition quiet_time (t : instant) :=
forall (j_hp : Job),
arrives_in arr_seq j_hp ->
@@ -47,7 +44,7 @@ Section BusyIntervalJLFP.
<<[t1, t_busy)>> is a (potentially unbounded) busy-interval prefix
iff the interval starts with a quiet time where a higher or equal
priority job is released and remains non-quiet. We also require
- job j to be released in the interval. *)
+ job [j] to be released in the interval. *)
Definition busy_interval_prefix (t1 t_busy : instant) :=
t1 < t_busy /\
quiet_time t1 /\
@@ -55,7 +52,7 @@ Section BusyIntervalJLFP.
t1 <= job_arrival j < t_busy.
(** Next, we say that an interval <<[t1, t2)>> is a busy interval iff
- [t1, t2) is a busy-interval prefix and t2 is a quiet time. *)
+ <<[t1, t2)>> is a busy-interval prefix and [t2] is a quiet time. *)
Definition busy_interval (t1 t2 : instant) :=
busy_interval_prefix t1 t2 /\
quiet_time t2.
@@ -66,8 +63,8 @@ Section BusyIntervalJLFP.
version of the notion of quiet time. *)
Section DecidableQuietTime.
- (** We say that t is a quiet time for j iff every higher-priority job from
- the arrival sequence that arrived before t has completed by that time. *)
+ (** We say that t is a quiet time for [j] iff every higher-priority job from
+ the arrival sequence that arrived before [t] has completed by that time. *)
Definition quiet_time_dec (j : Job) (t : instant) :=
all
(fun j_hp => hep_job j_hp j ==> (completed_by sched j_hp t))
diff --git a/analysis/definitions/carry_in.v b/analysis/definitions/carry_in.v
index 9d68ccfa407adc0addf0047b63f5b947ec1d3aab..f657e5bc283fd9286f297a2fa75be9dee6476a09 100644
--- a/analysis/definitions/carry_in.v
+++ b/analysis/definitions/carry_in.v
@@ -1,36 +1,32 @@
Require Export prosa.model.priority.classes.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require Import prosa.model.processor.ideal.
-
(** * No Carry-In *)
-(** In this module we define the notion of no carry-in time for uni-processor schedulers. *)
+(** In this module, we define the notion of a time without any carry-in work. *)
Section NoCarryIn.
-
+
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
- (** ... and any type of jobs associated with these tasks. *)
- Context {Job : JobType}.
- Context `{JobTask Job Task}.
- Context `{JobArrival Job}.
- Context `{JobCost Job}.
+ (** ... and any type of jobs associated with these tasks, where each
+ job has an arrival time and a cost. *)
+ Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job} `{JobCost Job}.
- (** Consider any arrival sequence with consistent arrivals. *)
+ (** Consider any arrival sequence of such jobs with consistent arrivals ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-
- (** Next, consider any ideal uni-processor schedule of this arrival sequence. *)
- Variable sched : schedule (ideal.processor_state Job).
- (** The processor has no carry-in at time t iff every job (regardless of priority)
- from the arrival sequence released before t has completed by that time. *)
+ (** ... and the resultant schedule. *)
+ Context {PState : Type} `{ProcessorState Job PState}.
+ Variable sched : schedule PState.
+
+ (** There is no carry-in at time [t] iff every job (regardless of priority)
+ from the arrival sequence released before [t] has completed by that time. *)
Definition no_carry_in (t : instant) :=
forall j_o,
arrives_in arr_seq j_o ->
arrived_before j_o t ->
completed_by sched j_o t.
-End NoCarryIn.
\ No newline at end of file
+End NoCarryIn.
diff --git a/analysis/definitions/priority_inversion.v b/analysis/definitions/priority_inversion.v
index a0363b49083acd27737d2fe743257a3be1193713..44728d620dfa4d95667ee28a557d870612d4aea9 100644
--- a/analysis/definitions/priority_inversion.v
+++ b/analysis/definitions/priority_inversion.v
@@ -1,5 +1,8 @@
Require Export prosa.analysis.definitions.busy_interval.
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import prosa.model.processor.ideal.
+
(** * Cumulative Priority Inversion for JLFP-models *)
(** In this module we define the notion of cumulative priority inversion for uni-processor for JLFP schedulers. *)
Section CumulativePriorityInversion.
diff --git a/analysis/definitions/request_bound_function.v b/analysis/definitions/request_bound_function.v
index 009cdb7c24d87906947761307e10e416e2da113f..c612ec57389979b3c30bbcad40358fe51368382c 100644
--- a/analysis/definitions/request_bound_function.v
+++ b/analysis/definitions/request_bound_function.v
@@ -1,11 +1,6 @@
Require Export prosa.model.task.arrival.curves.
Require Export prosa.model.priority.classes.
-(** The following definitions assume ideal uni-processor schedules.
- This restriction exists for historic reasons; the defined concepts
- could be generalized in future work. *)
-Require Import prosa.analysis.facts.model.ideal_schedule.
-
(** * Request Bound Function (RBF) *)
(** We define the notion of a task's request-bound function (RBF), as well as
@@ -23,9 +18,6 @@ Section TaskWorkloadBoundedByArrivalCurves.
Context `{JobTask Job Task}.
Context `{JobCost Job}.
- (** Consider any ideal uni-processor schedule of these jobs... *)
- Variable sched : schedule (ideal.processor_state Job).
-
(** ... and an FP policy that indicates a higher-or-equal priority
relation. *)
Context `{FP_policy Task}.
diff --git a/analysis/facts/model/rbf.v b/analysis/facts/model/rbf.v
index b328a868bd45ca7ab913404b08a2da2ed4cdb1b6..1a2cd077fe89fc2341578a5cd75cb70cbf62352d 100644
--- a/analysis/facts/model/rbf.v
+++ b/analysis/facts/model/rbf.v
@@ -27,8 +27,9 @@ Section ProofWorkloadBound.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
- (** ... and any ideal uni-processor schedule of this arrival sequence.*)
- Variable sched : schedule (ideal.processor_state Job).
+ (** ... and any schedule corresponding to this arrival sequence. *)
+ Context {PState : Type} `{ProcessorState Job PState}.
+ Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
(** Consider an FP policy that indicates a higher-or-equal priority relation. *)
diff --git a/analysis/facts/model/service_of_jobs.v b/analysis/facts/model/service_of_jobs.v
index 11300b13516d93b831cfc7bb51c4a7cfef197610..078603cf73736a535f921c7bd0cb43b44b23a1a8 100644
--- a/analysis/facts/model/service_of_jobs.v
+++ b/analysis/facts/model/service_of_jobs.v
@@ -38,10 +38,7 @@ Section GenericModelLemmas.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Let P be any predicate over jobs. *)
- Variable P : Job -> bool.
-
- (** Let's define some local names for clarity. *)
- Let arrivals_between := arrivals_between arr_seq.
+ Variable P : pred Job.
(** In this section, we prove that the service received by any set of jobs
is upper-bounded by the corresponding workload. *)
@@ -71,20 +68,20 @@ Section GenericModelLemmas.
Section ServiceCat.
(** We show that the total service of jobs released in a time interval <<[t1,t2)>>
- during [t1,t2) is equal to the sum of:
- (1) the total service of jobs released in time interval [t1, t) during time [t1, t)
- (2) the total service of jobs released in time interval [t1, t) during time [t, t2)
- and (3) the total service of jobs released in time interval [t, t2) during time [t, t2). *)
+ during <<[t1,t2)>> is equal to the sum of:
+ (1) the total service of jobs released in time interval <<[t1, t)>> during time <<[t1, t)>>
+ (2) the total service of jobs released in time interval <<[t1, t)>> during time <<[t, t2)>>
+ and (3) the total service of jobs released in time interval <<[t, t2)>> during time <<[t, t2)>>. *)
Lemma service_of_jobs_cat_scheduling_interval :
forall t1 t2 t,
t1 <= t <= t2 ->
- service_of_jobs sched P (arrivals_between t1 t2) t1 t2
- = service_of_jobs sched P (arrivals_between t1 t) t1 t
- + service_of_jobs sched P (arrivals_between t1 t) t t2
- + service_of_jobs sched P (arrivals_between t t2) t t2.
+ service_of_jobs sched P (arrivals_between arr_seq t1 t2) t1 t2
+ = service_of_jobs sched P (arrivals_between arr_seq t1 t) t1 t
+ + service_of_jobs sched P (arrivals_between arr_seq t1 t) t t2
+ + service_of_jobs sched P (arrivals_between arr_seq t t2) t t2.
Proof.
move => t1 t2 t /andP [GEt LEt].
- rewrite /arrivals_between (arrivals_between_cat _ _ t) //.
+ rewrite (arrivals_between_cat _ _ t) //.
rewrite {1}/service_of_jobs big_cat //=.
rewrite exchange_big //= (@big_cat_nat _ _ _ t) //=;
rewrite [in X in X + _ + _]exchange_big //= [in X in _ + X + _]exchange_big //=.
@@ -101,19 +98,19 @@ Section GenericModelLemmas.
Qed.
(** We show that the total service of jobs released in a time interval <<[t1,t2)>>
- during [t,t2) is equal to the sum of:
- (1) the total service of jobs released in a time interval [t1,t) during [t,t2)
- and (2) the total service of jobs released in a time interval [t,t2) during [t,t2). *)
+ during <<[t,t2)>> is equal to the sum of:
+ (1) the total service of jobs released in a time interval <<[t1,t)>> during <<[t,t2)>>
+ and (2) the total service of jobs released in a time interval <<[t,t2)>> during <<[t,t2)>>. *)
Lemma service_of_jobs_cat_arrival_interval :
forall t1 t2 t,
t1 <= t <= t2 ->
- service_of_jobs sched P (arrivals_between t1 t2) t t2 =
- service_of_jobs sched P (arrivals_between t1 t) t t2 +
- service_of_jobs sched P (arrivals_between t t2) t t2.
+ service_of_jobs sched P (arrivals_between arr_seq t1 t2) t t2 =
+ service_of_jobs sched P (arrivals_between arr_seq t1 t) t t2 +
+ service_of_jobs sched P (arrivals_between arr_seq t t2) t t2.
Proof.
move => t1 t2 t /andP [GEt LEt].
apply/eqP;rewrite eq_sym; apply/eqP.
- rewrite /arrivals_between [in X in _ = X](arrivals_between_cat _ _ t) //.
+ rewrite [in X in _ = X](arrivals_between_cat _ _ t) //.
by rewrite {3}/service_of_jobs -big_cat //=.
Qed.
@@ -283,7 +280,8 @@ Section IdealModelLemmas.
(** And state the proposition that all jobs are completed by time
[t_compl]. Next we show that this proposition is equivalent to
- the fact that [workload of jobs = service of jobs]. *)
+ the fact that the workload of the jobs is equal to the service
+ received by the jobs. *)
Let all_jobs_completed_by t_compl :=
forall j, j \in jobs -> P j -> completed_by j t_compl.