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.model.schedule.priority_driven.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [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.busy_interval.existence.
Require Export prosa.util.tactics.
Require Export prosa.model.task.preemption.parameters.
Require Export prosa.analysis.facts.model.preemption.
(** * Processor Executes HEP jobs at Preemption Point *)
(** In this file, we show that, given a busy interval of a job [j],
the processor is always busy scheduling a higher-or-equal-priority
job at any preemptive point inside the busy interval. *)
Section ProcessorBusyWithHEPJobAtPreemptionPoints .
(** Consider any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{Arrival : JobArrival Job}.
Context `{Cost : JobCost Job}.
(** Consider any arrival sequence with consistent arrivals ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
(** ... and any uniprocessor schedule of this arrival sequence. *)
Context {PState : ProcessorState Job}.
Hypothesis H_uni : uniprocessor_model PState.
Variable sched : schedule PState.
(** Consider a JLFP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive. *)
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.
(** In addition, we assume the existence of a function mapping a job
and its progress to a boolean value saying whether this job is
preemptable at its current point of execution. *)
Context `{JobPreemptable Job}.
(** Further, allow for any work-bearing notion of job readiness. *)
Context `{@JobReady Job PState Cost Arrival}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** We assume that the schedule is valid and that all jobs come from the arrival sequence. *)
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
(** Next, we assume that the schedule is a work-conserving schedule... *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** ... and the schedule respects the scheduling policy at every preemption point. *)
Hypothesis H_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
(** Consider any job [j] with positive job cost. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** Consider any busy interval prefix <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval_prefix :
busy_interval_prefix arr_seq sched j t1 t2.
(** Consider an arbitrary preemption time t ∈ <<[t1,t2)>>. *)
Variable t : instant.
Hypothesis H_t_in_busy_interval : t1 <= t < t2.
Hypothesis H_t_preemption_time : preemption_time arr_seq sched t.
(** First note since [t] lies inside the busy interval,
the processor cannot be idle at time [t]. *)
Lemma instant_t_is_not_idle :
~ is_idle arr_seq sched t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t
~ is_idle arr_seq sched t
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t
~ is_idle arr_seq sched t
by move => IDLE; apply : not_quiet_implies_not_idle => //.
Qed .
(** Next we consider two cases:
(1) [t] is less than [t2 - 1] and
(2) [t] is equal to [t2 - 1]. *)
(** In case when [t < t2 - 1], we use the fact that time instant
[t+1] is not a quiet time. The later implies that there is a
pending higher-or-equal priority job at time [t]. Thus, the
assumption that the schedule respects priority policy at
preemption points implies that the scheduled job must have a
higher-or-equal priority. *)
Lemma scheduled_at_preemption_time_implies_higher_or_equal_priority_lt :
t < t2.-1 ->
forall jhp ,
scheduled_at sched jhp t ->
hep_job jhp j.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t
t < t2.-1 ->
forall jhp : Job,
scheduled_at sched jhp t -> hep_job jhp j
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t
t < t2.-1 ->
forall jhp : Job,
scheduled_at sched jhp t -> hep_job jhp j
intros LTt2m1 jlp Sched_jlp; apply contraT; move => /negP NOTHP; exfalso .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j
False
move : (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2
False
apply NOTQUIET with (t := t.+1 ).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2
t1 < t.+1 < t2
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2
t1 < t.+1 < t2
apply /andP; split .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2
t1 < t.+1
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2
t1 < t.+1
by apply leq_ltn_trans with t1.
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2
t.+1 < t2
rewrite -subn1 ltn_subRL addnC in LTt2m1.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 LTt2m1 : t + 1 < t2
t.+1 < t2
by rewrite -[t.+1 ]addn1.
} Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2
quiet_time arr_seq sched j t.+1
intros j_hp ARR HP BEF.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j_hp : Job ARR : arrives_in arr_seq j_hp HP : hep_job j_hp j BEF : arrived_before j_hp t.+1
completed_by sched j_hp t.+1
apply contraT => NCOMP'; exfalso .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j_hp : Job ARR : arrives_in arr_seq j_hp HP : hep_job j_hp j BEF : arrived_before j_hp t.+1 NCOMP' : ~~ completed_by sched j_hp t.+1
False
have PEND : pending sched j_hp t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j_hp : Job ARR : arrives_in arr_seq j_hp HP : hep_job j_hp j BEF : arrived_before j_hp t.+1 NCOMP' : ~~ completed_by sched j_hp t.+1
pending sched j_hp t
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j_hp : Job ARR : arrives_in arr_seq j_hp HP : hep_job j_hp j BEF : arrived_before j_hp t.+1 NCOMP' : ~~ completed_by sched j_hp t.+1
pending sched j_hp t
apply /andP; split .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j_hp : Job ARR : arrives_in arr_seq j_hp HP : hep_job j_hp j BEF : arrived_before j_hp t.+1 NCOMP' : ~~ completed_by sched j_hp t.+1
has_arrived j_hp t
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j_hp : Job ARR : arrives_in arr_seq j_hp HP : hep_job j_hp j BEF : arrived_before j_hp t.+1 NCOMP' : ~~ completed_by sched j_hp t.+1
has_arrived j_hp t
by rewrite /has_arrived.
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j_hp : Job ARR : arrives_in arr_seq j_hp HP : hep_job j_hp j BEF : arrived_before j_hp t.+1 NCOMP' : ~~ completed_by sched j_hp t.+1
~~ completed_by sched j_hp t
by move : NCOMP'; apply contra, completion_monotonic.
} Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j_hp : Job ARR : arrives_in arr_seq j_hp HP : hep_job j_hp j BEF : arrived_before j_hp t.+1 NCOMP' : ~~ completed_by sched j_hp t.+1 PEND : pending sched j_hp t
False
apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' HEP']]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j_hp : Job ARR : arrives_in arr_seq j_hp HP : hep_job j_hp j BEF : arrived_before j_hp t.+1 NCOMP' : ~~ completed_by sched j_hp t.+1 j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP' : hep_job j' j_hp
False
have HEP : hep_job j' j by apply (H_priority_is_transitive j_hp).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j_hp : Job ARR : arrives_in arr_seq j_hp HP : hep_job j_hp j BEF : arrived_before j_hp t.+1 NCOMP' : ~~ completed_by sched j_hp t.+1 j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP' : hep_job j' j_hp HEP : hep_job j' j
False
clear HEP' NCOMP' BEF HP ARR j_hp.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j
False
have BACK: backlogged sched j' t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j
backlogged sched j' t
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j
backlogged sched j' t
apply /andP; split => [//|].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j
~~ scheduled_at sched j' t
apply /negP; intro SCHED'.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j SCHED' : scheduled_at sched j' t
False
move : (H_uni jlp j' sched t Sched_jlp SCHED') => EQ.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j SCHED' : scheduled_at sched j' t EQ : jlp = j'
False
by subst ; apply : NOTHP.
} Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j BACK : backlogged sched j' t
False
apply NOTHP, (H_priority_is_transitive j'); last by eapply HEP.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t LTt2m1 : t < t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j BACK : backlogged sched j' t
hep_job jlp j'
by eapply H_respects_policy; eauto .
Qed .
(** In the case when [t = t2 - 1], we cannot use the same proof
since [t+1 = t2], but [t2] is a quiet time. So we do a similar
case analysis on the fact that [t1 = t ∨ t1 < t]. *)
Lemma scheduled_at_preemption_time_implies_higher_or_equal_priority_eq :
t = t2.-1 ->
forall jhp ,
scheduled_at sched jhp t ->
hep_job jhp j.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t
t = t2.-1 ->
forall jhp : Job,
scheduled_at sched jhp t -> hep_job jhp j
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t
t = t2.-1 ->
forall jhp : Job,
scheduled_at sched jhp t -> hep_job jhp j
intros EQUALt2m1 jlp Sched_jlp; apply contraT; move => /negP NOTHP; exfalso .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j
False
move : (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2
False
rewrite leq_eqVlt in GEt; first move : GEt => /orP [/eqP EQUALt1 | LARGERt1].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 EQUALt1 : t1 = t
False
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 EQUALt1 : t1 = t
False
subst t t1; clear LEt SL.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t2.-1 t2 H_t_preemption_time : preemption_time arr_seq sched
t2.-1 H_t_in_busy_interval : t2.-1 <= t2.-1 < t2 jlp : Job Sched_jlp : scheduled_at sched jlp t2.-1 NOTHP : ~ hep_job jlp j INBI : t2.-1 <= job_arrival j < t2 NOTQUIET : forall t : nat,
t2.-1 < t < t2 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j t2.-1
False
have ARR : job_arrival j = t2.-1 .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t2.-1 t2 H_t_preemption_time : preemption_time arr_seq sched
t2.-1 H_t_in_busy_interval : t2.-1 <= t2.-1 < t2 jlp : Job Sched_jlp : scheduled_at sched jlp t2.-1 NOTHP : ~ hep_job jlp j INBI : t2.-1 <= job_arrival j < t2 NOTQUIET : forall t : nat,
t2.-1 < t < t2 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j t2.-1
job_arrival j = t2.-1
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t2.-1 t2 H_t_preemption_time : preemption_time arr_seq sched
t2.-1 H_t_in_busy_interval : t2.-1 <= t2.-1 < t2 jlp : Job Sched_jlp : scheduled_at sched jlp t2.-1 NOTHP : ~ hep_job jlp j INBI : t2.-1 <= job_arrival j < t2 NOTQUIET : forall t : nat,
t2.-1 < t < t2 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j t2.-1
job_arrival j = t2.-1
apply /eqP; rewrite eq_sym eqn_leq.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t2.-1 t2 H_t_preemption_time : preemption_time arr_seq sched
t2.-1 H_t_in_busy_interval : t2.-1 <= t2.-1 < t2 jlp : Job Sched_jlp : scheduled_at sched jlp t2.-1 NOTHP : ~ hep_job jlp j INBI : t2.-1 <= job_arrival j < t2 NOTQUIET : forall t : nat,
t2.-1 < t < t2 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j t2.-1
t2.-1 <= job_arrival j <= t2.-1
destruct t2 => [//|].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant i : nat H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j i.+1 .-1 i.+1 H_t_preemption_time : preemption_time arr_seq sched
i.+1 .-1 H_t_in_busy_interval : i.+1 .-1 <= i.+1 .-1 < i.+1 jlp : Job Sched_jlp : scheduled_at sched jlp i.+1 .-1 NOTHP : ~ hep_job jlp j INBI : i.+1 .-1 <= job_arrival j < i.+1 NOTQUIET : forall t : nat,
i.+1 .-1 < t < i.+1 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j i.+1 .-1
i.+1 .-1 <= job_arrival j <= i.+1 .-1
rewrite ltnS -pred_Sn in INBI.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant i : nat H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j i.+1 .-1 i.+1 H_t_preemption_time : preemption_time arr_seq sched
i.+1 .-1 H_t_in_busy_interval : i.+1 .-1 <= i.+1 .-1 < i.+1 jlp : Job Sched_jlp : scheduled_at sched jlp i.+1 .-1 NOTHP : ~ hep_job jlp j NOTQUIET : forall t : nat,
i.+1 .-1 < t < i.+1 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j i.+1 .-1 INBI : i <= job_arrival j <= i
i.+1 .-1 <= job_arrival j <= i.+1 .-1
by rewrite -pred_Sn.
} Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t2.-1 t2 H_t_preemption_time : preemption_time arr_seq sched
t2.-1 H_t_in_busy_interval : t2.-1 <= t2.-1 < t2 jlp : Job Sched_jlp : scheduled_at sched jlp t2.-1 NOTHP : ~ hep_job jlp j INBI : t2.-1 <= job_arrival j < t2 NOTQUIET : forall t : nat,
t2.-1 < t < t2 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j t2.-1 ARR : job_arrival j = t2.-1
False
have PEND: pending sched j t2.-1
by rewrite -ARR; apply job_pending_at_arrival.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t2.-1 t2 H_t_preemption_time : preemption_time arr_seq sched
t2.-1 H_t_in_busy_interval : t2.-1 <= t2.-1 < t2 jlp : Job Sched_jlp : scheduled_at sched jlp t2.-1 NOTHP : ~ hep_job jlp j INBI : t2.-1 <= job_arrival j < t2 NOTQUIET : forall t : nat,
t2.-1 < t < t2 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j t2.-1 ARR : job_arrival j = t2.-1 PEND : pending sched j t2.-1
False
apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [PENDhp HEPhp]]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t2.-1 t2 H_t_preemption_time : preemption_time arr_seq sched
t2.-1 H_t_in_busy_interval : t2.-1 <= t2.-1 < t2 jlp : Job Sched_jlp : scheduled_at sched jlp t2.-1 NOTHP : ~ hep_job jlp j INBI : t2.-1 <= job_arrival j < t2 NOTQUIET : forall t : nat,
t2.-1 < t < t2 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j t2.-1 ARR : job_arrival j = t2.-1 jhp : Job ARRhp : arrives_in arr_seq jhp PENDhp : job_ready sched jhp t2.-1 HEPhp : hep_job jhp j
False
eapply NOTHP, H_priority_is_transitive; last by apply HEPhp.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t2.-1 t2 H_t_preemption_time : preemption_time arr_seq sched
t2.-1 H_t_in_busy_interval : t2.-1 <= t2.-1 < t2 jlp : Job Sched_jlp : scheduled_at sched jlp t2.-1 NOTHP : ~ hep_job jlp j INBI : t2.-1 <= job_arrival j < t2 NOTQUIET : forall t : nat,
t2.-1 < t < t2 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j t2.-1 ARR : job_arrival j = t2.-1 jhp : Job ARRhp : arrives_in arr_seq jhp PENDhp : job_ready sched jhp t2.-1 HEPhp : hep_job jhp j
hep_job jlp jhp
apply (H_respects_policy _ _ t2.-1 ); auto .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t2.-1 t2 H_t_preemption_time : preemption_time arr_seq sched
t2.-1 H_t_in_busy_interval : t2.-1 <= t2.-1 < t2 jlp : Job Sched_jlp : scheduled_at sched jlp t2.-1 NOTHP : ~ hep_job jlp j INBI : t2.-1 <= job_arrival j < t2 NOTQUIET : forall t : nat,
t2.-1 < t < t2 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j t2.-1 ARR : job_arrival j = t2.-1 jhp : Job ARRhp : arrives_in arr_seq jhp PENDhp : job_ready sched jhp t2.-1 HEPhp : hep_job jhp j
backlogged sched jhp t2.-1
apply /andP; split => [//|].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t2.-1 t2 H_t_preemption_time : preemption_time arr_seq sched
t2.-1 H_t_in_busy_interval : t2.-1 <= t2.-1 < t2 jlp : Job Sched_jlp : scheduled_at sched jlp t2.-1 NOTHP : ~ hep_job jlp j INBI : t2.-1 <= job_arrival j < t2 NOTQUIET : forall t : nat,
t2.-1 < t < t2 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j t2.-1 ARR : job_arrival j = t2.-1 jhp : Job ARRhp : arrives_in arr_seq jhp PENDhp : job_ready sched jhp t2.-1 HEPhp : hep_job jhp j
~~ scheduled_at sched jhp t2.-1
apply /negP; intros SCHED.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t2.-1 t2 H_t_preemption_time : preemption_time arr_seq sched
t2.-1 H_t_in_busy_interval : t2.-1 <= t2.-1 < t2 jlp : Job Sched_jlp : scheduled_at sched jlp t2.-1 NOTHP : ~ hep_job jlp j INBI : t2.-1 <= job_arrival j < t2 NOTQUIET : forall t : nat,
t2.-1 < t < t2 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j t2.-1 ARR : job_arrival j = t2.-1 jhp : Job ARRhp : arrives_in arr_seq jhp PENDhp : job_ready sched jhp t2.-1 HEPhp : hep_job jhp j SCHED : scheduled_at sched jhp t2.-1
False
move : (H_uni _ _ sched _ SCHED Sched_jlp) => EQ.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t2.-1 t2 H_t_preemption_time : preemption_time arr_seq sched
t2.-1 H_t_in_busy_interval : t2.-1 <= t2.-1 < t2 jlp : Job Sched_jlp : scheduled_at sched jlp t2.-1 NOTHP : ~ hep_job jlp j INBI : t2.-1 <= job_arrival j < t2 NOTQUIET : forall t : nat,
t2.-1 < t < t2 ->
~ quiet_time arr_seq sched j tQUIET : quiet_time arr_seq sched j t2.-1 ARR : job_arrival j = t2.-1 jhp : Job ARRhp : arrives_in arr_seq jhp PENDhp : job_ready sched jhp t2.-1 HEPhp : hep_job jhp j SCHED : scheduled_at sched jhp t2.-1 EQ : jhp = jlp
False
by subst ; apply : NOTHP.
} Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t
False
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t
False
feed (NOTQUIET t); first by apply /andP; split . Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t
False
apply NOTQUIET; intros j_hp' IN HP ARR.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j_hp' : Job IN : arrives_in arr_seq j_hp' HP : hep_job j_hp' j ARR : arrived_before j_hp' t
completed_by sched j_hp' t
apply contraT => NOTCOMP'; exfalso .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j_hp' : Job IN : arrives_in arr_seq j_hp' HP : hep_job j_hp' j ARR : arrived_before j_hp' t NOTCOMP' : ~~ completed_by sched j_hp' t
False
have PEND : pending sched j_hp' t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j_hp' : Job IN : arrives_in arr_seq j_hp' HP : hep_job j_hp' j ARR : arrived_before j_hp' t NOTCOMP' : ~~ completed_by sched j_hp' t
pending sched j_hp' t
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j_hp' : Job IN : arrives_in arr_seq j_hp' HP : hep_job j_hp' j ARR : arrived_before j_hp' t NOTCOMP' : ~~ completed_by sched j_hp' t
pending sched j_hp' t
apply /andP; split .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j_hp' : Job IN : arrives_in arr_seq j_hp' HP : hep_job j_hp' j ARR : arrived_before j_hp' t NOTCOMP' : ~~ completed_by sched j_hp' t
has_arrived j_hp' t
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j_hp' : Job IN : arrives_in arr_seq j_hp' HP : hep_job j_hp' j ARR : arrived_before j_hp' t NOTCOMP' : ~~ completed_by sched j_hp' t
has_arrived j_hp' t
by rewrite /has_arrived ltnW.
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j_hp' : Job IN : arrives_in arr_seq j_hp' HP : hep_job j_hp' j ARR : arrived_before j_hp' t NOTCOMP' : ~~ completed_by sched j_hp' t
~~ completed_by sched j_hp' t
by move : NOTCOMP'; apply contra, completion_monotonic.
} Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j_hp' : Job IN : arrives_in arr_seq j_hp' HP : hep_job j_hp' j ARR : arrived_before j_hp' t NOTCOMP' : ~~ completed_by sched j_hp' t PEND : pending sched j_hp' t
False
apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' HEP']]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j_hp' : Job IN : arrives_in arr_seq j_hp' HP : hep_job j_hp' j ARR : arrived_before j_hp' t NOTCOMP' : ~~ completed_by sched j_hp' t j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP' : hep_job j' j_hp'
False
have HEP : hep_job j' j by apply (H_priority_is_transitive j_hp').Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j_hp' : Job IN : arrives_in arr_seq j_hp' HP : hep_job j_hp' j ARR : arrived_before j_hp' t NOTCOMP' : ~~ completed_by sched j_hp' t j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP' : hep_job j' j_hp' HEP : hep_job j' j
False
clear ARR HP IN HEP' NOTCOMP' j_hp'.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j
False
have BACK: backlogged sched j' t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j
backlogged sched j' t
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j
backlogged sched j' t
apply /andP; split => [//|].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j
~~ scheduled_at sched j' t
apply /negP; intro SCHED'.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j SCHED' : scheduled_at sched j' t
False
move : (H_uni jlp j' sched t Sched_jlp SCHED') => EQ.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j SCHED' : scheduled_at sched j' t EQ : jlp = j'
False
by subst ; apply : NOTHP.
} Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j BACK : backlogged sched j' t
False
apply NOTHP, (H_priority_is_transitive j'); last by eapply HEP.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t EQUALt2m1 : t = t2.-1 jlp : Job Sched_jlp : scheduled_at sched jlp t NOTHP : ~ hep_job jlp j LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : ~ quiet_time arr_seq sched j t INBI : t1 <= job_arrival j < t2 LARGERt1 : t1 < t j' : Job ARR' : arrives_in arr_seq j' READY' : job_ready sched j' t HEP : hep_job j' j BACK : backlogged sched j' t
hep_job jlp j'
by eapply H_respects_policy; eauto .
}
Qed .
(** By combining the above facts we conclude that a job that is
scheduled at time [t] has higher-or-equal priority. *)
Corollary scheduled_at_preemption_time_implies_higher_or_equal_priority :
forall jhp ,
scheduled_at sched jhp t ->
hep_job jhp j.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t
forall jhp : Job,
scheduled_at sched jhp t -> hep_job jhp j
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t
forall jhp : Job,
scheduled_at sched jhp t -> hep_job jhp j
move : (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2
forall jhp : Job,
scheduled_at sched jhp t -> hep_job jhp j
have : t <= t2.-1 by rewrite -subn1 leq_subRL_impl // addn1.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2
t <= t2.-1 ->
forall jhp : Job,
scheduled_at sched jhp t -> hep_job jhp j
rewrite leq_eqVlt => /orP [/eqP EQUALt2m1 | LTt2m1].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 EQUALt2m1 : t = t2.-1
forall jhp : Job,
scheduled_at sched jhp t -> hep_job jhp j
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 EQUALt2m1 : t = t2.-1
forall jhp : Job,
scheduled_at sched jhp t -> hep_job jhp j
by apply scheduled_at_preemption_time_implies_higher_or_equal_priority_eq.
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t GEt : t1 <= t LEt : t < t2 SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 LTt2m1 : t < t2.-1
forall jhp : Job,
scheduled_at sched jhp t -> hep_job jhp j
by apply scheduled_at_preemption_time_implies_higher_or_equal_priority_lt.
Qed .
(** Since a job that is scheduled at time [t] has higher-or-equal
priority, by properties of a busy interval it cannot arrive
before time instant [t1]. *)
Lemma scheduled_at_preemption_time_implies_arrived_between_within_busy_interval :
forall jhp ,
scheduled_at sched jhp t ->
arrived_between jhp t1 t2.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t
forall jhp : Job,
scheduled_at sched jhp t -> arrived_between jhp t1 t2
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t
forall jhp : Job,
scheduled_at sched jhp t -> arrived_between jhp t1 t2
intros jhp Sched_jhp.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t
arrived_between jhp t1 t2
rename H_work_conserving into WORK.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq WORK : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t
arrived_between jhp t1 t2
move : (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET INBI]]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq WORK : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2
arrived_between jhp t1 t2
move : (H_t_in_busy_interval) => /andP [GEt LEt].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq WORK : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2
arrived_between jhp t1 t2
have HP := scheduled_at_preemption_time_implies_higher_or_equal_priority _ Sched_jhp.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq WORK : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 HP : hep_job jhp j
arrived_between jhp t1 t2
move : (Sched_jhp) => PENDING.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq WORK : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 HP : hep_job jhp j PENDING : scheduled_at sched jhp t
arrived_between jhp t1 t2
eapply scheduled_implies_pending in PENDING => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq WORK : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 HP : hep_job jhp j PENDING : pending sched jhp t
arrived_between jhp t1 t2
apply /andP; split ; last by apply leq_ltn_trans with (n := t); first by move : PENDING => /andP [ARR _].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq WORK : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 HP : hep_job jhp j PENDING : pending sched jhp t
t1 <= job_arrival jhp
apply contraT; rewrite -ltnNge; intro LT; exfalso .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq WORK : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 HP : hep_job jhp j PENDING : pending sched jhp t LT : job_arrival jhp < t1
False
feed (QUIET jhp) => //. Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq WORK : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t SL : t1 < t2 QUIET : hep_job jhp j ->
arrived_before jhp t1 ->
completed_by sched jhp t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 HP : hep_job jhp j PENDING : pending sched jhp t LT : job_arrival jhp < t1
False
specialize (QUIET HP LT).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq WORK : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t SL : t1 < t2 QUIET : completed_by sched jhp t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 HP : hep_job jhp j PENDING : pending sched jhp t LT : job_arrival jhp < t1
False
have COMP: completed_by sched jhp t by apply : completion_monotonic QUIET.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq WORK : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t SL : t1 < t2 QUIET : completed_by sched jhp t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 HP : hep_job jhp j PENDING : pending sched jhp t LT : job_arrival jhp < t1 COMP : completed_by sched jhp t
False
apply completed_implies_not_scheduled in COMP => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq WORK : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t jhp : Job Sched_jhp : scheduled_at sched jhp t SL : t1 < t2 QUIET : completed_by sched jhp t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 HP : hep_job jhp j PENDING : pending sched jhp t LT : job_arrival jhp < t1 COMP : ~~ scheduled_at sched jhp t
False
by move : COMP => /negP COMP; apply COMP.
Qed .
(** From the above lemmas we prove that there is a job [jhp] that is
(1) scheduled at time [t], (2) has higher-or-equal priority, and
(3) arrived between [t1] and [t2]. *)
Corollary not_quiet_implies_exists_scheduled_hp_job_at_preemption_point :
exists j_hp ,
arrived_between j_hp t1 t2
/\ hep_job j_hp j
/\ scheduled_at sched j_hp t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t
exists j_hp : Job,
arrived_between j_hp t1 t2 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t
exists j_hp : Job,
arrived_between j_hp t1 t2 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
move : (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET INBI]]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2
exists j_hp : Job,
arrived_between j_hp t1 t2 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
move : (H_t_in_busy_interval) => /andP [GEt LEt].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2
exists j_hp : Job,
arrived_between j_hp t1 t2 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
have [IDLE|[j' SCHED]] := scheduled_at_cases _ H_valid_arrivals sched ltac :(by []) ltac :(by []) t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 IDLE : is_idle arr_seq sched t
exists j_hp : Job,
arrived_between j_hp t1 t2 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 IDLE : is_idle arr_seq sched t
exists j_hp : Job,
arrived_between j_hp t1 t2 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
by exfalso ; apply instant_t_is_not_idle.
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 j' : Job SCHED : scheduled_at sched j' t
exists j_hp : Job,
arrived_between j_hp t1 t2 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
exists j' ; repeat split => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 j' : Job SCHED : scheduled_at sched j' t
arrived_between j' t1 t2
* Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 j' : Job SCHED : scheduled_at sched j' t
arrived_between j' t1 t2
exact : scheduled_at_preemption_time_implies_arrived_between_within_busy_interval.
* Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H : JobPreemptable Job H0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 t : instant H_t_in_busy_interval : t1 <= t < t2 H_t_preemption_time : preemption_time arr_seq sched t SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tINBI : t1 <= job_arrival j < t2 GEt : t1 <= t LEt : t < t2 j' : Job SCHED : scheduled_at sched j' t
hep_job j' j
exact : scheduled_at_preemption_time_implies_higher_or_equal_priority.
Qed .
End ProcessorBusyWithHEPJobAtPreemptionPoints .
(** * Processor Executes HEP Jobs after Preemption Point *)
(** In this section, we prove that at any time instant after any
preemption point (inside the busy interval), the processor is
always busy scheduling a job with higher or equal priority. *)
Section ProcessorBusyWithHEPJobAfterPreemptionPoints .
(** 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 arrival sequence with consistent arrivals ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
(** ... and any uniprocessor schedule of this arrival sequence. *)
Context {PState : ProcessorState Job}.
Hypothesis H_uni : uniprocessor_model PState.
Variable sched : schedule PState.
(** Consider a JLFP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive. *)
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.
(** Consider a valid preemption model with known maximum non-preemptive
segment lengths. *)
Context `{TaskMaxNonpreemptiveSegment Task} `{JobPreemptable Job}.
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
(** Further, allow for any work-bearing notion of job readiness. *)
Context `{!JobReady Job PState}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** We assume that the schedule is valid. *)
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
(** Next, we assume that the schedule is work-conserving ... *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** ... and the schedule respects the scheduling policy at every preemption point. *)
Hypothesis H_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
(** Consider any job [j] with positive job cost. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** Consider any busy interval prefix <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval_prefix :
busy_interval_prefix arr_seq sched j t1 t2.
(** First, recall from the above section that the processor at any
preemption time is always busy scheduling a job with higher or equal
priority. *)
(** We show that, at any time instant after a preemption point, the
processor is always busy with a job with higher or equal
priority. *)
Lemma not_quiet_implies_exists_scheduled_hp_job_after_preemption_point :
forall tp t ,
preemption_time arr_seq sched tp ->
t1 <= tp < t2 ->
tp <= t < t2 ->
exists j_hp ,
arrived_between j_hp t1 t.+1 /\
hep_job j_hp j /\
scheduled_at sched j_hp 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2
forall (tp : instant) (t : nat),
preemption_time arr_seq sched tp ->
t1 <= tp < t2 ->
tp <= t < t2 ->
exists j_hp : Job,
arrived_between j_hp t1 t.+1 /\
hep_job j_hp j /\ scheduled_at sched j_hp 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2
forall (tp : instant) (t : nat),
preemption_time arr_seq sched tp ->
t1 <= tp < t2 ->
tp <= t < t2 ->
exists j_hp : Job,
arrived_between j_hp t1 t.+1 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
move => tp t PRPOINT /andP [GEtp LTtp] /andP [LEtp 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2
exists j_hp : Job,
arrived_between j_hp t1 t.+1 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
have [Idle|[jhp Sched_jhp]] :=
scheduled_at_cases _ H_valid_arrivals sched ltac :(by []) ltac :(by []) 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 Idle : is_idle arr_seq sched t
exists j_hp : Job,
arrived_between j_hp t1 t.+1 /\
hep_job j_hp j /\ scheduled_at sched j_hp 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 Idle : is_idle arr_seq sched t
exists j_hp : Job,
arrived_between j_hp t1 t.+1 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
eapply instant_t_is_not_idle in 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 Idle : is_idle arr_seq sched t
t1 <= t < t2
by apply /andP; split ; first apply leq_trans with tp. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t
exists j_hp : Job,
arrived_between j_hp t1 t.+1 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
exists jhp .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t
arrived_between jhp t1 t.+1 /\
hep_job jhp j /\ scheduled_at sched jhp t
have HP: hep_job jhp 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t
hep_job jhp 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t
hep_job jhp j
have PP := scheduling_of_any_segment_starts_with_preemption_time _
arr_seq H_valid_arrivals
sched H_sched_valid H_valid_preemption_model jhp t Sched_jhp.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t PP : uniprocessor_model PState ->
exists pt : nat,
job_arrival jhp <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched jhp t')
hep_job jhp j
feed PP => //. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t PP : exists pt : nat,
job_arrival jhp <= pt <= t /\
preemption_time arr_seq sched pt /\
(forall t' : nat,
pt <= t' <= t -> scheduled_at sched jhp t')
hep_job jhp j
move : PP => [prt [/andP [_ LE] [PR SCH]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jhp t'
hep_job jhp j
case E:(t1 <= prt).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jhp t'E : (t1 <= prt) = true
hep_job jhp 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jhp t'E : (t1 <= prt) = true
hep_job jhp j
move : E => /eqP /eqP E; rewrite subn_eq0 in E.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jhp t'E : t1 <= prt
hep_job jhp j
edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point as [jlp [_ [HEP SCHEDjhp]]] => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jhp t'E : t1 <= prt
t1 <= prt < 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jhp t'E : t1 <= prt
t1 <= prt < t2
by apply /andP; split ; last by apply leq_ltn_trans with 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jhp t'E : t1 <= prt jlp : Job HEP : hep_job jlp j SCHEDjhp : scheduled_at sched jlp prt
hep_job jhp j
enough (EQ : jhp = jlp); first by subst .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jhp t'E : t1 <= prt jlp : Job HEP : hep_job jlp j SCHEDjhp : scheduled_at sched jlp prt
jhp = jlp
apply : (H_uni _ _ _ prt); eauto ;
by apply SCH; 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jhp t'E : (t1 <= prt) = false
hep_job jhp j
move : E => /eqP /neqP E; rewrite -lt0n subn_gt0 in E.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jhp t'E : prt < t1
hep_job jhp j
apply negbNE; apply /negP; intros LP; rename jhp into jlp.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jlp : Job Sched_jhp : scheduled_at sched jlp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jlp t'E : prt < t1 LP : ~~ hep_job jlp j
False
edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point
as [jhp [_ [HEP SCHEDjhp]]]; try apply PRPOINT; move => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jlp : Job Sched_jhp : scheduled_at sched jlp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jlp t'E : prt < t1 LP : ~~ hep_job jlp j
(t1 <= tp < t2) = true
* Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jlp : Job Sched_jhp : scheduled_at sched jlp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jlp t'E : prt < t1 LP : ~~ hep_job jlp j
(t1 <= tp < t2) = true
by 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jlp : Job Sched_jhp : scheduled_at sched jlp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jlp t'E : prt < t1 LP : ~~ hep_job jlp j jhp : Job HEP : hep_job jhp j SCHEDjhp : scheduled_at sched jhp tp
False
move : LP => /negP LP; apply : LP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jlp : Job Sched_jhp : scheduled_at sched jlp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jlp t'E : prt < t1 jhp : Job HEP : hep_job jhp j SCHEDjhp : scheduled_at sched jhp tp
hep_job jlp j
enough (EQ : jhp = jlp); first by subst .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jlp : Job Sched_jhp : scheduled_at sched jlp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jlp t'E : prt < t1 jhp : Job HEP : hep_job jhp j SCHEDjhp : scheduled_at sched jhp tp
jhp = jlp
apply : (H_uni jhp _ _ tp); eauto .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jlp : Job Sched_jhp : scheduled_at sched jlp t prt : nat LE : prt <= t PR : preemption_time arr_seq sched prt SCH : forall t' : nat,
prt <= t' <= t -> scheduled_at sched jlp t'E : prt < t1 jhp : Job HEP : hep_job jhp j SCHEDjhp : scheduled_at sched jhp tp
scheduled_at sched jlp tp
by apply SCH; apply /andP; split ; first apply leq_trans with t1; auto . } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t HP : hep_job jhp j
arrived_between jhp t1 t.+1 /\
hep_job jhp j /\ scheduled_at sched jhp t
repeat 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t HP : hep_job jhp j
arrived_between jhp t1 t.+1
move : (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET EXj]]]; move : (Sched_jhp) => PENDING.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t HP : hep_job jhp j SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tEXj : t1 <= job_arrival j < t2 PENDING : scheduled_at sched jhp t
arrived_between jhp t1 t.+1
eapply scheduled_implies_pending in PENDING => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t HP : hep_job jhp j SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tEXj : t1 <= job_arrival j < t2 PENDING : pending sched jhp t
arrived_between jhp t1 t.+1
apply /andP; split ; last by apply leq_ltn_trans with (n := t); first by move : PENDING => /andP [ARR _].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t HP : hep_job jhp j SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tEXj : t1 <= job_arrival j < t2 PENDING : pending sched jhp t
t1 <= job_arrival jhp
apply contraT; rewrite -ltnNge; intro LT; exfalso .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t HP : hep_job jhp j SL : t1 < t2 QUIET : quiet_time arr_seq sched j t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tEXj : t1 <= job_arrival j < t2 PENDING : pending sched jhp t LT : job_arrival jhp < t1
False
feed (QUIET jhp) => //. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t HP : hep_job jhp j SL : t1 < t2 QUIET : hep_job jhp j ->
arrived_before jhp t1 ->
completed_by sched jhp t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tEXj : t1 <= job_arrival j < t2 PENDING : pending sched jhp t LT : job_arrival jhp < t1
False
specialize (QUIET HP 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job Sched_jhp : scheduled_at sched jhp t HP : hep_job jhp j SL : t1 < t2 QUIET : completed_by sched jhp t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tEXj : t1 <= job_arrival j < t2 PENDING : pending sched jhp t LT : job_arrival jhp < t1
False
move : Sched_jhp; apply /negP/completed_implies_not_scheduled => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job HP : hep_job jhp j SL : t1 < t2 QUIET : completed_by sched jhp t1 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tEXj : t1 <= job_arrival j < t2 PENDING : pending sched jhp t LT : job_arrival jhp < t1
completed_by sched jhp t
apply : completion_monotonic QUIET.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 tp : instant t : nat PRPOINT : preemption_time arr_seq sched tp GEtp : t1 <= tp LTtp : tp < t2 LEtp : tp <= t LTt : t < t2 jhp : Job HP : hep_job jhp j SL : t1 < t2 NOTQUIET : forall t : nat,
t1 < t < t2 ->
~ quiet_time arr_seq sched j tEXj : t1 <= job_arrival j < t2 PENDING : pending sched jhp t LT : job_arrival jhp < t1
t1 <= t
exact : leq_trans LEtp.
Qed .
(** Now, suppose there exists some constant [K] that bounds the
distance to a preemption time from the beginning of the busy
interval. *)
Variable K : duration.
Hypothesis H_preemption_time_exists :
exists pr_t , preemption_time arr_seq sched pr_t /\ t1 <= pr_t <= t1 + K.
(** Then we prove that the processor is always busy with a job
with higher-or-equal priority after time instant [t1 + K]. *)
Lemma not_quiet_implies_exists_scheduled_hp_job :
forall t ,
t1 + K <= t < t2 ->
exists j_hp ,
arrived_between j_hp t1 t.+1 /\
hep_job j_hp j /\
scheduled_at sched j_hp 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 K : duration H_preemption_time_exists : exists pr_t : instant,
preemption_time arr_seq
sched pr_t /\
t1 <= pr_t <= t1 + K
forall t : nat,
t1 + K <= t < t2 ->
exists j_hp : Job,
arrived_between j_hp t1 t.+1 /\
hep_job j_hp j /\ scheduled_at sched j_hp 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 K : duration H_preemption_time_exists : exists pr_t : instant,
preemption_time arr_seq
sched pr_t /\
t1 <= pr_t <= t1 + K
forall t : nat,
t1 + K <= t < t2 ->
exists j_hp : Job,
arrived_between j_hp t1 t.+1 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
move => t /andP [GE 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 K : duration H_preemption_time_exists : exists pr_t : instant,
preemption_time arr_seq
sched pr_t /\
t1 <= pr_t <= t1 + Kt : nat GE : t1 + K <= t LT : t < t2
exists j_hp : Job,
arrived_between j_hp t1 t.+1 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
move : H_preemption_time_exists => [prt [PR /andP [GEprt LEprt]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 K : duration H_preemption_time_exists : exists pr_t : instant,
preemption_time arr_seq
sched pr_t /\
t1 <= pr_t <= t1 + Kt : nat GE : t1 + K <= t LT : t < t2 prt : instant PR : preemption_time arr_seq sched prt GEprt : t1 <= prt LEprt : prt <= t1 + K
exists j_hp : Job,
arrived_between j_hp t1 t.+1 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
apply not_quiet_implies_exists_scheduled_hp_job_after_preemption_point with (tp := prt); eauto 2 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 K : duration H_preemption_time_exists : exists pr_t : instant,
preemption_time arr_seq
sched pr_t /\
t1 <= pr_t <= t1 + Kt : nat GE : t1 + K <= t LT : t < t2 prt : instant PR : preemption_time arr_seq sched prt GEprt : t1 <= prt LEprt : prt <= t1 + K
t1 <= prt < 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 K : duration H_preemption_time_exists : exists pr_t : instant,
preemption_time arr_seq
sched pr_t /\
t1 <= pr_t <= t1 + Kt : nat GE : t1 + K <= t LT : t < t2 prt : instant PR : preemption_time arr_seq sched prt GEprt : t1 <= prt LEprt : prt <= t1 + K
t1 <= prt < 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 K : duration H_preemption_time_exists : exists pr_t : instant,
preemption_time arr_seq
sched pr_t /\
t1 <= pr_t <= t1 + Kt : nat GE : t1 + K <= t LT : t < t2 prt : instant PR : preemption_time arr_seq sched prt GEprt : t1 <= prt LEprt : prt <= t1 + K
prt < t2
apply leq_ltn_trans with (t1 + K) => [//|].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 K : duration H_preemption_time_exists : exists pr_t : instant,
preemption_time arr_seq
sched pr_t /\
t1 <= pr_t <= t1 + Kt : nat GE : t1 + K <= t LT : t < t2 prt : instant PR : preemption_time arr_seq sched prt GEprt : t1 <= prt LEprt : prt <= t1 + K
t1 + K < t2
by apply leq_ltn_trans with 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 K : duration H_preemption_time_exists : exists pr_t : instant,
preemption_time arr_seq
sched pr_t /\
t1 <= pr_t <= t1 + Kt : nat GE : t1 + K <= t LT : t < t2 prt : instant PR : preemption_time arr_seq sched prt GEprt : t1 <= prt LEprt : prt <= t1 + K
prt <= t < 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_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uni : uniprocessor_model PState sched : schedule PState JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP H_priority_is_transitive : transitive_job_priorities
JLFP H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched JobReady0 : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval_prefix : busy_interval_prefix arr_seq
sched j t1 t2 K : duration H_preemption_time_exists : exists pr_t : instant,
preemption_time arr_seq
sched pr_t /\
t1 <= pr_t <= t1 + Kt : nat GE : t1 + K <= t LT : t < t2 prt : instant PR : preemption_time arr_seq sched prt GEprt : t1 <= prt LEprt : prt <= t1 + K
prt <= t
by apply leq_trans with (t1 + K).
Qed .
End ProcessorBusyWithHEPJobAfterPreemptionPoints .