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.analysis.definitions.priority_inversion.[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.analysis.facts.model.uniprocessor.
(** * Lemmas about Priority Inversion *)
(** This file collects basic facts about the notion of priority inversion in the
general context of arbitrary processor models. *)
Section PI .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Next, consider _any_ kind of processor state model, ... *)
Context {PState : ProcessorState Job}.
(** ... any valid arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any valid schedule. *)
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
(** Assume a given reflexive JLFP policy... *)
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
(** ... and consider an arbitrary job. *)
Variable j : Job.
(** ** Occurrence of Priority Inversion *)
(** First, we observe conditions under which priority inversions does, or does
not, arise. *)
(** Assume that [j] is scheduled at time [t], then there is no
priority inversion at time [t]. *)
Lemma sched_itself_implies_no_priority_inversion :
forall t ,
scheduled_at sched j t ->
~~ priority_inversion arr_seq sched j t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job
forall t : instant,
scheduled_at sched j t ->
~~ priority_inversion arr_seq sched j t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job
forall t : instant,
scheduled_at sched j t ->
~~ priority_inversion arr_seq sched j t
by move => t SCHED; rewrite negb_and negbK scheduled_jobs_at_iff// SCHED. Qed .
(** Conversely, if job [j] experiences a priority inversion at time [t], then
some (other) job is scheduled at the time, ... *)
Lemma priority_inversion_scheduled_at :
forall t ,
priority_inversion arr_seq sched j t ->
exists j' , scheduled_at sched j' t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job
forall t : instant,
priority_inversion arr_seq sched j t ->
exists j' : Job, scheduled_at sched j' t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job
forall t : instant,
priority_inversion arr_seq sched j t ->
exists j' : Job, scheduled_at sched j' t
move => t /andP [_ /hasP [j' SCHED _]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job t : instant j' : Job SCHED : j' \in scheduled_jobs_at arr_seq sched t
exists j' : Job, scheduled_at sched j' t
by exists j' ; move : SCHED; rewrite scheduled_jobs_at_iff.
Qed .
(** ... and thus there is no priority inversion at idle instants. *)
Lemma no_priority_inversion_when_idle :
forall t ,
is_idle arr_seq sched t ->
~~ priority_inversion arr_seq sched j t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job
forall t : instant,
is_idle arr_seq sched t ->
~~ priority_inversion arr_seq sched j t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job
forall t : instant,
is_idle arr_seq sched t ->
~~ priority_inversion arr_seq sched j t
move => t /[!is_idle_iff] /eqP // /[!scheduled_job_at_none] // IDLE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job t : instant IDLE : forall j : Job, ~~ scheduled_at sched j t
~~ priority_inversion arr_seq sched j t
apply : contraT => /negPn.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job t : instant IDLE : forall j : Job, ~~ scheduled_at sched j t
priority_inversion arr_seq sched j t -> false
move => /andP [_ /hasP [j' SCHED _]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job t : instant IDLE : forall j : Job, ~~ scheduled_at sched j tj' : Job SCHED : j' \in scheduled_jobs_at arr_seq sched t
false
rewrite scheduled_jobs_at_iff // in SCHED.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job t : instant IDLE : forall j : Job, ~~ scheduled_at sched j tj' : Job SCHED : scheduled_at sched j' t
false
by move : (IDLE j') => /negP.
Qed .
Section Uniprocessors .
(** ** Occurrence of Priority Inversion on Uniprocessors *)
(** Stronger conditions hold on uniprocessors since only one job can be
scheduled at any time. *)
Hypothesis H_uni : uniprocessor_model PState.
(** On a uniprocessor, the job scheduled when [j] incurs priority inversion
necessarily has lower priority than [j]. *)
Lemma priority_inversion_hep_job :
forall t j' ,
scheduled_at sched j' t ->
priority_inversion arr_seq sched j t = ~~ hep_job j' j.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState
forall (t : instant) (j' : Job),
scheduled_at sched j' t ->
priority_inversion arr_seq sched j t = ~~ hep_job j' j
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState
forall (t : instant) (j' : Job),
scheduled_at sched j' t ->
priority_inversion arr_seq sched j t = ~~ hep_job j' j
move => t j' SCHED'.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t
priority_inversion arr_seq sched j t = ~~ hep_job j' j
case HEP: (~~ hep_job _ _); apply /eqP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t HEP : ~~ hep_job j' j = true
priority_inversion arr_seq sched j t == true
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t HEP : ~~ hep_job j' j = true
priority_inversion arr_seq sched j t == true
rewrite eqb_id; apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t HEP : ~~ hep_job j' j = true
j \notin scheduled_jobs_at arr_seq sched t
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t HEP : ~~ hep_job j' j = true
j \notin scheduled_jobs_at arr_seq sched t
rewrite scheduled_jobs_at_iff //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t HEP : ~~ hep_job j' j = true
~~ scheduled_at sched j t
apply : scheduled_job_at_neq => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t HEP : ~~ hep_job j' j = true
j' != j
apply : contraT => /negPn/eqP EQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t HEP : ~~ hep_job j' j = true EQ : j' = j
false
by move : HEP; rewrite EQ H_priority_is_reflexive.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t HEP : ~~ hep_job j' j = true
has (fun jlp : Job => ~~ hep_job jlp j)
(scheduled_jobs_at arr_seq sched t)
apply /hasP; exists j' => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t HEP : ~~ hep_job j' j = true
j' \in scheduled_jobs_at arr_seq sched t
by rewrite scheduled_jobs_at_iff. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t HEP : ~~ hep_job j' j = false
priority_inversion arr_seq sched j t == false
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t HEP : ~~ hep_job j' j = false
priority_inversion arr_seq sched j t == false
rewrite eqbF_neg; apply contraT => /negPn /andP[_ /hasP [j'' /[!scheduled_jobs_at_iff] // SCHED'' HEP'']].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t HEP : ~~ hep_job j' j = false j'' : Job SCHED'' : scheduled_at sched j'' t HEP'' : ~~ hep_job j'' j
false
move : HEP HEP''.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t j'' : Job SCHED'' : scheduled_at sched j'' t
~~ hep_job j' j = false -> ~~ hep_job j'' j -> false
by have -> : j' = j'' by apply : H_uni. }
Qed .
(** Conversely, if a higher-priority job is scheduled on a uniprocessor, then
[j] does not incur priority inversion. *)
Corollary no_priority_inversion_when_hep_job_scheduled :
forall t j' ,
scheduled_at sched j' t ->
hep_job j' j ->
~~ priority_inversion arr_seq sched j t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState
forall (t : instant) (j' : Job),
scheduled_at sched j' t ->
hep_job j' j ->
~~ priority_inversion arr_seq sched j t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState
forall (t : instant) (j' : Job),
scheduled_at sched j' t ->
hep_job j' j ->
~~ priority_inversion arr_seq sched j t
move => t j' SCHED HEP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED : scheduled_at sched j' t HEP : hep_job j' j
~~ priority_inversion arr_seq sched j t
rewrite (priority_inversion_hep_job t j') //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED : scheduled_at sched j' t HEP : hep_job j' j
~~ ~~ hep_job j' j
by apply /negPn.
Qed .
(** From the above lemmas, we obtain a simplified definition of
[priority_inversion] that holds on uniprocessors. *)
Lemma uni_priority_inversion_P :
forall t ,
reflect (exists2 j', scheduled_at sched j' t & ~~ hep_job j' j)
(priority_inversion arr_seq sched j t).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState
forall t : instant,
reflect
(exists2 j' : Job,
scheduled_at sched j' t & ~~ hep_job j' j)
(priority_inversion arr_seq sched j t)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState
forall t : instant,
reflect
(exists2 j' : Job,
scheduled_at sched j' t & ~~ hep_job j' j)
(priority_inversion arr_seq sched j t)
move => t; apply : (iffP idP) => [PI | [j' SCHED' NHEP]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant PI : priority_inversion arr_seq sched j t
exists2 j' : Job,
scheduled_at sched j' t & ~~ hep_job j' j
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant PI : priority_inversion arr_seq sched j t
exists2 j' : Job,
scheduled_at sched j' t & ~~ hep_job j' j
have [j' SCHED'] := priority_inversion_scheduled_at t PI.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant PI : priority_inversion arr_seq sched j t j' : Job SCHED' : scheduled_at sched j' t
exists2 j' : Job,
scheduled_at sched j' t & ~~ hep_job j' j
by move : PI; rewrite (priority_inversion_hep_job t j').
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t NHEP : ~~ hep_job j' j
priority_inversion arr_seq sched j t
apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t NHEP : ~~ hep_job j' j
j \notin scheduled_jobs_at arr_seq sched t
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t NHEP : ~~ hep_job j' j
j \notin scheduled_jobs_at arr_seq sched t
rewrite scheduled_jobs_at_iff //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t NHEP : ~~ hep_job j' j
~~ scheduled_at sched j t
apply : scheduled_job_at_neq => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t NHEP : ~~ hep_job j' j
j' != j
by apply /eqP => EQ; move : NHEP; rewrite EQ H_priority_is_reflexive.
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job H_uni : uniprocessor_model PState t : instant j' : Job SCHED' : scheduled_at sched j' t NHEP : ~~ hep_job j' j
has (fun jlp : Job => ~~ hep_job jlp j)
(scheduled_jobs_at arr_seq sched t)
by apply /hasP; exists j' => //; rewrite scheduled_jobs_at_iff.
Qed .
End Uniprocessors .
(** ** Cumulative Priority Inversion *)
(** We observe that the cumulative priority inversion (CPI) that job
[j] incurs in an interval <<[t1, t2)>> can be split arbitrarily: is equal
to the sum of CPI in an interval <<[t1, t_mid)>> and CPI in an interval
<<[t_mid, t2)>>. *)
Lemma cumulative_priority_inversion_cat :
forall (t_mid t1 t2 : instant),
t1 <= t_mid ->
t_mid <= t2 ->
cumulative_priority_inversion arr_seq sched j t1 t2 =
cumulative_priority_inversion arr_seq sched j t1 t_mid
+ cumulative_priority_inversion arr_seq sched j t_mid t2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job
forall t_mid t1 t2 : instant,
t1 <= t_mid ->
t_mid <= t2 ->
cumulative_priority_inversion arr_seq sched j t1 t2 =
cumulative_priority_inversion arr_seq sched j t1 t_mid +
cumulative_priority_inversion arr_seq sched j t_mid t2
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job
forall t_mid t1 t2 : instant,
t1 <= t_mid ->
t_mid <= t2 ->
cumulative_priority_inversion arr_seq sched j t1 t2 =
cumulative_priority_inversion arr_seq sched j t1 t_mid +
cumulative_priority_inversion arr_seq sched j t_mid t2
intros t_mid t1 t2 LE1 LE2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job t_mid, t1, t2 : instant LE1 : t1 <= t_mid LE2 : t_mid <= t2
cumulative_priority_inversion arr_seq sched j t1 t2 =
cumulative_priority_inversion arr_seq sched j t1 t_mid +
cumulative_priority_inversion arr_seq sched j t_mid t2
rewrite /cumulative_priority_inversion -big_cat //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job t_mid, t1, t2 : instant LE1 : t1 <= t_mid LE2 : t_mid <= t2
\sum_(t1 <= t < t2)
priority_inversion arr_seq sched j t =
\sum_(i <- (index_iota t1 t_mid ++ index_iota t_mid t2))
priority_inversion arr_seq sched j i
replace (index_iota t1 t_mid ++ index_iota t_mid t2) with (index_iota t1 t2); first by reflexivity .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job t_mid, t1, t2 : instant LE1 : t1 <= t_mid LE2 : t_mid <= t2
index_iota t1 t2 =
index_iota t1 t_mid ++ index_iota t_mid t2
interval_to_duration t1 t_mid δ1. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job t1, t2 : instant δ1 : nat LE2 : t1 + δ1 <= t2
index_iota t1 t2 =
index_iota t1 (t1 + δ1) ++ index_iota (t1 + δ1) t2
interval_to_duration (t1 + δ1) t2 δ2. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job t1 : instant δ1, δ2 : nat
index_iota t1 (t1 + δ1 + δ2) =
index_iota t1 (t1 + δ1) ++
index_iota (t1 + δ1) (t1 + δ1 + δ2)
rewrite -!addnA /index_iota.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job t1 : instant δ1, δ2 : nat
iota t1 (t1 + (δ1 + δ2) - t1) =
iota t1 (t1 + δ1 - t1) ++
iota (t1 + δ1) (t1 + (δ1 + δ2) - (t1 + δ1))
erewrite iotaD_impl with (n_le := δ1); last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP j : Job t1 : instant δ1, δ2 : nat
iota t1 δ1 ++
iota (t1 + δ1) (t1 + (δ1 + δ2) - t1 - δ1) =
iota t1 (t1 + δ1 - t1) ++
iota (t1 + δ1) (t1 + (δ1 + δ2) - (t1 + δ1))
by rewrite !addKn addnA addKn.
Qed .
End PI .