Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.model.priority.elf.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.model.aggregate.workload.
Require Export prosa.analysis.facts.priority.classes.
Require Export prosa.analysis.definitions.priority.classes.
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.analysis.facts.priority.sequential.
Require Export prosa.analysis.facts.priority.gel.
(** 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 {Task : TaskType} `{PriorityPoint Task}.
(** ...and jobs of these tasks. *)
Context {Job : JobType} `{JobTask Job Task} `{JobCost Job} {AR : JobArrival Job}.
(** Consider any arbitrary FP policy ...*)
Variable FP : FP_policy Task.
(** ... that is reflexive, transitive, and total. *)
Hypothesis H_reflexive_priorities : reflexive_task_priorities FP.
Hypothesis H_transitive_priorities : transitive_task_priorities FP.
Hypothesis H_total_priorities : total_task_priorities FP.
(** ** 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 :
forall j j' ,
ep_task (job_task j) (job_task j') ->
(@hep_job _ (ELF FP) j j') = (@hep_job _ (GEL Job Task) j j').Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
forall j j' : Job,
ep_task (job_task j) (job_task j') ->
hep_job j j' = hep_job j j'
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
forall j j' : Job,
ep_task (job_task j) (job_task j') ->
hep_job j j' = hep_job j j'
move => j j' EP.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j, j' : Job EP : ep_task (job_task j) (job_task j')
hep_job j j' = hep_job j j'
rewrite [LHS]/hep_job/ELF.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j, j' : Job EP : ep_task (job_task j) (job_task j')
hp_task (job_task j) (job_task j')
|| hep_task (job_task j) (job_task j') && hep_job j j' =
hep_job j j'
have -> : hep_task (job_task j) (job_task j') = true by apply : ep_hep_task.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j, j' : Job EP : ep_task (job_task j) (job_task j')
hp_task (job_task j) (job_task j')
|| true && hep_job j j' = hep_job j j'
have -> : hp_task (job_task j) (job_task j') = false by apply /negbTE/ep_not_hp_task.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j, j' : Job EP : ep_task (job_task j) (job_task j')
false || true && hep_job j j' = hep_job j j'
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 :
forall j j' ,
same_task j j' ->
hep_job j j' = (job_arrival j <= job_arrival j').Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
forall j j' : Job,
same_task j j' ->
hep_job j j' = (job_arrival j <= job_arrival j')
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
forall j j' : Job,
same_task j j' ->
hep_job j j' = (job_arrival j <= job_arrival j')
move => j j' SAME.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j, j' : Job SAME : same_task j j'
hep_job j j' = (job_arrival j <= job_arrival j')
rewrite hep_job_elf_gel.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j, j' : Job SAME : same_task j j'
hep_job j j' = (job_arrival j <= job_arrival j')
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j, j' : Job SAME : same_task j j'
hep_job j j' = (job_arrival j <= job_arrival j')
by rewrite hep_job_arrival_gel.
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j, j' : Job SAME : same_task j j'
ep_task (job_task j) (job_task j')
by move : SAME => /eqP ->; exact : eq_reflexive.
Qed .
(** ELF is reflexive. *)
Lemma ELF_is_reflexive : reflexive_job_priorities (ELF FP).Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
reflexive_job_priorities (ELF FP)
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
reflexive_job_priorities (ELF FP)
by move => j; apply /orP; right ; apply /andP; split => //; exact : GEL_is_reflexive. Qed .
(** ELF is transitive. *)
Lemma ELF_is_transitive : transitive_job_priorities (ELF FP).Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
transitive_job_priorities (ELF FP)
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
transitive_job_priorities (ELF FP)
move => y x z.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP y, x, z : Job
hep_job x y -> hep_job y z -> hep_job x z
move => /orP [hpxy| /andP[hepxy jpxy]] => /orP[hpyz| /andP [hepyz jpyz]].Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP y, x, z : Job hpxy : hp_task (job_task x) (job_task y) hpyz : hp_task (job_task y) (job_task z)
hep_job x z
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP y, x, z : Job hpxy : hp_task (job_task x) (job_task y) hpyz : hp_task (job_task y) (job_task z)
hep_job x z
apply /orP; left ; exact : hp_trans hpyz. } Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP y, x, z : Job hpxy : hp_task (job_task x) (job_task y) hepyz : hep_task (job_task y) (job_task z) jpyz : hep_job y z
hep_job x z
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP y, x, z : Job hpxy : hp_task (job_task x) (job_task y) hepyz : hep_task (job_task y) (job_task z) jpyz : hep_job y z
hep_job x z
apply /orP; left ; exact : hp_hep_trans hepyz. } Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP y, x, z : Job hepxy : hep_task (job_task x) (job_task y) jpxy : hep_job x y hpyz : hp_task (job_task y) (job_task z)
hep_job x z
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP y, x, z : Job hepxy : hep_task (job_task x) (job_task y) jpxy : hep_job x y hpyz : hp_task (job_task y) (job_task z)
hep_job x z
apply /orP; left ; exact : hep_hp_trans hpyz. } Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP y, x, z : Job hepxy : hep_task (job_task x) (job_task y) jpxy : hep_job x y hepyz : hep_task (job_task y) (job_task z) jpyz : hep_job y z
hep_job x z
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP y, x, z : Job hepxy : hep_task (job_task x) (job_task y) jpxy : hep_job x y hepyz : hep_task (job_task y) (job_task z) jpyz : hep_job y z
hep_job x z
apply /orP; right ; apply /andP; split .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP y, x, z : Job hepxy : hep_task (job_task x) (job_task y) jpxy : hep_job x y hepyz : hep_task (job_task y) (job_task z) jpyz : hep_job y z
hep_task (job_task x) (job_task z)
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP y, x, z : Job hepxy : hep_task (job_task x) (job_task y) jpxy : hep_job x y hepyz : hep_task (job_task y) (job_task z) jpyz : hep_job y z
hep_task (job_task x) (job_task z)
exact : H_transitive_priorities hepyz.
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP y, x, z : Job hepxy : hep_task (job_task x) (job_task y) jpxy : hep_job x y hepyz : hep_task (job_task y) (job_task z) jpyz : hep_job y z
hep_job x z
by apply : (GEL_is_transitive y). }
Qed .
(** ELF is total. *)
Lemma ELF_is_total : total_job_priorities (ELF FP).Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
total_job_priorities (ELF FP)
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
total_job_priorities (ELF FP)
move => x y.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP x, y : Job
hep_job x y || hep_job y x
rewrite -implyNb; apply /implyP => /norP [Nhpxy /nandP [Nhpxy'|Njpxy] ].Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP x, y : Job Nhpxy : ~~ hp_task (job_task x) (job_task y) Nhpxy' : ~~ hep_task (job_task x) (job_task y)
hep_job y x
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP x, y : Job Nhpxy : ~~ hp_task (job_task x) (job_task y) Nhpxy' : ~~ hep_task (job_task x) (job_task y)
hep_job y x
by apply /orP; left ; rewrite -not_hep_hp_task. } Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP x, y : Job Nhpxy : ~~ hp_task (job_task x) (job_task y) Njpxy : ~~ hep_job x y
hep_job y x
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP x, y : Job Nhpxy : ~~ hp_task (job_task x) (job_task y) Njpxy : ~~ hep_job x y
hep_job y x
move : Nhpxy => /nandP [Nhepxy| NNhepyx].Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP x, y : Job Njpxy : ~~ hep_job x y Nhepxy : ~~ hep_task (job_task x) (job_task y)
hep_job y x
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP x, y : Job Njpxy : ~~ hep_job x y Nhepxy : ~~ hep_task (job_task x) (job_task y)
hep_job y x
by apply /orP; left ; rewrite -not_hep_hp_task. } Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP x, y : Job Njpxy : ~~ hep_job x y NNhepyx : ~~ ~~ hep_task (job_task y) (job_task x)
hep_job y x
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP x, y : Job Njpxy : ~~ hep_job x y NNhepyx : ~~ ~~ hep_task (job_task y) (job_task x)
hep_job y x
apply /orP; right .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP x, y : Job Njpxy : ~~ hep_job x y NNhepyx : ~~ ~~ hep_task (job_task y) (job_task x)
hep_task (job_task y) (job_task x) && hep_job y x
move : NNhepyx => /negbNE -> /=.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP x, y : Job Njpxy : ~~ hep_job x y
hep_job y x
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.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
JLFP_FP_compatible (ELF FP) FP
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
JLFP_FP_compatible (ELF FP) FP
split ; move => j1 j2.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j1, j2 : Job
hep_job j1 j2 -> hep_task (job_task j1) (job_task j2)
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j1, j2 : Job
hep_job j1 j2 -> hep_task (job_task j1) (job_task j2)
rewrite /hep_job /ELF.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j1, j2 : Job
hp_task (job_task j1) (job_task j2)
|| hep_task (job_task j1) (job_task j2) &&
hep_job j1 j2 ->
hep_task (job_task j1) (job_task j2)
by move => /orP [/andP [HPTASK1 HPTASK2] | /andP [HEPTASK HEPJOB]].
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j1, j2 : Job
hp_task (job_task j1) (job_task j2) -> hep_job j1 j2
move => HP_TASK.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP j1, j2 : Job HP_TASK : hp_task (job_task j1) (job_task j2)
hep_job j1 j2
by apply /orP; left .
Qed .
(** ** Sequentiality under ELF *)
(** The ELF policy satisfies the sequential-tasks hypothesis. *)
Lemma ELF_respects_sequential_tasks :
policy_respects_sequential_tasks (ELF FP).Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
policy_respects_sequential_tasks (ELF FP)
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
policy_respects_sequential_tasks (ELF FP)
by move => j1 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. *)
Section ELFImpliesSequentialTasks .
(** 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}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** ... and assume that the schedule is valid. *)
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
(** Consider any valid preemption model. *)
Context `{JobPreemptable Job}.
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
(** Assume an ELF schedule. *)
Hypothesis H_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched (ELF FP).
(** 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. *)
Lemma ELF_implies_sequential_tasks :
sequential_tasks arr_seq sched.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H2 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H3 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (ELF FP)
sequential_tasks arr_seq sched
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H2 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H3 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (ELF FP)
sequential_tasks arr_seq sched
move => j1 j2 t ARR1 ARR2 SAME LT.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H2 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H3 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (ELF FP) j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2
scheduled_at sched j2 t -> completed_by sched j1 t
apply : early_hep_job_is_scheduled => //;
first exact : ELF_is_transitive.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H2 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H3 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (ELF FP) j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2
always_higher_priority j1 j2
rewrite always_higher_priority_jlfp !hep_job_arrival_elf //.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H2 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H3 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (ELF FP) j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2
(job_arrival j1 <= job_arrival j2) &&
~~ (job_arrival j2 <= job_arrival j1)
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H2 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H3 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (ELF FP) j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2
(job_arrival j1 <= job_arrival j2) &&
~~ (job_arrival j2 <= job_arrival j1)
by rewrite -ltnNge; apply /andP; split => //.
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task H1 : JobCost Job AR : JobArrival Job FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H2 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H3 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (ELF FP) j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2
same_task j2 j1
by rewrite same_task_sym.
Qed .
End ELFImpliesSequentialTasks .
End ELFBasicFacts .
(** We add the above facts into a "Hint Database" basic_rt_facts, so Coq will
be able to apply them automatically where needed. *)
Global Hint Resolve
ELF_is_reflexive
ELF_is_transitive
ELF_is_total
ELF_is_JLFP_FP_compatible
ELF_respects_sequential_tasks
ELF_implies_sequential_tasks
: basic_rt_facts.