Library prosa.model.schedule.limited_preemptive

Require Export prosa.model.preemption.parameter.

Preemption Model Compliance

A preemption model restricts when jobs can be preempted. In this module, we specify the corresponding semantics, i.e., how a valid schedule must be restricted to be compliant with a given preemption model.
Section ScheduleWithLimitedPreemptions.

Consider any type of jobs, ...
  Context {Job : JobType}.

... any processor model, ...
  Context {PState : ProcessorState Job}.

... and any preemption model.
  Context `{JobPreemptable Job}.

Consider any arrival sequence ...
  Variable arr_seq : arrival_sequence Job.

... and a schedule of the jobs in the arrival sequence.
  Variable sched : schedule PState.

We say that a schedule respects the preemption model given by job_preemptable if non-preemptable jobs remain scheduled.
  Definition schedule_respects_preemption_model :=
    ∀ j t,
      arrives_in arr_seq j →
      ~~ job_preemptable j (service sched j t) →
      scheduled_at sched j t.

End ScheduleWithLimitedPreemptions.