Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.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.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" 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.definitions.work_bearing_readiness.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.model.preemption.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** 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. *)
Variable arr_seq : arrival_sequence Job.
(** 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_priorities.
(** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
Variable sched : schedule (ideal.processor_state Job).
(** ... 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.
(** ... 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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]]]; try eauto 2 .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t
~~ completed_by sched j1 pt
- Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t PEND1 : pending sched j1 pt
False
apply H_job_ready in PEND1 => //; destruct PEND1 as [j3 [ARR3 [READY3 HEP3]]].Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t 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 JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t 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
eapply H_priority_is_transitive; last by apply HEP3.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t 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 j3
eapply H_respects_policy; eauto 2 .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t 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 ; first by done .Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t 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; intros SCHED2.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t 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 := ideal_proc_model_is_a_uniprocessor_model _ _ _ pt SCHED2 ALL_SCHED.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 sched pt ALL_SCHED : scheduled_at sched j2 pt LE1 : job_arrival j2 <= pt LE2 : pt <= t 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 : j3 = j2
False
subst j2; rename j3 into j.Job : JobType Arrival : JobArrival Job Cost : JobCost Job arr_seq : arrival_sequence Job JLFP : JLFP_policy Job H_priority_is_transitive : transitive_priorities sched : schedule (ideal.processor_state Job) H : JobReady Job (ideal.processor_state Job) 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 : Job ARR : arrives_in arr_seq j1 j : Job AHP : always_higher_priority j1 j LE : job_arrival j1 < job_arrival j t : instant SCHED : scheduled_at sched j t NCOMPL : ~~ completed_by sched j1 t pt : nat PT : preemption_time sched pt LE1 : job_arrival j <= pt ALL_SCHED : scheduled_at sched j pt LE2 : pt <= t ARR3 : arrives_in arr_seq j READY3 : job_ready sched j pt HEP3 : hep_job j j1 NHEP : ~ hep_job_at pt j j1 HEP : hep_job_at pt j1 j SCHED2 : scheduled_at sched j pt
False
by specialize (AHP 0 ); destruct AHP; auto .
Qed .
End SequentialJLFP .