# Library prosa.model.schedule.preemption_time

# Preemption Times on a Uniprocessor

*point*in the job's execution. In this section, we define the notion of a preemption

*time*in a uniprocessor schedule based on the progress of the currently scheduled job.

Consider any type of jobs, ...

... any preemption model, ...

... any arrival sequence, ...

... any processor model, ...

... and any schedule.

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.

if (scheduled_job_at arr_seq sched t) is Some j then

job_preemptable j (service sched j t)

else true.

End PreemptionTime.