Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Import prosa.model.readiness.basic.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.model.task.sequentiality.
Require Export prosa.model.priority.fifo.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.analysis.definitions.priority_inversion.
Require Export prosa.analysis.facts.priority.sequential.
Require Export prosa.analysis.facts.readiness.basic.
Require Export prosa.analysis.facts.busy_interval.all .
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
Require Export prosa.analysis.facts.priority.inversion .
Require Export prosa.analysis.facts.busy_interval.service_inversion.
(** We first make some trivial observations about the FIFO priority policy to
avoid having to re-reason these steps repeatedly in the subsequent
proofs. *)
Section PriorityFacts .
(** Consider any type of jobs. *)
Context `{Job : JobType} {Arrival : JobArrival Job}.
(** Under FIFO scheduling, [hep_job] is simply a statement about arrival
times. *)
Fact hep_job_arrival_FIFO :
forall j j' ,
hep_job j j' = (job_arrival j <= job_arrival j').Job : JobType Arrival : JobArrival Job
forall j j' : Job,
hep_job j j' = (job_arrival j <= job_arrival j')
Proof .Job : JobType Arrival : JobArrival Job
forall j j' : Job,
hep_job j j' = (job_arrival j <= job_arrival j')
move => j j'.Job : JobType Arrival : JobArrival Job j, j' : Job
hep_job j j' = (job_arrival j <= job_arrival j')
by rewrite /hep_job /FIFO.
Qed .
(** Similarly, [~~ hep_job] implies a strict inequality on arrival times. *)
Fact not_hep_job_arrival_FIFO :
forall j j' ,
~~ hep_job j j' = (job_arrival j' < job_arrival j).Job : JobType Arrival : JobArrival Job
forall j j' : Job,
~~ hep_job j j' = (job_arrival j' < job_arrival j)
Proof .Job : JobType Arrival : JobArrival Job
forall j j' : Job,
~~ hep_job j j' = (job_arrival j' < job_arrival j)
by move => j j'; rewrite hep_job_arrival_FIFO -ltnNge. Qed .
(** Combining the above two facts, we get that, trivially, [~~ hep_job j j']
implies [hep_job j' j], ... *)
Fact not_hep_job_FIFO :
forall j j' ,
~~ hep_job j j' -> hep_job j' j.Job : JobType Arrival : JobArrival Job
forall j j' : Job, ~~ hep_job j j' -> hep_job j' j
Proof .Job : JobType Arrival : JobArrival Job
forall j j' : Job, ~~ hep_job j j' -> hep_job j' j
move => j j'; rewrite not_hep_job_arrival_FIFO hep_job_arrival_FIFO.Job : JobType Arrival : JobArrival Job j, j' : Job
job_arrival j' < job_arrival j ->
job_arrival j' <= job_arrival j
exact : ltnW.
Qed .
(** ... from which we can infer [always_higher_priority]. *)
Fact not_hep_job_always_higher_priority_FIFO :
forall j j' ,
~~ hep_job j j' -> always_higher_priority j' j.Job : JobType Arrival : JobArrival Job
forall j j' : Job,
~~ hep_job j j' -> always_higher_priority j' j
Proof .Job : JobType Arrival : JobArrival Job
forall j j' : Job,
~~ hep_job j j' -> always_higher_priority j' j
move => j j' NHEP.Job : JobType Arrival : JobArrival Job j, j' : Job NHEP : ~~ hep_job j j'
always_higher_priority j' j
rewrite always_higher_priority_jlfp; apply /andP; split => //.Job : JobType Arrival : JobArrival Job j, j' : Job NHEP : ~~ hep_job j j'
hep_job j' j
exact : not_hep_job_FIFO.
Qed .
End PriorityFacts .
(** 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 valid arrival sequence of such jobs ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
(** ... and the resulting uniprocessor schedule. *)
Context {PState : ProcessorState Job}.
Hypothesis H_uniproc : uniprocessor_model PState.
Variable sched : schedule PState.
(** We assume that the schedule is valid and work-conserving. *)
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 arr_seq sched j t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 arr_seq sched j t
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 arr_seq sched j t
move => j t IN /andP[ARR]; apply : contraNN => pijt.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 IN : arrives_in arr_seq j ARR : has_arrived j t pijt : priority_inversion arr_seq sched j t
completed_by sched j t
have [j' + PRIO] : exists2 j', scheduled_at sched j' t & ~~ hep_job j' j
by exact /uni_priority_inversion_P.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 IN : arrives_in arr_seq j ARR : has_arrived j t pijt : priority_inversion arr_seq sched j t j' : Job PRIO : ~~ hep_job j' j
scheduled_at sched j' t -> completed_by sched j t
apply : (early_hep_job_is_scheduled arr_seq) => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 IN : arrives_in arr_seq j ARR : has_arrived j t pijt : priority_inversion arr_seq sched j t j' : Job PRIO : ~~ hep_job j' j
job_arrival j < job_arrival j'
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 IN : arrives_in arr_seq j ARR : has_arrived j t pijt : priority_inversion arr_seq sched j t j' : Job PRIO : ~~ hep_job j' j
job_arrival j < job_arrival j'
by rewrite -not_hep_job_arrival_FIFO.
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 IN : arrives_in arr_seq j ARR : has_arrived j t pijt : priority_inversion arr_seq sched j t j' : Job PRIO : ~~ hep_job j' j
always_higher_priority j j'
exact : not_hep_job_always_higher_priority_FIFO.
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 H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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
apply : early_hep_job_is_scheduled => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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
job_arrival j_hp < job_arrival j'
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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
job_arrival j_hp < job_arrival j'
by rewrite -not_hep_job_arrival_FIFO.
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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
always_higher_priority j_hp j'
exact : not_hep_job_always_higher_priority_FIFO.
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 arr_seq sched tsk (constant 0 ).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 arr_seq sched tsk
(constant 0 )
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 arr_seq sched tsk
(constant 0 )
move => j ARRIN TASK POS t1 t2 BUSY.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 <=
constant 0 (job_arrival j - t1)
rewrite leqn0; apply /eqP; rewrite big_nat_eq0 => t /andP[T1 T2].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 arr_seq sched j t = 0
apply /eqP; rewrite eqb0.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 arr_seq sched j t
apply : contraT => /negPn pijt.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 pijt : priority_inversion arr_seq sched j t
false
have [j' SCHED NHEP] : exists2 j', scheduled_at sched j' t & ~~ hep_job j' j
by exact /uni_priority_inversion_P.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 pijt : priority_inversion arr_seq sched j t j' : Job SCHED : scheduled_at sched j' t NHEP : ~~ hep_job j' j
false
move : T1; rewrite leq_eqVlt => /orP [/eqP EQ | GT].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 T2 : t < t2 pijt : priority_inversion arr_seq sched j t j' : Job SCHED : scheduled_at sched j' t NHEP : ~~ hep_job j' j EQ : t1 = t
false
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 T2 : t < t2 pijt : priority_inversion arr_seq sched j t j' : Job SCHED : scheduled_at sched j' t NHEP : ~~ hep_job j' j EQ : t1 = t
false
have /completed_implies_scheduled_before [//|//|t' [/andP [+ +] _]]:
completed_by sched j t by apply : (scheduled_implies_higher_priority_completed j').Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 T2 : t < t2 pijt : priority_inversion arr_seq sched j t j' : Job SCHED : scheduled_at sched j' t NHEP : ~~ hep_job j' j EQ : t1 = t t' : nat
job_arrival j <= t' -> t' < t -> false
by have : t1 <= job_arrival j by []; rewrite -EQ; lia . } Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 T2 : t < t2 pijt : priority_inversion arr_seq sched j t j' : Job SCHED : scheduled_at sched j' t NHEP : ~~ hep_job j' j GT : t1 < t
false
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 T2 : t < t2 pijt : priority_inversion arr_seq sched j t j' : Job SCHED : scheduled_at sched j' t NHEP : ~~ hep_job j' j GT : t1 < t
false
exfalso ; apply : busy_interval_prefix_no_quiet_time => // [|? ARR HEP ARRB];
first by apply /andP; split ; [|exact : T2].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 T2 : t < t2 pijt : priority_inversion arr_seq sched j t j' : Job SCHED : scheduled_at sched j' t NHEP : ~~ hep_job j' j GT : t1 < t _j_hp_ : Job ARR : arrives_in arr_seq _j_hp_ HEP : hep_job _j_hp_ j ARRB : arrived_before _j_hp_ t
completed_by sched _j_hp_ t
apply : (scheduled_implies_higher_priority_completed j') => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 T2 : t < t2 pijt : priority_inversion arr_seq sched j t j' : Job SCHED : scheduled_at sched j' t NHEP : ~~ hep_job j' j GT : t1 < t _j_hp_ : Job ARR : arrives_in arr_seq _j_hp_ HEP : hep_job _j_hp_ j ARRB : arrived_before _j_hp_ t
~~ hep_job j' _j_hp_
move : NHEP; rewrite !not_hep_job_arrival_FIFO.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 T2 : t < t2 pijt : priority_inversion arr_seq sched j t j' : Job SCHED : scheduled_at sched j' t GT : t1 < t _j_hp_ : Job ARR : arrives_in arr_seq _j_hp_ HEP : hep_job _j_hp_ j ARRB : arrived_before _j_hp_ t
job_arrival j < job_arrival j' ->
job_arrival _j_hp_ < job_arrival j'
by apply : leq_trans. }
Qed .
(** As a corollary, FIFO implies the absence of service inversion. *)
Corollary FIFO_implies_no_service_inversion :
service_inversion_is_bounded_by arr_seq sched tsk (constant 0 ).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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
service_inversion_is_bounded_by arr_seq sched tsk
(constant 0 )
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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
service_inversion_is_bounded_by arr_seq sched tsk
(constant 0 )
move => j ARR TSK POS t1 t2 PREF.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 ARR : arrives_in arr_seq j TSK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant PREF : busy_interval_prefix arr_seq sched j t1 t2
cumulative_service_inversion arr_seq sched j t1 t2 <=
constant 0 (job_arrival j - t1)
rewrite (leqRW (cumul_service_inv_le_cumul_priority_inv _ _ _ _ _ _ _ _ _ _)) //=.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 ARR : arrives_in arr_seq j TSK : job_of_task tsk j POS : 0 < job_cost jt1, t2 : instant PREF : busy_interval_prefix arr_seq sched j t1 t2
cumulative_priority_inversion arr_seq sched j t1 t2 <=
constant 0 (job_arrival j - t1)
by apply FIFO_implies_no_pi.
Qed .
End PriorityInversionBounded .
(** 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 H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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
apply : (early_hep_job_is_scheduled) => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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
apply : not_hep_job_always_higher_priority_FIFO.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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
~~ hep_job j2 j1
by rewrite not_hep_job_arrival_FIFO.
Qed .
(** We also note that the [FIFO] policy respects sequential tasks. *)
Fact fifo_respects_sequential_tasks : policy_respects_sequential_tasks (FIFO Job).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 (FIFO Job)
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 (FIFO Job)
by move => j1 j2 SAME ARRLE; rewrite hep_job_arrival_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 H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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; apply /negP => /andP [/andP [SCHED1 NCOMPL] SCHED2].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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
case SJA: (scheduled_job_at arr_seq sched t) => [j'|].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 j' : Job SJA : scheduled_job_at arr_seq sched t = Some j'
False
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 j' : Job SJA : scheduled_job_at arr_seq sched t = Some j'
False
move : SJA => /eqP; rewrite scheduled_job_at_scheduled_at // => SCHED'.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 j' : Job SCHED' : scheduled_at sched j' t
False
have : ~~ hep_job j j'.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 j' : Job SCHED' : scheduled_at sched j' t
~~ hep_job j j'
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 j' : Job SCHED' : scheduled_at sched j' t
~~ hep_job j j'
apply : H_no_superfluous_preemptions; last exact : SCHED'.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 j' : Job SCHED' : scheduled_at sched j' t
preempted_at sched j t
by repeat (apply /andP ; split ). } Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 j' : Job SCHED' : scheduled_at sched j' t
~~ hep_job j j' -> False
rewrite /hep_job /fifo.FIFO -ltnNge => EARLIER.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 j' : Job SCHED' : scheduled_at sched j' t EARLIER : job_arrival j' < job_arrival j
False
eapply (early_hep_job_is_scheduled arr_seq) with (JLFP:=FIFO Job) in SCHED1 => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t j' : Job SCHED' : scheduled_at sched j' t EARLIER : job_arrival j' < job_arrival j SCHED1 : completed_by sched j' t.-1
False
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t j' : Job SCHED' : scheduled_at sched j' t EARLIER : job_arrival j' < job_arrival j SCHED1 : completed_by sched j' t.-1
False
apply scheduled_implies_not_completed in SCHED' => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 NCOMPL : ~~ completed_by sched j t SCHED2 : ~~ scheduled_at sched j t j' : Job SCHED' : ~~ completed_by sched j' t EARLIER : job_arrival j' < job_arrival j SCHED1 : completed_by sched j' t.-1
False
by eapply (incompletion_monotonic sched j' t.-1 t) in SCHED'; [move : SCHED' => /negP|lia ].
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 j' : Job SCHED' : scheduled_at sched j' t EARLIER : job_arrival j' < job_arrival j
always_higher_priority j' j
by move => ?; apply /andP; split ; [apply ltnW | rewrite -ltnNge //=]. } Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 SJA : scheduled_job_at arr_seq sched t = None
False
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 SJA : scheduled_job_at arr_seq sched t = None
False
move : SJA; rewrite scheduled_job_at_none => // NSCHED.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 NSCHED : forall j : Job, ~~ scheduled_at sched j t
False
have [j' SCHED']: exists j' , scheduled_at sched j' t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 NSCHED : forall j : Job, ~~ scheduled_at sched j t
exists j' : Job, scheduled_at sched j' t
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 NSCHED : forall j : Job, ~~ scheduled_at sched j t
exists j' : Job, scheduled_at sched j' t
apply : (H_work_conservation j t) => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 NSCHED : forall j : Job, ~~ scheduled_at sched j t
backlogged sched j t
apply /andP; split => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 NSCHED : forall j : Job, ~~ scheduled_at sched j t
job_ready sched j t
rewrite /job_ready/basic_ready_instance/pending.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 NSCHED : forall j : Job, ~~ scheduled_at sched j t
has_arrived j t && ~~ completed_by sched j t
apply /andP; split => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 NSCHED : forall j : Job, ~~ scheduled_at sched j t
has_arrived j t
have : has_arrived j t.-1 ; last by rewrite /has_arrived; lia .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 NSCHED : forall j : Job, ~~ scheduled_at sched j t
has_arrived j t.-1
exact : has_arrived_scheduled. } Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 NSCHED : forall j : Job, ~~ scheduled_at sched j tj' : Job SCHED' : scheduled_at sched j' t
False
by move : (NSCHED j') => /negP. }
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 H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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 H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState 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.