Commit 8915b81d authored by Björn Brandenburg's avatar Björn Brandenburg

make processor state instances global and transparent

parent 7ba40605
......@@ -10,7 +10,7 @@ Section State.
Definition processor_state := option Job.
Instance pstate_instance : ProcessorState Job (option Job) :=
Global Instance pstate_instance : ProcessorState Job (option Job) :=
{
scheduled_in j s := s == Some j;
service_in j s := s == Some j
......
......@@ -13,7 +13,7 @@ Section Schedule.
Definition identical_state := processor num_cpus -> processor_state.
Instance multiproc_state : ProcessorState Job (identical_state) :=
Global Instance multiproc_state : ProcessorState Job (identical_state) :=
{
scheduled_in j s := [exists cpu, scheduled_in j (s cpu)];
service_in j s := \sum_(cpu < num_cpus) service_in j (s cpu)
......@@ -27,5 +27,5 @@ Section Schedule.
case: (boolP (scheduled_in _ _))=>//= Habs.
exfalso; apply: Hsched.
by exists c.
Qed.
Defined.
End Schedule.
......@@ -31,12 +31,12 @@ Section State.
End Service.
Instance pstate_instance : ProcessorState Job (processor_state) :=
Global Instance pstate_instance : ProcessorState Job (processor_state) :=
{
scheduled_in := scheduled_in;
service_in := service_in
}.
Proof.
by move=> j [|j'|j']//=->.
Qed.
Defined.
End State.
......@@ -27,12 +27,12 @@ Section State.
End Service.
Instance pstate_instance : ProcessorState Job processor_state :=
Global Instance pstate_instance : ProcessorState Job processor_state :=
{
scheduled_in := scheduled_in;
service_in := service_in
}.
Proof.
by move=> j []//= j' s->.
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