Library rt.restructuring.model.schedule.priority_based.preemptive
(* We now define what it means for a schedule to respect a priority *)
(* We only define it for a JLDP policy since the definitions for JLDP and JLFP are the same
and can be used through the conversions *)
Section Priority.
Context {Job: JobType} {Task: TaskType}.
Context `{JobCost Job} `{JobArrival Job}.
Context `{JLDP_policy Job}.
Variable arr_seq : arrival_sequence Job.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
Context `{JobReady Job PState}.
Variable sched : schedule PState.
Definition respects_preemptive_priorities :=
∀ j j_hp t,
arrives_in arr_seq j →
backlogged sched j t →
scheduled_at sched j_hp t →
hep_job_at t j_hp j.
End Priority.