Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.definitions.always_higher_priority.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.definitions.work_bearing_readiness.
Require Export prosa.analysis.facts.model.preemption.
(** In this section, we prove that, given two jobs [j1] and [j2], if
job [j1] arrives earlier than job [j2] and [j1] always has higher
priority than [j2], then [j2] is scheduled only after [j1] is
completed. *)
Section SequentialJLFP .
(** Consider any type of jobs. *)
Context {Job : JobType}.
Context `{Arrival : JobArrival Job}.
Context `{Cost : JobCost Job}.
(** Consider any arrival sequence with consistent arrival times. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
(** Consider a JLFP-policy that indicates a higher-or-equal priority
relation, and assume that this relation is transitive. *)
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.
(** Allow for any uniprocessor model. *)
Context {PState : ProcessorState Job}.
Hypothesis H_uniproc : uniprocessor_model PState.
(** Next, consider any schedule of the arrival sequence, ... *)
Variable sched : schedule PState.
(** ... allow for any work-bearing notion of job readiness, ... *)
Context `{@JobReady Job PState Cost Arrival}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** ... and assume that the schedule is valid. *)
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
(** In addition, we assume the existence of a function mapping jobs
to their preemption points ... *)
Context `{JobPreemptable Job}.
(** ... and assume that it defines a valid preemption model. *)
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
(** Next, we assume that the schedule respects the scheduling policy at every preemption point.... *)
Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
(** ... and that jobs must arrive to execute. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
(** We show that, given two jobs [j1] and [j2], if job [j1] arrives
earlier than job [j2] and [j1] always has higher priority than
[j2], then [j2] is scheduled only after [j1] is completed. *)
Lemma early_hep_job_is_scheduled :
forall j1 j2 ,
arrives_in arr_seq j1 ->
job_arrival j1 < job_arrival j2 ->
always_higher_priority j1 j2 ->
forall t ,
scheduled_at sched j2 t ->
completed_by sched j1 t.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched
forall j1 j2 : Job,
arrives_in arr_seq j1 ->
job_arrival j1 < job_arrival j2 ->
always_higher_priority j1 j2 ->
forall t : instant,
scheduled_at sched j2 t -> completed_by sched j1 t
Proof .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched
forall j1 j2 : Job,
arrives_in arr_seq j1 ->
job_arrival j1 < job_arrival j2 ->
always_higher_priority j1 j2 ->
forall t : instant,
scheduled_at sched j2 t -> completed_by sched j1 t
move => j1 j2 ARR LE AHP t SCHED.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t
completed_by sched j1 t
apply /negPn/negP; intros NCOMPL.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t
False
edestruct scheduling_of_any_segment_starts_with_preemption_time
as [pt [LET [PT ALL_SCHED]]] => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat LET : job_arrival j2 <= pt <= t PT : preemption_time arr_seq sched pt ALL_SCHED : forall t' : nat,
pt <= t' <= t -> scheduled_at sched j2 t'
False
move : LET => /andP [LE1 LE2].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : forall t' : nat,
pt <= t' <= t -> scheduled_at sched j2 t'LE1 : job_arrival j2 <= pt LE2 : pt <= t
False
specialize (ALL_SCHED pt); feed ALL_SCHED; first by apply /andP; split .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t
False
have PEND1: pending sched j1 pt.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t
pending sched j1 pt
{ Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t
pending sched j1 pt
apply /andP; split .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t
has_arrived j1 pt
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t
has_arrived j1 pt
by rewrite /has_arrived; lia .
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t
~~ completed_by sched j1 pt
by move : NCOMPL; apply contra, completion_monotonic. } Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t PEND1 : pending sched j1 pt
False
have [j3 [ARR3 [READY3 HEP3]]] := (H_job_ready _ _ ARR PEND1).Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t PEND1 : pending sched j1 pt j3 : Job ARR3 : arrives_in arr_seq j3 READY3 : job_ready sched j3 pt HEP3 : hep_job j3 j1
False
move : (AHP pt) => /andP[HEP /negP NHEP]; eapply NHEP.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t PEND1 : pending sched j1 pt j3 : Job ARR3 : arrives_in arr_seq j3 READY3 : job_ready sched j3 pt HEP3 : hep_job j3 j1 HEP : hep_job_at pt j1 j2 NHEP : ~ hep_job_at pt j2 j1
hep_job_at pt j2 j1
apply : H_priority_is_transitive; last exact : HEP3.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t PEND1 : pending sched j1 pt j3 : Job ARR3 : arrives_in arr_seq j3 READY3 : job_ready sched j3 pt HEP3 : hep_job j3 j1 HEP : hep_job_at pt j1 j2 NHEP : ~ hep_job_at pt j2 j1
hep_job j2 j3
apply : H_respects_policy => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t PEND1 : pending sched j1 pt j3 : Job ARR3 : arrives_in arr_seq j3 READY3 : job_ready sched j3 pt HEP3 : hep_job j3 j1 HEP : hep_job_at pt j1 j2 NHEP : ~ hep_job_at pt j2 j1
backlogged sched j3 pt
apply /andP; split => //.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t PEND1 : pending sched j1 pt j3 : Job ARR3 : arrives_in arr_seq j3 READY3 : job_ready sched j3 pt HEP3 : hep_job j3 j1 HEP : hep_job_at pt j1 j2 NHEP : ~ hep_job_at pt j2 j1
~~ scheduled_at sched j3 pt
apply /negP => SCHED2.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t PEND1 : pending sched j1 pt j3 : Job ARR3 : arrives_in arr_seq j3 READY3 : job_ready sched j3 pt HEP3 : hep_job j3 j1 HEP : hep_job_at pt j1 j2 NHEP : ~ hep_job_at pt j2 j1 SCHED2 : scheduled_at sched j3 pt
False
have EQ: j2 = j3 by apply : H_uniproc; eauto .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq JLFP : JLFP_policy Job H_priority_is_transitive : transitive_job_priorities
JLFP PState : ProcessorState Job H_uniproc : uniprocessor_model PState sched : schedule PState H : JobReady Job PState H_job_ready : work_bearing_readiness arr_seq sched H_sched_valid : valid_schedule sched arr_seq H0 : JobPreemptable Job H_valid_preemption_model : valid_preemption_model
arr_seq sched H_respects_policy : respects_JLFP_policy_at_preemption_point
arr_seq sched JLFP H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j1, j2 : Job ARR : arrives_in arr_seq j1 LE : job_arrival j1 < job_arrival j2 AHP : always_higher_priority j1 j2 t : instant SCHED : scheduled_at sched j2 t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time arr_seq sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t PEND1 : pending sched j1 pt j3 : Job ARR3 : arrives_in arr_seq j3 READY3 : job_ready sched j3 pt HEP3 : hep_job j3 j1 HEP : hep_job_at pt j1 j2 NHEP : ~ hep_job_at pt j2 j1 SCHED2 : scheduled_at sched j3 pt EQ : j2 = j3
False
by subst j2.
Qed .
End SequentialJLFP .