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 Import prosa.model.readiness.basic.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]
Require Export prosa.model.task.sequentiality.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.model.priority.fifo.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.model.schedule.work_conserving.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.definitions.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 "[ 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.priority.sequential.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.readiness.basic.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.preemption.job.nonpreemptive.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]
(** In this section, we prove some fundamental properties of the FIFO policy. *)
Section BasicLemmas .
(** We assume the basic (i.e., Liu & Layland)
readiness model under which any pending job is ready. *)
#[local] Existing Instance basic_ready_instance .
(** Consider any type of jobs with arrival times and execution costs. *)
Context `{Job : JobType} {Arrival : JobArrival Job} {Cost : JobCost Job}.
(** Consider any arrival sequence of such jobs ... *)
Variable arr_seq : arrival_sequence Job.
(** ... and the resulting ideal uniprocessor schedule. We assume that the
schedule is valid and work-conserving. *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_schedule_is_valid : valid_schedule sched arr_seq.
Hypothesis H_work_conservation : work_conserving arr_seq sched.
(** Suppose jobs have preemption points ... *)
Context `{JobPreemptable Job}.
(** ...and that the preemption model is valid. *)
Hypothesis H_valid_preemption_model :
valid_preemption_model arr_seq sched.
(** Assume that the schedule respects the FIFO scheduling policy whenever jobs
are preemptable. *)
Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job).
(** We observe that there is no priority inversion in a
FIFO-compliant schedule. *)
Lemma FIFO_implies_no_priority_inversion :
forall j t ,
arrives_in arr_seq j ->
pending sched j t ->
~ priority_inversion sched j t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job)
forall (j : Job) (t : instant),
arrives_in arr_seq j ->
pending sched j t -> ~ priority_inversion sched j t
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job)
forall (j : Job) (t : instant),
arrives_in arr_seq j ->
pending sched j t -> ~ priority_inversion sched j t
move => j t ARRIVES /andP [ARRIVED /negP NCOMPL] [NSCHED [jlp /andP [SCHED PRIO]]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant ARRIVES : arrives_in arr_seq j ARRIVED : has_arrived j t NCOMPL : ~ completed_by sched j t NSCHED : ~~ scheduled_at sched j t jlp : Job SCHED : scheduled_at sched jlp t PRIO : ~~ hep_job jlp j
False
move : PRIO; rewrite /hep_job /FIFO -ltnNge => LT.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant ARRIVES : arrives_in arr_seq j ARRIVED : has_arrived j t NCOMPL : ~ completed_by sched j t NSCHED : ~~ scheduled_at sched j t jlp : Job SCHED : scheduled_at sched jlp t LT : job_arrival j < job_arrival jlp
False
apply : NCOMPL; eapply early_hep_job_is_scheduled; rt_eauto.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant ARRIVES : arrives_in arr_seq j ARRIVED : has_arrived j t NSCHED : ~~ scheduled_at sched j t jlp : Job SCHED : scheduled_at sched jlp t LT : job_arrival j < job_arrival jlp
always_higher_priority j jlp
by intros t'; apply /andP; split ; unfold hep_job_at, JLFP_to_JLDP, hep_job, FIFO; lia .
Qed .
(** In this section, we prove the cumulative priority inversion for any task
is bounded by [0]. *)
Section PriorityInversionBounded .
(** Consider any kind of tasks. *)
Context `{Task : TaskType} `{JobTask Job Task}.
(** Consider a task [tsk]. *)
Variable tsk : Task.
(** Assume the arrival times are consistent. *)
Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
(** Assume that the schedule follows the FIFO policy at preemption time. *)
Hypothesis H_respects_policy_at_preemption_point :
respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job).
(** Assume the schedule is valid. *)
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
(** Assume there are no duplicates in the arrival sequence. *)
Hypothesis H_arrival_sequence_is_a_set : arrival_sequence_uniq arr_seq.
(** Then we prove that the amount of priority inversion is bounded by 0. *)
Lemma FIFO_implies_no_pi :
priority_inversion_is_bounded_by_constant arr_seq sched tsk 0 .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq
priority_inversion_is_bounded_by_constant arr_seq
sched tsk 0
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq
priority_inversion_is_bounded_by_constant arr_seq
sched tsk 0
move => j ARRIN TASK POS t1 t2 BUSY.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2
cumulative_priority_inversion arr_seq sched j t1 t2 <=
0
rewrite /priority_inversion.cumulative_priority_inversion.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2
\sum_(t1 <= t < t2)
priority_inversion_dec arr_seq sched j t <= 0
have -> : \sum_(t1 <= t < t2) priority_inversion_dec arr_seq sched j t = 0 ;
last by done .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2
\sum_(t1 <= t < t2)
priority_inversion_dec arr_seq sched j t = 0
rewrite big_nat_eq0 => t /andP[T1 T2].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 t : nat T1 : t1 <= t T2 : t < t2
priority_inversion_dec arr_seq sched j t = 0
apply /eqP; rewrite eqb0.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 t : nat T1 : t1 <= t T2 : t < t2
~~ priority_inversion_dec arr_seq sched j t
apply /negP => /priority_inversion_P INV.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 t : nat T1 : t1 <= t T2 : t < t2 INV : jobs_come_from_arrival_sequence sched arr_seq ->
jobs_must_arrive_to_execute sched ->
consistent_arrival_times arr_seq ->
priority_inversion sched j t
False
feed_n 3 INV; rt_eauto. Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 t : nat T1 : t1 <= t T2 : t < t2 INV : priority_inversion sched j t
False
move : INV => [NSCHED [j__lp /andP [SCHED LP]]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 t : nat T1 : t1 <= t T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LP : ~~ hep_job j__lp j
False
move : LP; rewrite /hep_job /FIFO -ltnNge => LT.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 t : nat T1 : t1 <= t T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp
False
have COMPL: completed_by sched j t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 t : nat T1 : t1 <= t T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp
completed_by sched j t
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 t : nat T1 : t1 <= t T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp
completed_by sched j t
apply : early_hep_job_is_scheduled; rt_eauto.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 t : nat T1 : t1 <= t T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp
always_higher_priority j j__lp
move => t'; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FIFO -ltnNge.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 t : nat T1 : t1 <= t T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp t' : instant
(job_arrival j <= job_arrival j__lp) &&
(job_arrival j < job_arrival j__lp)
by apply /andP; split ; first apply ltnW. } Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 t : nat T1 : t1 <= t T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp COMPL : completed_by sched j t
False
move : BUSY => [LE [QT [NQT /andP[ARR1 ARR2]]]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant t : nat T1 : t1 <= t T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp COMPL : completed_by sched j t LE : t1 < t2 QT : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j tARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
False
move : T1; rewrite leq_eqVlt => /orP [/eqP EQ | GT].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant t : nat T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp COMPL : completed_by sched j t LE : t1 < t2 QT : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j tARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 EQ : t1 = t
False
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant t : nat T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp COMPL : completed_by sched j t LE : t1 < t2 QT : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j tARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 EQ : t1 = t
False
subst t; apply completed_implies_scheduled_before in COMPL; rt_eauto.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant NSCHED : ~~ scheduled_at sched j t1 T2 : t1 < t2 j__lp : Job SCHED : scheduled_at sched j__lp t1 LT : job_arrival j < job_arrival j__lp COMPL : exists t' : nat,
job_arrival j <= t' < t1 /\
scheduled_at sched j t'LE : t1 < t2 QT : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j tARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
False
by case : COMPL => [t' [/andP [ARR3 LT__temp] SCHED__temp]]; lia . } Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant t : nat T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp COMPL : completed_by sched j t LE : t1 < t2 QT : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j tARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 GT : t1 < t
False
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant t : nat T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp COMPL : completed_by sched j t LE : t1 < t2 QT : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j tARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 GT : t1 < t
False
apply : NQT; first (apply /andP; split ; [exact GT | lia ]).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant t : nat T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp COMPL : completed_by sched j t LE : t1 < t2 QT : quiet_time arr_seq sched j t1 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 GT : t1 < t
quiet_time arr_seq sched j t
intros ? ARR HEP ARRB; rewrite /hep_job /FIFO in HEP.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant t : nat T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp COMPL : completed_by sched j t LE : t1 < t2 QT : quiet_time arr_seq sched j t1 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 GT : t1 < t j_hp : Job ARR : arrives_in arr_seq j_hp ARRB : arrived_before j_hp t HEP : job_arrival j_hp <= job_arrival j
completed_by sched j_hp t
eapply early_hep_job_is_scheduled; rt_eauto; first by lia .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task tsk : Task H_consistent_arrival_times : consistent_arrival_times
arr_seq H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point
arr_seq sched
(FIFO Job) H_valid_schedule : valid_schedule sched arr_seq H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq j : Job ARRIN : arrives_in arr_seq j TASK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant t : nat T2 : t < t2 NSCHED : ~~ scheduled_at sched j t j__lp : Job SCHED : scheduled_at sched j__lp t LT : job_arrival j < job_arrival j__lp COMPL : completed_by sched j t LE : t1 < t2 QT : quiet_time arr_seq sched j t1 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 GT : t1 < t j_hp : Job ARR : arrives_in arr_seq j_hp ARRB : arrived_before j_hp t HEP : job_arrival j_hp <= job_arrival j
always_higher_priority j_hp j__lp
by move => t'; apply /andP; split ; rewrite /hep_job_at /FIFO /JLFP_to_JLDP /hep_job //=; lia . }
Qed .
End PriorityInversionBounded .
(** We prove that in a FIFO-compliant schedule, if a job [j] is
scheduled, then all jobs with higher priority than [j] have been
completed. *)
Lemma scheduled_implies_higher_priority_completed :
forall j t ,
scheduled_at sched j t ->
forall j_hp ,
arrives_in arr_seq j_hp ->
~~hep_job j j_hp ->
completed_by sched j_hp t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job)
forall (j : Job) (t : instant),
scheduled_at sched j t ->
forall j_hp : Job,
arrives_in arr_seq j_hp ->
~~ hep_job j j_hp -> completed_by sched j_hp t
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job)
forall (j : Job) (t : instant),
scheduled_at sched j t ->
forall j_hp : Job,
arrives_in arr_seq j_hp ->
~~ hep_job j j_hp -> completed_by sched j_hp t
move => j' t SCHED j_hp ARRjhp HEP.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j' : Job t : instant SCHED : scheduled_at sched j' t j_hp : Job ARRjhp : arrives_in arr_seq j_hp HEP : ~~ hep_job j' j_hp
completed_by sched j_hp t
have EARLIER: job_arrival j_hp < job_arrival j' by rewrite -ltnNge in HEP.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j' : Job t : instant SCHED : scheduled_at sched j' t j_hp : Job ARRjhp : arrives_in arr_seq j_hp HEP : ~~ hep_job j' j_hp EARLIER : job_arrival j_hp < job_arrival j'
completed_by sched j_hp t
eapply (early_hep_job_is_scheduled arr_seq _ sched _ _ _ _ j_hp j' _ _ _ t).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j' : Job t : instant SCHED : scheduled_at sched j' t j_hp : Job ARRjhp : arrives_in arr_seq j_hp HEP : ~~ hep_job j' j_hp EARLIER : job_arrival j_hp < job_arrival j'
scheduled_at sched j' t
Unshelve .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j' : Job t : instant SCHED : scheduled_at sched j' t j_hp : Job ARRjhp : arrives_in arr_seq j_hp HEP : ~~ hep_job j' j_hp EARLIER : job_arrival j_hp < job_arrival j'
scheduled_at sched j' t
all : rt_eauto.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j' : Job t : instant SCHED : scheduled_at sched j' t j_hp : Job ARRjhp : arrives_in arr_seq j_hp HEP : ~~ hep_job j' j_hp EARLIER : job_arrival j_hp < job_arrival j'
always_higher_priority j_hp j'
move => t'; apply /andP; split => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j' : Job t : instant SCHED : scheduled_at sched j' t j_hp : Job ARRjhp : arrives_in arr_seq j_hp HEP : ~~ hep_job j' j_hp EARLIER : job_arrival j_hp < job_arrival j' t' : instant
hep_job_at t' j_hp j'
by apply ltnW.
Qed .
(** The next lemma considers FIFO schedules in the context of tasks. *)
Section SequentialTasks .
(** If the scheduled jobs stem from a set of tasks, ... *)
Context {Task : TaskType}.
Context `{JobTask Job Task}.
(** ... then the tasks in a FIFO-compliant schedule necessarily
execute sequentially. *)
Lemma tasks_execute_sequentially : sequential_tasks arr_seq sched.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task
sequential_tasks arr_seq sched
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task
sequential_tasks arr_seq sched
move => j1 j2 t ARRj1 ARRj2 SAME_TASKx LT => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task j1, j2 : Job t : instant ARRj1 : arrives_in arr_seq j1 ARRj2 : arrives_in arr_seq j2 SAME_TASKx : same_task j1 j2 LT : job_arrival j1 < job_arrival j2
scheduled_at sched j2 t -> completed_by sched j1 t
eapply (early_hep_job_is_scheduled); try rt_eauto.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task j1, j2 : Job t : instant ARRj1 : arrives_in arr_seq j1 ARRj2 : arrives_in arr_seq j2 SAME_TASKx : same_task j1 j2 LT : job_arrival j1 < job_arrival j2
always_higher_priority j1 j2
by move => ?; apply /andP; split ; [apply ltnW | rewrite -ltnNge //=].
Qed .
(** We also note that the [FIFO] policy respects sequential tasks. *)
Fact fifo_respects_sequential_tasks : policy_respects_sequential_tasks.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task
policy_respects_sequential_tasks
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) Task : TaskType H0 : JobTask Job Task
policy_respects_sequential_tasks
by move => j1 j2 SAME ARRLE; rewrite /hep_job /FIFO. Qed .
End SequentialTasks .
(** Finally, let us further assume that there are no needless
preemptions among jobs of equal priority. *)
Hypothesis H_no_superfluous_preemptions : no_superfluous_preemptions sched.
(** In the absence of superfluous preemptions and under assumption
of the basic readiness model, there are no preemptions at all in
a FIFO-compliant schedule. *)
Lemma no_preemptions_under_FIFO :
forall j t ,
~~ preempted_at sched j t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched
forall (j : Job) (t : instant),
~~ preempted_at sched j t
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched
forall (j : Job) (t : instant),
~~ preempted_at sched j t
move => j t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched j : Job t : instant
~~ preempted_at sched j t
apply /negP.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched j : Job t : instant
~ preempted_at sched j t
intros CONTR.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched j : Job t : instant CONTR : preempted_at sched j t
False
move : CONTR => /andP [/andP [SCHED1 NCOMPL] SCHED2].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched j : Job t : instant SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t
False
move : H_schedule_is_valid => [COME MUST].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched j : Job t : instant SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched
False
move : (ideal_proc_model_sched_case_analysis sched t) => [IDLE |[s INTER]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched j : Job t : instant SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched IDLE : ideal.is_idle sched t
False
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched j : Job t : instant SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched IDLE : ideal.is_idle sched t
False
specialize (H_work_conservation j t).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq j : Job t : instant H_work_conservation : arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job,
scheduled_at sched j_other t H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched IDLE : ideal.is_idle sched t
False
destruct H_work_conservation as [j_other SCHEDj_other]; first by eapply (COME j t.-1 SCHED1).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq j : Job t : instant H_work_conservation : arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job,
scheduled_at sched j_other t H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched IDLE : ideal.is_idle sched t
backlogged sched j t
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq j : Job t : instant H_work_conservation : arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job,
scheduled_at sched j_other t H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched IDLE : ideal.is_idle sched t
backlogged sched j t
do 2 (apply /andP; split ; last by done ).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq j : Job t : instant H_work_conservation : arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job,
scheduled_at sched j_other t H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched IDLE : ideal.is_idle sched t
has_arrived j t
eapply scheduled_implies_pending in SCHED1; try rt_eauto.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq j : Job t : instant H_work_conservation : arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job,
scheduled_at sched j_other t H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched IDLE : ideal.is_idle sched t SCHED1 : pending sched j t.-1
has_arrived j t
move : SCHED1 => /andP [HAS COMPL].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq j : Job t : instant H_work_conservation : arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job,
scheduled_at sched j_other t H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched IDLE : ideal.is_idle sched t HAS : has_arrived j t.-1 COMPL : ~~ completed_by sched j t.-1
has_arrived j t
by apply leq_trans with t.-1 ; [exact HAS| lia ].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq j : Job t : instant H_work_conservation : arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job,
scheduled_at sched j_other t H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched IDLE : ideal.is_idle sched t j_other : Job SCHEDj_other : scheduled_at sched j_other t
False
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq j : Job t : instant H_work_conservation : arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job,
scheduled_at sched j_other t H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched IDLE : ideal.is_idle sched t j_other : Job SCHEDj_other : scheduled_at sched j_other t
False
move : SCHEDj_other IDLE.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq j : Job t : instant H_work_conservation : arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job,
scheduled_at sched j_other t H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched j_other : Job
scheduled_at sched j_other t ->
ideal.is_idle sched t -> False
rewrite scheduled_at_def => /eqP SCHED /eqP IDLE.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq j : Job t : instant H_work_conservation : arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job,
scheduled_at sched j_other t H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched j_other : Job SCHED : sched t = Some j_other IDLE : sched t = None
False
by rewrite IDLE in SCHED. } Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched j : Job t : instant SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched s : Job INTER : scheduled_at sched s t
False
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched j : Job t : instant SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched s : Job INTER : scheduled_at sched s t
False
specialize (H_no_superfluous_preemptions t j s).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant s : Job H_no_superfluous_preemptions : preempted_at sched j t ->
scheduled_at sched s t ->
~~ hep_job_at t j s SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched INTER : scheduled_at sched s t
False
have HEP : ~~ hep_job j s.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant s : Job H_no_superfluous_preemptions : preempted_at sched j t ->
scheduled_at sched s t ->
~~ hep_job_at t j s SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched INTER : scheduled_at sched s t
~~ hep_job j s
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant s : Job H_no_superfluous_preemptions : preempted_at sched j t ->
scheduled_at sched s t ->
~~ hep_job_at t j s SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched INTER : scheduled_at sched s t
~~ hep_job j s
apply H_no_superfluous_preemptions; last by done .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant s : Job H_no_superfluous_preemptions : preempted_at sched j t ->
scheduled_at sched s t ->
~~ hep_job_at t j s SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched INTER : scheduled_at sched s t
preempted_at sched j t
by repeat (apply /andP ; split ; try by done ).
} Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant s : Job H_no_superfluous_preemptions : preempted_at sched j t ->
scheduled_at sched s t ->
~~ hep_job_at t j s SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched INTER : scheduled_at sched s t HEP : ~~ hep_job j s
False
rewrite /hep_job /fifo.FIFO -ltnNge in HEP.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant s : Job H_no_superfluous_preemptions : preempted_at sched j t ->
scheduled_at sched s t ->
~~ hep_job_at t j s SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched INTER : scheduled_at sched s t HEP : job_arrival s < job_arrival j
False
eapply (early_hep_job_is_scheduled arr_seq ) in SCHED1; try rt_eauto.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant s : Job H_no_superfluous_preemptions : preempted_at sched j t ->
scheduled_at sched s t ->
~~ hep_job_at t j s NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched INTER : scheduled_at sched s t HEP : job_arrival s < job_arrival j SCHED1 : completed_by sched s t.-1
False
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant s : Job H_no_superfluous_preemptions : preempted_at sched j t ->
scheduled_at sched s t ->
~~ hep_job_at t j s NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched INTER : scheduled_at sched s t HEP : job_arrival s < job_arrival j SCHED1 : completed_by sched s t.-1
False
apply scheduled_implies_not_completed in INTER; rt_eauto.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant s : Job H_no_superfluous_preemptions : preempted_at sched j t ->
scheduled_at sched s t ->
~~ hep_job_at t j s NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched INTER : ~~ completed_by sched s t HEP : job_arrival s < job_arrival j SCHED1 : completed_by sched s t.-1
False
by eapply (incompletion_monotonic sched s t.-1 t) in INTER; [move : INTER => /negP|lia ].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant s : Job H_no_superfluous_preemptions : preempted_at sched j t ->
scheduled_at sched s t ->
~~ hep_job_at t j s SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched INTER : scheduled_at sched s t HEP : job_arrival s < job_arrival j
always_higher_priority s j
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) j : Job t : instant s : Job H_no_superfluous_preemptions : preempted_at sched j t ->
scheduled_at sched s t ->
~~ hep_job_at t j s SCHED1 : scheduled_at sched j t.-1 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t COME : jobs_come_from_arrival_sequence sched arr_seq MUST : jobs_must_be_ready_to_execute sched INTER : scheduled_at sched s t HEP : job_arrival s < job_arrival j
always_higher_priority s j
by move => ?; apply /andP; split ; [apply ltnW | rewrite -ltnNge //=]. }
Qed .
(** It immediately follows that FIFO schedules are
non-preemptive. *)
Corollary FIFO_is_nonpreemptive : nonpreemptive_schedule sched.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched
nonpreemptive_schedule sched
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_schedule_is_valid : valid_schedule sched arr_seq H_work_conservation : work_conserving arr_seq sched H : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched (FIFO Job) H_no_superfluous_preemptions : no_superfluous_preemptions
sched
nonpreemptive_schedule sched
by rewrite -no_preemptions_equiv_nonpreemptive; apply no_preemptions_under_FIFO.
Qed .
End BasicLemmas .
(** We add the following lemmas to the basic facts database *)
Global Hint Resolve
fifo_respects_sequential_tasks
tasks_execute_sequentially
: basic_rt_facts.