Commit 780f7045 authored by Björn Brandenburg's avatar Björn Brandenburg

port only_one_job_scheduled for the ideal schedule

parent 2d5026a8
Require Export rt.behavior.facts.service.
Require Export rt.behavior.facts.completion.
Require Export rt.behavior.facts.ideal_schedule.
From rt.behavior.schedule Require Import schedule ideal.
(* 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. *)
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.
(* 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. Proof. rewrite /scheduled_at
/scheduled_in /pstate_instance => t /eqP -> /eqP EQ. by inversion EQ.
Qed.
End OnlyOneJobScheduled.
......@@ -17,5 +17,7 @@ Section State.
}.
Proof.
by move=> j [j'->|].
Qed.
Defined.
End State.
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