# 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 `{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) +
Proof.
by move : H_j'_hep; rewrite /hep_job /GEL /job_priority_point; lia.
Qed.

Using the above lemma, we prove that for any higher-or-equal priority job j', the term job_arrival j + task_priority_point j) - task_priority_point 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) +
Proof.
apply: (@Z.le_trans _ (Z.of_nat (job_arrival j'))); first by lia.
by apply: hep_job_arrives_before.
Qed.

End HEPJobArrival.

Next, we prove that the GEL policy respects sequential tasks.
Proof.
movej1 j2 /eqP TSK ARR.
rewrite /hep_job /GEL /job_priority_point TSK.
by lia.
Qed.

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

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.
Proof.
movej1 j2 t ARR1 ARR2 /eqP SAME LT.
eapply early_hep_job_is_scheduled ⇒ //; rt_eautot'.
rewrite /hep_job_at /JLFP_to_JLDP /hep_job /GEL /job_priority_point SAME.
by lia.
Qed.