# Library prosa.analysis.facts.priority.edf

Require Import prosa.model.priority.edf.

Require Import prosa.model.task.absolute_deadline.

Require Import prosa.model.task.preemption.parameters.

Require Import prosa.model.task.absolute_deadline.

Require Import prosa.model.task.preemption.parameters.

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.

Context {Job : JobType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

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.

Global Hint Resolve EDF_respects_sequential_tasks : basic_rt_facts.

Require Export prosa.model.task.sequentiality.

Require Export prosa.analysis.facts.busy_interval.priority_inversion.

Require Export prosa.analysis.facts.priority.sequential.

Require Export prosa.model.task.sequentiality.

Require Export prosa.analysis.facts.busy_interval.priority_inversion.

Require Export prosa.analysis.facts.priority.sequential.

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.

Context {Job : JobType}.

Context `{JobTask Job Task}.

Context `{Arrival : JobArrival Job}.

Context `{Cost : JobCost Job}.

Context `{JobTask Job Task}.

Context `{Arrival : JobArrival Job}.

Context `{Cost : JobCost Job}.

Consider any arrival sequence.

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

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

Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.

Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

... 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.