Built with
Alectryon , running Coq+SerAPI v8.17.0+0.17.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.Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.analysis.facts.busy_interval.ideal.busy_interval.Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.util.tactics.
(** * 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_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** ... and any ideal uniprocessor schedule of this arrival sequence. *)
Variable sched : schedule (ideal.processor_state Job).
(** 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 (ideal.processor_state Job) 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.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence 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 :
~ ideal_is_idle sched t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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
~ ideal_is_idle sched t
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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
~ ideal_is_idle sched t
by move => IDLE; exfalso ; 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 : (ideal_proc_model_is_a_uniprocessor_model jlp j' sched t Sched_jlp SCHED') => EQ.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 : (ideal_proc_model_is_a_uniprocessor_model _ _ sched _ SCHED Sched_jlp) => EQ.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 : (ideal_proc_model_is_a_uniprocessor_model jlp j' sched t Sched_jlp SCHED') => EQ.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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, H_jobs_come_from_arrival_sequence into CONS.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq CONS : jobs_come_from_arrival_sequence 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq CONS : jobs_come_from_arrival_sequence 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq CONS : jobs_come_from_arrival_sequence 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq CONS : jobs_come_from_arrival_sequence 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq CONS : jobs_come_from_arrival_sequence 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq CONS : jobs_come_from_arrival_sequence 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq CONS : jobs_come_from_arrival_sequence 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq CONS : jobs_come_from_arrival_sequence 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); first by eapply CONS, Sched_jhp. Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq CONS : jobs_come_from_arrival_sequence 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq CONS : jobs_come_from_arrival_sequence 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq CONS : jobs_come_from_arrival_sequence 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq CONS : jobs_come_from_arrival_sequence 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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
ideal_proc_model_sched_case_analysis sched t jhp. Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 : ideal_is_idle 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 : ideal_is_idle 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 jhp : Job Sched_jhp : scheduled_at sched jhp t
exists j_hp : Job,
arrived_between j_hp t1 t2 /\
hep_job j_hp j /\ scheduled_at sched j_hp t
exists jhp .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 jhp : Job Sched_jhp : scheduled_at sched jhp t
arrived_between jhp t1 t2 /\
hep_job jhp j /\ scheduled_at sched jhp t
repeat split .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 jhp : Job Sched_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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 jhp : Job Sched_jhp : scheduled_at sched jhp t
arrived_between jhp 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_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 jhp : Job Sched_jhp : scheduled_at sched jhp t
hep_job jhp j
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 jhp : Job Sched_jhp : scheduled_at sched jhp t
hep_job jhp j
exact : scheduled_at_preemption_time_implies_higher_or_equal_priority.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 jhp : Job Sched_jhp : scheduled_at sched jhp t
scheduled_at sched jhp t
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq sched : schedule (processor_state Job) 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 (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
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 jhp : Job Sched_jhp : scheduled_at sched jhp t
scheduled_at sched jhp t
by [].
Qed .
End ProcessorBusyWithHEPJobAtPreemptionPoints .