Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.facts.model.workload.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.model.ideal.service_of_jobs.
Require Export prosa.analysis.facts.busy_interval.quiet_time.
Require Export prosa.analysis.facts.busy_interval.existence.
Require Export prosa.analysis.definitions.work_bearing_readiness.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.util.tactics.
(** * Busy Interval From Workload Bound *)
(** In the following, we derive an alternative condition for the existence of a
busy interval based on the total workload. If the total workload generated
by the task set is bounded, then there necessarily exists a moment without
any carry-in workload, from which it follows that a busy interval has ended. *)
Section BusyIntervalExistence .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any valid arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arr_seq : valid_arrival_sequence arr_seq.
(** Allow for any fully-consuming uniprocessor model. *)
Context {PState : ProcessorState Job}.
Hypothesis H_uniproc : uniprocessor_model PState.
Hypothesis H_fully_consuming_proc_model : fully_consuming_proc_model PState.
(** Next, consider any schedule of the arrival sequence ... *)
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume a given reflexive JLFP policy. *)
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
(** Further, allow for any work-bearing notion of job readiness ... *)
Context `{!JobReady Job PState}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** ... and assume that the schedule is work-conserving. *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** ** Times without Carry-In *)
(** As the first step, we derive a sufficient condition for the existence of a
no-carry-in instant for uniprocessor for JLFP schedulers. *)
(** We start by noting that, trivially, the processor has no carry-in at the
beginning (i.e., has no carry-in at time instant [0]). *)
Lemma no_carry_in_at_zero :
no_carry_in arr_seq sched 0 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched
no_carry_in arr_seq sched 0
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched
no_carry_in arr_seq sched 0
by move => j _ +; rewrite /arrived_before ltn0. Qed .
(** Next, we relate idle times to the no-carry-in condition. First, the
presence of a pending job implies that the processor isn't idle due to
work-conservation. *)
Lemma pending_job_not_idle :
forall j t ,
arrives_in arr_seq j ->
pending sched j t ->
~ is_idle arr_seq sched t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched
forall (j : Job) (t : instant),
arrives_in arr_seq j ->
pending sched j t -> ~ is_idle arr_seq sched t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched
forall (j : Job) (t : instant),
arrives_in arr_seq j ->
pending sched j t -> ~ is_idle arr_seq sched t
move => j t ARR PEND IDLE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched j : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t IDLE : is_idle arr_seq sched t
False
have [jhp [ARRhp [READYhp _]]] :
exists j_hp : Job, arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
by apply : H_job_ready.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched j : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t IDLE : is_idle arr_seq sched t jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t
False
move : IDLE; rewrite is_idle_iff => /eqP; rewrite scheduled_job_at_none => // IDLE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched j : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : forall j : Job, ~~ scheduled_at sched j t
False
have [j_other SCHED]: exists j_other : Job, scheduled_at sched j_other t
by apply : H_work_conserving ARRhp _; apply /andP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched j : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : forall j : Job, ~~ scheduled_at sched j tj_other : Job SCHED : scheduled_at sched j_other t
False
by move : (IDLE j_other) => /negP.
Qed .
(** Second, an idle time implies no carry in at this time instant. *)
Lemma idle_instant_no_carry_in :
forall t ,
is_idle arr_seq sched t ->
no_carry_in arr_seq sched t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched
forall t : instant,
is_idle arr_seq sched t -> no_carry_in arr_seq sched t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched
forall t : instant,
is_idle arr_seq sched t -> no_carry_in arr_seq sched t
move => t IDLE j ARR HA.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched t : instant IDLE : is_idle arr_seq sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t
completed_by sched j t
apply /negPn/negP => NCOMP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched t : instant IDLE : is_idle arr_seq sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t
False
apply : (pending_job_not_idle j t) => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched t : instant IDLE : is_idle arr_seq sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t
pending sched j t
by apply /andP; split ; rewrite // /has_arrived ltnW.
Qed .
(** Moreover, an idle time implies no carry in at the next time instant, too. *)
Lemma idle_instant_next_no_carry_in :
forall t ,
is_idle arr_seq sched t ->
no_carry_in arr_seq sched t.+1 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched
forall t : instant,
is_idle arr_seq sched t ->
no_carry_in arr_seq sched t.+1
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched
forall t : instant,
is_idle arr_seq sched t ->
no_carry_in arr_seq sched t.+1
move => t IDLE j ARR HA.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched t : instant IDLE : is_idle arr_seq sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1
completed_by sched j t.+1
apply /negPn/negP => NCOMP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched t : instant IDLE : is_idle arr_seq sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1
False
apply : (pending_job_not_idle j t) => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched t : instant IDLE : is_idle arr_seq sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1
pending sched j t
apply /andP; split ; rewrite // /has_arrived.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched t : instant IDLE : is_idle arr_seq sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1
~~ completed_by sched j t
by apply : incompletion_monotonic NCOMP.
Qed .
(** ** Bounded-Workload Assumption *)
(** We now introduce the central assumption from which we deduce the existence
of a busy interval. *)
(** To this end, recall the notion of workload of all jobs released in a
given interval <<[t1, t2)>>... *)
Let total_workload t1 t2 :=
workload_of_jobs predT (arrivals_between arr_seq t1 t2).
(** ... and total service of jobs within some time interval <<[t1, t2)>>. *)
Let total_service t1 t2 :=
service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2.
(** We assume that, for some positive [Δ], the sum of the total
blackout and the total workload generated in any interval of
length [Δ] starting with no carry-in is bounded by [Δ]. Note
that this assumption bounds the total workload of jobs released
in a time interval <<[t, t + Δ)>> regardless of their
priorities. *)
Variable Δ : duration.
Hypothesis H_delta_positive : Δ > 0 .
Hypothesis H_workload_is_bounded :
forall t ,
no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) + total_workload t (t + Δ) <= Δ.
(** In the following, we also require a unit-speed processor. *)
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
(** ** Existence of a No-Carry-In Instant *)
(** Next we prove that, if for any time instant [t] there is a point where the
total workload generated since [t] is upper-bounded by the length of the
interval, there must exist a no-carry-in instant. *)
Section ProcessorIsNotTooBusy .
(** As a stepping stone, we prove in the following section that for any time
instant [t] there exists another time instant <<t' ∈ (t, t + Δ]>> such
that the processor has no carry-in at time [t']. *)
Section ProcessorIsNotTooBusyInduction .
(** Consider an arbitrary time instant [t] ... *)
Variable t : duration.
(** ... such that there is no carry-in at time [t]. *)
Hypothesis H_no_carry_in : no_carry_in arr_seq sched t.
(** First, recall that the total service is bounded by the total
workload. Therefore the sum of the total blackout and the
total service of jobs in the interval <<[t, t + Δ)>> is
bounded by [Δ]. *)
Lemma total_service_is_bounded_by_Δ :
blackout_during sched t (t + Δ) + total_service t (t + Δ) <= Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t
blackout_during sched t (t + Δ) +
total_service t (t + Δ) <= Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t
blackout_during sched t (t + Δ) +
total_service t (t + Δ) <= Δ
have EQ: \sum_(t <= x < t + Δ) 1 = Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t
\sum_(t <= x < t + Δ) 1 = Δ
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t
\sum_(t <= x < t + Δ) 1 = Δ
by rewrite big_const_nat iter_addn mul1n addn0 -{2 }[t]addn0 subnDl subn0. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQ : \sum_(t <= x < t + Δ) 1 = Δ
blackout_during sched t (t + Δ) +
total_service t (t + Δ) <= Δ
rewrite -{3 }EQ {EQ}.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t
blackout_during sched t (t + Δ) +
total_service t (t + Δ) <= \sum_(t <= x < t + Δ) 1
rewrite /total_service /blackout_during /supply.blackout_during.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t
\sum_(t <= t < t + Δ) is_blackout sched t +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t (t + Δ) <=
\sum_(t <= x < t + Δ) 1
rewrite /service_of_jobs/service_during/service_at exchange_big //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t
\sum_(t <= t < t + Δ) is_blackout sched t +
\sum_(t <= j < t + Δ)
\sum_(i <- arrivals_between arr_seq 0 (t + Δ))
service_in i (sched j) <=
\sum_(t <= x < t + Δ) 1
rewrite -big_split //= leq_sum //; move => t' _.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t t' : nat
is_blackout sched t' +
\sum_(i <- arrivals_between arr_seq 0 (t + Δ))
service_in i (sched t') <= 1
have [BL|SUP] := blackout_or_supply sched t'.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t t' : nat BL : is_blackout sched t'
is_blackout sched t' +
\sum_(i <- arrivals_between arr_seq 0 (t + Δ))
service_in i (sched t') <= 1
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t t' : nat BL : is_blackout sched t'
is_blackout sched t' +
\sum_(i <- arrivals_between arr_seq 0 (t + Δ))
service_in i (sched t') <= 1
rewrite -[1 ]addn0; apply leq_add; first by case : (is_blackout).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t t' : nat BL : is_blackout sched t'
\sum_(i <- arrivals_between arr_seq 0 (t + Δ))
service_in i (sched t') <= 0
rewrite leqn0; apply /eqP; apply big1 => j _.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t t' : nat BL : is_blackout sched t' j : Job
service_in j (sched t') = 0
eapply no_service_during_blackout in BL.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t t' : nat j : Job BL : service_at sched ?j t' = 0
service_in j (sched t') = 0
by apply : BL. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t t' : nat SUP : has_supply sched t'
is_blackout sched t' +
\sum_(i <- arrivals_between arr_seq 0 (t + Δ))
service_in i (sched t') <= 1
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t t' : nat SUP : has_supply sched t'
is_blackout sched t' +
\sum_(i <- arrivals_between arr_seq 0 (t + Δ))
service_in i (sched t') <= 1
rewrite /is_blackout SUP add0n.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t t' : nat SUP : has_supply sched t'
\sum_(i <- arrivals_between arr_seq 0 (t + Δ))
service_in i (sched t') <= 1
exact : service_of_jobs_le_1. }
Qed .
(** Next we consider two cases:
(1) The case when the sum of blackout and service is strictly less than [Δ], and
(2) the case when the sum of blackout and service is equal to [Δ]. *)
(** In the first case, we use the pigeonhole principle to
conclude that there is an idle time instant; which in turn
implies existence of a time instant with no carry-in. *)
Lemma low_total_service_implies_existence_of_time_with_no_carry_in :
blackout_during sched t (t + Δ) + total_service t (t + Δ) < Δ ->
exists δ ,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t
blackout_during sched t (t + Δ) +
total_service t (t + Δ) < Δ ->
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t
blackout_during sched t (t + Δ) +
total_service t (t + Δ) < Δ ->
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
rewrite /total_service-{3 }[Δ]addn0 -{2 }(subnn t) addnBA // [Δ + t]addnC => LTS.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
have [t_idle [/andP [LEt GTe] IDLE]]: exists t0 : nat,
t <= t0 < t + Δ
/\ is_idle arr_seq sched t0.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ
exists t0 : nat,
t <= t0 < t + Δ /\ is_idle arr_seq sched t0
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ
exists t0 : nat,
t <= t0 < t + Δ /\ is_idle arr_seq sched t0
apply : low_service_implies_existence_of_idle_time_rs =>//.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ
blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t (t + Δ) <
t + Δ - t
rewrite !subnKC in LTS; try by apply leq_addr.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) < Δ
blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t (t + Δ) <
t + Δ - t
by rewrite addKn. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat LEt : t <= t_idle GTe : t_idle < t + Δ IDLE : is_idle arr_seq sched t_idle
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
move : LEt; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle arr_seq sched t_idle EQ : t = t_idle
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle arr_seq sched t_idle EQ : t = t_idle
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
exists 0 ; split => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle arr_seq sched t_idle EQ : t = t_idle
no_carry_in arr_seq sched (t.+1 + 0 )
rewrite addn0 EQ => s ARR BEF.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle arr_seq sched t_idle EQ : t = t_idle s : Job ARR : arrives_in arr_seq s BEF : arrived_before s t_idle.+1
completed_by sched s t_idle.+1
by apply : idle_instant_next_no_carry_in. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle arr_seq sched t_idle LT : t < t_idle
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
have EX: exists γ , t_idle = t + γ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle arr_seq sched t_idle LT : t < t_idle
exists γ : nat, t_idle = t + γ
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle arr_seq sched t_idle LT : t < t_idle
exists γ : nat, t_idle = t + γ
by exists (t_idle - t); rewrite subnKC // ltnW. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle arr_seq sched t_idle LT : t < t_idle EX : exists γ : nat, t_idle = t + γ
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
move : EX => [γ EQ].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle arr_seq sched t_idle LT : t < t_idle γ : nat EQ : t_idle = t + γ
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
move : GTe LT; rewrite EQ ltn_add2l -{1 }[t]addn0 ltn_add2l => GTe LT.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat IDLE : is_idle arr_seq sched t_idle γ : nat EQ : t_idle = t + γ GTe : γ < Δ LT : 0 < γ
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
exists (γ .-1 ); split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat IDLE : is_idle arr_seq sched t_idle γ : nat EQ : t_idle = t + γ GTe : γ < Δ LT : 0 < γ
γ.-1 < Δ
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat IDLE : is_idle arr_seq sched t_idle γ : nat EQ : t_idle = t + γ GTe : γ < Δ LT : 0 < γ
γ.-1 < Δ
apply leq_trans with γ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat IDLE : is_idle arr_seq sched t_idle γ : nat EQ : t_idle = t + γ GTe : γ < Δ LT : 0 < γ
γ.-1 < γ
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat IDLE : is_idle arr_seq sched t_idle γ : nat EQ : t_idle = t + γ GTe : γ < Δ LT : 0 < γ
γ.-1 < γ
by rewrite prednK.
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat IDLE : is_idle arr_seq sched t_idle γ : nat EQ : t_idle = t + γ GTe : γ < Δ LT : 0 < γ
γ <= Δ
by rewrite ltnW.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat IDLE : is_idle arr_seq sched t_idle γ : nat EQ : t_idle = t + γ GTe : γ < Δ LT : 0 < γ
no_carry_in arr_seq sched (t.+1 + γ.-1 )
rewrite -subn1 -addn1 -addnA subnKC // => s ARR BEF.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t LTS : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + (t + Δ - t)) < Δ t_idle : nat IDLE : is_idle arr_seq sched t_idle γ : nat EQ : t_idle = t + γ GTe : γ < Δ LT : 0 < γs : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + γ)
completed_by sched s (t + γ)
exact : idle_instant_no_carry_in.
Qed .
(** In the second case, the sum of blackout and service within
the time interval <<[t, t + Δ)>> is equal to [Δ]. We also
know that the total workload is lower-bounded by the total
service and upper-bounded by [Δ]. Therefore, the total
workload is equal to the total service, which implies
completion of all jobs by time [t + Δ] and hence no carry-in
at time [t + Δ]. *)
Lemma completion_of_all_jobs_implies_no_carry_in :
blackout_during sched t (t + Δ) + total_service t (t + Δ) = Δ ->
no_carry_in arr_seq sched (t + Δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t
blackout_during sched t (t + Δ) +
total_service t (t + Δ) = Δ ->
no_carry_in arr_seq sched (t + Δ)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t
blackout_during sched t (t + Δ) +
total_service t (t + Δ) = Δ ->
no_carry_in arr_seq sched (t + Δ)
rewrite /total_service => EQserv s ARR BEF.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ)
completed_by sched s (t + Δ)
move : (H_workload_is_bounded t) => WORK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ
completed_by sched s (t + Δ)
have EQ: total_workload 0 (t + Δ)
= service_of_jobs sched predT (arrivals_between arr_seq 0 (t + Δ)) 0 (t + Δ);
last exact : workload_eq_service_impl_all_jobs_have_completed.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ
total_workload 0 (t + Δ) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) 0 (t + Δ)
have CONSIST: consistent_arrival_times arr_seq by [].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq
total_workload 0 (t + Δ) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) 0 (t + Δ)
have COMPL := all_jobs_have_completed_impl_workload_eq_service
_ arr_seq CONSIST sched
H_jobs_must_arrive_to_execute
H_completed_jobs_dont_execute
predT 0 t t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : unit_service_proc_model PState ->
(forall j : Job,
j \in arrivals_between arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t
total_workload 0 (t + Δ) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) 0 (t + Δ)
feed_n 2 COMPL => //. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : (forall j : Job,
j \in arrivals_between arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t
forall j : Job,
j \in arrivals_between arr_seq 0 t ->
predT j -> completed_by sched j t
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : (forall j : Job,
j \in arrivals_between arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t
forall j : Job,
j \in arrivals_between arr_seq 0 t ->
predT j -> completed_by sched j t
move => j A B; apply : H_no_carry_in.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : (forall j : Job,
j \in arrivals_between arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t j : Job A : j \in arrivals_between arr_seq 0 t B : predT j
arrives_in arr_seq j
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : (forall j : Job,
j \in arrivals_between arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t j : Job A : j \in arrivals_between arr_seq 0 t B : predT j
arrives_in arr_seq j
apply : in_arrivals_implies_arrived =>//.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : (forall j : Job,
j \in arrivals_between arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t j : Job A : j \in arrivals_between arr_seq 0 t B : predT j
arrived_before j t
by have : arrived_between j 0 t
by apply : (in_arrivals_implies_arrived_between arr_seq). } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t
total_workload 0 (t + Δ) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) 0 (t + Δ)
apply /eqP; rewrite eqn_leq; apply /andP; split ;
last by apply : service_of_jobs_le_workload.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t
total_workload 0 (t + Δ) <=
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) 0 (t + Δ)
rewrite /total_workload (workload_of_jobs_cat arr_seq t);
last by apply /andP; split ; [|rewrite leq_addr].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t
workload_of_jobs predT (arrivals_between arr_seq 0 t) +
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) 0 (t + Δ)
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t
workload_of_jobs predT (arrivals_between arr_seq 0 t) +
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) 0 (t + Δ)
rewrite (service_of_jobs_cat_scheduling_interval _ _ _ _ _ _ _ t) //;
last by apply /andP; split ; [|rewrite leq_addr].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t
workload_of_jobs predT (arrivals_between arr_seq 0 t) +
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t +
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq t (t + Δ)) t (t + Δ)
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t
workload_of_jobs predT (arrivals_between arr_seq 0 t) +
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t +
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq t (t + Δ)) t (t + Δ)
rewrite COMPL -addnA leq_add2l.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq t (t + Δ)) t (t + Δ)
rewrite -service_of_jobs_cat_arrival_interval;
last by apply /andP; split ; [|rewrite leq_addr].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t : duration H_no_carry_in : no_carry_in arr_seq sched t EQserv : blackout_during sched t (t + Δ) +
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t
(t + Δ) = Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ) WORK : no_carry_in arr_seq sched t ->
blackout_during sched t (t + Δ) +
total_workload t (t + Δ) <= Δ CONSIST : consistent_arrival_times arr_seq COMPL : workload_of_jobs predT
(arrivals_between arr_seq 0 t) =
service_of_jobs sched predT
(arrivals_between arr_seq 0 t) 0 t
workload_of_jobs predT
(arrivals_between arr_seq t (t + Δ)) <=
service_of_jobs sched predT
(arrivals_between arr_seq 0 (t + Δ)) t (t + Δ)
by evar (b : nat); rewrite -(leq_add2l b) EQserv.
Qed .
End ProcessorIsNotTooBusyInduction .
(** Finally, we show that any interval of length [Δ] contains a time instant
with no carry-in. *)
Lemma processor_is_not_too_busy :
forall t , exists δ ,
δ < Δ /\ no_carry_in arr_seq sched (t + δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState
forall t : nat,
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t + δ)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState
forall t : nat,
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t + δ)
elim => [|t [δ [LE FQT]]];
first by exists 0 ; split ; [ | rewrite addn0; apply : no_carry_in_at_zero].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat LE : δ < Δ FQT : no_carry_in arr_seq sched (t + δ)
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
move : (posnP δ) => [Z|POS]; last first .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat LE : δ < Δ FQT : no_carry_in arr_seq sched (t + δ) POS : 0 < δ
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat LE : δ < Δ FQT : no_carry_in arr_seq sched (t + δ) POS : 0 < δ
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
exists (δ .-1 ); split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat LE : δ < Δ FQT : no_carry_in arr_seq sched (t + δ) POS : 0 < δ
δ.-1 < Δ
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat LE : δ < Δ FQT : no_carry_in arr_seq sched (t + δ) POS : 0 < δ
δ.-1 < Δ
by apply : leq_trans LE; rewrite prednK.
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat LE : δ < Δ FQT : no_carry_in arr_seq sched (t + δ) POS : 0 < δ
no_carry_in arr_seq sched (t.+1 + δ.-1 )
by rewrite -subn1 -addn1 -addnA subnKC //.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat LE : δ < Δ FQT : no_carry_in arr_seq sched (t + δ) Z : δ = 0
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
move : FQT; rewrite Z addn0 => FQT {LE}.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat Z : δ = 0 FQT : no_carry_in arr_seq sched t
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
move : (total_service_is_bounded_by_Δ t); rewrite leq_eqVlt => /orP [/eqP EQ | LT].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat Z : δ = 0 FQT : no_carry_in arr_seq sched t EQ : blackout_during sched t (t + Δ) +
total_service t (t + Δ) = Δ
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat Z : δ = 0 FQT : no_carry_in arr_seq sched t EQ : blackout_during sched t (t + Δ) +
total_service t (t + Δ) = Δ
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
exists (Δ .-1 ); split ; first by rewrite prednK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat Z : δ = 0 FQT : no_carry_in arr_seq sched t EQ : blackout_during sched t (t + Δ) +
total_service t (t + Δ) = Δ
no_carry_in arr_seq sched (t.+1 + Δ.-1 )
rewrite addSn -subn1 -addn1 -addnA subnK //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat Z : δ = 0 FQT : no_carry_in arr_seq sched t EQ : blackout_during sched t (t + Δ) +
total_service t (t + Δ) = Δ
no_carry_in arr_seq sched (t + Δ)
by apply : completion_of_all_jobs_implies_no_carry_in.
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState t, δ : nat Z : δ = 0 FQT : no_carry_in arr_seq sched t LT : blackout_during sched t (t + Δ) +
total_service t (t + Δ) < Δ
exists δ : nat,
δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ)
by apply :low_total_service_implies_existence_of_time_with_no_carry_in.
Qed .
End ProcessorIsNotTooBusy .
(** ** Busy Interval Existence *)
(** Consider an arbitrary job [j] with positive cost. *)
Variable j : Job.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** We show that there must exist a busy interval <<[t1, t2)>> that
contains the arrival time of [j]. *)
Theorem busy_interval_from_total_workload_bound :
exists t1 t2 ,
t1 <= job_arrival j < t2
/\ t2 <= t1 + Δ
/\ busy_interval arr_seq sched j t1 t2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j
exists t1 t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j
exists t1 t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
rename H_from_arrival_sequence into ARR, H_job_cost_positive into POS.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j
exists t1 t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
edestruct (exists_busy_interval_prefix
arr_seq H_valid_arr_seq
sched j ARR H_priority_is_reflexive (job_arrival j))
as [t1 [PREFIX GE]]; first by apply : job_pending_at_arrival.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE : t1 <= job_arrival j <= job_arrival j
exists t1 t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
move : GE => /andP [GE1 _].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j
exists t1 t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
exists t1 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j
exists t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
have [δ [LE nCAR]]: exists δ : nat, δ < Δ /\ no_carry_in arr_seq sched (t1.+1 + δ)
by apply : processor_is_not_too_busy => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ)
exists t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
have QT : quiet_time arr_seq sched j (t1.+1 + δ) by apply : no_carry_in_implies_quiet_time.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ)
exists t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
have EX: exists t2 , ((t1 < t2 <= t1.+1 + δ) && quiet_time_dec arr_seq sched j t2).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ)
exists t2 : nat,
(t1 < t2 <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j t2
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ)
exists t2 : nat,
(t1 < t2 <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j t2
exists (t1 .+1 + δ); apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ)
t1 < t1.+1 + δ <= t1.+1 + δ
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ)
t1 < t1.+1 + δ <= t1.+1 + δ
by apply /andP; split ; first rewrite addSn ltnS leq_addr.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ)
quiet_time_dec arr_seq sched j (t1.+1 + δ)
exact /quiet_time_P. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) EX : exists t2 : nat,
(t1 < t2 <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j t2
exists t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
move : (ex_minnP EX) => [t2 /andP [/andP [GTt2 LEt2] QUIET] MIN]; clear EX.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= n
exists t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
have NEQ: t1 <= job_arrival j < t2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= n
t1 <= job_arrival j < t2
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= n
t1 <= job_arrival j < t2
apply /andP; split => [//|].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= n
job_arrival j < t2
rewrite ltnNge; apply /negP => CONTR.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nCONTR : t2 <= job_arrival j
False
have [_ [_ [NQT _]]] := PREFIX.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nCONTR : t2 <= job_arrival j NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ quiet_time arr_seq sched j t
False
have {}NQT := NQT t2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nCONTR : t2 <= job_arrival j NQT : t1 < t2 < (job_arrival j).+1 ->
~ quiet_time arr_seq sched j t2
False
feed NQT; first by (apply /andP; split ; [|rewrite ltnS]). Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nCONTR : t2 <= job_arrival j NQT : ~ quiet_time arr_seq sched j t2
False
by apply : NQT; apply /quiet_time_P. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2
exists t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
exists t2 ; split => [//|]; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2
t2 <= t1 + Δ
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2
t2 <= t1 + Δ
by apply : (leq_trans LEt2); rewrite addSn ltn_add2l. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2
busy_interval arr_seq sched j t1 t2
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2
busy_interval arr_seq sched j t1 t2
move : PREFIX => [_ [QTt1 [NQT _]]]; repeat split => //; last by exact /quiet_time_P.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ quiet_time arr_seq sched j t
forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j t
move => t /andP [GEt LTt] QTt.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ quiet_time arr_seq sched j tt : nat GEt : t1 < t LTt : t < t2 QTt : quiet_time arr_seq sched j t
False
feed (MIN t);
last by move : LTt; rewrite ltnNge; move => /negP LTt; apply : LTt. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ quiet_time arr_seq sched j tt : nat GEt : t1 < t LTt : t < t2 QTt : quiet_time arr_seq sched j t
(t1 < t <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j t
apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ quiet_time arr_seq sched j tt : nat GEt : t1 < t LTt : t < t2 QTt : quiet_time arr_seq sched j t
t1 < t <= t1.+1 + δ
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ quiet_time arr_seq sched j tt : nat GEt : t1 < t LTt : t < t2 QTt : quiet_time arr_seq sched j t
t1 < t <= t1.+1 + δ
by apply /andP; split ; last (apply leq_trans with t2; [apply ltnW |]).
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arr_seq : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState H_fully_consuming_proc_model : fully_consuming_proc_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between arr_seq t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
no_carry_in arr_seq sched t ->
blackout_during sched t
(t + Δ) +
total_workload t (t + Δ) <= ΔH_unit_service_proc_model : unit_service_proc_model
PState j : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ nCAR : no_carry_in arr_seq sched (t1.+1 + δ) QT : quiet_time arr_seq sched j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ quiet_time arr_seq sched j tt : nat GEt : t1 < t LTt : t < t2 QTt : quiet_time arr_seq sched j t
quiet_time_dec arr_seq sched j t
exact /quiet_time_P. }
Qed .
End BusyIntervalExistence .