From cd6b0e14e8669b9550f5b74a45580978dc319765 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 15 Oct 2019 15:41:52 +0200
Subject: [PATCH] split out service.v + ready.v from schedule.v and add all.v
---
.../analysis/abstract/core/abstract_rta.v | 2 +-
.../analysis/abstract/core/abstract_seq_rta.v | 18 +--
.../analysis/abstract/core/definitions.v | 2 +-
.../core/run_to_completion_threshold.v | 2 +-
...ondition_for_run_to_completion_threshold.v | 2 +-
restructuring/analysis/arrival/rbf.v | 2 +-
.../analysis/arrival/workload_bound.v | 2 +-
restructuring/analysis/basic_facts/arrivals.v | 2 +-
.../analysis/basic_facts/completion.v | 2 +-
.../analysis/basic_facts/deadlines.v | 2 +-
restructuring/analysis/basic_facts/service.v | 2 +-
.../analysis/basic_facts/service_of_jobs.v | 6 +-
restructuring/analysis/schedulability.v | 2 +-
restructuring/analysis/task_schedule.v | 2 +-
restructuring/analysis/transform/prefix.v | 2 +-
restructuring/analysis/transform/swap.v | 2 +-
restructuring/analysis/workload.v | 2 +-
restructuring/behavior/all.v | 6 +
restructuring/behavior/ready.v | 75 ++++++++++
restructuring/behavior/schedule.v | 129 ------------------
restructuring/behavior/service.v | 60 ++++++++
.../model/aggregate/service_of_jobs.v | 2 +-
restructuring/model/aggregate/workload.v | 2 +-
restructuring/model/arrival/arrival_curves.v | 2 +-
restructuring/model/arrival/sporadic.v | 2 +-
restructuring/model/job.v | 2 +-
.../model/preemption/preemption_model.v | 2 +-
restructuring/model/processor/ideal.v | 2 +-
.../model/processor/multiprocessor.v | 2 +-
.../model/processor/platform_properties.v | 2 +-
restructuring/model/processor/spin.v | 2 +-
restructuring/model/processor/varspeed.v | 2 +-
restructuring/model/readiness/basic.v | 2 +-
restructuring/model/readiness/jitter.v | 2 +-
restructuring/model/schedule/edf.v | 2 +-
.../schedule/priority_based/preemptive.v | 2 +-
restructuring/model/schedule/sequential.v | 2 +-
.../model/schedule/work_conserving.v | 2 +-
restructuring/model/task.v | 3 +-
39 files changed, 186 insertions(+), 175 deletions(-)
create mode 100644 restructuring/behavior/all.v
create mode 100644 restructuring/behavior/ready.v
create mode 100644 restructuring/behavior/service.v
diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index 0bc2fd8d4..cab1b614c 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -1,5 +1,5 @@
From rt.util Require Import tactics nat sum ssromega.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Import job task preemption.preemption_model.
From rt.restructuring.analysis Require Import schedulability ideal_schedule.
From rt.restructuring.analysis.abstract Require Import run_to_completion_threshold.
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index 1f028a88d..08d40389f 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -1,5 +1,5 @@
From rt.util Require Import epsilon tactics rewrite_facilities sum counting list.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Import service.
From rt.restructuring.model Require Import job task preemption.preemption_model.
From rt.restructuring.model.arrival Require Import arrival_curves.
From rt.restructuring.model.schedule Require Import sequential.
@@ -241,7 +241,7 @@ Section Sequential_Abstract_RTA.
Proof.
move => JA; move: (H_j2_from_tsk) => /eqP TSK2eq.
move: (posnP (@job_cost _ H3 j2)) => [ZERO|POS].
- { by rewrite /completed_by /schedule.completed_by ZERO. }
+ { by rewrite /completed_by /service.completed_by ZERO. }
move: (H_interference_and_workload_consistent_with_sequential_jobs
j1 t1 t2 H_j1_arrives H_j1_from_tsk H_j1_cost_positive H_busy_interval) => SWEQ.
eapply all_jobs_have_completed_equiv_workload_eq_service
@@ -336,7 +336,7 @@ Section Sequential_Abstract_RTA.
rewrite /cumul_task_interference /definitions.cumul_interference
/Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
/task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
- /service_of_jobs.service_of_jobs_at /scheduled_at /schedule.scheduled_at /scheduled_in;
+ /service_of_jobs.service_of_jobs_at /scheduled_at /service.scheduled_at /scheduled_in;
simpl.
rewrite !H_idle.
rewrite big1_eq addn0 add0n.
@@ -369,7 +369,7 @@ Section Sequential_Abstract_RTA.
rewrite /cumul_task_interference /definitions.cumul_interference
/Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
/task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
- /service_of_jobs.service_of_jobs_at /scheduled_at /schedule.scheduled_at /scheduled_in; simpl.
+ /service_of_jobs.service_of_jobs_at /scheduled_at /service.scheduled_at /scheduled_in; simpl.
have ARRs: arrives_in arr_seq j'; first by apply H_jobs_come_from_arrival_sequence with t; apply/eqP.
rewrite H_sched H_not_job_of_tsk; simpl.
rewrite (negbTE (option_inj_neq (neqprop_to_neqbool
@@ -410,7 +410,7 @@ Section Sequential_Abstract_RTA.
rewrite /cumul_task_interference /definitions.cumul_interference
/Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
/task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
- /service_of_jobs.service_of_jobs_at /scheduled_at /schedule.scheduled_at /scheduled_in; simpl.
+ /service_of_jobs.service_of_jobs_at /scheduled_at /service.scheduled_at /scheduled_in; simpl.
have ARRs: arrives_in arr_seq j'; first by apply H_jobs_come_from_arrival_sequence with t; apply/eqP.
rewrite H_sched H_not_job_of_tsk addn0; simpl;
rewrite [Some j' == Some j](negbTE (option_inj_neq (neq_sym H_j_neq_j'))) addn0.
@@ -419,7 +419,7 @@ Section Sequential_Abstract_RTA.
{ by move: H_t_in_interval => /andP [NEQ1 NEQ2]; apply/andP; split; last apply ltn_trans with (t1 + x). }
move: (H_work_conserving j t1 t2 t H_j_arrives H_job_of_tsk H_job_cost_positive H_busy_interval NEQT) => [Hn _].
apply/eqP;rewrite eq_sym eqb_id; apply/negPn/negP; intros CONTR; move: CONTR => /negP CONTR.
- apply Hn in CONTR; rewrite /schedule.scheduled_at in CONTR; simpl in CONTR.
+ apply Hn in CONTR; rewrite /service.scheduled_at in CONTR; simpl in CONTR.
by rewrite H_sched [Some j' == Some j](negbTE (option_inj_neq (neq_sym H_j_neq_j'))) in CONTR.
}
rewrite big_mkcond; apply/sum_seq_gt0P; exists j'; split; last first.
@@ -469,14 +469,14 @@ Section Sequential_Abstract_RTA.
rewrite /cumul_task_interference /definitions.cumul_interference
/Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
/task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
- /service_of_jobs.service_of_jobs_at /scheduled_at /schedule.scheduled_at /scheduled_in.
+ /service_of_jobs.service_of_jobs_at /scheduled_at /service.scheduled_at /scheduled_in.
rewrite H_sched H_job_of_tsk neq_antirefl addn0; simpl.
move: (H_work_conserving j _ _ t H_j_arrives H_job_of_tsk H_job_cost_positive H_busy_interval) => WORK.
feed WORK.
{ move: H_t_in_interval => /andP [NEQ1 NEQ2].
by apply/andP; split; last apply ltn_trans with (t1 + x). }
move: WORK => [_ ZIJT].
- feed ZIJT; first by rewrite /schedule.scheduled_at /scheduled_at H_sched; simpl.
+ feed ZIJT; first by rewrite /service.scheduled_at /scheduled_at H_sched; simpl.
move: ZIJT => /negP /eqP; rewrite eqb_negLR; simpl; move => /eqP ZIJT; rewrite ZIJT; simpl; rewrite add0n.
rewrite !eq_refl; simpl; rewrite big_mkcond //=; apply/sum_seq_gt0P.
by exists j; split; [apply j_is_in_arrivals_between | rewrite /job_of_task H_job_of_tsk H_sched !eq_refl].
@@ -696,7 +696,7 @@ Section Sequential_Abstract_RTA.
move: (posnP (@job_cost _ H3 j)) => [ZERO|POS].
{ exfalso.
move: COMPL => /negP COMPL; apply: COMPL.
- by rewrite /schedule.completed_by /completed_by ZERO.
+ by rewrite /service.completed_by /completed_by ZERO.
}
set (A := job_arrival j - t1) in *.
apply leq_trans with
diff --git a/restructuring/analysis/abstract/core/definitions.v b/restructuring/analysis/abstract/core/definitions.v
index 125492f69..56e6d79be 100644
--- a/restructuring/analysis/abstract/core/definitions.v
+++ b/restructuring/analysis/abstract/core/definitions.v
@@ -1,5 +1,5 @@
From rt.util Require Import all.
-From rt.restructuring.behavior Require Import job schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Import task processor.ideal.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/abstract/core/run_to_completion_threshold.v b/restructuring/analysis/abstract/core/run_to_completion_threshold.v
index b25bf326b..3df959fd1 100644
--- a/restructuring/analysis/abstract/core/run_to_completion_threshold.v
+++ b/restructuring/analysis/abstract/core/run_to_completion_threshold.v
@@ -1,5 +1,5 @@
From rt.util Require Import epsilon sum tactics search_arg.
-From rt.restructuring.behavior Require Import job schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import completion.
From rt.restructuring.model Require Import job task preemption.preemption_model.
diff --git a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
index bf2f724f0..bf6fa2b34 100644
--- a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
+++ b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
@@ -1,5 +1,5 @@
From rt.util Require Import nat sum tactics.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Import job task preemption.preemption_model.
From rt.restructuring.analysis Require Import service completion ideal_schedule.
From rt.restructuring.analysis.abstract Require Import run_to_completion_threshold core.definitions.
diff --git a/restructuring/analysis/arrival/rbf.v b/restructuring/analysis/arrival/rbf.v
index cb9b77140..6159f10d3 100644
--- a/restructuring/analysis/arrival/rbf.v
+++ b/restructuring/analysis/arrival/rbf.v
@@ -1,5 +1,5 @@
From rt.util Require Import all.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Import job task.
From rt.restructuring.model.aggregate Require Import task_arrivals.
From rt.restructuring.model.arrival Require Import arrival_curves.
diff --git a/restructuring/analysis/arrival/workload_bound.v b/restructuring/analysis/arrival/workload_bound.v
index 91688c0b4..11d998cce 100644
--- a/restructuring/analysis/arrival/workload_bound.v
+++ b/restructuring/analysis/arrival/workload_bound.v
@@ -1,5 +1,5 @@
From rt.util Require Import sum.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Import task schedule.priority_based.priorities.
From rt.restructuring.model.aggregate Require Import task_arrivals.
From rt.restructuring.model.arrival Require Import arrival_curves.
diff --git a/restructuring/analysis/basic_facts/arrivals.v b/restructuring/analysis/basic_facts/arrivals.v
index 75602ba60..361c73159 100644
--- a/restructuring/analysis/basic_facts/arrivals.v
+++ b/restructuring/analysis/basic_facts/arrivals.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export arrival_sequence schedule.
+From rt.restructuring.behavior Require Export all.
From rt.util Require Import all.
(* In this section, we relate job readiness to [has_arrived]. *)
diff --git a/restructuring/analysis/basic_facts/completion.v b/restructuring/analysis/basic_facts/completion.v
index 582c4d829..4263486dd 100644
--- a/restructuring/analysis/basic_facts/completion.v
+++ b/restructuring/analysis/basic_facts/completion.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Export service.
From rt.util Require Import nat.
diff --git a/restructuring/analysis/basic_facts/deadlines.v b/restructuring/analysis/basic_facts/deadlines.v
index 1196bd3e3..7fe7696ff 100644
--- a/restructuring/analysis/basic_facts/deadlines.v
+++ b/restructuring/analysis/basic_facts/deadlines.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Export service completion.
(** In this file, we observe basic properties of the behavioral job
diff --git a/restructuring/analysis/basic_facts/service.v b/restructuring/analysis/basic_facts/service.v
index 9b3c2cf31..44539d945 100644
--- a/restructuring/analysis/basic_facts/service.v
+++ b/restructuring/analysis/basic_facts/service.v
@@ -1,5 +1,5 @@
From mathcomp Require Import ssrnat ssrbool fintype.
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model.processor Require Export platform_properties.
From rt.util Require Import tactics step_function sum.
diff --git a/restructuring/analysis/basic_facts/service_of_jobs.v b/restructuring/analysis/basic_facts/service_of_jobs.v
index 3924225e0..4e84ffafe 100644
--- a/restructuring/analysis/basic_facts/service_of_jobs.v
+++ b/restructuring/analysis/basic_facts/service_of_jobs.v
@@ -1,5 +1,5 @@
From rt.util Require Import tactics sum.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Import service.
From rt.restructuring.model Require Export service_of_jobs.
From rt.restructuring.model Require Import task schedule.priority_based.priorities processor.ideal.
From rt.restructuring.analysis Require Import workload.
@@ -255,10 +255,10 @@ Section IdealModelLemmas.
rewrite /workload_of_jobs in EQ.
rewrite (big_rem j) ?Pj //= in EQ.
move: EQ => /eqP; rewrite addn_eq0; move => /andP [CZ _].
- unfold completed_by, schedule.completed_by.
+ unfold completed_by, service.completed_by.
by move: CZ => /eqP CZ; rewrite CZ.
}
- { unfold workload_of_jobs, service_of_jobs in EQ; unfold completed_by, schedule.completed_by.
+ { unfold workload_of_jobs, service_of_jobs in EQ; unfold completed_by, service.completed_by.
rewrite /service -(service_during_cat _ _ _ t1); last by apply/andP; split.
rewrite cumulative_service_before_job_arrival_zero // add0n.
rewrite <- sum_majorant_eqn with (F1 := fun j => service_during sched j t1 t_compl)
diff --git a/restructuring/analysis/schedulability.v b/restructuring/analysis/schedulability.v
index 7226af674..0e332a9e3 100644
--- a/restructuring/analysis/schedulability.v
+++ b/restructuring/analysis/schedulability.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Export task.
From rt.restructuring.analysis.basic_facts Require Export completion.
From rt.util Require Export seqset.
diff --git a/restructuring/analysis/task_schedule.v b/restructuring/analysis/task_schedule.v
index 8bc83c0f0..dd846c6e3 100644
--- a/restructuring/analysis/task_schedule.v
+++ b/restructuring/analysis/task_schedule.v
@@ -1,5 +1,5 @@
From rt.restructuring.model Require Import task.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/transform/prefix.v b/restructuring/analysis/transform/prefix.v
index 2187ebe2a..d00625856 100644
--- a/restructuring/analysis/transform/prefix.v
+++ b/restructuring/analysis/transform/prefix.v
@@ -1,5 +1,5 @@
From mathcomp Require Import ssrnat ssrbool fintype.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis Require Import basic_facts.all.
(** This file provides an operation that transforms a finite prefix of
diff --git a/restructuring/analysis/transform/swap.v b/restructuring/analysis/transform/swap.v
index 6f32fc7d3..f44a40557 100644
--- a/restructuring/analysis/transform/swap.v
+++ b/restructuring/analysis/transform/swap.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule job.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import all.
(** This file defines simple allocation substitutions and a swapping operation
diff --git a/restructuring/analysis/workload.v b/restructuring/analysis/workload.v
index 453d1e281..aab4291b2 100644
--- a/restructuring/analysis/workload.v
+++ b/restructuring/analysis/workload.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Export workload schedule.priority_based.priorities.
From rt.restructuring.analysis Require Import basic_facts.arrivals.
diff --git a/restructuring/behavior/all.v b/restructuring/behavior/all.v
new file mode 100644
index 000000000..f12642cbe
--- /dev/null
+++ b/restructuring/behavior/all.v
@@ -0,0 +1,6 @@
+Require Export rt.restructuring.behavior.time.
+Require Export rt.restructuring.behavior.job.
+Require Export rt.restructuring.behavior.arrival_sequence.
+Require Export rt.restructuring.behavior.schedule.
+Require Export rt.restructuring.behavior.service.
+Require Export rt.restructuring.behavior.ready.
diff --git a/restructuring/behavior/ready.v b/restructuring/behavior/ready.v
new file mode 100644
index 000000000..2a5c9773d
--- /dev/null
+++ b/restructuring/behavior/ready.v
@@ -0,0 +1,75 @@
+From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
+From rt.restructuring.behavior Require Export service.
+
+
+(* We define a general notion of readiness of a job: a job can be
+ scheduled only when it is ready. This notion of readiness is a general
+ concept that is used to model jitter, self-suspensions, etc. Crucially, we
+ require that any sensible notion of readiness is a refinement of the notion
+ of a pending job, i.e., any ready job must also be pending. *)
+Class JobReady (Job : JobType) (PState : Type)
+ `{ProcessorState Job PState} `{JobCost Job} `{JobArrival Job} :=
+ {
+ job_ready : schedule PState -> Job -> instant -> bool;
+ any_ready_job_is_pending : forall sched j t, job_ready sched j t -> pending sched j t;
+ }.
+
+(* Based on the general notion of readiness, we define what it means to be
+ backlogged, i.e., ready to run but not executing. *)
+Section Backlogged.
+ (* Conside any kinds of jobs and any kind of processor state. *)
+ Context {Job : JobType} {PState : Type}.
+ Context `{ProcessorState Job PState}.
+
+ (* Allow for any notion of readiness. *)
+ Context `{JobReady Job PState}.
+
+ (* Job j is backlogged at time t iff it is ready and not scheduled. *)
+ Definition backlogged (sched : schedule PState) (j : Job) (t : instant) :=
+ job_ready sched j t && ~~ scheduled_at sched j t.
+
+End Backlogged.
+
+
+(* With the readiness concept in place, we define the notion of valid schedules. *)
+Section ValidSchedule.
+ (* Consider any kinds of jobs and any kind of processor state. *)
+ Context {Job : JobType} {PState : Type}.
+ Context `{ProcessorState Job PState}.
+
+ (* Consider any schedule. *)
+ Variable sched : schedule PState.
+
+ Context `{JobArrival Job}.
+
+ (* We define whether jobs come from some arrival sequence... *)
+ Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) :=
+ forall j t, scheduled_at sched j t -> arrives_in arr_seq j.
+
+ (* ..., whether a job can only be scheduled if it has arrived ... *)
+ Definition jobs_must_arrive_to_execute :=
+ forall j t, scheduled_at sched j t -> has_arrived j t.
+
+ Context `{JobCost Job}.
+ Context `{JobReady Job PState}.
+
+ (* ..., whether a job can only be scheduled if it is ready ... *)
+ Definition jobs_must_be_ready_to_execute :=
+ forall j t, scheduled_at sched j t -> job_ready sched j t.
+
+ (* ... and whether a job cannot be scheduled after it completes. *)
+ Definition completed_jobs_dont_execute :=
+ forall j t, scheduled_at sched j t -> service sched j t < job_cost j.
+
+ (* We say that the schedule is valid iff
+ - jobs come from some arrival sequence
+ - a job is scheduled if it is ready *)
+ Definition valid_schedule (arr_seq : arrival_sequence Job) :=
+ jobs_come_from_arrival_sequence arr_seq /\
+ jobs_must_be_ready_to_execute.
+
+ (* Note that we do not explicitly require that a valid schedule satisfies
+ jobs_must_arrive_to_execute or completed_jobs_dont_execute because these
+ properties are implied by jobs_must_be_ready_to_execute. *)
+
+End ValidSchedule.
diff --git a/restructuring/behavior/schedule.v b/restructuring/behavior/schedule.v
index 71d4153f5..d52e29116 100644
--- a/restructuring/behavior/schedule.v
+++ b/restructuring/behavior/schedule.v
@@ -22,132 +22,3 @@ Class ProcessorState (Job : JobType) (State : Type) :=
(* A schedule maps an instant to a processor state *)
Definition schedule (PState : Type) := instant -> PState.
-Section Schedule.
- Context {Job : JobType} {PState : Type}.
- Context `{ProcessorState Job PState}.
-
- Variable sched : schedule PState.
-
- (* First, we define whether a job j is scheduled at time t, ... *)
- Definition scheduled_at (j : Job) (t : instant) := scheduled_in j (sched t).
-
- (* ... and the instantaneous service received by
- job j at time t. *)
- Definition service_at (j : Job) (t : instant) := service_in j (sched t).
-
- (* Based on the notion of instantaneous service, we define the
- cumulative service received by job j during any interval [t1, t2). *)
- Definition service_during (j : Job) (t1 t2 : instant) :=
- \sum_(t1 <= t < t2) service_at j t.
-
- (* Using the previous definition, we define the cumulative service
- received by job j up to time t, i.e., during interval [0, t). *)
- Definition service (j : Job) (t : instant) := service_during j 0 t.
-
- Context `{JobCost Job}.
- Context `{JobDeadline Job}.
- Context `{JobArrival Job}.
-
- (* Next, we say that job j has completed by time t if it received enough
- service in the interval [0, t). *)
- Definition completed_by (j : Job) (t : instant) := service j t >= job_cost j.
-
- (* We say that job j completes at time t if it has completed by time t but
- not by time t - 1 *)
- Definition completes_at (j : Job) (t : instant) := ~~ completed_by j t.-1 && completed_by j t.
-
- (* We say that R is a response time bound of a job j if j has completed
- by R units after its arrival *)
- Definition job_response_time_bound (j : Job) (R : duration) :=
- completed_by j (job_arrival j + R).
-
- (* We say that a job meets its deadline if it completes by its absolute deadline *)
- Definition job_meets_deadline (j : Job) :=
- completed_by j (job_deadline j).
-
- (* Job j is pending at time t iff it has arrived but has not yet completed. *)
- Definition pending (j : Job) (t : instant) := has_arrived j t && ~~ completed_by j t.
-
- (* Job j is pending earlier and at time t iff it has arrived before time t
- and has not been completed yet. *)
- Definition pending_earlier_and_at (j : Job) (t : instant) :=
- arrived_before j t && ~~ completed_by j t.
-
- (* Let's define the remaining cost of job j as the amount of service
- that has to be received for its completion. *)
- Definition remaining_cost j t :=
- job_cost j - service j t.
-
-End Schedule.
-
-(* We next define a general notion of readiness of a job: a job can be
- scheduled only when it is ready. This notion of readiness is a general
- concept that is used to model jitter, self-suspensions, etc. Crucially, we
- require that any sensible notion of readiness is a refinement of the notion
- of a pending job, i.e., any ready job must also be pending. *)
-Class JobReady (Job : JobType) (PState : Type)
- `{ProcessorState Job PState} `{JobCost Job} `{JobArrival Job} :=
- {
- job_ready : schedule PState -> Job -> instant -> bool;
- any_ready_job_is_pending : forall sched j t, job_ready sched j t -> pending sched j t;
- }.
-
-(* Based on the general notion of readiness, we define what it means to be
- backlogged, i.e., ready to run but not executing. *)
-Section Backlogged.
- (* Conside any kinds of jobs and any kind of processor state. *)
- Context {Job : JobType} {PState : Type}.
- Context `{ProcessorState Job PState}.
-
- (* Allow for any notion of readiness. *)
- Context `{JobReady Job PState}.
-
- (* Job j is backlogged at time t iff it is ready and not scheduled. *)
- Definition backlogged (sched : schedule PState) (j : Job) (t : instant) :=
- job_ready sched j t && ~~ scheduled_at sched j t.
-
-End Backlogged.
-
-
-(* In this section, we define valid schedules. *)
-Section ValidSchedule.
- (* Consider any kinds of jobs and any kind of processor state. *)
- Context {Job : JobType} {PState : Type}.
- Context `{ProcessorState Job PState}.
-
- (* Consider any schedule. *)
- Variable sched : schedule PState.
-
- Context `{JobArrival Job}.
-
- (* We define whether jobs come from some arrival sequence... *)
- Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) :=
- forall j t, scheduled_at sched j t -> arrives_in arr_seq j.
-
- (* ..., whether a job can only be scheduled if it has arrived ... *)
- Definition jobs_must_arrive_to_execute :=
- forall j t, scheduled_at sched j t -> has_arrived j t.
-
- Context `{JobCost Job}.
- Context `{JobReady Job PState}.
-
- (* ..., whether a job can only be scheduled if it is ready ... *)
- Definition jobs_must_be_ready_to_execute :=
- forall j t, scheduled_at sched j t -> job_ready sched j t.
-
- (* ... and whether a job cannot be scheduled after it completes. *)
- Definition completed_jobs_dont_execute :=
- forall j t, scheduled_at sched j t -> service sched j t < job_cost j.
-
- (* We say that the schedule is valid iff
- - jobs come from some arrival sequence
- - a job is scheduled if it is ready *)
- Definition valid_schedule (arr_seq : arrival_sequence Job) :=
- jobs_come_from_arrival_sequence arr_seq /\
- jobs_must_be_ready_to_execute.
-
- (* Note that we do not explicitly require that a valid schedule satisfies
- jobs_must_arrive_to_execute or completed_jobs_dont_execute because these
- properties are implied by jobs_must_be_ready_to_execute. *)
-
-End ValidSchedule.
diff --git a/restructuring/behavior/service.v b/restructuring/behavior/service.v
new file mode 100644
index 000000000..e33780555
--- /dev/null
+++ b/restructuring/behavior/service.v
@@ -0,0 +1,60 @@
+From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
+From rt.restructuring.behavior Require Export schedule.
+
+Section Service.
+ Context {Job : JobType} {PState : Type}.
+ Context `{ProcessorState Job PState}.
+
+ Variable sched : schedule PState.
+
+ (* First, we define whether a job j is scheduled at time t, ... *)
+ Definition scheduled_at (j : Job) (t : instant) := scheduled_in j (sched t).
+
+ (* ... and the instantaneous service received by
+ job j at time t. *)
+ Definition service_at (j : Job) (t : instant) := service_in j (sched t).
+
+ (* Based on the notion of instantaneous service, we define the
+ cumulative service received by job j during any interval [t1, t2). *)
+ Definition service_during (j : Job) (t1 t2 : instant) :=
+ \sum_(t1 <= t < t2) service_at j t.
+
+ (* Using the previous definition, we define the cumulative service
+ received by job j up to time t, i.e., during interval [0, t). *)
+ Definition service (j : Job) (t : instant) := service_during j 0 t.
+
+ Context `{JobCost Job}.
+ Context `{JobDeadline Job}.
+ Context `{JobArrival Job}.
+
+ (* Next, we say that job j has completed by time t if it received enough
+ service in the interval [0, t). *)
+ Definition completed_by (j : Job) (t : instant) := service j t >= job_cost j.
+
+ (* We say that job j completes at time t if it has completed by time t but
+ not by time t - 1 *)
+ Definition completes_at (j : Job) (t : instant) := ~~ completed_by j t.-1 && completed_by j t.
+
+ (* We say that R is a response time bound of a job j if j has completed
+ by R units after its arrival *)
+ Definition job_response_time_bound (j : Job) (R : duration) :=
+ completed_by j (job_arrival j + R).
+
+ (* We say that a job meets its deadline if it completes by its absolute deadline *)
+ Definition job_meets_deadline (j : Job) :=
+ completed_by j (job_deadline j).
+
+ (* Job j is pending at time t iff it has arrived but has not yet completed. *)
+ Definition pending (j : Job) (t : instant) := has_arrived j t && ~~ completed_by j t.
+
+ (* Job j is pending earlier and at time t iff it has arrived before time t
+ and has not been completed yet. *)
+ Definition pending_earlier_and_at (j : Job) (t : instant) :=
+ arrived_before j t && ~~ completed_by j t.
+
+ (* Let's define the remaining cost of job j as the amount of service
+ that has to be received for its completion. *)
+ Definition remaining_cost j t :=
+ job_cost j - service j t.
+
+End Service.
diff --git a/restructuring/model/aggregate/service_of_jobs.v b/restructuring/model/aggregate/service_of_jobs.v
index 7aab4cdad..b8ade1047 100644
--- a/restructuring/model/aggregate/service_of_jobs.v
+++ b/restructuring/model/aggregate/service_of_jobs.v
@@ -1,5 +1,5 @@
From rt.util Require Import tactics sum.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Import task schedule.priority_based.priorities processor.ideal.
From rt.restructuring.analysis Require Import workload.
From rt.restructuring.analysis.basic_facts Require Import arrivals completion ideal_schedule.
diff --git a/restructuring/model/aggregate/workload.v b/restructuring/model/aggregate/workload.v
index 891124dd2..0160115f3 100644
--- a/restructuring/model/aggregate/workload.v
+++ b/restructuring/model/aggregate/workload.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Import task schedule.priority_based.priorities.
From rt.restructuring.analysis Require Import basic_facts.arrivals.
diff --git a/restructuring/model/arrival/arrival_curves.v b/restructuring/model/arrival/arrival_curves.v
index e33d68c96..4a7c2bf62 100644
--- a/restructuring/model/arrival/arrival_curves.v
+++ b/restructuring/model/arrival/arrival_curves.v
@@ -1,5 +1,5 @@
From rt.util Require Import all.
-From rt.restructuring.behavior Require Export arrival_sequence.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Import task_arrivals.
(* In this section, we define the notion of arrival curves, which
diff --git a/restructuring/model/arrival/sporadic.v b/restructuring/model/arrival/sporadic.v
index a0b1c60c3..fb19b8d1e 100644
--- a/restructuring/model/arrival/sporadic.v
+++ b/restructuring/model/arrival/sporadic.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export arrival_sequence.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Export task.
Section TaskMinInterArrivalTime.
diff --git a/restructuring/model/job.v b/restructuring/model/job.v
index 40ddc1a91..9701ef485 100644
--- a/restructuring/model/job.v
+++ b/restructuring/model/job.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export time job.
+From rt.restructuring.behavior Require Export all.
From mathcomp Require Export eqtype ssrnat.
(* In this section, we introduce properties of a job. *)
diff --git a/restructuring/model/preemption/preemption_model.v b/restructuring/model/preemption/preemption_model.v
index d60e9903a..0669e2cfa 100644
--- a/restructuring/model/preemption/preemption_model.v
+++ b/restructuring/model/preemption/preemption_model.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Import job schedule.
+From rt.restructuring.behavior Require Import all.
From rt.restructuring.model Require Import job task.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/model/processor/ideal.v b/restructuring/model/processor/ideal.v
index a08ca228e..ca65de81f 100644
--- a/restructuring/model/processor/ideal.v
+++ b/restructuring/model/processor/ideal.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
(** First let us define the notion of an ideal schedule state, as done in Prosa
so far: either a job is scheduled or the system is idle. *)
diff --git a/restructuring/model/processor/multiprocessor.v b/restructuring/model/processor/multiprocessor.v
index f9a4dc60d..f84a7d6db 100644
--- a/restructuring/model/processor/multiprocessor.v
+++ b/restructuring/model/processor/multiprocessor.v
@@ -1,5 +1,5 @@
From mathcomp Require Export fintype.
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
Section Schedule.
diff --git a/restructuring/model/processor/platform_properties.v b/restructuring/model/processor/platform_properties.v
index dedc5544e..1ad0b7cb0 100644
--- a/restructuring/model/processor/platform_properties.v
+++ b/restructuring/model/processor/platform_properties.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
(* To reason about classes of schedule types / processor models, we define the
following properties that a processor model might possess. *)
diff --git a/restructuring/model/processor/spin.v b/restructuring/model/processor/spin.v
index 12108fc33..44826d232 100644
--- a/restructuring/model/processor/spin.v
+++ b/restructuring/model/processor/spin.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
(** Next we define a processor state that includes the possibility of spinning,
where spinning jobs do not progress (= don't get service). *)
diff --git a/restructuring/model/processor/varspeed.v b/restructuring/model/processor/varspeed.v
index b31855d7f..2708b1490 100644
--- a/restructuring/model/processor/varspeed.v
+++ b/restructuring/model/processor/varspeed.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
(** Next, let us define a schedule with variable execution speed. *)
Section State.
diff --git a/restructuring/model/readiness/basic.v b/restructuring/model/readiness/basic.v
index ccda30e46..6b16bfab6 100644
--- a/restructuring/model/readiness/basic.v
+++ b/restructuring/model/readiness/basic.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import completion.
(* We define the readiness indicator function for the classic Liu & Layland
diff --git a/restructuring/model/readiness/jitter.v b/restructuring/model/readiness/jitter.v
index 49e5e2e6a..a61b7a6b1 100644
--- a/restructuring/model/readiness/jitter.v
+++ b/restructuring/model/readiness/jitter.v
@@ -1,5 +1,5 @@
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
From rt.util Require Import nat.
diff --git a/restructuring/model/schedule/edf.v b/restructuring/model/schedule/edf.v
index 5ba654c22..90c09b19f 100644
--- a/restructuring/model/schedule/edf.v
+++ b/restructuring/model/schedule/edf.v
@@ -1,5 +1,5 @@
From mathcomp Require Import ssrnat ssrbool fintype.
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
(** In this file, we define what it means to be an "EDF schedule". *)
Section DefinitionOfEDF.
diff --git a/restructuring/model/schedule/priority_based/preemptive.v b/restructuring/model/schedule/priority_based/preemptive.v
index c8d265402..2bfcdf195 100644
--- a/restructuring/model/schedule/priority_based/preemptive.v
+++ b/restructuring/model/schedule/priority_based/preemptive.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule arrival_sequence.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Export priorities.
(* We now define what it means for a schedule to respect a priority *)
diff --git a/restructuring/model/schedule/sequential.v b/restructuring/model/schedule/sequential.v
index 664414f6d..08c91c41b 100644
--- a/restructuring/model/schedule/sequential.v
+++ b/restructuring/model/schedule/sequential.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Export task.
Section PropertyOfSequentiality.
diff --git a/restructuring/model/schedule/work_conserving.v b/restructuring/model/schedule/work_conserving.v
index a37e357a7..e5447011b 100644
--- a/restructuring/model/schedule/work_conserving.v
+++ b/restructuring/model/schedule/work_conserving.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule arrival_sequence.
+From rt.restructuring.behavior Require Export all.
(* In this file, we introduce a restrictive definition of work conserving
uniprocessor schedules. The definition is restrictive because it does not
diff --git a/restructuring/model/task.v b/restructuring/model/task.v
index b325e42d6..f25bdb465 100644
--- a/restructuring/model/task.v
+++ b/restructuring/model/task.v
@@ -1,6 +1,5 @@
From mathcomp Require Export ssrbool.
-From rt.restructuring.behavior Require Export job.
-From rt.restructuring.behavior Require Export arrival_sequence.
+From rt.restructuring.behavior Require Export all.
(* Throughout the library we assume that tasks have decidable equality *)
Definition TaskType := eqType.
--
GitLab