# Library prosa.model.schedule.preemption_time

# Preemption Times

*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.

Consider any type of jobs, ...

... any preemption model, ...

... and any ideal uniprocessor schedule of such jobs.

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 sched t is Some j then

job_preemptable j (service sched j t)

else true.

End PreemptionTime.

if sched t is Some j then

job_preemptable j (service sched j t)

else true.

End PreemptionTime.