Commit 47c0d32f authored by Björn Brandenburg's avatar Björn Brandenburg

make processor state explicit in platform properties

This avoids the need to use @-notation when establishing platform
properties (e.g., in facts about ideal schedules).

Thanks to Maxime for the suggestion.
parent 72f608f3
Pipeline #20326 passed with stages
in 5 minutes and 19 seconds
...@@ -75,7 +75,7 @@ Section CompletionFacts. ...@@ -75,7 +75,7 @@ Section CompletionFacts.
* remaining positive cost. *) * remaining positive cost. *)
(** Assume a scheduled job always receives some positive service. *) (** 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. *) (** Then a scheduled job has positive remaining cost. *)
Corollary scheduled_implies_positive_remaining_cost: Corollary scheduled_implies_positive_remaining_cost:
...@@ -139,7 +139,7 @@ Section ServiceAndCompletionFacts. ...@@ -139,7 +139,7 @@ Section ServiceAndCompletionFacts.
Variable j: Job. Variable j: Job.
(** Assume that a scheduled job receives exactly one time unit of service. *) (** 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 (** 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 job's total cost if service increases only by one at each step since
...@@ -206,7 +206,7 @@ Section ServiceAndCompletionFacts. ...@@ -206,7 +206,7 @@ Section ServiceAndCompletionFacts.
Section GuaranteedService. Section GuaranteedService.
(** Assume a scheduled job always receives some positive service. *) (** 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. *) (** Assume that jobs are not released early. *)
Context `{JobArrival Job}. Context `{JobArrival Job}.
...@@ -323,7 +323,7 @@ Section CompletedJobs. ...@@ -323,7 +323,7 @@ Section CompletedJobs.
always receive non-zero service and cumulative service never exceeds job always receive non-zero service and cumulative service never exceeds job
costs. *) costs. *)
Lemma ideal_progress_completed_jobs: Lemma ideal_progress_completed_jobs:
ideal_progress_proc_model -> ideal_progress_proc_model PState ->
(forall j t, service sched j t <= job_cost j) -> (forall j t, service sched j t <= job_cost j) ->
completed_jobs_dont_execute sched. completed_jobs_dont_execute sched.
Proof. Proof.
......
...@@ -22,7 +22,7 @@ Section DeadlineFacts. ...@@ -22,7 +22,7 @@ Section DeadlineFacts.
Hypothesis H_completed_jobs: completed_jobs_dont_execute sched. Hypothesis H_completed_jobs: completed_jobs_dont_execute sched.
(** ...and scheduled jobs always receive service. *) (** ...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 (** 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 its deadline must be later than any point at which it is
......
...@@ -10,7 +10,7 @@ Section ScheduleClass. ...@@ -10,7 +10,7 @@ Section ScheduleClass.
(** We note that the ideal processor model is indeed a uniprocessor (** We note that the ideal processor model is indeed a uniprocessor
model. *) model. *)
Lemma ideal_proc_model_is_a_uniprocessor_model: Lemma ideal_proc_model_is_a_uniprocessor_model:
@uniprocessor_model _ (processor_state Job) _. uniprocessor_model (processor_state Job).
Proof. Proof.
move=> j1 j2 sched t. move=> j1 j2 sched t.
by rewrite /scheduled_at=> /eqP-> /eqP[->]. by rewrite /scheduled_at=> /eqP-> /eqP[->].
...@@ -20,7 +20,7 @@ Section ScheduleClass. ...@@ -20,7 +20,7 @@ Section ScheduleClass.
of ideal-progress models, i.e., a scheduled job always receives of ideal-progress models, i.e., a scheduled job always receives
service. *) service. *)
Lemma ideal_proc_model_ensures_ideal_progress: Lemma ideal_proc_model_ensures_ideal_progress:
@ideal_progress_proc_model _ (processor_state Job) _. ideal_progress_proc_model (processor_state Job).
Proof. Proof.
move=> j s /eqP /eqP SOME. move=> j s /eqP /eqP SOME.
by rewrite /service_in /pstate_instance SOME. by rewrite /service_in /pstate_instance SOME.
...@@ -28,7 +28,7 @@ Section ScheduleClass. ...@@ -28,7 +28,7 @@ Section ScheduleClass.
(** The ideal processor model is a unit-service model. *) (** The ideal processor model is a unit-service model. *)
Lemma ideal_proc_model_provides_unit_service: Lemma ideal_proc_model_provides_unit_service:
@unit_service_proc_model _ (processor_state Job) _. unit_service_proc_model (processor_state Job).
Proof. Proof.
move=> j s. move=> j s.
rewrite /service_in /pstate_instance. rewrite /service_in /pstate_instance.
...@@ -36,3 +36,4 @@ Section ScheduleClass. ...@@ -36,3 +36,4 @@ Section ScheduleClass.
Qed. Qed.
End ScheduleClass. End ScheduleClass.
...@@ -140,7 +140,7 @@ Section UnitService. ...@@ -140,7 +140,7 @@ Section UnitService.
Context `{ProcessorState Job PState}. Context `{ProcessorState Job PState}.
(** Let's consider a unit-service model... *) (** 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. *) (** ...and a given schedule. *)
Variable sched: schedule PState. Variable sched: schedule PState.
...@@ -343,7 +343,7 @@ Section RelationToScheduled. ...@@ -343,7 +343,7 @@ Section RelationToScheduled.
further prove the converse. *) further prove the converse. *)
(** Assume j always receives some positive service. *) (** 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 (** In other words, not being scheduled is equivalent to receiving zero
service. *) service. *)
...@@ -552,7 +552,7 @@ Section RelationToScheduled. ...@@ -552,7 +552,7 @@ Section RelationToScheduled.
we can translate this into a claim about scheduled_at. *) we can translate this into a claim about scheduled_at. *)
(** Assume j always receives some positive service. *) (** 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 (** We show that job j is scheduled at some point t < t1 iff j is scheduled
at some point t' < t2. *) at some point t' < t2. *)
......
...@@ -53,7 +53,7 @@ Section GenericModelLemmas. ...@@ -53,7 +53,7 @@ Section GenericModelLemmas.
(** Assume that the processor model is a unit service moodel. I.e., (** 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. *) 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. *) (** Then, we prove that the service received by those jobs is no larger than their workload. *)
Lemma service_of_jobs_le_workload: Lemma service_of_jobs_le_workload:
......
...@@ -330,8 +330,8 @@ Section SwappedScheduleProperties. ...@@ -330,8 +330,8 @@ Section SwappedScheduleProperties.
swap, assuming an ideal unit-service model (i.e., scheduled jobs receive swap, assuming an ideal unit-service model (i.e., scheduled jobs receive
exactly one unit of service). *) exactly one unit of service). *)
Lemma swapped_completed_jobs_dont_execute: Lemma swapped_completed_jobs_dont_execute:
unit_service_proc_model -> unit_service_proc_model PState ->
ideal_progress_proc_model -> ideal_progress_proc_model PState ->
completed_jobs_dont_execute sched -> completed_jobs_dont_execute sched ->
completed_jobs_dont_execute sched'. completed_jobs_dont_execute sched'.
Proof. Proof.
...@@ -376,7 +376,7 @@ Section EDFSwap. ...@@ -376,7 +376,7 @@ Section EDFSwap.
completed_jobs_dont_execute sched. completed_jobs_dont_execute sched.
(** ...and scheduled jobs always receive service. *) (** ...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]... *) (** Suppose we are given two specific times [t1] and [t2]... *)
Variable t1 t2: instant. Variable t1 t2: instant.
......
...@@ -3,9 +3,12 @@ From rt.restructuring.behavior Require Export all. ...@@ -3,9 +3,12 @@ From rt.restructuring.behavior Require Export all.
(** To reason about classes of schedule types / processor models, we define the (** To reason about classes of schedule types / processor models, we define the
following properties that a processor model might possess. *) following properties that a processor model might possess. *)
Section ProcessorModels. 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 {Job : JobType}.
Context {PState : Type}. Variable PState : Type.
Context `{ProcessorState Job PState}. Context `{ProcessorState Job PState}.
(** We say that a processor model provides unit service if no (** We say that a processor model provides unit service if no
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment