Library rt.restructuring.model.preemption.fully_nonpreemptive
Platform for Fully Non-Preemptive Model
In this section, we instantiate job_preemptable for the fully non-preemptive model.
Consider any type of jobs.
We say that the model is fully non-preemptive iff no job
can be preempted until its completion.
Global Instance fully_nonpreemptive_model : JobPreemptable Job :=
{
job_preemptable (j : Job) (ρ : work) := (ρ == 0) || (ρ == job_cost j)
}.
End FullyNonPreemptiveModel.
{
job_preemptable (j : Job) (ρ : work) := (ρ == 0) || (ρ == job_cost j)
}.
End FullyNonPreemptiveModel.