From 0b7a65db88eda147458adc53fe82ad8d65c6c393 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 25 Feb 2022 14:45:46 +0100
Subject: [PATCH] Put State inside ProcessorState
It was a parameter but that wasn't of any use,
it was just making everything more noisy.
---
analysis/abstract/abstract_rta.v | 9 +++--
analysis/abstract/definitions.v | 3 +-
analysis/abstract/run_to_completion.v | 5 ++-
analysis/definitions/busy_interval.v | 3 +-
analysis/definitions/carry_in.v | 2 +-
analysis/definitions/completion_sequence.v | 3 +-
analysis/definitions/job_response_time.v | 3 +-
analysis/definitions/progress.v | 3 +-
analysis/definitions/readiness.v | 4 +--
analysis/definitions/schedulability.v | 9 ++---
analysis/definitions/schedule_prefix.v | 2 +-
analysis/definitions/tardiness.v | 3 +-
analysis/definitions/work_bearing_readiness.v | 5 ++-
analysis/facts/behavior/arrivals.v | 9 +++--
analysis/facts/behavior/completion.v | 19 ++++------
analysis/facts/behavior/deadlines.v | 3 +-
analysis/facts/behavior/service.v | 15 +++-----
analysis/facts/busy_interval/busy_interval.v | 4 +--
analysis/facts/busy_interval/carry_in.v | 2 +-
.../facts/busy_interval/priority_inversion.v | 4 +--
analysis/facts/model/preemption.v | 2 +-
analysis/facts/model/rbf.v | 2 +-
analysis/facts/model/sequential.v | 3 +-
analysis/facts/model/service_of_jobs.v | 10 ++----
analysis/facts/preemption/job/preemptive.v | 7 ++--
.../rtc_threshold/job_preemptable.v | 3 +-
analysis/facts/preemption/task/preemptive.v | 3 +-
analysis/facts/priority/edf.v | 2 +-
analysis/facts/priority/sequential.v | 2 +-
analysis/facts/readiness/backlogged.v | 6 ++--
analysis/facts/readiness/basic.v | 3 +-
analysis/facts/readiness/sequential.v | 3 +-
analysis/facts/transform/edf_opt.v | 3 +-
analysis/facts/transform/replace_at.v | 3 +-
analysis/facts/transform/swaps.v | 11 +++---
analysis/transform/prefix.v | 3 +-
analysis/transform/swap.v | 11 +++---
analysis/transform/wc_trans.v | 2 +-
behavior/ready.v | 15 ++++----
behavior/schedule.v | 9 +++--
behavior/service.v | 3 +-
.../definitions/generic_scheduler.v | 6 ++--
implementation/facts/generic_schedule.v | 5 ++-
model/aggregate/service_of_jobs.v | 3 +-
model/preemption/parameter.v | 3 +-
model/processor/ideal.v | 35 ++++++++-----------
model/processor/multiprocessor.v | 10 +++---
model/processor/platform_properties.v | 3 +-
model/processor/spin.v | 5 +--
model/processor/varspeed.v | 5 +--
model/readiness/basic.v | 4 +--
model/readiness/jitter.v | 7 ++--
model/readiness/sequential.v | 9 ++---
model/readiness/suspension.v | 7 ++--
model/schedule/edf.v | 10 +-----
model/schedule/limited_preemptive.v | 2 +-
model/schedule/nonpreemptive.v | 3 +-
model/schedule/priority_driven.v | 3 +-
model/schedule/tdma.v | 3 +-
model/schedule/work_conserving.v | 6 ++--
model/task/preemption/parameters.v | 6 ++--
model/task/sequentiality.v | 4 +--
results/fixed_priority/rta/bounded_nps.v | 2 +-
results/fixed_priority/rta/bounded_pi.v | 2 +-
64 files changed, 140 insertions(+), 219 deletions(-)
diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index 5ba0516f4..2e68fdeff 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -25,8 +25,7 @@ Section Abstract_RTA.
Context `{JobPreemptable Job}.
(** Consider any kind of uni-service ideal processor state model. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
@@ -271,7 +270,7 @@ Section Abstract_RTA.
move: H_busy_interval => [[/andP [GT LT] _] _].
have ESERV :=
@j_receives_at_least_run_to_completion_threshold
- _ _ H1 H2 H3 PState H5 _ _ arr_seq sched tsk interference interfering_workload
+ _ _ H1 H2 H3 PState _ _ arr_seq sched tsk interference interfering_workload
_ j _ _ _ t1 t2 _ (job_rtct j) _ ((A + F) - optimism).
feed_n 7 ESERV; eauto 2.
specialize (ESERV H3 H4).
@@ -500,7 +499,7 @@ Section Abstract_RTA.
simpl in IB; rewrite H_equivalent in IB; last by apply ltn_trans with A.
have ESERV :=
@j_receives_at_least_run_to_completion_threshold
- _ _ H1 H2 H3 PState H5 _ _ arr_seq sched tsk
+ _ _ H1 H2 H3 PState _ _ arr_seq sched tsk
interference interfering_workload _ j _ _ _ t1 t2 _ (job_rtct j) _ (A_sp + F_sp).
feed_n 7 ESERV; eauto 2.
specialize (ESERV H3 H4).
@@ -552,4 +551,4 @@ Section Abstract_RTA.
with (j := j) (t1 := t1) (t2 := t2) (A_sp := A1) (F_sp := F1); auto.
Qed.
-End Abstract_RTA.
+End Abstract_RTA.
diff --git a/analysis/abstract/definitions.v b/analysis/abstract/definitions.v
index f5da2b51b..686db1043 100644
--- a/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -22,8 +22,7 @@ Section AbstractRTADefinitions.
Context `{JobCost Job}.
(** Consider any kind of processor state model. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Consider any arrival sequence... *)
Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/abstract/run_to_completion.v b/analysis/abstract/run_to_completion.v
index ba9a0ca0e..c717c5c4d 100644
--- a/analysis/abstract/run_to_completion.v
+++ b/analysis/abstract/run_to_completion.v
@@ -28,8 +28,7 @@ Section AbstractRTARunToCompletionThreshold.
Context `{JobPreemptable Job}.
(** Consider any kind of uni-service ideal processor state model. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
@@ -181,7 +180,7 @@ Section AbstractRTARunToCompletionThreshold.
move => t ES.
set (job_cost j - job_rtct j) as job_last.
have LSNP := @job_nonpreemptive_after_run_to_completion_threshold
- Job H2 H3 _ _ arr_seq sched _ j _ t.
+ Job H2 H3 _ arr_seq sched _ j _ t.
apply negbNE; apply/negP; intros CONTR.
have SCHED: forall t', t <= t' <= t + job_last -> scheduled_at sched j t'.
{ move => t' /andP [GE LT].
diff --git a/analysis/definitions/busy_interval.v b/analysis/definitions/busy_interval.v
index 16e2e4589..05f34720f 100644
--- a/analysis/definitions/busy_interval.v
+++ b/analysis/definitions/busy_interval.v
@@ -11,8 +11,7 @@ Section BusyIntervalJLFP.
Context `{JobCost Job}.
(** Consider any kind of processor state model. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Consider any arrival sequence with consistent arrivals ... *)
Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/definitions/carry_in.v b/analysis/definitions/carry_in.v
index b83bf9798..dc49b2269 100644
--- a/analysis/definitions/carry_in.v
+++ b/analysis/definitions/carry_in.v
@@ -18,7 +18,7 @@ Section NoCarryIn.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** ... and the resultant schedule. *)
- Context {PState : Type} `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
(** There is no carry-in at time [t] iff every job (regardless of priority)
diff --git a/analysis/definitions/completion_sequence.v b/analysis/definitions/completion_sequence.v
index d53960d65..c3a34a49e 100644
--- a/analysis/definitions/completion_sequence.v
+++ b/analysis/definitions/completion_sequence.v
@@ -11,8 +11,7 @@ Section CompletionSequence.
(** Consider any kind of jobs with a cost
and any kind of processor state. *)
- Context {Job : JobType} `{JobCost Job} {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {Job : JobType} `{JobCost Job} {PState : ProcessorState Job}.
(** Consider any job arrival sequence. *)
Variable arr_seq: arrival_sequence Job.
diff --git a/analysis/definitions/job_response_time.v b/analysis/definitions/job_response_time.v
index 78375007f..9cc463eb1 100644
--- a/analysis/definitions/job_response_time.v
+++ b/analysis/definitions/job_response_time.v
@@ -10,8 +10,7 @@ Section JobResponseTimeExceeds.
Context `{JobArrival Job}.
(** ... and any kind of processor state. *)
- Context `{PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context `{PState : ProcessorState Job}.
(** Consider any schedule. *)
Variable sched : schedule PState.
diff --git a/analysis/definitions/progress.v b/analysis/definitions/progress.v
index ce5480af5..40962cb31 100644
--- a/analysis/definitions/progress.v
+++ b/analysis/definitions/progress.v
@@ -12,8 +12,7 @@ Section Progress.
Context `{JobCost Job}.
(** ... and any kind of schedule. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** For a given job and a given schedule... *)
Variable sched : schedule PState.
diff --git a/analysis/definitions/readiness.v b/analysis/definitions/readiness.v
index d03d7fa58..c54d8a99a 100644
--- a/analysis/definitions/readiness.v
+++ b/analysis/definitions/readiness.v
@@ -12,7 +12,7 @@ Section ReadinessModelProperties.
Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
(** ... and any kind of processor model, ... *)
- Context {PState: Type} `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** ... consider a notion of job readiness. *)
Variable ReadinessModel : JobReady Job PState.
@@ -46,5 +46,3 @@ Section ReadinessModelProperties.
~~ job_preemptable j (service sched j t) -> job_ready sched j t.
End ReadinessModelProperties.
-
-
diff --git a/analysis/definitions/schedulability.v b/analysis/definitions/schedulability.v
index 2d0974ca8..d3ee7d7bf 100644
--- a/analysis/definitions/schedulability.v
+++ b/analysis/definitions/schedulability.v
@@ -18,8 +18,7 @@ Section Task.
Context `{JobTask Job Task}.
(** ... and any kind of processor state. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
@@ -65,8 +64,7 @@ Section Schedulability.
Context `{JobTask Job Task}.
(** ... and any kind of processor state. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
@@ -115,8 +113,7 @@ Section AllDeadlinesMet.
Context `{JobDeadline Job}.
(** ... any given type of processor states. *)
- Context {PState: eqType}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** We say that all deadlines are met if every job scheduled at some
point in the schedule meets its deadline. Note that this is a
diff --git a/analysis/definitions/schedule_prefix.v b/analysis/definitions/schedule_prefix.v
index 1f7c8053c..38cd8797f 100644
--- a/analysis/definitions/schedule_prefix.v
+++ b/analysis/definitions/schedule_prefix.v
@@ -9,7 +9,7 @@ Section PrefixDefinition.
Context {Job : JobType}.
(** ... and any kind of processor model, ... *)
- Context {PState: Type} `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** ... two schedules share an identical prefix if they are pointwise
identical (at least) up to a fixed horizon. *)
diff --git a/analysis/definitions/tardiness.v b/analysis/definitions/tardiness.v
index 6a5519cc3..5970274d4 100644
--- a/analysis/definitions/tardiness.v
+++ b/analysis/definitions/tardiness.v
@@ -18,8 +18,7 @@ Section Tardiness.
Context `{JobTask Job Task}.
(** ... and any kind of processor state. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Further, consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
diff --git a/analysis/definitions/work_bearing_readiness.v b/analysis/definitions/work_bearing_readiness.v
index cf010bd7b..9d5a80b0b 100644
--- a/analysis/definitions/work_bearing_readiness.v
+++ b/analysis/definitions/work_bearing_readiness.v
@@ -18,11 +18,10 @@ Section WorkBearingReadiness.
Context {Job : JobType} {Task : TaskType} `{JobArrival Job} `{JobCost Job}.
(** ... and any kind of processor state. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Further, allow for any notion of job readiness. *)
- Context `{JobReady Job PState}.
+ Context {jr : JobReady Job PState}.
(** Consider any job arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
index 7c7f02d7a..606b93135 100644
--- a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -39,8 +39,7 @@ End ArrivalPredicates.
Section Arrived.
(** Consider any kinds of jobs and any kind of processor state. *)
- Context {Job : JobType} {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {Job : JobType} {PState : ProcessorState Job}.
(** Consider any schedule... *)
Variable sched : schedule PState.
@@ -49,7 +48,7 @@ Section Arrived.
notion of readiness. *)
Context `{JobCost Job}.
Context `{JobArrival Job}.
- Context `{JobReady Job PState}.
+ Context {jr : JobReady Job PState}.
(** First, we note that readiness models are by definition consistent
w.r.t. [pending]. *)
@@ -57,7 +56,7 @@ Section Arrived.
forall j t,
job_ready sched j t -> pending sched j t.
Proof.
- move: H5 => [is_ready CONSISTENT].
+ move: jr => [is_ready CONSISTENT].
move=> j t READY.
apply CONSISTENT.
by exact READY.
@@ -345,4 +344,4 @@ Section ArrivalSequencePrefix.
End ArrivalTimes.
-End ArrivalSequencePrefix.
+End ArrivalSequencePrefix.
diff --git a/analysis/facts/behavior/completion.v b/analysis/facts/behavior/completion.v
index 484910f6d..f7ce9f59f 100644
--- a/analysis/facts/behavior/completion.v
+++ b/analysis/facts/behavior/completion.v
@@ -14,8 +14,7 @@ Section CompletionFacts.
Context `{JobArrival Job}.
(** ...any kind of processor model,... *)
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** ...and a given schedule. *)
Variable sched: schedule PState.
@@ -163,8 +162,7 @@ Section ServiceAndCompletionFacts.
Context `{JobCost Job}.
(** ...any kind of processor model,... *)
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** ...and a given schedule. *)
Variable sched: schedule PState.
@@ -277,8 +275,7 @@ Section PositiveCost.
Context `{JobArrival Job}.
(** ...any kind of processor model,... *)
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** ...and a given schedule. *)
Variable sched: schedule PState.
@@ -325,8 +322,7 @@ End PositiveCost.
Section CompletedJobs.
(** Consider any kinds of jobs and any kind of processor state. *)
- Context {Job : JobType} {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {Job : JobType} {PState : ProcessorState Job}.
(** Consider any schedule... *)
Variable sched : schedule PState.
@@ -335,7 +331,7 @@ Section CompletedJobs.
readiness. *)
Context `{JobCost Job}.
Context `{JobArrival Job}.
- Context `{JobReady Job PState}.
+ Context {jr : JobReady Job PState}.
(** We observe that a given job is ready only if it is also incomplete... *)
Lemma ready_implies_incomplete:
@@ -393,7 +389,8 @@ Global Hint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_f
(** Next, we relate the completion of jobs in schedules with identical prefixes. *)
Section CompletionInTwoSchedules.
(** Consider any processor model and any type of jobs with costs, arrival times, and a notion of readiness. *)
- Context {PState: Type} {Job: JobType} `{ProcessorState Job PState} `{JobReady Job PState}.
+ Context {Job: JobType} {PState: ProcessorState Job}.
+ Context {jc : JobCost Job} {ja : JobArrival Job} {jr : JobReady Job PState}.
(** If two schedules share a common prefix, then (in the prefix) jobs
complete in one schedule iff they complete in the other. *)
@@ -424,5 +421,3 @@ Section CompletionInTwoSchedules.
End CompletionInTwoSchedules.
-
-
diff --git a/analysis/facts/behavior/deadlines.v b/analysis/facts/behavior/deadlines.v
index 1cc4e6374..eab3862b8 100644
--- a/analysis/facts/behavior/deadlines.v
+++ b/analysis/facts/behavior/deadlines.v
@@ -10,8 +10,7 @@ Section DeadlineFacts.
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.
(** ... any given type of processor states. *)
- Context {PState: eqType}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** First, we derive two properties from the fact that a job is incomplete at
some point in time. *)
diff --git a/analysis/facts/behavior/service.v b/analysis/facts/behavior/service.v
index d835330c0..94d0d4fc4 100644
--- a/analysis/facts/behavior/service.v
+++ b/analysis/facts/behavior/service.v
@@ -14,8 +14,7 @@ Section Composition.
(** Consider any job type and any processor state. *)
Context {Job: JobType}.
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** For any given schedule... *)
Variable sched: schedule PState.
@@ -137,8 +136,7 @@ Section UnitService.
(** Consider any job type and any processor state. *)
Context {Job : JobType}.
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Let's consider a unit-service model... *)
Hypothesis H_unit_service: unit_service_proc_model PState.
@@ -239,8 +237,7 @@ Section Monotonicity.
(** Consider any job type and any processor model. *)
Context {Job: JobType}.
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** Consider any given schedule... *)
Variable sched: schedule PState.
@@ -264,8 +261,7 @@ End Monotonicity.
Section RelationToScheduled.
Context {Job: JobType}.
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** Consider any given schedule... *)
Variable sched: schedule PState.
@@ -640,8 +636,7 @@ Section ServiceInTwoSchedules.
(** Consider any job type and any processor model. *)
Context {Job: JobType}.
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** Consider any two given schedules... *)
Variable sched1 sched2: schedule PState.
diff --git a/analysis/facts/busy_interval/busy_interval.v b/analysis/facts/busy_interval/busy_interval.v
index e4e7a001d..7cf5cd230 100644
--- a/analysis/facts/busy_interval/busy_interval.v
+++ b/analysis/facts/busy_interval/busy_interval.v
@@ -40,7 +40,7 @@ Section ExistsBusyIntervalJLFP.
Context `{JLFP_policy Job}.
(** Further, allow for any work-bearing notion of job readiness. *)
- Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+ Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** For simplicity, let's define some local names. *)
@@ -301,7 +301,7 @@ Section ExistsBusyIntervalJLFP.
rewrite -{3}[Δ](sum_of_ones t1) exchange_big //=.
apply/eqP; rewrite eqn_leq; apply/andP; split.
{ rewrite leq_sum // => t' _.
- have SCH := @service_of_jobs_le_1 _ _ _ _ _ sched predT (arrivals_between 0 (t1 + Δ)).
+ have SCH := @service_of_jobs_le_1 _ _ _ _ sched predT (arrivals_between 0 (t1 + Δ)).
by eapply leq_trans; last apply SCH; eauto using arrivals_uniq with basic_facts. }
{ rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=
leq_sum // => t' /andP [/andP [LT GT] _]; apply/sum_seq_gt0P.
diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index e4fe3aeff..2601666fd 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -50,7 +50,7 @@ Section ExistsNoCarryIn.
Let quiet_time := quiet_time arr_seq sched.
(** Further, allow for any work-bearing notion of job readiness. *)
- Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+ Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** Assume that the schedule is work-conserving, ... *)
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index dbb3f5f22..b8d88135e 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -54,7 +54,7 @@ Section PriorityInversionIsBounded.
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
(** Further, allow for any work-bearing notion of job readiness. *)
- Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+ Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** We assume that the schedule is valid and that all jobs come from the arrival sequence. *)
@@ -577,7 +577,7 @@ Section PriorityInversionIsBounded.
have Fact: exists Δ, t' = t1 + Δ.
{ by exists (t' - t1); apply/eqP; rewrite eq_sym; apply/eqP; rewrite subnKC. }
move: Fact => [Δ EQ]; subst t'.
- have NPPJ := @no_intermediate_preemption_point (@service _ _ _ sched jlp (t1 + Δ)).
+ have NPPJ := @no_intermediate_preemption_point (@service _ _ sched jlp (t1 + Δ)).
apply proj1 in CORR; specialize (CORR jlp ARRs).
move: CORR => [_ [_ [T _] ]].
apply T; apply: NPPJ; apply/andP; split.
diff --git a/analysis/facts/model/preemption.v b/analysis/facts/model/preemption.v
index d2feb8504..f38a46af5 100644
--- a/analysis/facts/model/preemption.v
+++ b/analysis/facts/model/preemption.v
@@ -63,7 +63,7 @@ Section PreemptionFacts.
Context {Job : JobType}.
Context `{Arrival : JobArrival Job}.
Context `{Cost : JobCost Job}.
- Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+ Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/facts/model/rbf.v b/analysis/facts/model/rbf.v
index 8dd1a6911..31df27fef 100644
--- a/analysis/facts/model/rbf.v
+++ b/analysis/facts/model/rbf.v
@@ -28,7 +28,7 @@ Section ProofWorkloadBound.
Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
(** ... any schedule corresponding to this arrival sequence, ... *)
- Context {PState : Type} `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
diff --git a/analysis/facts/model/sequential.v b/analysis/facts/model/sequential.v
index 352ac9cb1..c4a79f3a2 100644
--- a/analysis/facts/model/sequential.v
+++ b/analysis/facts/model/sequential.v
@@ -12,8 +12,7 @@ Section ExecutionOrder.
Context `{JobCost Job}.
(** ... and any kind of processor state model. *)
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** Consider any arrival sequence ... *)
diff --git a/analysis/facts/model/service_of_jobs.v b/analysis/facts/model/service_of_jobs.v
index aa7acd2a6..83fca850a 100644
--- a/analysis/facts/model/service_of_jobs.v
+++ b/analysis/facts/model/service_of_jobs.v
@@ -23,8 +23,7 @@ Section GenericModelLemmas.
Context `{JobCost Job}.
(** Consider any kind of processor state model, ... *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** ... any job arrival sequence with consistent arrivals, .... *)
Variable arr_seq : arrival_sequence Job.
@@ -103,8 +102,7 @@ Section UnitServiceModelLemmas.
Context `{JobCost Job}.
(** Consider any kind of unit-service processor state model. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
(** Consider any arrival sequence with consistent arrivals. *)
@@ -245,8 +243,7 @@ Section UnitServiceUniProcessorModelLemmas.
Context `{JobCost Job}.
(** Consider any kind of unit-service uniprocessor state model. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
Hypothesis H_uniprocessor_model : uniprocessor_model PState.
@@ -400,5 +397,4 @@ Section IdealModelLemmas.
by rewrite eqxx.
Qed.
-
End IdealModelLemmas.
diff --git a/analysis/facts/preemption/job/preemptive.v b/analysis/facts/preemption/job/preemptive.v
index 95319c424..bb8fc1366 100644
--- a/analysis/facts/preemption/job/preemptive.v
+++ b/analysis/facts/preemption/job/preemptive.v
@@ -15,8 +15,7 @@ Section FullyPreemptiveModel.
Context `{JobCost Job}.
(** Consider any kind of processor state model, ... *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** ... any job arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
@@ -42,7 +41,7 @@ Section FullyPreemptiveModel.
intros.
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points.
- by rewrite H2; compute.
+ by rewrite H1; compute.
Qed.
(** ... or ε when [job_cost j > 0]. *)
@@ -65,4 +64,4 @@ Section FullyPreemptiveModel.
Qed.
End FullyPreemptiveModel.
-Global Hint Resolve valid_fully_preemptive_model : basic_facts.
\ No newline at end of file
+Global Hint Resolve valid_fully_preemptive_model : basic_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 8dba9cc61..8f8a503d7 100644
--- a/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -17,8 +17,7 @@ Section RunToCompletionThreshold.
Context `{JobPreemptable Job}.
(** Consider any kind of processor state model, ... *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** ... any job arrival sequence, ... *)
Variable arr_seq: arrival_sequence Job.
diff --git a/analysis/facts/preemption/task/preemptive.v b/analysis/facts/preemption/task/preemptive.v
index 8c073c259..512b68311 100644
--- a/analysis/facts/preemption/task/preemptive.v
+++ b/analysis/facts/preemption/task/preemptive.v
@@ -22,8 +22,7 @@ Section FullyPreemptiveModel.
Context `{JobCost Job}.
(** Consider any kind of processor state model, ... *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** ... any job arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/facts/priority/edf.v b/analysis/facts/priority/edf.v
index e36790624..ed19b6a0a 100644
--- a/analysis/facts/priority/edf.v
+++ b/analysis/facts/priority/edf.v
@@ -66,7 +66,7 @@ Section SequentialEDF.
Variable sched : schedule (ideal.processor_state Job).
(** ... allow for any work-bearing notion of job readiness, ... *)
- Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+ Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** ... and assume that the schedule is valid. *)
diff --git a/analysis/facts/priority/sequential.v b/analysis/facts/priority/sequential.v
index 0834ff21c..54acdac97 100644
--- a/analysis/facts/priority/sequential.v
+++ b/analysis/facts/priority/sequential.v
@@ -24,7 +24,7 @@ Section SequentialJLFP.
Variable sched : schedule (ideal.processor_state Job).
(** ... allow for any work-bearing notion of job readiness, ... *)
- Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+ Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** ... and assume that the schedule is valid. *)
diff --git a/analysis/facts/readiness/backlogged.v b/analysis/facts/readiness/backlogged.v
index f7b88aa84..bae0ed03c 100644
--- a/analysis/facts/readiness/backlogged.v
+++ b/analysis/facts/readiness/backlogged.v
@@ -10,10 +10,10 @@ Section BackloggedJobs.
Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
(** ... and any kind of processor model, ... *)
- Context {PState : Type} `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** ... and allow for any notion of job readiness. *)
- Context `{JobReady Job PState}.
+ Context {jr : JobReady Job PState}.
(** Given an arrival sequence and a schedule ... *)
Variable arr_seq : arrival_sequence Job.
@@ -65,7 +65,7 @@ Section NonClairvoyance.
Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
(** ... any kind of processor model, ... *)
- Context {PState : Type} `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** ... and allow for any non-clairvoyant notion of job readiness. *)
Context {RM : JobReady Job PState}.
diff --git a/analysis/facts/readiness/basic.v b/analysis/facts/readiness/basic.v
index 2c83ce771..c3e0d39f5 100644
--- a/analysis/facts/readiness/basic.v
+++ b/analysis/facts/readiness/basic.v
@@ -11,8 +11,7 @@ Section LiuAndLaylandReadiness.
Context {Job : JobType}.
(** ... and any kind of processor state. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Suppose jobs have an arrival time and a cost. *)
Context `{JobArrival Job} `{JobCost Job}.
diff --git a/analysis/facts/readiness/sequential.v b/analysis/facts/readiness/sequential.v
index 219a7244a..9330505d7 100644
--- a/analysis/facts/readiness/sequential.v
+++ b/analysis/facts/readiness/sequential.v
@@ -18,8 +18,7 @@ Section SequentialTasksReadiness.
Context `{JobCost Job}.
(** ... and any kind of processor state. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/facts/transform/edf_opt.v b/analysis/facts/transform/edf_opt.v
index 4350c7c6c..952163fbc 100644
--- a/analysis/facts/transform/edf_opt.v
+++ b/analysis/facts/transform/edf_opt.v
@@ -424,8 +424,7 @@ Section MakeEDFAtFacts.
have ARR_j: job_arrival j <= t_edf by apply fsc_found_job_arrival with (sched := sched) (j1 := j_orig) => //; rewrite scheduled_at_def.
now rewrite -EQ'.
+ move=> SCHED_j.
- apply H_jobs_must_arrive_to_execute.
- now rewrite scheduled_at_def /scheduled_in /pstate_instance.
+ by apply H_jobs_must_arrive_to_execute; rewrite scheduled_at_def.
Qed.
(** We connect the fact that a job is scheduled in [sched'] to the
diff --git a/analysis/facts/transform/replace_at.v b/analysis/facts/transform/replace_at.v
index 3dc797d62..ea0039ef4 100644
--- a/analysis/facts/transform/replace_at.v
+++ b/analysis/facts/transform/replace_at.v
@@ -9,8 +9,7 @@ Section ReplaceAtFacts.
Context {Job : JobType}.
(** ... and any given type of processor states, ... *)
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** ...consider any given reference schedule. *)
Variable sched: schedule PState.
diff --git a/analysis/facts/transform/swaps.v b/analysis/facts/transform/swaps.v
index 575e19c7c..701258520 100644
--- a/analysis/facts/transform/swaps.v
+++ b/analysis/facts/transform/swaps.v
@@ -9,8 +9,7 @@ Section SwappedFacts.
(** For any given type of jobs... *)
Context {Job : JobType}.
(** ... any given type of processor states: *)
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** ...consider any given reference schedule. *)
Variable sched: schedule PState.
@@ -282,8 +281,7 @@ Section SwappedScheduleProperties.
(** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(** ... any given type of processor states: *)
- Context {PState: eqType}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** ...consider any given reference schedule. *)
Variable sched: schedule PState.
@@ -364,8 +362,7 @@ Section EDFSwap.
(** For any given type of jobs with costs and deadlines... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.
(** ... any given type of processor states... *)
- Context {PState: eqType}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** ...consider a given reference schedule... *)
Variable sched: schedule PState.
@@ -469,4 +466,4 @@ Section EDFSwap.
+ by apply uninvolved_implies_deadline_met.
Qed.
- End EDFSwap.
+End EDFSwap.
diff --git a/analysis/transform/prefix.v b/analysis/transform/prefix.v
index 99670dad1..82f976f51 100644
--- a/analysis/transform/prefix.v
+++ b/analysis/transform/prefix.v
@@ -11,8 +11,7 @@ Section SchedulePrefixMap.
Context {Job : JobType}.
(** ... any given type of processor states ... *)
- Context {PState: eqType}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** ... we define a procedure that applies a given function to every
point in a given finite prefix of the schedule.
diff --git a/analysis/transform/swap.v b/analysis/transform/swap.v
index 268bd4d13..8c6dd1704 100644
--- a/analysis/transform/swap.v
+++ b/analysis/transform/swap.v
@@ -9,8 +9,7 @@ Section ReplaceAt.
(** For any given type of jobs... *)
Context {Job : JobType}.
(** ... any given type of processor states, ... *)
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** ...consider any given reference schedule. *)
Variable original_sched: schedule PState.
@@ -23,20 +22,18 @@ Section ReplaceAt.
(** Then the schedule with replacement is simply one that returns the given
[new_state] at [t'], and the original allocation at all other times. *)
- Definition replace_at (t : instant) :=
- if t' == t then new_state else (original_sched t).
+ Definition replace_at : schedule PState :=
+ fun t => if t' == t then new_state else (original_sched t).
End ReplaceAt.
-
(** Based on [replace_at], we define the notion of a schedule with swapped
allocations. *)
Section Swapped.
(** For any given type of jobs... *)
Context {Job : JobType}.
(** ... any given type of processor states, ... *)
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** ...consider any given reference schedule. *)
Variable original_sched: schedule PState.
diff --git a/analysis/transform/wc_trans.v b/analysis/transform/wc_trans.v
index 8a984bb23..4722e1720 100644
--- a/analysis/transform/wc_trans.v
+++ b/analysis/transform/wc_trans.v
@@ -59,7 +59,7 @@ Section WCTransformation.
(** The point-wise transformation procedure: given a schedule and a
time [t1], ensure that the schedule is work-conserving at time
[t1]. *)
- Definition make_wc_at sched t1 :=
+ Definition make_wc_at sched t1 : schedule PState :=
match sched t1 with
| Some j => sched (* leave working instants alone *)
| None =>
diff --git a/behavior/ready.v b/behavior/ready.v
index 049b1d43c..c13bc9143 100644
--- a/behavior/ready.v
+++ b/behavior/ready.v
@@ -9,8 +9,8 @@ Require Export prosa.behavior.service.
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} :=
+Class JobReady (Job : JobType) (PState : ProcessorState Job)
+ {jc : JobCost Job} {ja : JobArrival Job} :=
{
job_ready : schedule PState -> Job -> instant -> bool;
@@ -26,11 +26,10 @@ Class JobReady (Job : JobType) (PState : Type)
backlogged, i.e., ready to run but not executing. *)
Section Backlogged.
(** Consider any kinds of jobs and any kind of processor state. *)
- Context {Job : JobType} {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {Job : JobType} {PState : ProcessorState Job}.
(** Allow for any notion of readiness. *)
- Context `{JobReady Job PState}.
+ Context {jc : JobCost Job} {ja : JobArrival Job} {jr : 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) :=
@@ -44,8 +43,7 @@ End Backlogged.
(** With the readiness concept in place, we define the notion of valid schedules. *)
Section ValidSchedule.
(** Consider any kind of jobs and any kind of processor state. *)
- Context {Job : JobType} {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {Job : JobType} {PState : ProcessorState Job}.
(** Consider any schedule. *)
Variable sched : schedule PState.
@@ -60,8 +58,7 @@ Section ValidSchedule.
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}.
+ Context {jc : JobCost Job} {ja : JobArrival Job} {jr : JobReady Job PState}.
(** ..., whether a job can only be scheduled if it is ready ... *)
Definition jobs_must_be_ready_to_execute :=
diff --git a/behavior/schedule.v b/behavior/schedule.v
index 2353d536b..1eb487cef 100644
--- a/behavior/schedule.v
+++ b/behavior/schedule.v
@@ -20,8 +20,9 @@ Require Export prosa.behavior.arrival_sequence.
In the most simple case (i.e., an ideal uniprocessor state—see
[model/processor/ideal.v]), at any given time, either a particular job is
scheduled or the processor is idle. *)
-Class ProcessorState (Job : JobType) (State : Type) :=
+Class ProcessorState (Job : JobType) :=
{
+ State : Type;
(** A [ProcessorState] instance provides a finite set of cores on which
jobs can be scheduled. In the case of uniprocessors, this is irrelevant
and may be ignored (by convention, the unit type is used as a
@@ -42,6 +43,7 @@ Class ProcessorState (Job : JobType) (State : Type) :=
service_on_implies_scheduled_on :
forall j s r, ~~ scheduled_on j s r -> service_on j s r = 0
}.
+Coercion State : ProcessorState >-> Sortclass.
(** The above definition of the [ProcessorState] interface provides
the predicate [scheduled_on] and the function [service_on], which
@@ -57,7 +59,7 @@ Section ProcessorIn.
(** Consider any type of jobs... *)
Context {Job : JobType}.
(** ...and any type of processor state. *)
- Context {State : Type} `{ProcessorState Job State}.
+ Context {State : ProcessorState Job}.
(** For a given processor state, the [scheduled_in] predicate checks
whether a given job is running on any core in that state. *)
@@ -78,7 +80,8 @@ End ProcessorIn.
each instant to a processor state, which reflects state of the computing
platform at the specific time (e.g., which job is presently scheduled). *)
-Definition schedule (PState : Type) := instant -> PState.
+Definition schedule {Job : JobType} (PState : ProcessorState Job) :=
+ instant -> PState.
(** The following line instructs Coq to not let proofs use knowledge of how
[scheduled_on] and [service_on] are defined. Instead,
diff --git a/behavior/service.v b/behavior/service.v
index b4ff0fa7e..f503d7ef0 100644
--- a/behavior/service.v
+++ b/behavior/service.v
@@ -6,8 +6,7 @@ Section Service.
(** * Service of a Job *)
(** Consider any kind of jobs and any kind of processor state. *)
- Context {Job : JobType} {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {Job : JobType} {PState : ProcessorState Job}.
(** Consider any schedule. *)
Variable sched : schedule PState.
diff --git a/implementation/definitions/generic_scheduler.v b/implementation/definitions/generic_scheduler.v
index 7270f996b..bfd21eaf2 100644
--- a/implementation/definitions/generic_scheduler.v
+++ b/implementation/definitions/generic_scheduler.v
@@ -11,7 +11,7 @@ Require Export prosa.analysis.transform.swap.
Section PointwisePolicy.
(** Consider any type of jobs and type of schedule. *)
Context {Job : JobType}.
- Variable PState : Type.
+ Variable PState : ProcessorState Job.
(** A pointwise scheduling policy is a function that, given a schedule prefix
that is valid up to time [t - 1], decides what to schedule at time
@@ -21,8 +21,7 @@ End PointwisePolicy.
Section GenericSchedule.
(** Consider any type of jobs and type of schedule. *)
- Context {Job : JobType} {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {Job : JobType} {PState : ProcessorState Job}.
(** Suppose we are given a policy function that, given a schedule prefix that
is valid up to time [t - 1], decides what to schedule at time [t]. *)
@@ -52,4 +51,3 @@ Section GenericSchedule.
schedule_up_to t t.
End GenericSchedule.
-
diff --git a/implementation/facts/generic_schedule.v b/implementation/facts/generic_schedule.v
index 7c092d4a9..6de5e8de0 100644
--- a/implementation/facts/generic_schedule.v
+++ b/implementation/facts/generic_schedule.v
@@ -10,8 +10,7 @@ Require Export prosa.analysis.facts.transform.replace_at.
Section GenericScheduleProperties.
(** For any type of jobs and type of schedule, ... *)
- Context {Job : JobType} {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {Job : JobType} {PState : ProcessorState Job}.
(** ... any scheduling policy, and ... *)
Variable policy : PointwisePolicy PState.
@@ -61,7 +60,7 @@ Section GenericScheduleProperties.
elim: h => [LT|h IH LT].
{ rewrite /schedule_up_to rest_of_schedule_invariant // => ZERO.
now subst. }
- { rewrite /schedule_up_to rest_of_schedule_invariant -/(schedule_up_to _ h t);
+ { rewrite /schedule_up_to rest_of_schedule_invariant -/(schedule_up_to _ _ h t);
first by apply IH => //; apply ltn_trans with (n := h.+1).
move=> EQ. move: LT.
now rewrite EQ ltnn. }
diff --git a/model/aggregate/service_of_jobs.v b/model/aggregate/service_of_jobs.v
index 0771d2ce7..83bb8f0ad 100644
--- a/model/aggregate/service_of_jobs.v
+++ b/model/aggregate/service_of_jobs.v
@@ -15,8 +15,7 @@ Section ServiceOfJobs.
Context `{JobTask Job Task}.
(** Consider any kind of processor model, ... *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** ... any job arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
diff --git a/model/preemption/parameter.v b/model/preemption/parameter.v
index be3211a50..46e04302a 100644
--- a/model/preemption/parameter.v
+++ b/model/preemption/parameter.v
@@ -100,8 +100,7 @@ Section PreemptionModel.
Context `{JLDP_policy Job}.
(** Consider any kind of processor model, ... *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** ... any job arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
diff --git a/model/processor/ideal.v b/model/processor/ideal.v
index e41aa0903..8d384aa3c 100644
--- a/model/processor/ideal.v
+++ b/model/processor/ideal.v
@@ -17,33 +17,26 @@ Section State.
(** Consider any type of jobs. *)
Variable Job: JobType.
- (** We define the ideal "processor state" as an [option Job], which means
- that it is either [Some j] (where [j] is a [Job]) or [None] (which we use
- to indicate an idle instant). *)
- Definition processor_state := option Job.
-
- (** Based on this definition, we say that a given job [j] is scheduled in a
- given state [s] iff [s] is [Some j]. *)
- Let ideal_scheduled_at (j : Job) (s : processor_state) := s == Some j.
-
- (** Similarly, we say that a given job [j] receives service in a given state
- [s] iff [s] is [Some j]. *)
- Let ideal_service_in (j : Job) (s : processor_state) := s == Some j.
-
- (** Next, we connect the just-defined notion of an ideal processor state with
+ (** We connect the notion of an ideal processor state with
the generic interface for the processor-state abstraction in Prosa by
declaring a so-called instance of the [ProcessorState] typeclass. *)
- Global Program Instance pstate_instance : ProcessorState Job processor_state :=
+ Global Program Instance processor_state : ProcessorState Job :=
{
+ (** We define the ideal "processor state" as an [option Job],
+ which means that it is either [Some j] (where [j] is a
+ [Job]) or [None] (which we use to indicate an idle
+ instant). *)
+ State := option Job;
(** As this is a uniprocessor model, cores are implicitly defined
as the [unit] type containing a single element as a placeholder. *)
- scheduled_on j s (_ : unit) := ideal_scheduled_at j s;
- service_on j s (_ : unit) := ideal_service_in j s;
+ (** We say that a given job [j] is scheduled in a
+ given state [s] iff [s] is [Some j]. *)
+ scheduled_on j s (_ : unit) := s == Some j;
+ (** Similarly, we say that a given job [j] receives service in a
+ given state [s] iff [s] is [Some j]. *)
+ service_on j s (_ : unit) := s == Some j;
}.
- Next Obligation.
- rewrite /ideal_service_in /nat_of_bool.
- by case: ifP H =>// SOME /negP [].
- Defined.
+ Next Obligation. by rewrite /nat_of_bool; case: ifP H => // ? /negP[]. Qed.
End State.
diff --git a/model/processor/multiprocessor.v b/model/processor/multiprocessor.v
index 5c015eff7..c4cd507ea 100644
--- a/model/processor/multiprocessor.v
+++ b/model/processor/multiprocessor.v
@@ -22,8 +22,7 @@ Section Schedule.
Variable Job: JobType.
(** ... and consider any type of per-processor state. *)
- Variable processor_state: Type.
- Context `{ProcessorState Job processor_state}.
+ Variable processor_state: ProcessorState Job.
(** Given a desired number of processors [num_cpus], we define a finite type
of integers from [0] to [num_cpus - 1]. The purpose of this definition is
@@ -59,16 +58,17 @@ Section Schedule.
(** Finally, we connect the above definitions with the generic Prosa
interface for processor models. *)
- Global Program Instance multiproc_state : ProcessorState Job multiprocessor_state :=
+ Global Program Instance multiproc_state : ProcessorState Job :=
{
+ State := multiprocessor_state;
scheduled_on := multiproc_scheduled_on;
service_on := multiproc_service_on
}.
Next Obligation.
- move: j s r H0.
+ move: j s r H.
move=> j mps cpu.
by apply: service_in_implies_scheduled_in.
- Defined.
+ Qed.
(** From the instance [multiproc_state], we get the function [service_in].
The service received by a given job [j] in a given multiprocessor state
diff --git a/model/processor/platform_properties.v b/model/processor/platform_properties.v
index f33c8dc6b..bc26d070a 100644
--- a/model/processor/platform_properties.v
+++ b/model/processor/platform_properties.v
@@ -10,8 +10,7 @@ Section ProcessorModels.
implicit context) because it is the primary subject of the following
definitions. *)
Context {Job : JobType}.
- Variable PState : Type.
- Context `{ProcessorState Job PState}.
+ Variable PState : ProcessorState Job.
(** We say that a processor model provides unit service if no job ever
receives more than one unit of service at any time. *)
diff --git a/model/processor/spin.v b/model/processor/spin.v
index e570c266c..e3a1faad3 100644
--- a/model/processor/spin.v
+++ b/model/processor/spin.v
@@ -48,8 +48,9 @@ Section State.
(** Finally, we connect the above definitions with the generic Prosa
interface for abstract processor states. *)
- Global Program Instance pstate_instance : ProcessorState Job (processor_state) :=
+ Global Program Instance pstate_instance : ProcessorState Job :=
{
+ State := processor_state;
scheduled_on := spin_scheduled_on;
service_on := spin_service_on
}.
@@ -58,5 +59,5 @@ Section State.
case: s=>//= j' _.
rewrite /nat_of_bool.
by case: ifP.
- Defined.
+ Qed.
End State.
diff --git a/model/processor/varspeed.v b/model/processor/varspeed.v
index bddd7f508..d03f36293 100644
--- a/model/processor/varspeed.v
+++ b/model/processor/varspeed.v
@@ -45,8 +45,9 @@ Section State.
(** Finally, we connect the above definitions to the generic Prosa interface
for processor states. *)
- Global Program Instance pstate_instance : ProcessorState Job processor_state :=
+ Global Program Instance pstate_instance : ProcessorState Job :=
{
+ State := processor_state;
scheduled_on := varspeed_scheduled_on;
service_on := varspeed_service_on
}.
@@ -54,6 +55,6 @@ Section State.
move: r H.
case: s=>//= j' v _.
by case: ifP.
- Defined.
+ Qed.
End State.
diff --git a/model/readiness/basic.v b/model/readiness/basic.v
index e08463dac..05eef0bee 100644
--- a/model/readiness/basic.v
+++ b/model/readiness/basic.v
@@ -11,8 +11,7 @@ Section LiuAndLaylandReadiness.
Context {Job : JobType}.
(** ... and any kind of processor state. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Suppose jobs have an arrival time and a cost. *)
Context `{JobArrival Job} `{JobCost Job}.
@@ -24,4 +23,3 @@ Section LiuAndLaylandReadiness.
}.
End LiuAndLaylandReadiness.
-
diff --git a/model/readiness/jitter.v b/model/readiness/jitter.v
index 82530a73c..ada5b38ce 100644
--- a/model/readiness/jitter.v
+++ b/model/readiness/jitter.v
@@ -23,8 +23,7 @@ Section ReadinessOfJitteryJobs.
Context {Job : JobType}.
(** ... and any kind of processor state. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Suppose jobs have an arrival time, a cost, and exhibit release jitter. *)
Context `{JobArrival Job} `{JobCost Job} `{JobJitter Job}.
@@ -41,10 +40,10 @@ Section ReadinessOfJitteryJobs.
job_ready sched j t := is_released j t && ~~ completed_by sched j t
}.
Next Obligation.
- move: H3 => /andP [REL UNFINISHED].
+ move: H2 => /andP [REL UNFINISHED].
rewrite /pending. apply /andP. split => //.
move: REL. rewrite /is_released /has_arrived.
by apply leq_addk.
- Defined.
+ Qed.
End ReadinessOfJitteryJobs.
diff --git a/model/readiness/sequential.v b/model/readiness/sequential.v
index e6e4aef4d..1a85f7b1b 100644
--- a/model/readiness/sequential.v
+++ b/model/readiness/sequential.v
@@ -19,8 +19,7 @@ Section SequentialTasksReadiness.
Context `{JobCost Job}.
(** ... and any kind of processor state. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Consider any job arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
@@ -34,8 +33,6 @@ Section SequentialTasksReadiness.
pending sched j t &&
prior_jobs_complete arr_seq sched j t
}.
- Next Obligation.
- by move: H3 => /andP [T _].
- Defined.
-
+ Next Obligation. by move: H2 => /andP[]. Qed.
+
End SequentialTasksReadiness.
diff --git a/model/readiness/suspension.v b/model/readiness/suspension.v
index 0db533d8c..43926684f 100644
--- a/model/readiness/suspension.v
+++ b/model/readiness/suspension.v
@@ -22,8 +22,7 @@ Section ReadinessOfSelfSuspendingJobs.
Context {Job : JobType}.
(** ... and any kind of processor state. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Suppose jobs have an arrival time, a cost, and that they exhibit
self-suspensions. *)
@@ -49,11 +48,11 @@ Section ReadinessOfSelfSuspendingJobs.
job_ready sched j t := suspension_has_passed sched j t && ~~ completed_by sched j t
}.
Next Obligation.
- move: H3 => /andP [PASSED UNFINISHED].
+ move: H2 => /andP [PASSED UNFINISHED].
rewrite /pending. apply /andP. split => //.
move: PASSED. rewrite /suspension_has_passed /has_arrived => /andP [ARR _].
by move: ARR; apply leq_addk.
- Defined.
+ Qed.
End ReadinessOfSelfSuspendingJobs.
diff --git a/model/schedule/edf.v b/model/schedule/edf.v
index 632d90adf..947d79c58 100644
--- a/model/schedule/edf.v
+++ b/model/schedule/edf.v
@@ -31,8 +31,7 @@ Section AlternativeDefinitionOfEDF.
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(** ... and any processor model. *)
- Context {PState: eqType}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** We say that a schedule is _locally EDF-compliant_ at a given point in
time [t] if the job [j] scheduled at time [t] has a deadline that is
@@ -59,10 +58,3 @@ Section AlternativeDefinitionOfEDF.
Definition EDF_schedule (sched: schedule PState) := forall t, EDF_at sched t.
End AlternativeDefinitionOfEDF.
-
-
-
-
-
-
-
diff --git a/model/schedule/limited_preemptive.v b/model/schedule/limited_preemptive.v
index cf32cb78a..dbf659caf 100644
--- a/model/schedule/limited_preemptive.v
+++ b/model/schedule/limited_preemptive.v
@@ -12,7 +12,7 @@ Section ScheduleWithLimitedPreemptions.
Context {Job : JobType}.
(** ... any processor model, ... *)
- Context {PState : Type} `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** ... and any preemption model. *)
Context `{JobPreemptable Job}.
diff --git a/model/schedule/nonpreemptive.v b/model/schedule/nonpreemptive.v
index 36c3858e2..803e88a97 100644
--- a/model/schedule/nonpreemptive.v
+++ b/model/schedule/nonpreemptive.v
@@ -13,8 +13,7 @@ Section NonpreemptiveSchedule.
Context `{JobCost Job}.
(** ... and any kind of processor model. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** We say that a given schedule is _nonpreemptive_ if every job,
once it is scheduled, remains scheduled until completion. *)
diff --git a/model/schedule/priority_driven.v b/model/schedule/priority_driven.v
index 14dbe0d96..cb8d74027 100644
--- a/model/schedule/priority_driven.v
+++ b/model/schedule/priority_driven.v
@@ -30,7 +30,7 @@ Section Priority.
(** ... and consider any preemption model and notion of readiness. *)
Context `{JobPreemptable Job}.
- Context `{JobReady Job (ideal.processor_state Job)}.
+ Context {jr : JobReady Job (ideal.processor_state Job)}.
(** Given any job arrival sequence... *)
Variable arr_seq : arrival_sequence Job.
@@ -53,4 +53,3 @@ Section Priority.
hep_job_at t j_hp j.
End Priority.
-
diff --git a/model/schedule/tdma.v b/model/schedule/tdma.v
index 68f5fd46f..5f79fecc1 100644
--- a/model/schedule/tdma.v
+++ b/model/schedule/tdma.v
@@ -113,7 +113,8 @@ Section TDMASchedule.
Context {Task : TaskType} {Job : JobType}.
- Context `{JobArrival Job} `{JobCost Job} `{JobReady Job (option Job)} `{JobTask Job Task}.
+ Context {ja : JobArrival Job} {jc : JobCost Job}.
+ Context {jr : JobReady Job (ideal.processor_state Job)} `{JobTask Job Task}.
(** Consider any job arrival sequence... *)
Variable arr_seq : arrival_sequence Job.
diff --git a/model/schedule/work_conserving.v b/model/schedule/work_conserving.v
index 41f23a3a5..47a97cd57 100644
--- a/model/schedule/work_conserving.v
+++ b/model/schedule/work_conserving.v
@@ -20,11 +20,10 @@ Section WorkConserving.
Context `{JobCost Job}.
(** ... and any kind of processor model. *)
- Context {PState: Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState: ProcessorState Job}.
(** Further, allow for any notion of job readiness. *)
- Context `{JobReady Job PState}.
+ Context {jr : JobReady Job PState}.
(** Given an arrival sequence and a schedule ... *)
Variable arr_seq : arrival_sequence Job.
@@ -47,4 +46,3 @@ Section WorkConserving.
[seq j <- arrivals_up_to arr_seq t | backlogged sched j t].
End WorkConserving.
-
diff --git a/model/task/preemption/parameters.v b/model/task/preemption/parameters.v
index bd034d7df..914978dbf 100644
--- a/model/task/preemption/parameters.v
+++ b/model/task/preemption/parameters.v
@@ -78,8 +78,7 @@ Section ValidPreemptionModel.
Context `{JobPreemptable Job}.
(** Consider any kind of processor state model, ... *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** ... any job arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
@@ -150,8 +149,7 @@ Section ValidTaskRunToCompletionThreshold.
Context `{TaskRunToCompletionThreshold Task}.
(** Further, consider any kind of processor model, ... *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** ... any job arrival sequence, ... *)
Variable arr_seq: arrival_sequence Job.
diff --git a/model/task/sequentiality.v b/model/task/sequentiality.v
index d2562128f..d836729e8 100644
--- a/model/task/sequentiality.v
+++ b/model/task/sequentiality.v
@@ -17,8 +17,7 @@ Section PropertyOfSequentiality.
Context `{JobCost Job}.
(** ... and any kind of processor model. *)
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
+ Context {PState : ProcessorState Job}.
(** Consider any arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
@@ -44,6 +43,5 @@ Section PropertyOfSequentiality.
all
(fun j_tsk => completed_by sched j_tsk t)
(task_arrivals_before arr_seq (job_task j) (job_arrival j)).
-
End PropertyOfSequentiality.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 4b072f3df..40bce6903 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -49,7 +49,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Variable sched : schedule (ideal.processor_state Job).
(** ... allow for any work-bearing notion of job readiness, ... *)
- Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+ Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** ... and assume that the schedule is valid. *)
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 2285d0e24..3f5966098 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -54,7 +54,7 @@ Section AbstractRTAforFPwithArrivalCurves.
Variable sched : schedule (ideal.processor_state Job).
(** ... allow for any work-bearing notion of job readiness, ... *)
- Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+ Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** ... and assume that the schedule is valid. *)
--
GitLab