Library prosa.analysis.facts.priority.gel

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

Consider any type of tasks and jobs.
  Context `{Task : TaskType} {Job : JobType} `{JobTask Job Task} `{PriorityPoint Task}.
  Context `{JobArrival Job}.

  Section HEPJobArrival.
Consider a job j...
    Variable j : Job.

... and a higher or equal priority job j'.
    Variable j' : Job.
    Hypothesis H_j'_hep : hep_job j' j.

The arrival time of j' is bounded as follows.
    Lemma hep_job_arrives_before :
      (Z.of_nat (job_arrival j')
         Z.of_nat (job_arrival j) +
           task_priority_point (job_task j) - task_priority_point (job_task j'))%Z.

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.
    Corollary hep_job_arrives_after_zero :
      (0 Z.of_nat (job_arrival j) +
             task_priority_point (job_task j) - task_priority_point (job_task j'))%Z.

  End HEPJobArrival.

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

Consider any arrival sequence.
    Variable arr_seq : arrival_sequence Job.

Next, consider any ideal uni-processor schedule of this arrival sequence, ...
    Variable sched : schedule (ideal.processor_state Job).

    Context `{JobArrival Job} `{JobCost Job}.
... allow for any work-bearing notion of job readiness, ...
... and assume that the schedule is valid.
    Hypothesis H_sched_valid : valid_schedule sched arr_seq.

In addition, we assume the existence of a function mapping jobs to their preemption points ...
    Context `{JobPreemptable Job}.

... 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.
Global Hint Resolve
GEL_respects_sequential_tasks
  : basic_rt_facts.