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);
      idle_in s := \sum_(cpu < num_cpus) idle_in (s cpu)
    }.
End Schedule.