Library rt.restructuring.behavior.schedule.multiprocessor
Section Schedule.
Variable Job: JobType.
Variable processor_state: Type.
Context `{ProcessorState Job processor_state}.
Definition processor (num_cpus: nat) := 'I_num_cpus.
Variable num_cpus : nat.
Definition identical_state := processor num_cpus → processor_state.
Global Instance multiproc_state : ProcessorState Job (identical_state) :=
{
scheduled_in j s := [∃ cpu, scheduled_in j (s cpu)];
service_in j s := \sum_(cpu < num_cpus) service_in j (s cpu)
}.
End Schedule.