Library rt.restructuring.model.schedule.priority_based.preemption_aware
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.behavior Require Import all.
From rt.restructuring.model Require Import priorities processor.ideal.
From rt.restructuring.model.preemption Require Import preemption_time job.parameters.
We now define what it means for a schedule to respect a priority
in the presence of jobs with non-preemptive segments. 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.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
Context `{JobReady Job (ideal.processor_state Job)}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
Context `{JobReady Job (ideal.processor_state Job)}.
Consider any job arrival sequence...
...and any uniprocessor schedule of these jobs.
We say that a JLDP policy ...
...is respected by the schedule iff, at every preemption point,
a scheduled task has higher (or same) priority than (as) any
backlogged job.
Definition respects_policy_at_preemption_point :=
∀ j j_hp t,
arrives_in arr_seq j →
preemption_time sched t →
backlogged sched j t →
scheduled_at sched j_hp t →
hep_job_at t j_hp j.
End Priority.
∀ j j_hp t,
arrives_in arr_seq j →
preemption_time sched t →
backlogged sched j t →
scheduled_at sched j_hp t →
hep_job_at t j_hp j.
End Priority.