diff --git a/restructuring/analysis/basic_facts/completion.v b/restructuring/analysis/basic_facts/completion.v
index eeec87ba7467579b65c7c88fdb428b99a2a58dab..bb9ed0f1f2eead62c4eeb6c0c955d91ede6c2a18 100644
--- a/restructuring/analysis/basic_facts/completion.v
+++ b/restructuring/analysis/basic_facts/completion.v
@@ -75,7 +75,7 @@ Section CompletionFacts.
* remaining positive cost. *)
(** Assume a scheduled job always receives some positive service. *)
- Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
+ Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
(** Then a scheduled job has positive remaining cost. *)
Corollary scheduled_implies_positive_remaining_cost:
@@ -139,7 +139,7 @@ Section ServiceAndCompletionFacts.
Variable j: Job.
(** Assume that a scheduled job receives exactly one time unit of service. *)
- Hypothesis H_unit_service: unit_service_proc_model.
+ Hypothesis H_unit_service: unit_service_proc_model PState.
(** To begin with, we establish that the cumulative service never exceeds a
job's total cost if service increases only by one at each step since
@@ -206,7 +206,7 @@ Section ServiceAndCompletionFacts.
Section GuaranteedService.
(** Assume a scheduled job always receives some positive service. *)
- Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
+ Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
(** Assume that jobs are not released early. *)
Context `{JobArrival Job}.
@@ -323,7 +323,7 @@ Section CompletedJobs.
always receive non-zero service and cumulative service never exceeds job
costs. *)
Lemma ideal_progress_completed_jobs:
- ideal_progress_proc_model ->
+ ideal_progress_proc_model PState ->
(forall j t, service sched j t <= job_cost j) ->
completed_jobs_dont_execute sched.
Proof.
diff --git a/restructuring/analysis/basic_facts/deadlines.v b/restructuring/analysis/basic_facts/deadlines.v
index 40b86d777565533bc079b30838fc2d08add8a6b2..afe7ed64c058e20d7f8a2125d1d1ded767e5337d 100644
--- a/restructuring/analysis/basic_facts/deadlines.v
+++ b/restructuring/analysis/basic_facts/deadlines.v
@@ -22,7 +22,7 @@ Section DeadlineFacts.
Hypothesis H_completed_jobs: completed_jobs_dont_execute sched.
(** ...and scheduled jobs always receive service. *)
- Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
+ Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
(** We observe that, if a job is known to meet its deadline, then
its deadline must be later than any point at which it is
diff --git a/restructuring/analysis/basic_facts/ideal_schedule.v b/restructuring/analysis/basic_facts/ideal_schedule.v
index f74ecf24627d61013ea5db0a8edf704004c8d17b..abda98b04691fd0b844ab5c9e54c3560f753d3a0 100644
--- a/restructuring/analysis/basic_facts/ideal_schedule.v
+++ b/restructuring/analysis/basic_facts/ideal_schedule.v
@@ -10,7 +10,7 @@ Section ScheduleClass.
(** We note that the ideal processor model is indeed a uniprocessor
model. *)
Lemma ideal_proc_model_is_a_uniprocessor_model:
- @uniprocessor_model _ (processor_state Job) _.
+ uniprocessor_model (processor_state Job).
Proof.
move=> j1 j2 sched t.
by rewrite /scheduled_at=> /eqP-> /eqP[->].
@@ -20,7 +20,7 @@ Section ScheduleClass.
of ideal-progress models, i.e., a scheduled job always receives
service. *)
Lemma ideal_proc_model_ensures_ideal_progress:
- @ideal_progress_proc_model _ (processor_state Job) _.
+ ideal_progress_proc_model (processor_state Job).
Proof.
move=> j s /eqP /eqP SOME.
by rewrite /service_in /pstate_instance SOME.
@@ -28,7 +28,7 @@ Section ScheduleClass.
(** The ideal processor model is a unit-service model. *)
Lemma ideal_proc_model_provides_unit_service:
- @unit_service_proc_model _ (processor_state Job) _.
+ unit_service_proc_model (processor_state Job).
Proof.
move=> j s.
rewrite /service_in /pstate_instance.
@@ -36,3 +36,4 @@ Section ScheduleClass.
Qed.
End ScheduleClass.
+
diff --git a/restructuring/analysis/basic_facts/service.v b/restructuring/analysis/basic_facts/service.v
index 533c860f1f1a445d0be7f1fbad62959fbc5ddfca..a054fb7a1bd871ff9b81f15dafa49b688c4eedc4 100644
--- a/restructuring/analysis/basic_facts/service.v
+++ b/restructuring/analysis/basic_facts/service.v
@@ -140,7 +140,7 @@ Section UnitService.
Context `{ProcessorState Job PState}.
(** Let's consider a unit-service model... *)
- Hypothesis H_unit_service: unit_service_proc_model.
+ Hypothesis H_unit_service: unit_service_proc_model PState.
(** ...and a given schedule. *)
Variable sched: schedule PState.
@@ -343,7 +343,7 @@ Section RelationToScheduled.
further prove the converse. *)
(** Assume j always receives some positive service. *)
- Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
+ Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
(** In other words, not being scheduled is equivalent to receiving zero
service. *)
@@ -552,7 +552,7 @@ Section RelationToScheduled.
we can translate this into a claim about scheduled_at. *)
(** Assume j always receives some positive service. *)
- Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
+ Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
(** We show that job j is scheduled at some point t < t1 iff j is scheduled
at some point t' < t2. *)
diff --git a/restructuring/analysis/basic_facts/service_of_jobs.v b/restructuring/analysis/basic_facts/service_of_jobs.v
index dea898eb415295c56d2df1f2dbb933f538db30da..af2d4468b4b066bc7d66b7c0b65b9bfe7e94f869 100644
--- a/restructuring/analysis/basic_facts/service_of_jobs.v
+++ b/restructuring/analysis/basic_facts/service_of_jobs.v
@@ -53,7 +53,7 @@ Section GenericModelLemmas.
(** Assume that the processor model is a unit service moodel. I.e.,
no job ever receives more than one unit of service at any time. *)
- Hypothesis H_unit_service : unit_service_proc_model.
+ Hypothesis H_unit_service : unit_service_proc_model PState.
(** Then, we prove that the service received by those jobs is no larger than their workload. *)
Lemma service_of_jobs_le_workload:
diff --git a/restructuring/analysis/transform/facts/swaps.v b/restructuring/analysis/transform/facts/swaps.v
index b104c1093d5aa8274ea63a2d3257447b9b34f482..6f02a1014f92f08fd7691582921d1ee0024b2c18 100644
--- a/restructuring/analysis/transform/facts/swaps.v
+++ b/restructuring/analysis/transform/facts/swaps.v
@@ -330,8 +330,8 @@ Section SwappedScheduleProperties.
swap, assuming an ideal unit-service model (i.e., scheduled jobs receive
exactly one unit of service). *)
Lemma swapped_completed_jobs_dont_execute:
- unit_service_proc_model ->
- ideal_progress_proc_model ->
+ unit_service_proc_model PState ->
+ ideal_progress_proc_model PState ->
completed_jobs_dont_execute sched ->
completed_jobs_dont_execute sched'.
Proof.
@@ -376,7 +376,7 @@ Section EDFSwap.
completed_jobs_dont_execute sched.
(** ...and scheduled jobs always receive service. *)
- Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
+ Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
(** Suppose we are given two specific times [t1] and [t2]... *)
Variable t1 t2: instant.
diff --git a/restructuring/model/processor/platform_properties.v b/restructuring/model/processor/platform_properties.v
index 9beb1443c676f4b19f678157c0088919d7e2f167..f79e30e2319d38f04f2e1fec88a447b115af9d97 100644
--- a/restructuring/model/processor/platform_properties.v
+++ b/restructuring/model/processor/platform_properties.v
@@ -3,9 +3,12 @@ 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. *)
Section ProcessorModels.
- (** Consider any job type and any processor state. *)
+ (** Consider any job type and any processor state. Note: we make the
+ processor state an explicit variable (rather than implicit
+ context) because it is the primary subject of the following
+ definitions. *)
Context {Job : JobType}.
- Context {PState : Type}.
+ Variable PState : Type.
Context `{ProcessorState Job PState}.
(** We say that a processor model provides unit service if no