# Library prosa.model.schedule.preemption_time

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

# Preemption Times on a Uniprocessor

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 a uniprocessor schedule based on the progress of the currently scheduled job.
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.