Library rt.restructuring.model.preemption.fully_preemptive
Platform for Fully Premptive Model
In this section, we instantiate job_preemptable for the fully preemptive model.
Consider any type of jobs.
In the fully preemptive model any job can be preempted at any time.
Global Program Instance fully_preemptive_model : JobPreemptable Job :=
{
job_preemptable (j : Job) (ρ : work) := true
}.
End FullyPreemptiveModel.
{
job_preemptable (j : Job) (ρ : work) := true
}.
End FullyPreemptiveModel.