Library prosa.analysis.facts.priority.gel

In this file we state and prove some basic facts about the GEL scheduling policy.

Consider any type of tasks and jobs.

Consider a job j...

... and a higher or equal priority job j'.

The arrival time of j' is bounded as follows.

Using the above lemma, we prove that for any higher-or-equal priority job j', the term job_arrival j + task_priority_point (job_task j) - task_priority_point (job_task j') is positive. Note that the function Z.of_nat is used to convert natural numbers to integers.

Next, we prove that the GEL policy respects sequential tasks.

In this section, we prove that in a schedule following the GEL policy, tasks are always sequential.

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.

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

To prove sequentiality, we use the lemma early_hep_job_is_scheduled. Clearly, under the GEL 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 GEL implies the sequential_tasks property.

We add the following lemma to the basic facts database.