# Library prosa.analysis.facts.priority.elf

In this section, we state and prove some basic facts about the ELF scheduling policy.
Section ELFBasicFacts.

Consider any type of tasks with relative priority points...

Context {Job : JobType} `{JobTask Job Task} `{JobCost Job} {AR : JobArrival Job}.

Consider any arbitrary FP policy ...

... that is reflexive, transitive, and total.

## Basic properties of the ELF policy

We first note that, by definition, ELF reduces to GEL for equal-priority tasks.
Remark hep_job_elf_gel :
j j',
(@hep_job _ (ELF FP) j j') = (@hep_job _ (GEL Job Task) j j').
Proof.
movej j' EP.
rewrite [LHS]/hep_job/ELF.
by rewrite andTb orFb.
Qed.

We then show that if we are looking at two jobs of the same task, then hep_job is a statement about their respective arrival times.
Fact hep_job_arrival_elf :
j j',
hep_job j j' = (job_arrival j job_arrival j').
Proof.
movej j' SAME.
rewrite hep_job_elf_gel.
- by rewrite hep_job_arrival_gel.
- by move: SAME ⇒ /eqP ->; exact: eq_reflexive.
Qed.

ELF is reflexive.
Lemma ELF_is_reflexive : reflexive_job_priorities (ELF FP).
Proof. by movej; apply /orP; right; apply/andP; split⇒ //; exact: GEL_is_reflexive. Qed.

ELF is transitive.
Lemma ELF_is_transitive : transitive_job_priorities (ELF FP).
Proof.
movey x z.
move⇒ /orP [hpxy| /andP[hepxy jpxy]] ⇒ /orP[hpyz| /andP [hepyz jpyz]].
{ apply/orP; left; exact: hp_trans hpyz. }
{ apply/orP; left; exact: hp_hep_trans hepyz. }
{ apply/orP; left; exact: hep_hp_trans hpyz. }
{ apply/orP; right; apply /andP; split.
- exact: H_transitive_priorities hepyz.
- by apply: (GEL_is_transitive y). }
Qed.

ELF is total.
Lemma ELF_is_total : total_job_priorities (ELF FP).
Proof.
movex y.
rewrite -implyNb; apply/implyP ⇒ /norP [Nhpxy /nandP [Nhpxy'|Njpxy] ].
{ by apply /orP; left; rewrite -not_hep_hp_task. }
{ move: Nhpxy ⇒ /nandP [Nhepxy| NNhepyx].
{ by apply /orP; left; rewrite -not_hep_hp_task. }
{ apply /orP; right. move: NNhepyx ⇒ /negbNE → /=.
move: Njpxy; unfold hep_job, GEL; lia. }}
Qed.

The ELF policy is JLFP_FP_compatible.
Lemma ELF_is_JLFP_FP_compatible :
JLFP_FP_compatible (ELF FP) FP.
Proof.
split; movej1 j2.
- rewrite /hep_job /ELF.
by apply /orP; left.
Qed.

## Sequentiality under ELF

The ELF policy satisfies the sequential-tasks hypothesis.
Proof. by movej1 j2 TSK ARR; rewrite hep_job_arrival_elf. Qed.

In this section, we prove that tasks always execute sequentially in a uniprocessor schedule following the ELF policy.
Consider any valid arrival sequence.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.

Allow for any uniprocessor model.
Context {PState : ProcessorState Job}.
Hypothesis H_uniproc : uniprocessor_model PState.

Next, consider any schedule of the arrival sequence, ...
Variable sched : schedule PState.

... allow for any work-bearing notion of job readiness, ...
Context `{@JobReady Job PState _ AR}.

... and assume that the schedule is valid.
Hypothesis H_sched_valid : valid_schedule sched arr_seq.

Consider any valid preemption model.
Assume an ELF schedule.
To prove sequentiality, we use the lemma early_hep_job_is_scheduled. Clearly, under the ELF 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, ELF implies the sequential_tasks property.
Proof.
movej1 j2 t ARR1 ARR2 SAME LT.
apply: early_hep_job_is_scheduled ⇒ //;
first exact: ELF_is_transitive.
rewrite always_higher_priority_jlfp !hep_job_arrival_elf //.
- by rewrite -ltnNge; apply/andP; split ⇒ //.
Qed.