Library prosa.model.schedule.preemption_time

Require Export prosa.model.schedule.scheduled.
Require Export prosa.model.preemption.parameter.

Preemption Times

The preemption framework defines a generic predicate job_preemptable as the interface to various preemption models. Crucially, job_preemptable does not depend on the current schedule or the current time, but only on the job's progress, i.e., it indicates the presence or absence of a preemption point in the job's execution. In this section, we define the notion of a preemption time in an ideal uniprocessor schedule base on the progress of the currently scheduled job.

NB: For legacy reasons, the following definition are currently specific to ideal uniprocessor schedules. Lifting this assumption is future work (https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/76).

Section PreemptionTime.

Consider any type of jobs, ...

Context {Job : JobType}.

... any preemption model, ...

Context `{JobPreemptable Job}.

... any arrival sequence, ...

Variable arr_seq : arrival_sequence Job.

... any processor model, ...

Context {PState : ProcessorState Job}.

... and any schedule.

Variable sched : schedule PState.

We say that a time t is a preemption time iff the job that is currently scheduled at t, if any, can be preempted according to the predicate job_preemptable (which encodes the preemption model). An idle instant is always a preemption time.

  Definition preemption_time (t : instant) :=
    if (scheduled_job_at arr_seq sched t) is Some j then
      job_preemptable j (service sched j t)
    else true.

End PreemptionTime.