Library prosa.analysis.facts.priority.edf

We first make some trivial observations about EDF priorities to avoid repeating these steps in subsequent proofs.

Consider any type of jobs with arrival times.

First, consider the general case where jobs have arbitrary deadlines.

Assume EDF priorities based on (arbitrary) job_deadline parameters.

Under EDF, higher-or-equal priority implies no later absolute deadline.

The EDF policy is reflexive by assumption.

The EDF policy is transitive by assumption.

The EDF policy is total by assumption.

A job with a strictly earlier deadline has higher-or-equal priority.

Conversely, if a job does not have higher-or-equal priority, then the other job has no later deadline.

Second, consider the case where job (absolute) deadlines are derived from task (relative) deadlines.

If the jobs stem from tasks with relative deadlines ...

If EDF priorities are derived from task_deadline, ...

... then a higher-or-equal priority job's arrival time is constrained.

Conversely, a strictly earlier arrival time plus relative deadline implies higher-or-equal priority.

For jobs of the same task, a strictly earlier arrival implies an earlier absolute deadline.

EDF scheduling respects the 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 scheduling implies that tasks are executed sequentially.

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.

Allow for any uniprocessor model.

Consider any valid arrival sequence.

Next, consider any schedule of this arrival sequence, ...

Assume EDF scheduling.

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

Assume an EDF schedule.

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.