Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.model.schedule.priority_driven.[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 ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.model.scheduled.
(** In this section, we establish two basic facts about preemption times. *)
Section PreemptionTimes .
(** Consider any type of jobs. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** In addition, we assume the existence of a function mapping a job and
its progress to a boolean value saying whether this job is
preemptable at its current point of execution. *)
Context `{JobPreemptable Job}.
(** Consider any valid arrival sequence *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
(** Allow for any uniprocessor model. *)
Context {PState : ProcessorState Job}.
Hypothesis H_uniproc : uniprocessor_model PState.
(** Next, consider any schedule of the arrival sequence... *)
Variable sched : schedule PState.
(** ... where jobs come from the arrival sequence and don't execute before
their arrival time. *)
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_must_arrive : jobs_must_arrive_to_execute sched.
(** Consider a valid preemption model. *)
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
(** We start with a trivial fact that, given a time interval <<[t1,
t2)>>, the interval either contains a preemption time [t] or it
does not. *)
Lemma preemption_time_interval_case :
forall t1 t2 ,
(forall t , t1 <= t < t2 -> ~~ preemption_time arr_seq sched t)
\/ (exists t ,
t1 <= t < t2
/\ preemption_time arr_seq sched t
/\ forall t' , t1 <= t' -> preemption_time arr_seq sched t' -> t <= t').Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall t1 t2 : nat,
(forall t : nat,
t1 <= t < t2 -> ~~ preemption_time arr_seq sched t) \/
(exists t : nat,
t1 <= t < t2 /\
preemption_time arr_seq sched t /\
(forall t' : nat,
t1 <= t' ->
preemption_time arr_seq sched t' -> t <= t'))
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall t1 t2 : nat,
(forall t : nat,
t1 <= t < t2 -> ~~ preemption_time arr_seq sched t) \/
(exists t : nat,
t1 <= t < t2 /\
preemption_time arr_seq sched t /\
(forall t' : nat,
t1 <= t' ->
preemption_time arr_seq sched t' -> t <= t'))
by apply earliest_pred_element_exists_case. Qed .
(** An idle instant is a preemption time. *)
Lemma idle_time_is_pt :
forall t ,
is_idle arr_seq sched t ->
preemption_time arr_seq sched t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall t : instant,
is_idle arr_seq sched t ->
preemption_time arr_seq sched t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall t : instant,
is_idle arr_seq sched t ->
preemption_time arr_seq sched t
by move => t; rewrite is_idle_iff /preemption_time => /eqP ->. Qed .
(** We show that time 0 is a preemption time. *)
Lemma zero_is_pt : preemption_time arr_seq sched 0 .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
preemption_time arr_seq sched 0
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
preemption_time arr_seq sched 0
rewrite /preemption_time.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
match scheduled_job_at arr_seq sched 0 with
| Some j => job_preemptable j (service sched j 0 )
| None => true
end
case SCHED: (scheduled_job_at _ _ 0 ) => [j|//].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job SCHED : scheduled_job_at arr_seq sched 0 = Some j
job_preemptable j (service sched j 0 )
have ARR: arrives_in arr_seq j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job SCHED : scheduled_job_at arr_seq sched 0 = Some j
arrives_in arr_seq j
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job SCHED : scheduled_job_at arr_seq sched 0 = Some j
arrives_in arr_seq j
apply : H_jobs_come_from_arrival_sequence.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job SCHED : scheduled_job_at arr_seq sched 0 = Some j
scheduled_at sched j ?Goal0
rewrite -(scheduled_job_at_scheduled_at arr_seq) //; exact /eqP/SCHED. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job SCHED : scheduled_job_at arr_seq sched 0 = Some j ARR : arrives_in arr_seq j
job_preemptable j (service sched j 0 )
rewrite /service /service_during big_geq //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job SCHED : scheduled_job_at arr_seq sched 0 = Some j ARR : arrives_in arr_seq j
job_preemptable j 0
by move : (H_valid_preemption_model j ARR) => [PP _].
Qed .
(** Also, we show that the first instant of execution is a preemption time. *)
Lemma first_moment_is_pt :
forall j prt ,
arrives_in arr_seq j ->
~~ scheduled_at sched j prt ->
scheduled_at sched j prt.+1 ->
preemption_time arr_seq sched prt.+1 .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (prt : instant),
arrives_in arr_seq j ->
~~ scheduled_at sched j prt ->
scheduled_at sched j prt.+1 ->
preemption_time arr_seq sched prt.+1
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (prt : instant),
arrives_in arr_seq j ->
~~ scheduled_at sched j prt ->
scheduled_at sched j prt.+1 ->
preemption_time arr_seq sched prt.+1
move => s pt ARR NSCHED SCHED.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job pt : instant ARR : arrives_in arr_seq s NSCHED : ~~ scheduled_at sched s pt SCHED : scheduled_at sched s pt.+1
preemption_time arr_seq sched pt.+1
move : (SCHED); rewrite /preemption_time -(scheduled_job_at_scheduled_at arr_seq) // => /eqP ->.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job pt : instant ARR : arrives_in arr_seq s NSCHED : ~~ scheduled_at sched s pt SCHED : scheduled_at sched s pt.+1
job_preemptable s (service sched s pt.+1 )
by move : (H_valid_preemption_model s ARR) => [_ [_ [_ P]]]; apply P.
Qed .
(** If a job is scheduled at a point in time that is not a preemption time,
then it was previously scheduled. *)
Lemma neg_pt_scheduled_at :
forall j t ,
scheduled_at sched j t.+1 ->
~~ preemption_time arr_seq sched t.+1 ->
scheduled_at sched j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t : nat),
scheduled_at sched j t.+1 ->
~~ preemption_time arr_seq sched t.+1 ->
scheduled_at sched j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t : nat),
scheduled_at sched j t.+1 ->
~~ preemption_time arr_seq sched t.+1 ->
scheduled_at sched j t
move => j t sched_at_next.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : nat sched_at_next : scheduled_at sched j t.+1
~~ preemption_time arr_seq sched t.+1 ->
scheduled_at sched j t
apply contraNT => NSCHED.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : nat sched_at_next : scheduled_at sched j t.+1 NSCHED : ~~ scheduled_at sched j t
preemption_time arr_seq sched t.+1
exact : (first_moment_is_pt j).
Qed .
(** If a job is scheduled at time [t-1] and time [t] is not a
preemption time, then the job is scheduled at time [t] as
well. *)
Lemma neg_pt_scheduled_before :
forall j t ,
~~ preemption_time arr_seq sched t ->
scheduled_at sched j t.-1 ->
scheduled_at sched j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t : instant),
~~ preemption_time arr_seq sched t ->
scheduled_at sched j t.-1 -> scheduled_at sched j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t : instant),
~~ preemption_time arr_seq sched t ->
scheduled_at sched j t.-1 -> scheduled_at sched j t
move => j t NP SCHED; apply negbNE; apply /negP => NSCHED.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant NP : ~~ preemption_time arr_seq sched t SCHED : scheduled_at sched j t.-1 NSCHED : ~~ scheduled_at sched j t
False
have [Z|POS] := posnP t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant NP : ~~ preemption_time arr_seq sched t SCHED : scheduled_at sched j t.-1 NSCHED : ~~ scheduled_at sched j t Z : t = 0
False
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant NP : ~~ preemption_time arr_seq sched t SCHED : scheduled_at sched j t.-1 NSCHED : ~~ scheduled_at sched j t Z : t = 0
False
by move : SCHED; subst => //= => SCHED; rewrite SCHED in NSCHED. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant NP : ~~ preemption_time arr_seq sched t SCHED : scheduled_at sched j t.-1 NSCHED : ~~ scheduled_at sched j t POS : 0 < t
False
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant NP : ~~ preemption_time arr_seq sched t SCHED : scheduled_at sched j t.-1 NSCHED : ~~ scheduled_at sched j t POS : 0 < t
False
edestruct scheduled_at_cases as [IDLE| [s SCHEDs]] => //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant NP : ~~ preemption_time arr_seq sched t SCHED : scheduled_at sched j t.-1 NSCHED : ~~ scheduled_at sched j t POS : 0 < tIDLE : is_idle arr_seq sched ?t
False
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant NP : ~~ preemption_time arr_seq sched t SCHED : scheduled_at sched j t.-1 NSCHED : ~~ scheduled_at sched j t POS : 0 < tIDLE : is_idle arr_seq sched ?t
False
move : NP => /negP NP; apply : NP; rewrite /preemption_time.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t.-1 NSCHED : ~~ scheduled_at sched j t POS : 0 < tIDLE : is_idle arr_seq sched ?t
match scheduled_job_at arr_seq sched t with
| Some j => job_preemptable j (service sched j t)
| None => true
end
by rewrite is_idle_iff in IDLE; move : IDLE => /eqP ->. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant NP : ~~ preemption_time arr_seq sched t SCHED : scheduled_at sched j t.-1 NSCHED : ~~ scheduled_at sched j t POS : 0 < ts : Job SCHEDs : scheduled_at sched s ?t
False
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant NP : ~~ preemption_time arr_seq sched t SCHED : scheduled_at sched j t.-1 NSCHED : ~~ scheduled_at sched j t POS : 0 < ts : Job SCHEDs : scheduled_at sched s ?t
False
instantiate (1 := t) in SCHEDs.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant NP : ~~ preemption_time arr_seq sched t SCHED : scheduled_at sched j t.-1 NSCHED : ~~ scheduled_at sched j t POS : 0 < ts : Job SCHEDs : scheduled_at sched s t
False
destruct t as [ | t]; [by done | rewrite -pred_Sn in SCHED].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : nat NP : ~~ preemption_time arr_seq sched t.+1 NSCHED : ~~ scheduled_at sched j t.+1 POS : 0 < t.+1 s : Job SCHEDs : scheduled_at sched s t.+1 SCHED : scheduled_at sched j t
False
move : (SCHEDs) => SCHEDst; eapply neg_pt_scheduled_at in SCHEDs => //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : nat NP : ~~ preemption_time arr_seq sched t.+1 NSCHED : ~~ scheduled_at sched j t.+1 POS : 0 < t.+1 s : Job SCHEDs : scheduled_at sched s t SCHED : scheduled_at sched j t SCHEDst : scheduled_at sched s t.+1
False
have EQ : s = j by apply : H_uniproc; [apply SCHEDs | apply SCHED].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : nat NP : ~~ preemption_time arr_seq sched t.+1 NSCHED : ~~ scheduled_at sched j t.+1 POS : 0 < t.+1 s : Job SCHEDs : scheduled_at sched s t SCHED : scheduled_at sched j t SCHEDst : scheduled_at sched s t.+1 EQ : s = j
False
by subst ; rewrite SCHEDst in NSCHED. } }
Qed .
(** Next we extend the above lemma to an interval. That is, as long as there
is no preemption time, a job will remain scheduled. *)
Lemma neg_pt_scheduled_continuously_before :
forall j t1 t2 ,
scheduled_at sched j t1 ->
t1 <= t2 ->
(forall t , t1 < t <= t2 -> ~~ preemption_time arr_seq sched t) ->
scheduled_at sched j t2.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t1 : instant) (t2 : nat),
scheduled_at sched j t1 ->
t1 <= t2 ->
(forall t : nat,
t1 < t <= t2 -> ~~ preemption_time arr_seq sched t) ->
scheduled_at sched j t2
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t1 : instant) (t2 : nat),
scheduled_at sched j t1 ->
t1 <= t2 ->
(forall t : nat,
t1 < t <= t2 -> ~~ preemption_time arr_seq sched t) ->
scheduled_at sched j t2
move => j1 t1 t2 SCHEDBEF LE NPT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1 : instant t2 : nat SCHEDBEF : scheduled_at sched j1 t1 LE : t1 <= t2 NPT : forall t : nat,
t1 < t <= t2 ->
~~ preemption_time arr_seq sched t
scheduled_at sched j1 t2
interval_to_duration t1 t2 t. Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1 : instant SCHEDBEF : scheduled_at sched j1 t1 t : nat NPT : forall t0 : nat,
t1 < t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0
scheduled_at sched j1 (t1 + t)
induction t as [ | t IHt]; first by rewrite addn0.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1 : instant SCHEDBEF : scheduled_at sched j1 t1 t : nat NPT : forall t0 : nat,
t1 < t0 <= t1 + t.+1 ->
~~ preemption_time arr_seq sched t0IHt : (forall t0 : nat,
t1 < t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j1 (t1 + t)
scheduled_at sched j1 (t1 + t.+1 )
apply neg_pt_scheduled_before; last rewrite addnS -pred_Sn.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1 : instant SCHEDBEF : scheduled_at sched j1 t1 t : nat NPT : forall t0 : nat,
t1 < t0 <= t1 + t.+1 ->
~~ preemption_time arr_seq sched t0IHt : (forall t0 : nat,
t1 < t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j1 (t1 + t)
~~ preemption_time arr_seq sched (t1 + t.+1 )
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1 : instant SCHEDBEF : scheduled_at sched j1 t1 t : nat NPT : forall t0 : nat,
t1 < t0 <= t1 + t.+1 ->
~~ preemption_time arr_seq sched t0IHt : (forall t0 : nat,
t1 < t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j1 (t1 + t)
~~ preemption_time arr_seq sched (t1 + t.+1 )
by apply NPT; lia .
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1 : instant SCHEDBEF : scheduled_at sched j1 t1 t : nat NPT : forall t0 : nat,
t1 < t0 <= t1 + t.+1 ->
~~ preemption_time arr_seq sched t0IHt : (forall t0 : nat,
t1 < t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j1 (t1 + t)
scheduled_at sched j1 (t1 + t)
by apply IHt => ??; apply NPT; lia .
Qed .
(** Conversely if a job is scheduled at some time [t2] and
we know that there is no preemption time between [t1]
and [t2] then the job must have been scheduled at [t1]
too. *)
Lemma neg_pt_scheduled_continuously_after :
forall j t1 t2 ,
scheduled_at sched j t2 ->
t1 <= t2 ->
(forall t , t1 <= t <= t2 -> ~~ preemption_time arr_seq sched t) ->
scheduled_at sched j t1.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t1 : nat) (t2 : instant),
scheduled_at sched j t2 ->
t1 <= t2 ->
(forall t : nat,
t1 <= t <= t2 -> ~~ preemption_time arr_seq sched t) ->
scheduled_at sched j t1
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t1 : nat) (t2 : instant),
scheduled_at sched j t2 ->
t1 <= t2 ->
(forall t : nat,
t1 <= t <= t2 -> ~~ preemption_time arr_seq sched t) ->
scheduled_at sched j t1
move => j1 t1 t2 SCHEDBEF LE NPT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1 : nat t2 : instant SCHEDBEF : scheduled_at sched j1 t2 LE : t1 <= t2 NPT : forall t : nat,
t1 <= t <= t2 ->
~~ preemption_time arr_seq sched t
scheduled_at sched j1 t1
interval_to_duration t1 t2 t. Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1, t : nat NPT : forall t0 : nat,
t1 <= t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0SCHEDBEF : scheduled_at sched j1 (t1 + t)
scheduled_at sched j1 t1
induction t as [ | t IHt]; first by rewrite addn0 in SCHEDBEF.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1, t : nat NPT : forall t0 : nat,
t1 <= t0 <= t1 + t.+1 ->
~~ preemption_time arr_seq sched t0SCHEDBEF : scheduled_at sched j1 (t1 + t.+1 ) IHt : (forall t0 : nat,
t1 <= t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j1 (t1 + t) ->
scheduled_at sched j1 t1
scheduled_at sched j1 t1
apply IHt.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1, t : nat NPT : forall t0 : nat,
t1 <= t0 <= t1 + t.+1 ->
~~ preemption_time arr_seq sched t0SCHEDBEF : scheduled_at sched j1 (t1 + t.+1 ) IHt : (forall t0 : nat,
t1 <= t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j1 (t1 + t) ->
scheduled_at sched j1 t1
forall t0 : nat,
t1 <= t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1, t : nat NPT : forall t0 : nat,
t1 <= t0 <= t1 + t.+1 ->
~~ preemption_time arr_seq sched t0SCHEDBEF : scheduled_at sched j1 (t1 + t.+1 ) IHt : (forall t0 : nat,
t1 <= t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j1 (t1 + t) ->
scheduled_at sched j1 t1
forall t0 : nat,
t1 <= t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0
move => ??.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1, t : nat NPT : forall t0 : nat,
t1 <= t0 <= t1 + t.+1 ->
~~ preemption_time arr_seq sched t0SCHEDBEF : scheduled_at sched j1 (t1 + t.+1 ) IHt : (forall t0 : nat,
t1 <= t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j1 (t1 + t) ->
scheduled_at sched j1 t1 _t_ : nat _Hyp_ : t1 <= _t_ <= t1 + t
~~ preemption_time arr_seq sched _t_
apply NPT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1, t : nat NPT : forall t0 : nat,
t1 <= t0 <= t1 + t.+1 ->
~~ preemption_time arr_seq sched t0SCHEDBEF : scheduled_at sched j1 (t1 + t.+1 ) IHt : (forall t0 : nat,
t1 <= t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j1 (t1 + t) ->
scheduled_at sched j1 t1 _t_ : nat _Hyp_ : t1 <= _t_ <= t1 + t
t1 <= _t_ <= t1 + t.+1
by lia .
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1, t : nat NPT : forall t0 : nat,
t1 <= t0 <= t1 + t.+1 ->
~~ preemption_time arr_seq sched t0SCHEDBEF : scheduled_at sched j1 (t1 + t.+1 ) IHt : (forall t0 : nat,
t1 <= t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j1 (t1 + t) ->
scheduled_at sched j1 t1
scheduled_at sched j1 (t1 + t)
apply neg_pt_scheduled_at; first by rewrite -addnS.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1, t : nat NPT : forall t0 : nat,
t1 <= t0 <= t1 + t.+1 ->
~~ preemption_time arr_seq sched t0SCHEDBEF : scheduled_at sched j1 (t1 + t.+1 ) IHt : (forall t0 : nat,
t1 <= t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j1 (t1 + t) ->
scheduled_at sched j1 t1
~~ preemption_time arr_seq sched (t1 + t).+1
apply NPT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j1 : Job t1, t : nat NPT : forall t0 : nat,
t1 <= t0 <= t1 + t.+1 ->
~~ preemption_time arr_seq sched t0SCHEDBEF : scheduled_at sched j1 (t1 + t.+1 ) IHt : (forall t0 : nat,
t1 <= t0 <= t1 + t ->
~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j1 (t1 + t) ->
scheduled_at sched j1 t1
t1 <= (t1 + t).+1 <= t1 + t.+1
by lia .
Qed .
(** Finally, using the above two lemmas we can prove that, if there is no
preemption time in an interval <<[t1, t2)>>, then if a job is scheduled
at time <<t ∈ [t1, t2)>>, then the same job is also scheduled at
another time <<t' ∈ [t1, t2)>>. *)
Lemma neg_pt_scheduled_continuous :
forall j t1 t2 t t' ,
t1 <= t < t2 ->
t1 <= t' < t2 ->
(forall t , t1 <= t < t2 -> ~~ preemption_time arr_seq sched t) ->
scheduled_at sched j t ->
scheduled_at sched j t'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t1 t2 t t' : nat),
t1 <= t < t2 ->
t1 <= t' < t2 ->
(forall t0 : nat,
t1 <= t0 < t2 -> ~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j t -> scheduled_at sched j t'
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t1 t2 t t' : nat),
t1 <= t < t2 ->
t1 <= t' < t2 ->
(forall t0 : nat,
t1 <= t0 < t2 -> ~~ preemption_time arr_seq sched t0) ->
scheduled_at sched j t -> scheduled_at sched j t'
move => j t1 t2 t t' NEQ1 NEQ2 NP SCHED.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2, t, t' : nat NEQ1 : t1 <= t < t2 NEQ2 : t1 <= t' < t2 NP : forall t : nat,
t1 <= t < t2 ->
~~ preemption_time arr_seq sched tSCHED : scheduled_at sched j t
scheduled_at sched j t'
case (t <= t') eqn : EQ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2, t, t' : nat NEQ1 : t1 <= t < t2 NEQ2 : t1 <= t' < t2 NP : forall t : nat,
t1 <= t < t2 ->
~~ preemption_time arr_seq sched tSCHED : scheduled_at sched j t EQ : (t <= t') = true
scheduled_at sched j t'
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2, t, t' : nat NEQ1 : t1 <= t < t2 NEQ2 : t1 <= t' < t2 NP : forall t : nat,
t1 <= t < t2 ->
~~ preemption_time arr_seq sched tSCHED : scheduled_at sched j t EQ : (t <= t') = true
scheduled_at sched j t'
apply : neg_pt_scheduled_continuously_before => //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2, t, t' : nat NEQ1 : t1 <= t < t2 NEQ2 : t1 <= t' < t2 NP : forall t : nat,
t1 <= t < t2 ->
~~ preemption_time arr_seq sched tSCHED : scheduled_at sched j t EQ : (t <= t') = true
forall t0 : nat,
t < t0 <= t' -> ~~ preemption_time arr_seq sched t0
move => ??.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2, t, t' : nat NEQ1 : t1 <= t < t2 NEQ2 : t1 <= t' < t2 NP : forall t : nat,
t1 <= t < t2 ->
~~ preemption_time arr_seq sched tSCHED : scheduled_at sched j t EQ : (t <= t') = true _t_ : nat _Hyp_ : t < _t_ <= t'
~~ preemption_time arr_seq sched _t_
apply NP.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2, t, t' : nat NEQ1 : t1 <= t < t2 NEQ2 : t1 <= t' < t2 NP : forall t : nat,
t1 <= t < t2 ->
~~ preemption_time arr_seq sched tSCHED : scheduled_at sched j t EQ : (t <= t') = true _t_ : nat _Hyp_ : t < _t_ <= t'
t1 <= _t_ < t2
by lia .
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2, t, t' : nat NEQ1 : t1 <= t < t2 NEQ2 : t1 <= t' < t2 NP : forall t : nat,
t1 <= t < t2 ->
~~ preemption_time arr_seq sched tSCHED : scheduled_at sched j t EQ : (t <= t') = false
scheduled_at sched j t'
apply (neg_pt_scheduled_continuously_after j t' t) => //; first by lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2, t, t' : nat NEQ1 : t1 <= t < t2 NEQ2 : t1 <= t' < t2 NP : forall t : nat,
t1 <= t < t2 ->
~~ preemption_time arr_seq sched tSCHED : scheduled_at sched j t EQ : (t <= t') = false
forall t0 : nat,
t' <= t0 <= t -> ~~ preemption_time arr_seq sched t0
move => ??.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2, t, t' : nat NEQ1 : t1 <= t < t2 NEQ2 : t1 <= t' < t2 NP : forall t : nat,
t1 <= t < t2 ->
~~ preemption_time arr_seq sched tSCHED : scheduled_at sched j t EQ : (t <= t') = false _t_ : nat _Hyp_ : t' <= _t_ <= t
~~ preemption_time arr_seq sched _t_
apply NP.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2, t, t' : nat NEQ1 : t1 <= t < t2 NEQ2 : t1 <= t' < t2 NP : forall t : nat,
t1 <= t < t2 ->
~~ preemption_time arr_seq sched tSCHED : scheduled_at sched j t EQ : (t <= t') = false _t_ : nat _Hyp_ : t' <= _t_ <= t
t1 <= _t_ < t2
by lia .
Qed .
(** If we observe two different jobs scheduled at two points in time, then
there necessarily is a preemption time in between. *)
Lemma neq_scheduled_at_pt :
forall j t ,
scheduled_at sched j t ->
forall j' t' ,
scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt, preemption_time arr_seq sched pt & t < pt <= t'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t : instant),
scheduled_at sched j t ->
forall (j' : Job) (t' : instant),
scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t'
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t : instant),
scheduled_at sched j t ->
forall (j' : Job) (t' : instant),
scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t'
move => j t SCHED j'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job
forall t' : instant,
scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t'
elim .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job
scheduled_at sched j' 0 ->
j != j' ->
t <= 0 ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= 0
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job
scheduled_at sched j' 0 ->
j != j' ->
t <= 0 ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= 0
move => SCHED' NEQ /[!leqn0]/eqP EQ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job SCHED' : scheduled_at sched j' 0 NEQ : j != j' EQ : t = 0
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= 0
exfalso ; apply /neqP; [exact : NEQ|].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job SCHED' : scheduled_at sched j' 0 NEQ : j != j' EQ : t = 0
j = j'
apply : H_uniproc.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job SCHED' : scheduled_at sched j' 0 NEQ : j != j' EQ : t = 0
scheduled_at ?Goal0 j ?Goal1
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job SCHED' : scheduled_at sched j' 0 NEQ : j != j' EQ : t = 0
scheduled_at ?Goal0 j ?Goal1
exact : SCHED.
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job SCHED' : scheduled_at sched j' 0 NEQ : j != j' EQ : t = 0
scheduled_at sched j' t
by rewrite EQ. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job
forall n : nat,
(scheduled_at sched j' n ->
j != j' ->
t <= n ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= n) ->
scheduled_at sched j' n.+1 ->
j != j' ->
t <= n.+1 ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= n.+1
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job
forall n : nat,
(scheduled_at sched j' n ->
j != j' ->
t <= n ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= n) ->
scheduled_at sched j' n.+1 ->
j != j' ->
t <= n.+1 ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= n.+1
move => t' IH SCHED' NEQ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t' SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j'
t <= t'.+1 ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t'.+1
rewrite leq_eqVlt => /orP [/eqP EQ|LT //].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t' SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' EQ : t = t'.+1
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t'.+1
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t' SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' EQ : t = t'.+1
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t'.+1
exfalso ; apply /neqP; [exact : NEQ|].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t' SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' EQ : t = t'.+1
j = j'
by rewrite -EQ in SCHED'; exact : (H_uniproc _ _ _ _ SCHED SCHED').
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t' SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t'.+1
have [PT|NPT] := boolP (preemption_time arr_seq sched t'.+1 );
first by exists t' .+1 => //; apply /andP; split .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t' SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 NPT : ~~ preemption_time arr_seq sched t'.+1
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t'.+1
have [pt PT /andP [tpt ptt']] :
exists2 pt, preemption_time arr_seq sched pt & t < pt <= t'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t' SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 NPT : ~~ preemption_time arr_seq sched t'.+1
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t'
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t' SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 NPT : ~~ preemption_time arr_seq sched t'.+1
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t'
apply : IH => //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 NPT : ~~ preemption_time arr_seq sched t'.+1
scheduled_at sched j' t'
by apply : neg_pt_scheduled_at. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t' SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 NPT : ~~ preemption_time arr_seq sched t'.+1 pt : instant PT : preemption_time arr_seq sched pt tpt : t < pt ptt' : pt <= t'
exists2 pt : instant,
preemption_time arr_seq sched pt & t < pt <= t'.+1
by exists pt => //; apply /andP; split . }
Qed .
(** We can strengthen the above lemma to say that there exists a preemption
time such that, after the preemption point, the next job to be scheduled
is scheduled continuously. *)
Lemma neq_scheduled_at_pt_continuous_sched :
forall j t ,
scheduled_at sched j t ->
forall j' t' ,
scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt ,
preemption_time arr_seq sched pt
/\ t < pt <= t'
/\ scheduled_at sched j' pt.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t : instant),
scheduled_at sched j t ->
forall (j' : Job) (t' : instant),
scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t : instant),
scheduled_at sched j t ->
forall (j' : Job) (t' : instant),
scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt
move => j t SCHED j'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job
forall t' : instant,
scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt
elim .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job
scheduled_at sched j' 0 ->
j != j' ->
t <= 0 ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= 0 /\ scheduled_at sched j' pt
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job
scheduled_at sched j' 0 ->
j != j' ->
t <= 0 ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= 0 /\ scheduled_at sched j' pt
move => SCHED' NEQ /[!leqn0]/eqP EQ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job SCHED' : scheduled_at sched j' 0 NEQ : j != j' EQ : t = 0
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= 0 /\ scheduled_at sched j' pt
exfalso ; apply /neqP; [exact : NEQ|].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job SCHED' : scheduled_at sched j' 0 NEQ : j != j' EQ : t = 0
j = j'
apply : H_uniproc.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job SCHED' : scheduled_at sched j' 0 NEQ : j != j' EQ : t = 0
scheduled_at ?Goal0 j ?Goal1
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job SCHED' : scheduled_at sched j' 0 NEQ : j != j' EQ : t = 0
scheduled_at ?Goal0 j ?Goal1
exact : SCHED.
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job SCHED' : scheduled_at sched j' 0 NEQ : j != j' EQ : t = 0
scheduled_at sched j' t
by rewrite EQ. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job
forall n : nat,
(scheduled_at sched j' n ->
j != j' ->
t <= n ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= n /\ scheduled_at sched j' pt) ->
scheduled_at sched j' n.+1 ->
j != j' ->
t <= n.+1 ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= n.+1 /\ scheduled_at sched j' pt
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job
forall n : nat,
(scheduled_at sched j' n ->
j != j' ->
t <= n ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= n /\ scheduled_at sched j' pt) ->
scheduled_at sched j' n.+1 ->
j != j' ->
t <= n.+1 ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= n.+1 /\ scheduled_at sched j' pt
move => t' IH SCHED' NEQ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j'
t <= t'.+1 ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t'.+1 /\ scheduled_at sched j' pt
rewrite leq_eqVlt => /orP [/eqP EQ|LT //].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' EQ : t = t'.+1
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t'.+1 /\ scheduled_at sched j' pt
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' EQ : t = t'.+1
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t'.+1 /\ scheduled_at sched j' pt
exfalso ; apply /neqP; [exact : NEQ|].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' EQ : t = t'.+1
j = j'
by rewrite -EQ in SCHED'; exact : (H_uniproc _ _ _ _ SCHED SCHED').
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t'.+1 /\ scheduled_at sched j' pt
have [PT|NPT] := boolP (preemption_time arr_seq sched t'.+1 ).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 PT : preemption_time arr_seq sched t'.+1
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t'.+1 /\ scheduled_at sched j' pt
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 PT : preemption_time arr_seq sched t'.+1
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t'.+1 /\ scheduled_at sched j' pt
exists t' .+1 => //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 PT : preemption_time arr_seq sched t'.+1
preemption_time arr_seq sched t'.+1 /\
t < t'.+1 <= t'.+1 /\ scheduled_at sched j' t'.+1
split ; [done | split ; [|done ]].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 PT : preemption_time arr_seq sched t'.+1
t < t'.+1 <= t'.+1
by lia .
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : scheduled_at sched j' t' ->
j != j' ->
t <= t' ->
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' pt SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 NPT : ~~ preemption_time arr_seq sched t'.+1
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t'.+1 /\ scheduled_at sched j' pt
feed_n 3 IH; [by apply neg_pt_scheduled_at => // | done |lia |]. Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat IH : exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t' /\ scheduled_at sched j' ptSCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 NPT : ~~ preemption_time arr_seq sched t'.+1
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t'.+1 /\ scheduled_at sched j' pt
move : IH => [pt [PT [IN1 SCHED1]]].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 NPT : ~~ preemption_time arr_seq sched t'.+1 pt : instant PT : preemption_time arr_seq sched pt IN1 : t < pt <= t' SCHED1 : scheduled_at sched j' pt
exists pt : instant,
preemption_time arr_seq sched pt /\
t < pt <= t'.+1 /\ scheduled_at sched j' pt
exists pt .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable 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_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_must_arrive : jobs_must_arrive_to_execute sched H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t : instant SCHED : scheduled_at sched j t j' : Job t' : nat SCHED' : scheduled_at sched j' t'.+1 NEQ : j != j' LT : t < t'.+1 NPT : ~~ preemption_time arr_seq sched t'.+1 pt : instant PT : preemption_time arr_seq sched pt IN1 : t < pt <= t' SCHED1 : scheduled_at sched j' pt
preemption_time arr_seq sched pt /\
t < pt <= t'.+1 /\ scheduled_at sched j' pt
by split ; [done | split ; [lia |done ]]. }
Qed .
End PreemptionTimes .
(** In this section, we prove a lemma relating scheduling and preemption times. *)
Section PreemptionFacts .
(** Consider any type of jobs. *)
Context {Job : JobType}.
Context `{Arrival : JobArrival Job}.
Context `{Cost : JobCost Job}.
(** Allow for any uniprocessor model. *)
Context {PState : ProcessorState Job}.
Hypothesis H_uniproc : uniprocessor_model PState.
Context `{@JobReady Job PState Cost Arrival}.
(** Consider any valid arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
(** Next, consider any valid schedule of this arrival sequence. *)
Variable sched : schedule PState.
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
(** In addition, we assume the existence of a function mapping jobs to their preemption points ... *)
Context `{JobPreemptable Job}.
(** ... and assume that it defines a valid preemption model. *)
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
(** We prove that every nonpreemptive segment always begins with a preemption time. *)
Lemma scheduling_of_any_segment_starts_with_preemption_time :
forall j t ,
scheduled_at sched j t ->
exists pt ,
job_arrival j <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' , pt <= t' <= t -> scheduled_at sched j t').Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t : instant),
scheduled_at sched j t ->
exists pt : nat,
job_arrival j <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched j t')
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t : instant),
scheduled_at sched j t ->
exists pt : nat,
job_arrival j <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched j t')
intros s t SCHEDst.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t
exists pt : nat,
job_arrival s <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched s t')
have EX: exists t' , (t' <= t) && (scheduled_at sched s t')
&& (all (fun t'' => scheduled_at sched s t'') (index_iota t' t.+1 )).Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t
exists t' : nat,
(t' <= t) && scheduled_at sched s t' &&
all [eta scheduled_at sched s] (index_iota t' t.+1 )
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t
exists t' : nat,
(t' <= t) && scheduled_at sched s t' &&
all [eta scheduled_at sched s] (index_iota t' t.+1 )
exists t .Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t
(t <= t) && scheduled_at sched s t &&
all [eta scheduled_at sched s] (index_iota t t.+1 )
apply /andP; split ; [ by apply /andP; split | ].Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t
all [eta scheduled_at sched s] (index_iota t t.+1 )
apply /allP; intros t'.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t t' : Datatypes_nat__canonical__eqtype_Equality
t' \in index_iota t t.+1 -> scheduled_at sched s t'
by rewrite mem_index_iota ltnS -eqn_leq; move => /eqP <-.
} Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t EX : exists t' : nat,
(t' <= t) && scheduled_at sched s t' &&
all [eta scheduled_at sched s]
(index_iota t' t.+1 )
exists pt : nat,
job_arrival s <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched s t')
have MATE : jobs_must_arrive_to_execute sched by [].Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t EX : exists t' : nat,
(t' <= t) && scheduled_at sched s t' &&
all [eta scheduled_at sched s]
(index_iota t' t.+1 )MATE : jobs_must_arrive_to_execute sched
exists pt : nat,
job_arrival s <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched s t')
move : (H_sched_valid) => [COME_ARR READY].Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t EX : exists t' : nat,
(t' <= t) && scheduled_at sched s t' &&
all [eta scheduled_at sched s]
(index_iota t' t.+1 )MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched
exists pt : nat,
job_arrival s <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched s t')
have MIN := ex_minnP EX.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t EX : exists t' : nat,
(t' <= t) && scheduled_at sched s t' &&
all [eta scheduled_at sched s]
(index_iota t' t.+1 )MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched MIN : ex_minn_spec
(fun t' : nat =>
(t' <= t) && scheduled_at sched s t' &&
all [eta scheduled_at sched s]
(index_iota t' t.+1 ))
(ex_minn
(P:=fun t' : nat =>
(t' <= t) && scheduled_at sched s t' &&
all [eta scheduled_at sched s]
(index_iota t' t.+1 )) EX)
exists pt : nat,
job_arrival s <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched s t')
move : MIN => [mpt /andP [/andP [LT1 SCHEDsmpt] /allP ALL] MIN]; clear EX.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt <= t SCHEDsmpt : scheduled_at sched s mpt ALL : {in index_iota mpt t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt <= n
exists pt : nat,
job_arrival s <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched s t')
destruct mpt as [|mpt].Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched LT1 : 0 <= tSCHEDsmpt : scheduled_at sched s 0 ALL : {in index_iota 0 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
0 <= n
exists pt : nat,
job_arrival s <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched s t')
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched LT1 : 0 <= tSCHEDsmpt : scheduled_at sched s 0 ALL : {in index_iota 0 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
0 <= n
exists pt : nat,
job_arrival s <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched s t')
exists 0 ; repeat split .Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched LT1 : 0 <= tSCHEDsmpt : scheduled_at sched s 0 ALL : {in index_iota 0 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
0 <= n
job_arrival s <= 0 <= t
+ Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched LT1 : 0 <= tSCHEDsmpt : scheduled_at sched s 0 ALL : {in index_iota 0 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
0 <= n
job_arrival s <= 0 <= t
by apply /andP; split => //; apply MATE.
+ Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched LT1 : 0 <= tSCHEDsmpt : scheduled_at sched s 0 ALL : {in index_iota 0 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
0 <= n
preemption_time arr_seq sched 0
eapply (zero_is_pt arr_seq); eauto 2 .
+ Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched LT1 : 0 <= tSCHEDsmpt : scheduled_at sched s 0 ALL : {in index_iota 0 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
0 <= n
forall t' : nat,
0 <= t' <= t -> scheduled_at sched s t'
by intros ; apply ALL; rewrite mem_iota subn0 add0n ltnS.
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < n
exists pt : nat,
job_arrival s <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched s t')
have NSCHED: ~~ scheduled_at sched s mpt.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < n
~~ scheduled_at sched s mpt
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < n
~~ scheduled_at sched s mpt
apply /negP; intros SCHED.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nSCHED : scheduled_at sched s mpt
False
enough (F : mpt < mpt); first by rewrite ltnn in F.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nSCHED : scheduled_at sched s mpt
mpt < mpt
apply MIN.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nSCHED : scheduled_at sched s mpt
(mpt <= t) && scheduled_at sched s mpt &&
all [eta scheduled_at sched s] (index_iota mpt t.+1 )
apply /andP; split ; [by apply /andP; split ; [ apply ltnW | ] | ].Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nSCHED : scheduled_at sched s mpt
all [eta scheduled_at sched s] (index_iota mpt t.+1 )
apply /allP; intros t'.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nSCHED : scheduled_at sched s mpt t' : Datatypes_nat__canonical__eqtype_Equality
t' \in index_iota mpt t.+1 -> scheduled_at sched s t'
rewrite mem_index_iota; move => /andP [GE LE].Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nSCHED : scheduled_at sched s mpt t' : Datatypes_nat__canonical__eqtype_Equality GE : mpt <= t' LE : t' < t.+1
scheduled_at sched s t'
move : GE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LT].Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nSCHED : scheduled_at sched s mpt t' : Datatypes_nat__canonical__eqtype_Equality LE : t' < t.+1 EQ : mpt = t'
scheduled_at sched s t'
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nSCHED : scheduled_at sched s mpt t' : Datatypes_nat__canonical__eqtype_Equality LE : t' < t.+1 EQ : mpt = t'
scheduled_at sched s t'
by subst t'.
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nSCHED : scheduled_at sched s mpt t' : Datatypes_nat__canonical__eqtype_Equality LE : t' < t.+1 LT : mpt < t'
scheduled_at sched s t'
by apply ALL; rewrite mem_index_iota; apply /andP; split .
} Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nNSCHED : ~~ scheduled_at sched s mpt
exists pt : nat,
job_arrival s <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched s t')
have PP: preemption_time arr_seq sched mpt.+1
by eapply (first_moment_is_pt arr_seq) with (j := s); eauto 2 .Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nNSCHED : ~~ scheduled_at sched s mpt PP : preemption_time arr_seq sched mpt.+1
exists pt : nat,
job_arrival s <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched s t')
exists mpt .+1 ; repeat split => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nNSCHED : ~~ scheduled_at sched s mpt PP : preemption_time arr_seq sched mpt.+1
job_arrival s <= mpt.+1 <= t
+ Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nNSCHED : ~~ scheduled_at sched s mpt PP : preemption_time arr_seq sched mpt.+1
job_arrival s <= mpt.+1 <= t
by apply /andP; split => [|//]; apply MATE in SCHEDsmpt.
+ Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nNSCHED : ~~ scheduled_at sched s mpt PP : preemption_time arr_seq sched mpt.+1
forall t' : nat,
mpt < t' <= t -> scheduled_at sched s t'
move => t' /andP [GE LE].Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched s : Job t : instant SCHEDst : scheduled_at sched s t MATE : jobs_must_arrive_to_execute sched COME_ARR : jobs_come_from_arrival_sequence sched
arr_seq READY : jobs_must_be_ready_to_execute sched mpt : nat LT1 : mpt < t SCHEDsmpt : scheduled_at sched s mpt.+1 ALL : {in index_iota mpt.+1 t.+1 ,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
scheduled_at sched s x} MIN : forall n : nat,
(n <= t) && scheduled_at sched s n &&
all [eta scheduled_at sched s]
(index_iota n t.+1 ) ->
mpt < nNSCHED : ~~ scheduled_at sched s mpt PP : preemption_time arr_seq sched mpt.+1 t' : nat GE : mpt < t' LE : t' <= t
scheduled_at sched s t'
by apply ALL; rewrite mem_index_iota; apply /andP; split .
Qed .
(** We strengthen the above lemma to say that the preemption time that a segment
starts with must lie between the last preemption time and the instant we
know the job is scheduled at. *)
Lemma scheduling_of_any_segment_starts_with_preemption_time_continuously_sched :
forall j t1 t2 ,
t1 <= t2 ->
preemption_time arr_seq sched t1 ->
scheduled_at sched j t2 ->
exists ptst ,
t1 <= ptst <= t2
/\ preemption_time arr_seq sched ptst
/\ scheduled_at sched j ptst.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t1 t2 : nat),
t1 <= t2 ->
preemption_time arr_seq sched t1 ->
scheduled_at sched j t2 ->
exists ptst : nat,
t1 <= ptst <= t2 /\
preemption_time arr_seq sched ptst /\
scheduled_at sched j ptst
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall (j : Job) (t1 t2 : nat),
t1 <= t2 ->
preemption_time arr_seq sched t1 ->
scheduled_at sched j t2 ->
exists ptst : nat,
t1 <= ptst <= t2 /\
preemption_time arr_seq sched ptst /\
scheduled_at sched j ptst
move => j t1 t2 GE PREEMPT SCHED.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2 : nat GE : t1 <= t2 PREEMPT : preemption_time arr_seq sched t1 SCHED : scheduled_at sched j t2
exists ptst : nat,
t1 <= ptst <= t2 /\
preemption_time arr_seq sched ptst /\
scheduled_at sched j ptst
have [pt [/andP[LEpt GEpt][PREEMPT' NSCHED]]] :=
scheduling_of_any_segment_starts_with_preemption_time j t2 SCHED.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2 : nat GE : t1 <= t2 PREEMPT : preemption_time arr_seq sched t1 SCHED : scheduled_at sched j t2 pt : nat LEpt : job_arrival j <= pt GEpt : pt <= t2 PREEMPT' : preemption_time arr_seq sched pt NSCHED : forall t' : nat,
pt <= t' <= t2 -> scheduled_at sched j t'
exists ptst : nat,
t1 <= ptst <= t2 /\
preemption_time arr_seq sched ptst /\
scheduled_at sched j ptst
case (t1 <= pt) eqn : T1pt;
first by (exists pt ; split ; [lia | split ; [done | apply NSCHED => //]; lia ]).Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2 : nat GE : t1 <= t2 PREEMPT : preemption_time arr_seq sched t1 SCHED : scheduled_at sched j t2 pt : nat LEpt : job_arrival j <= pt GEpt : pt <= t2 PREEMPT' : preemption_time arr_seq sched pt NSCHED : forall t' : nat,
pt <= t' <= t2 -> scheduled_at sched j t'T1pt : (t1 <= pt) = false
exists ptst : nat,
t1 <= ptst <= t2 /\
preemption_time arr_seq sched ptst /\
scheduled_at sched j ptst
move : T1pt => /negP /negP Eq.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2 : nat GE : t1 <= t2 PREEMPT : preemption_time arr_seq sched t1 SCHED : scheduled_at sched j t2 pt : nat LEpt : job_arrival j <= pt GEpt : pt <= t2 PREEMPT' : preemption_time arr_seq sched pt NSCHED : forall t' : nat,
pt <= t' <= t2 -> scheduled_at sched j t'Eq : ~~ (t1 <= pt)
exists ptst : nat,
t1 <= ptst <= t2 /\
preemption_time arr_seq sched ptst /\
scheduled_at sched j ptst
rewrite -ltnNge in Eq.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2 : nat GE : t1 <= t2 PREEMPT : preemption_time arr_seq sched t1 SCHED : scheduled_at sched j t2 pt : nat LEpt : job_arrival j <= pt GEpt : pt <= t2 PREEMPT' : preemption_time arr_seq sched pt NSCHED : forall t' : nat,
pt <= t' <= t2 -> scheduled_at sched j t'Eq : pt < t1
exists ptst : nat,
t1 <= ptst <= t2 /\
preemption_time arr_seq sched ptst /\
scheduled_at sched j ptst
exists t1 .Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2 : nat GE : t1 <= t2 PREEMPT : preemption_time arr_seq sched t1 SCHED : scheduled_at sched j t2 pt : nat LEpt : job_arrival j <= pt GEpt : pt <= t2 PREEMPT' : preemption_time arr_seq sched pt NSCHED : forall t' : nat,
pt <= t' <= t2 -> scheduled_at sched j t'Eq : pt < t1
t1 <= t1 <= t2 /\
preemption_time arr_seq sched t1 /\
scheduled_at sched j t1
split ; [lia |split ; [done |]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2 : nat GE : t1 <= t2 PREEMPT : preemption_time arr_seq sched t1 SCHED : scheduled_at sched j t2 pt : nat LEpt : job_arrival j <= pt GEpt : pt <= t2 PREEMPT' : preemption_time arr_seq sched pt NSCHED : forall t' : nat,
pt <= t' <= t2 -> scheduled_at sched j t'Eq : pt < t1
scheduled_at sched j t1
apply NSCHED.Job : JobType Arrival : JobArrival Job Cost : JobCost Job PState : ProcessorState Job H_uniproc : uniprocessor_model PState H : JobReady Job PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job t1, t2 : nat GE : t1 <= t2 PREEMPT : preemption_time arr_seq sched t1 SCHED : scheduled_at sched j t2 pt : nat LEpt : job_arrival j <= pt GEpt : pt <= t2 PREEMPT' : preemption_time arr_seq sched pt NSCHED : forall t' : nat,
pt <= t' <= t2 -> scheduled_at sched j t'Eq : pt < t1
pt <= t1 <= t2
lia .
Qed .
End PreemptionFacts .