Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.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.facts.busy_interval.priority_inversion.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.model.ideal.schedule.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** * Lemmas about Priority Inversion for ideal uni-processors *)
(** In this section, we prove a few useful properties about the notion
of priority inversion for ideal uni-processors. *)
Section PIIdealProcessorModelLemmas .
(** 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}.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Consider a JLFP-policy that indicates a higher-or-equal priority relation,
and assume that this relation is reflexive. *)
Context `{JLFP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
(** Let [tsk] be any task to be analyzed. *)
Variable tsk : Task.
(** Consider a job [j] of task [tsk]. In this subsection, job [j] is
deemed to be the main job with respect to which the priority
inversion is computed. *)
Variable j : Job.
Hypothesis H_j_tsk : job_of_task tsk j.
(** Consider a time instant [t]. *)
Variable t : instant.
(** We prove that if the processor is idle at time [t], then there
is no priority inversion. *)
Lemma idle_implies_no_priority_inversion :
is_idle sched t ->
priority_inversion_dec arr_seq sched j t = false.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant
is_idle sched t ->
priority_inversion_dec arr_seq sched j t = false
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant
is_idle sched t ->
priority_inversion_dec arr_seq sched j t = false
unfold priority_inversion_dec; intros IDLE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant IDLE : is_idle sched t
~~ scheduled_at sched j t &&
has
(fun jlp : Job =>
scheduled_at sched jlp t && ~~ hep_job jlp j)
(arrivals_before arr_seq t.+1 ) = false
apply /eqP; rewrite eqbF_neg negb_and Bool.negb_involutive; apply /orP; right .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant IDLE : is_idle sched t
~~
has
(fun jlp : Job =>
scheduled_at sched jlp t && ~~ hep_job jlp j)
(arrivals_before arr_seq t.+1 )
apply /hasPn; intros s IN.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant IDLE : is_idle sched t s : Job IN : s \in arrivals_before arr_seq t.+1
~~ (scheduled_at sched s t && ~~ hep_job s j)
rewrite negb_and Bool.negb_involutive; apply /orP; left .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant IDLE : is_idle sched t s : Job IN : s \in arrivals_before arr_seq t.+1
~~ scheduled_at sched s t
by move : IDLE => /eqP; rewrite scheduled_at_def => ->.
Qed .
(** Next, consider an additional job [j'] and assume it is scheduled
at time [t]. *)
Variable j' : Job.
Hypothesis H_j'_sched : scheduled_at sched j' t.
(** Then, we prove that from point of view of job [j], priority
inversion appears iff [s] has lower priority than job [j]. *)
Lemma priority_inversion_equiv_sched_lower_priority :
priority_inversion_dec 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 arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t
priority_inversion_dec 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 arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t
priority_inversion_dec arr_seq sched j t =
~~ hep_job j' j
rewrite /priority_inversion_dec.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t
~~ scheduled_at sched j t &&
has
(fun jlp : Job =>
scheduled_at sched jlp t && ~~ hep_job jlp j)
(arrivals_before arr_seq t.+1 ) = ~~ hep_job j' j
destruct (scheduled_at _ j _) eqn :SCHED2; rewrite //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = true
false = ~~ hep_job j' j
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = true
false = ~~ hep_job j' j
have EQ: j = j' by eapply ideal_proc_model_is_a_uniprocessor_model; eauto .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = true EQ : j = j'
false = ~~ hep_job j' j
subst j'; symmetry ; apply /eqP; rewrite eqbF_neg Bool.negb_involutive.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant H_j'_sched : scheduled_at sched j t SCHED2 : scheduled_at sched j t = true
hep_job j j
by apply (H_priority_is_reflexive 0 ).
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = false
has
(fun jlp : Job =>
scheduled_at sched jlp t && ~~ hep_job jlp j)
(arrivals_before arr_seq t.+1 ) = ~~ hep_job j' j
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = false
has
(fun jlp : Job =>
scheduled_at sched jlp t && ~~ hep_job jlp j)
(arrivals_before arr_seq t.+1 ) = ~~ hep_job j' j
destruct (hep_job) eqn :HEP; rewrite //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = false HEP : hep_job j' j = true
has
(fun jlp : Job =>
scheduled_at sched jlp t && ~~ hep_job jlp j)
(arrivals_before arr_seq t.+1 ) = false
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = false HEP : hep_job j' j = true
has
(fun jlp : Job =>
scheduled_at sched jlp t && ~~ hep_job jlp j)
(arrivals_before arr_seq t.+1 ) = false
apply /eqP; rewrite eqbF_neg; apply /hasPn; intros l IN.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = false HEP : hep_job j' j = true l : Job IN : l \in arrivals_before arr_seq t.+1
~~ (scheduled_at sched l t && ~~ hep_job l j)
destruct (scheduled_at _ l _) eqn :SCHED3; rewrite //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = false HEP : hep_job j' j = true l : Job IN : l \in arrivals_before arr_seq t.+1 SCHED3 : scheduled_at sched l t = true
~~ ~~ hep_job l j
have EQ: l = j' by eapply ideal_proc_model_is_a_uniprocessor_model; eauto .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = false HEP : hep_job j' j = true l : Job IN : l \in arrivals_before arr_seq t.+1 SCHED3 : scheduled_at sched l t = true EQ : l = j'
~~ ~~ hep_job l j
by subst j'; rewrite HEP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = false HEP : hep_job j' j = false
has
(fun jlp : Job =>
scheduled_at sched jlp t && ~~ hep_job jlp j)
(arrivals_before arr_seq t.+1 ) = true
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = false HEP : hep_job j' j = false
has
(fun jlp : Job =>
scheduled_at sched jlp t && ~~ hep_job jlp j)
(arrivals_before arr_seq t.+1 ) = true
apply /hasP; exists j' .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = false HEP : hep_job j' j = false
j' \in arrivals_before arr_seq t.+1
rt_eauto. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t SCHED2 : scheduled_at sched j t = false HEP : hep_job j' j = false
scheduled_at sched j' t && ~~ hep_job j' j
by rewrite H_j'_sched HEP.
}
Qed .
(** Assume that [j'] has higher-or-equal priority than job [j], then
we prove that there is no priority inversion for job [j]. *)
Lemma sched_hep_implies_no_priority_inversion :
hep_job j' j ->
priority_inversion_dec arr_seq sched j t = false.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t
hep_job j' j ->
priority_inversion_dec arr_seq sched j t = false
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t
hep_job j' j ->
priority_inversion_dec arr_seq sched j t = false
intros HEP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t HEP : hep_job j' j
priority_inversion_dec arr_seq sched j t = false
apply /negP; intros CONTR; move : CONTR => /andP [NSCHED /hasP [j'' _ /andP [SCHED PRIO]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t HEP : hep_job j' j NSCHED : ~~ scheduled_at sched j t j'' : Job SCHED : scheduled_at sched j'' t PRIO : ~~ hep_job j'' j
False
have HF := ideal_proc_model_is_a_uniprocessor_model _ _ _ _ H_j'_sched SCHED; subst j'.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j'' : Job HEP : hep_job j'' j H_j'_sched : scheduled_at sched j'' t NSCHED : ~~ scheduled_at sched j t SCHED : scheduled_at sched j'' t PRIO : ~~ hep_job j'' j
False
by rewrite HEP in PRIO.
Qed .
(** Assume that [j'] has lower priority than job [j], then
we prove that [j] incurs priority inversion. *)
Lemma sched_lp_implies_priority_inversion :
~~ hep_job j' j ->
priority_inversion_dec arr_seq sched j t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t
~~ hep_job j' j ->
priority_inversion_dec arr_seq sched j t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t
~~ hep_job j' j ->
priority_inversion_dec arr_seq sched j t
intros LP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j
priority_inversion_dec 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 arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j
~~ scheduled_at sched j t
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j
~~ scheduled_at sched j t
apply /negP; intros SCHED.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j SCHED : scheduled_at sched j t
False
have HF := ideal_proc_model_is_a_uniprocessor_model _ _ _ _ H_j'_sched SCHED; subst j'.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant LP : ~~ hep_job j j H_j'_sched, SCHED : scheduled_at sched j t
False
move : (LP) => /negP HH; apply : HH.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant LP : ~~ hep_job j j H_j'_sched, SCHED : scheduled_at sched j t
hep_job j j
specialize (H_priority_is_reflexive 0 ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive (T:=Job)
(hep_job_at 0 ) tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant LP : ~~ hep_job j j H_j'_sched, SCHED : scheduled_at sched j t
hep_job j j
unfold hep_job_at, JLFP_to_JLDP in *.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive (T:=Job)
(fun j1 : Job =>
[eta hep_job j1]) tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant LP : ~~ hep_job j j H_j'_sched, SCHED : scheduled_at sched j t
hep_job j j
by erewrite H_priority_is_reflexive; eauto 2 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j
has
(fun jlp : Job =>
scheduled_at sched jlp t && ~~ hep_job jlp j)
(arrivals_before arr_seq t.+1 )
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j
has
(fun jlp : Job =>
scheduled_at sched jlp t && ~~ hep_job jlp j)
(arrivals_before arr_seq t.+1 )
apply /hasP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j
exists2 x : Job,
x \in arrivals_before arr_seq t.+1 &
scheduled_at sched x t && ~~ hep_job x j
exists j' .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j
j' \in arrivals_before arr_seq t.+1
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j
j' \in arrivals_before arr_seq t.+1
apply arrived_between_implies_in_arrivals; eauto 2 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j
arrived_between j' 0 t.+1
apply /andP; split ; try done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j
job_arrival j' < t.+1
by rewrite ltnS; apply H_jobs_must_arrive_to_execute.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j
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 arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule (processor_state Job) 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 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H3 : JLFP_policy Job H_priority_is_reflexive : reflexive_priorities tsk : Task j : Job H_j_tsk : job_of_task tsk j t : instant j' : Job H_j'_sched : scheduled_at sched j' t LP : ~~ hep_job j' j
scheduled_at sched j' t && ~~ hep_job j' j
by apply /andP; split .
Qed .
End PIIdealProcessorModelLemmas .