Library prosa.analysis.facts.priority.edf

In this section, we prove a few properties about EDF policy.

Consider any type of tasks with relative deadlines ...

... and any type of jobs associated with these tasks.

Consider any arrival sequence.

EDF respects sequential tasks hypothesis.

We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply it automatically.

In this section, we prove that EDF priority policy implies that tasks are sequential.

Consider any type of tasks ...

... with a bound on the maximum non-preemptive segment length. The bound is needed to ensure that, at any instant, it always exists a subsequent preemption time in which the scheduler can, if needed, switch to another higher-priority job.

Further, consider any type of jobs associated with these tasks.

Consider any arrival sequence.

Next, consider any ideal uni-processor schedule of this arrival sequence, ...

... allow for any work-bearing notion of job readiness, ...

... and assume that the schedule is valid.

In addition, we assume the existence of a function mapping jobs to their preemption points ...

... and assume that it defines a valid preemption model with bounded non-preemptive segments.

Next, we assume that the schedule respects the scheduling policy at every preemption point.

To prove sequentiality, we use lemma early_hep_job_is_scheduled. Clearly, under the EDF priority policy, jobs satisfy the conditions described by the lemma (i.e., given two jobs j1 and j2 from the same task, if j1 arrives earlier than j2, then j1 always has a higher priority than job j2, and hence completes before j2); therefore EDF implies sequential tasks.