Library prosa.model.schedule.nonpreemptive

Require Export prosa.behavior.all.

Nonpreemptive Schedules

In this module, we introduce a simple alternative definition of nonpreemptive schedules. Take also note of the fully nonpreemptive preemption model in model.preemption.fully_nonpreemptive.
Consider any type of jobs with execution costs ...
  Context {Job : JobType}.
  Context `{JobCost Job}.

... and any kind of processor model.
  Context {PState : ProcessorState Job}.

We say that a given schedule is nonpreemptive if every job, once it is scheduled, remains scheduled until completion.
  Definition nonpreemptive_schedule (sched : schedule PState) :=
     (j : Job) (t t' : instant),
      t t'
      scheduled_at sched j t
      ~~ completed_by sched j t'
      scheduled_at sched j t'.

End NonpreemptiveSchedule.