Commit 503b22a1 authored by Björn Brandenburg's avatar Björn Brandenburg

start classification of processor models

To allow reasoning about an entire class of types of schedules /
processor modules, it's useful to have named definitions for various
invariants that processor models ensure. Let's collect these centrally
where we introduce processor models and schedules.
parent bbefd14d
......@@ -74,8 +74,7 @@ Section CompletionFacts.
* remaining positive cost. *)
(* Assume a scheduled job always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced:
forall j s, scheduled_in j s -> service_in j s > 0.
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
(* Then a scheduled job has positive remaining cost. *)
Corollary scheduled_implies_positive_remaining_cost:
......@@ -132,7 +131,7 @@ End CompletionFacts.
Section ServiceAndCompletionFacts.
(** In this section, we establish some facts that are really about service,
but are also related to completion and rely on some of the above lemmas.
Hence they are in this file, rather than service_facts.v. *)
Hence they are in this file rather than in the service facts file. *)
(* Consider any job type,...*)
Context {Job: JobType}.
......@@ -158,8 +157,7 @@ Section ServiceAndCompletionFacts.
Section GuaranteedService.
(* Assume a scheduled job always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced:
forall j s, scheduled_in j s -> service_in j s > 0.
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
(* Then we can easily show that the service never exceeds the total cost of
the job. *)
......
From rt.restructuring.behavior.schedule Require Import ideal.
From rt.restructuring.behavior.schedule Require Import ideal platform_properties.
(* Note: we do not re-export the basic definitions to avoid littering the global
namespace with type class instances. *)
(* In this section we show that an ideal schedule is unique at any point. *)
Section OnlyOneJobScheduled.
(* Consider any job type and the ideal processor
model. *)
(* In this section we estlish the classes to which an ideal schedule belongs. *)
Section ScheduleClass.
(* Consider any job type and the ideal processor model. *)
Context {Job: JobType}.
(* Consider an ideal schedule... *)
Variable sched: schedule (processor_state Job).
(* ...and two given jobs that are to be scheduled. *)
Variable j1 j2: Job.
(* We note that the ideal processor model is a uniprocessor
model. *)
Lemma ideal_proc_model_is_a_uniprocessor_model:
@uniprocessor_model _ (processor_state Job) _.
Proof.
move=> j1 j2 sched t.
by rewrite /scheduled_at=> /eqP-> /eqP[->].
Qed.
(* At any time t, if both j1 and j2 are scheduled, then they must be the same
job. *)
Lemma only_one_job_scheduled:
forall t,
scheduled_at sched j1 t ->
scheduled_at sched j2 t ->
j1 = j2.
(* We observe that the ideal processor model falls into the category
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) _.
Proof.
by rewrite /scheduled_at=>t/eqP->/eqP[->].
move=> j s /eqP /eqP SOME.
by rewrite /service_in /pstate_instance SOME.
Qed.
End OnlyOneJobScheduled.
End ScheduleClass.
From mathcomp Require Import ssrnat ssrbool fintype.
From rt.restructuring.behavior Require Export schedule.
From rt.restructuring.behavior Require Export schedule schedule.platform_properties.
From rt.util Require Import tactics step_function sum.
(** In this file, we establish basic facts about the service received by
......@@ -138,10 +138,6 @@ Section UnitService.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
(* We say that a kind processor state provides unit service if no
job ever receives more than one unit of service at any time. *)
Definition unit_service_proc_model := forall j s, service_in j s <= 1.
(* Let's consider a unit-service model... *)
Hypothesis H_unit_service: unit_service_proc_model.
......@@ -347,8 +343,7 @@ Section RelationToScheduled.
further prove the converse. *)
(* Assume j always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced:
forall s, scheduled_in j s -> service_in j s > 0.
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
(* In other words, not being scheduled is equivalent to receiving zero
service. *)
......@@ -360,7 +355,7 @@ Section RelationToScheduled.
split => [NOT_SCHED | NO_SERVICE].
- apply negbTE in NOT_SCHED.
by rewrite service_implies_scheduled //.
- apply (contra (H_scheduled_implies_serviced (sched t))).
- apply (contra (H_scheduled_implies_serviced j (sched t))).
by rewrite -eqn0Ngt; apply /eqP => //.
Qed.
......@@ -392,7 +387,7 @@ Section RelationToScheduled.
rewrite service_during_service_at.
exists t'; split => //.
move: SCHED. rewrite /scheduled_at /service_at.
by apply (H_scheduled_implies_serviced (sched t')).
by apply (H_scheduled_implies_serviced j (sched t')).
Qed.
(* ...which again applies to total service, too. *)
......@@ -558,8 +553,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:
forall s, scheduled_in j s -> service_in j s > 0.
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
(* We show that job j is scheduled at some point t < t1 iff j is scheduled
at some point t' < t2. *)
......@@ -572,7 +566,7 @@ Section RelationToScheduled.
{
move=> B. apply/idP/idP => /existsP [b P]; apply /existsP; exists b.
- by move: P; rewrite /scheduled_at /service_at;
apply (H_scheduled_implies_serviced (sched b)).
apply (H_scheduled_implies_serviced j (sched b)).
- by apply service_at_implies_scheduled_at.
}
rewrite !CONV.
......
From rt.restructuring.behavior Require Export schedule.
(* 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. *)
Context {Job: JobType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
(* We say that a processor model provides unit service if no
job ever receives more than one unit of service at any time. *)
Definition unit_service_proc_model :=
forall j s, service_in j s <= 1.
(* We say that a processor model offers ideal progress if a scheduled job
always receives non-zero service. *)
Definition ideal_progress_proc_model :=
forall j s, scheduled_in j s -> service_in j s > 0.
(* In a uniprocessor model, the scheduled job is always unique. *)
Definition uniprocessor_model :=
forall j1 j2 s t,
scheduled_at s j1 t ->
scheduled_at s j2 t ->
j1 = j2.
End ProcessorModels.
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