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.schedule.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]
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.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 ->
~~ is_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 ->
~~ is_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 ->
~~ is_priority_inversion sched j t
move => j t ARRIVES PENDINGj.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 PENDINGj : pending sched j t
~~ is_priority_inversion sched j t
rewrite /is_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) j : Job t : instant ARRIVES : arrives_in arr_seq j PENDINGj : pending sched j t
~~
match sched t with
| Some jlp => ~~ hep_job jlp j
| None => false
end
move : (ideal_proc_model_sched_case_analysis sched t) => [/eqP -> //|[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) j : Job t : instant ARRIVES : arrives_in arr_seq j PENDINGj : pending sched j t s : Job INTER : scheduled_at sched s t
~~
match sched t with
| Some jlp => ~~ hep_job jlp j
| None => false
end
have -> : sched t = Some s; first by apply /eqP; rewrite -scheduled_at_def.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 PENDINGj : pending sched j t s : Job INTER : scheduled_at sched s t
~~ ~~ hep_job s j
apply /negP; apply /negPn.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 PENDINGj : pending sched j t s : Job INTER : scheduled_at sched s t
~~ ~~ hep_job s j
rewrite Bool.negb_involutive.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 PENDINGj : pending sched j t s : Job INTER : scheduled_at sched s t
hep_job s j
destruct (s == j) eqn :EQ; first by move : EQ => /eqP ->; rewrite /hep_job /fifo.FIFO.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 PENDINGj : pending sched j t s : Job INTER : scheduled_at sched s t EQ : (s == j) = false
hep_job s j
destruct (hep_job s j) eqn :HEP; first 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 ARRIVES : arrives_in arr_seq j PENDINGj : pending sched j t s : Job INTER : scheduled_at sched s t EQ : (s == j) = false HEP : hep_job s j = false
false
move : HEP => /negP/negP 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 ARRIVES : arrives_in arr_seq j PENDINGj : pending sched j t s : Job INTER : scheduled_at sched s t EQ : (s == j) = false HEP : ~~ hep_job s j
false
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 ARRIVES : arrives_in arr_seq j PENDINGj : pending sched j t s : Job INTER : scheduled_at sched s t EQ : (s == j) = false HEP : job_arrival j < job_arrival s
false
contradict PENDINGj.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 s : Job INTER : scheduled_at sched s t EQ : (s == j) = false HEP : job_arrival j < job_arrival s
~ pending sched j t
apply /negP; rewrite negb_and.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 s : Job INTER : scheduled_at sched s t EQ : (s == j) = false HEP : job_arrival j < job_arrival s
~~ has_arrived j t || ~~ ~~ completed_by sched j t
apply /orP; right ; apply /negPn.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 s : Job INTER : scheduled_at sched s t EQ : (s == j) = false HEP : job_arrival j < job_arrival s
completed_by sched j t
have -> : scheduled_at sched s t -> 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) j : Job t : instant ARRIVES : arrives_in arr_seq j s : Job INTER : scheduled_at sched s t EQ : (s == j) = false HEP : job_arrival j < job_arrival s
scheduled_at sched s t -> completed_by sched j 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) j : Job t : instant ARRIVES : arrives_in arr_seq j s : Job INTER : scheduled_at sched s t EQ : (s == j) = false HEP : job_arrival j < job_arrival s
always_higher_priority 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 ARRIVES : arrives_in arr_seq j s : Job INTER : scheduled_at sched s t EQ : (s == j) = false HEP : job_arrival j < job_arrival s
always_higher_priority j s
by move => ?; apply /andP; split ; [apply ltnW | rewrite -ltnNge //=].
Qed .
(** 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 .
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 .