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.facts.model.workload.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.carry_in.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.busy_interval.busy_interval.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]
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import prosa.model.processor.ideal.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.ideal.service_of_jobs.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]
(** * Existence of No Carry-In Instant *)
(** In this section, we derive an alternative condition for the
existence of a busy interval. The new condition requires the total
workload (instead of the high-priority workload) generated by the
task set to be bounded. *)
(** Next, we derive a sufficient condition for existence of
no carry-in instant for uniprocessor for JLFP schedulers *)
Section ExistsNoCarryIn .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context {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.
(** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume a given JLFP policy. *)
Context `{JLFP_policy Job}.
(** For simplicity, let's define some local names. *)
Let job_pending_at := pending sched.
Let job_completed_by := completed_by sched.
Let arrivals_between := arrivals_between arr_seq.
Let no_carry_in := no_carry_in arr_seq sched.
Let quiet_time := quiet_time arr_seq sched.
(** 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.
(** Assume that the schedule is work-conserving, ... *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** ... and there are no duplicate job arrivals. *)
Hypothesis H_arrival_sequence_is_a_set :
arrival_sequence_uniq arr_seq.
(** The fact that there is no carry-in at time instant [t] trivially
implies that [t] is a quiet time. *)
Lemma no_carry_in_implies_quiet_time :
forall j t ,
no_carry_in t ->
quiet_time j t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq
forall (j : Job) (t : instant),
no_carry_in t -> quiet_time j t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq
forall (j : Job) (t : instant),
no_carry_in t -> quiet_time j t
by intros j t FQT j_hp ARR HP BEF; apply FQT.
Qed .
(** We show that an idle time implies no carry in at this time instant. *)
Lemma idle_instant_implies_no_carry_in_at_t :
forall t ,
is_idle sched t ->
no_carry_in t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq
forall t : instant, is_idle sched t -> no_carry_in t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq
forall t : instant, is_idle sched t -> no_carry_in t
intros ? IDLE j ARR HA.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t
completed_by sched j t
apply /negPn/negP; intros NCOMP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t
False
have PEND : job_pending_at j t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t
job_pending_at j t
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t
job_pending_at j t
apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t
has_arrived j t
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t
has_arrived j t
by rewrite /has_arrived ltnW.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t
~~ completed_by sched j t
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t
~~ completed_by sched j t
by move : NCOMP; apply contra, completion_monotonic.
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t PEND : job_pending_at j t
False
apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [READYhp _]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t
False
move : IDLE => /eqP IDLE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None
False
move : (H_work_conserving _ t ARRhp) => NIDLE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None NIDLE : backlogged sched jhp t ->
exists j_other : Job,
scheduled_at sched j_other t
False
feed NIDLE. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None NIDLE : backlogged sched jhp t ->
exists j_other : Job,
scheduled_at sched j_other t
backlogged sched jhp t
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None NIDLE : backlogged sched jhp t ->
exists j_other : Job,
scheduled_at sched j_other t
backlogged sched jhp t
apply /andP; split ; first by done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None NIDLE : backlogged sched jhp t ->
exists j_other : Job,
scheduled_at sched j_other t
~~ scheduled_at sched jhp t
by rewrite scheduled_at_def IDLE.
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None NIDLE : exists j_other : Job,
scheduled_at sched j_other t
False
move : NIDLE => [j' SCHED].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t NCOMP : ~~ completed_by sched j t jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None j' : Job SCHED : scheduled_at sched j' t
False
by rewrite scheduled_at_def IDLE in SCHED.
Qed .
(** Moreover, an idle time implies no carry in at the next time instant. *)
Lemma idle_instant_implies_no_carry_in_at_t_pl_1 :
forall t ,
is_idle sched t ->
no_carry_in t.+1 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq
forall t : instant,
is_idle sched t -> no_carry_in t.+1
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq
forall t : instant,
is_idle sched t -> no_carry_in t.+1
intros ? IDLE j ARR HA.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1
completed_by sched j t.+1
apply /negPn/negP; intros NCOMP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1
False
have PEND : job_pending_at j t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1
job_pending_at j t
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1
job_pending_at j t
apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1
has_arrived j t
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1
has_arrived j t
by rewrite /has_arrived.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1
~~ completed_by sched j t
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1
~~ completed_by sched j t
by move : NCOMP; apply contra, completion_monotonic.
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1 PEND : job_pending_at j t
False
apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [READYhp _]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant IDLE : is_idle sched t j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1 jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t
False
move : IDLE => /eqP IDLE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1 jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None
False
move : (H_work_conserving _ t ARRhp) => NIDLE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1 jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None NIDLE : backlogged sched jhp t ->
exists j_other : Job,
scheduled_at sched j_other t
False
feed NIDLE. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1 jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None NIDLE : backlogged sched jhp t ->
exists j_other : Job,
scheduled_at sched j_other t
backlogged sched jhp t
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1 jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None NIDLE : backlogged sched jhp t ->
exists j_other : Job,
scheduled_at sched j_other t
backlogged sched jhp t
apply /andP; split ; first by done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1 jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None NIDLE : backlogged sched jhp t ->
exists j_other : Job,
scheduled_at sched j_other t
~~ scheduled_at sched jhp t
by rewrite scheduled_at_def IDLE.
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1 jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None NIDLE : exists j_other : Job,
scheduled_at sched j_other t
False
move : NIDLE => [j' SCHED].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq t : instant j : Job ARR : arrives_in arr_seq j HA : arrived_before j t.+1 NCOMP : ~~ completed_by sched j t.+1 jhp : Job ARRhp : arrives_in arr_seq jhp READYhp : job_ready sched jhp t IDLE : sched t = None j' : Job SCHED : scheduled_at sched j' t
False
by rewrite scheduled_at_def IDLE in SCHED.
Qed .
(** Let the priority relation be reflexive. *)
Hypothesis H_priority_is_reflexive : reflexive_priorities.
(** Recall the notion of workload of all jobs released in a given interval <<[t1, t2)>>... *)
Let total_workload t1 t2 :=
workload_of_jobs predT (arrivals_between t1 t2).
(** ... and total service of jobs within some time interval <<[t1, t2)>>. *)
Let total_service t1 t2 :=
service_of_jobs sched predT (arrivals_between 0 t2) t1 t2.
(** Assume that for some positive [Δ], the sum of requested workload
at time [t + Δ] is bounded by [Δ] (i.e., the supply). Note that
this assumption bounds the total workload of jobs released in a
time interval <<[t, t + Δ)>> regardless of their priorities. *)
Variable Δ : duration.
Hypothesis H_delta_positive : Δ > 0 .
Hypothesis H_workload_is_bounded : forall t , total_workload t (t + Δ) <= Δ.
(** Next we prove that, since for any time instant [t] there is a
point where the total workload is upper-bounded by the supply,
the processor encounters no-carry-in instants at least every [Δ]
time units. *)
Section ProcessorIsNotTooBusy .
(** We start by proving that the processor has no carry-in at the
beginning (i.e., has no carry-in at time instant [0]). *)
Lemma no_carry_in_at_the_beginning :
no_carry_in 0 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δ
no_carry_in 0
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δ
no_carry_in 0
intros s ARR AB; exfalso .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δs : Job ARR : arrives_in arr_seq s AB : arrived_before s 0
False
by rewrite /arrived_before ltn0 in AB.
Qed .
(** In this section, we prove that for any time instant [t] there
exists another time instant <<t' ∈ (t, t + Δ]>> such that the
processor has no carry-in at time [t']. *)
Section ProcessorIsNotTooBusyInduction .
(** Consider an arbitrary time instant [t]... *)
Variable t : duration.
(** ...such that the processor has no carry-in at time [t]. *)
Hypothesis H_no_carry_in : no_carry_in t.
(** First, recall that the total service is bounded by the total workload. Therefore
the total service of jobs in the interval <<[t, t + Δ)>> is bounded by [Δ]. *)
Lemma total_service_is_bounded_by_Δ :
total_service t (t + Δ) <= Δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t
total_service t (t + Δ) <= Δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t
total_service t (t + Δ) <= Δ
unfold total_service.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t
service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t (t + Δ) <= Δ
rewrite -{3 }[Δ]addn0 -{2 }(subnn t) addnBA // [in X in _ <= X]addnC.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t
service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t (t + Δ) <= t + Δ - t
apply service_of_jobs_le_length_of_interval'; rt_auto.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t
uniq (arrivals_between 0 (t + Δ))
by eapply arrivals_uniq; eauto 2 .
Qed .
(** Next we consider two cases:
(1) The case when the total service is strictly less than [Δ], and
(2) the case when the total service is equal to [Δ]. *)
(** In the first case, we use the pigeonhole principle to
conclude that there is an idle time instant; which in turn
implies existence of a time instant with no carry-in. *)
Lemma low_total_service_implies_existence_of_time_with_no_carry_in :
total_service t (t + Δ) < Δ ->
exists δ , δ < Δ /\ no_carry_in (t.+1 + δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t
total_service t (t + Δ) < Δ ->
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t
total_service t (t + Δ) < Δ ->
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
unfold total_service; intros LT.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t LT : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) < Δ
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
rewrite -{3 }[Δ]addn0 -{2 }(subnn t) addnBA // [Δ + t]addnC in LT.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t LT : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) <
t + Δ - t
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
eapply low_service_implies_existence_of_idle_time in LT; eauto .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t LT : exists t0 : nat,
t <= t0 < t + Δ /\ is_idle sched t0
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
move : LT => [t_idle [/andP [LEt GTe] IDLE]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t t_idle : nat LEt : t <= t_idle GTe : t_idle < t + Δ IDLE : is_idle sched t_idle
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
move : LEt; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle sched t_idle EQ : t = t_idle
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle sched t_idle EQ : t = t_idle
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
exists 0 ; split ; first done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle sched t_idle EQ : t = t_idle
no_carry_in (t.+1 + 0 )
rewrite addn0; subst t_idle.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t IDLE : is_idle sched t GTe : t < t + Δ
no_carry_in t.+1
intros s ARR BEF.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t IDLE : is_idle sched t GTe : t < t + Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s t.+1
completed_by sched s t.+1
apply idle_instant_implies_no_carry_in_at_t_pl_1 in IDLE; try done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t IDLE : no_carry_in t.+1 GTe : t < t + Δ s : Job ARR : arrives_in arr_seq s BEF : arrived_before s t.+1
completed_by sched s t.+1
by apply IDLE.
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle sched t_idle LT : t < t_idle
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
have EX: exists γ , t_idle = t + γ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle sched t_idle LT : t < t_idle
exists γ : nat, t_idle = t + γ
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle sched t_idle LT : t < t_idle
exists γ : nat, t_idle = t + γ
by exists (t_idle - t); rewrite subnKC // ltnW. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t t_idle : nat GTe : t_idle < t + Δ IDLE : is_idle sched t_idle LT : t < t_idle EX : exists γ : nat, t_idle = t + γ
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
move : EX => [γ EQ]; subst t_idle; rewrite ltn_add2l in GTe.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t γ : nat LT : t < t + γ IDLE : is_idle sched (t + γ) GTe : γ < Δ
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
rewrite -{1 }[t]addn0 ltn_add2l in LT.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t γ : nat IDLE : is_idle sched (t + γ) GTe : γ < Δ LT : 0 < γ
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
exists (γ .-1 ); split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t γ : nat IDLE : is_idle sched (t + γ) GTe : γ < Δ LT : 0 < γ
γ.-1 < Δ
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t γ : nat IDLE : is_idle sched (t + γ) GTe : γ < Δ LT : 0 < γ
γ.-1 < Δ
apply leq_trans with γ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t γ : nat IDLE : is_idle sched (t + γ) GTe : γ < Δ LT : 0 < γ
γ.-1 < γ
by rewrite prednK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t γ : nat IDLE : is_idle sched (t + γ) GTe : γ < Δ LT : 0 < γ
γ <= Δ
by rewrite ltnW.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t γ : nat IDLE : is_idle sched (t + γ) GTe : γ < Δ LT : 0 < γ
no_carry_in (t.+1 + γ.-1 )
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t γ : nat IDLE : is_idle sched (t + γ) GTe : γ < Δ LT : 0 < γ
no_carry_in (t.+1 + γ.-1 )
rewrite -subn1 -addn1 -addnA subnKC //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t γ : nat IDLE : is_idle sched (t + γ) GTe : γ < Δ LT : 0 < γ
no_carry_in (t + γ)
intros s ARR BEF.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t γ : nat IDLE : is_idle sched (t + γ) GTe : γ < Δ LT : 0 < γs : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + γ)
completed_by sched s (t + γ)
by apply idle_instant_implies_no_carry_in_at_t.
Qed .
(** In the second case, the total service within the time
interval <<[t, t + Δ)>> is equal to [Δ]. On the other hand,
we know that the total workload is lower-bounded by the
total service and upper-bounded by [Δ]. Therefore, the total
workload is equal to the total service, which implies
completion of all jobs by time [t + Δ] and hence no carry-in
at time [t + Δ]. *)
Lemma completion_of_all_jobs_implies_no_carry_in :
total_service t (t + Δ) = Δ ->
no_carry_in (t + Δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t
total_service t (t + Δ) = Δ -> no_carry_in (t + Δ)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t
total_service t (t + Δ) = Δ -> no_carry_in (t + Δ)
unfold total_service; intros EQserv.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ
no_carry_in (t + Δ)
move : (H_workload_is_bounded t); move => WORK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ
no_carry_in (t + Δ)
have EQ: total_workload 0 (t + Δ) = service_of_jobs sched predT (arrivals_between 0 (t + Δ)) 0 (t + Δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ
total_workload 0 (t + Δ) =
service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) 0 (t + Δ)
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ
total_workload 0 (t + Δ) =
service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) 0 (t + Δ)
intros .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ
total_workload 0 (t + Δ) =
service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) 0 (t + Δ)
have COMPL := all_jobs_have_completed_impl_workload_eq_service
_ arr_seq H_arrival_times_are_consistent sched
H_jobs_must_arrive_to_execute
H_completed_jobs_dont_execute
predT 0 t t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : unit_service_proc_model (processor_state Job) ->
(forall j : Job,
j
\in arrival_sequence.arrivals_between
arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
total_workload 0 (t + Δ) =
service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) 0 (t + Δ)
feed_n 2 COMPL; rt_auto. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : (forall j : Job,
j
\in arrival_sequence.arrivals_between
arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
forall j : Job,
j \in arrival_sequence.arrivals_between arr_seq 0 t ->
predT j -> completed_by sched j t
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : (forall j : Job,
j
\in arrival_sequence.arrivals_between
arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
forall j : Job,
j \in arrival_sequence.arrivals_between arr_seq 0 t ->
predT j -> completed_by sched j t
intros j A B; apply H_no_carry_in.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : (forall j : Job,
j
\in arrival_sequence.arrivals_between
arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t j : Job A : j
\in arrival_sequence.arrivals_between arr_seq 0
t B : predT j
arrives_in arr_seq j
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : (forall j : Job,
j
\in arrival_sequence.arrivals_between
arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t j : Job A : j
\in arrival_sequence.arrivals_between arr_seq 0
t B : predT j
arrives_in arr_seq j
eapply in_arrivals_implies_arrived; eauto 2 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : (forall j : Job,
j
\in arrival_sequence.arrivals_between
arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t j : Job A : j
\in arrival_sequence.arrivals_between arr_seq 0
t B : predT j
arrived_before j t
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : (forall j : Job,
j
\in arrival_sequence.arrivals_between
arr_seq 0 t ->
predT j -> completed_by sched j t) ->
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t j : Job A : j
\in arrival_sequence.arrivals_between arr_seq 0
t B : predT j
arrived_before j t
eapply in_arrivals_implies_arrived_between in A; eauto 2 .
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
total_workload 0 (t + Δ) =
service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) 0 (t + Δ)
apply /eqP; rewrite eqn_leq; apply /andP; split ;
last by apply service_of_jobs_le_workload;
auto using ideal_proc_model_provides_unit_service.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
total_workload 0 (t + Δ) <=
service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) 0 (t + Δ)
rewrite /total_workload (workload_of_jobs_cat arr_seq t); last first .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
0 <= t <= t + Δ
apply /andP; split ; [by done | by rewrite leq_addr].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0 t) +
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq t (t + Δ)) <=
service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) 0 (t + Δ)
rewrite (service_of_jobs_cat_scheduling_interval _ _ _ _ _ _ _ t); try done ; first last .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
0 <= t <= t + Δ
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
0 <= t <= t + Δ
by apply /andP; split ; [by done | by rewrite leq_addr]. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0 t) +
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq t (t + Δ)) <=
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0 t) 0 t +
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0 t) t
(t + Δ) +
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq t (t + Δ))
t (t + Δ)
rewrite COMPL -addnA leq_add2l.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq t (t + Δ)) <=
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0 t) t
(t + Δ) +
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq t (t + Δ))
t (t + Δ)
rewrite -service_of_jobs_cat_arrival_interval; last first .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
0 <= t <= t + Δ
apply /andP; split ; [by done | by rewrite leq_addr].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq t (t + Δ)) <=
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0 (t + Δ))
t (t + Δ)
rewrite EQserv.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ COMPL : workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq 0
t) =
service_of_jobs sched predT
(arrival_sequence.arrivals_between arr_seq 0
t) 0 t
workload_of_jobs predT
(arrival_sequence.arrivals_between arr_seq t (t + Δ)) <=
Δ
by apply H_workload_is_bounded.
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ EQ : total_workload 0 (t + Δ) =
service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) 0
(t + Δ)
no_carry_in (t + Δ)
intros s ARR BEF.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : duration H_no_carry_in : no_carry_in t EQserv : service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) t
(t + Δ) = Δ WORK : total_workload t (t + Δ) <= Δ EQ : total_workload 0 (t + Δ) =
service_of_jobs sched predT
(arrivals_between 0 (t + Δ)) 0
(t + Δ) s : Job ARR : arrives_in arr_seq s BEF : arrived_before s (t + Δ)
completed_by sched s (t + Δ)
by eapply workload_eq_service_impl_all_jobs_have_completed; rt_eauto.
Qed .
End ProcessorIsNotTooBusyInduction .
(** Finally, we show that any interval of length [Δ] contains a time instant with no carry-in. *)
Lemma processor_is_not_too_busy :
forall t , exists δ , δ < Δ /\ no_carry_in (t + δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δ
forall t : nat,
exists δ : nat, δ < Δ /\ no_carry_in (t + δ)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δ
forall t : nat,
exists δ : nat, δ < Δ /\ no_carry_in (t + δ)
induction t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δ
exists δ : nat, δ < Δ /\ no_carry_in (0 + δ)
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δ
exists δ : nat, δ < Δ /\ no_carry_in (0 + δ)
by exists 0 ; split ; [ | rewrite addn0; apply no_carry_in_at_the_beginning]. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : nat IHt : exists δ : nat, δ < Δ /\ no_carry_in (t + δ)
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : nat IHt : exists δ : nat, δ < Δ /\ no_carry_in (t + δ)
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
move : IHt => [δ [LE FQT]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt, δ : nat LE : δ < Δ FQT : no_carry_in (t + δ)
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
move : (posnP δ) => [Z|POS]; last first .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt, δ : nat LE : δ < Δ FQT : no_carry_in (t + δ) POS : 0 < δ
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt, δ : nat LE : δ < Δ FQT : no_carry_in (t + δ) POS : 0 < δ
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
exists (δ .-1 ); split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt, δ : nat LE : δ < Δ FQT : no_carry_in (t + δ) POS : 0 < δ
δ.-1 < Δ
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt, δ : nat LE : δ < Δ FQT : no_carry_in (t + δ) POS : 0 < δ
δ.-1 < Δ
by apply leq_trans with δ; [rewrite prednK | apply ltnW].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt, δ : nat LE : δ < Δ FQT : no_carry_in (t + δ) POS : 0 < δ
no_carry_in (t.+1 + δ.-1 )
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt, δ : nat LE : δ < Δ FQT : no_carry_in (t + δ) POS : 0 < δ
no_carry_in (t.+1 + δ.-1 )
by rewrite -subn1 -addn1 -addnA subnKC //.
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt, δ : nat LE : δ < Δ FQT : no_carry_in (t + δ) Z : δ = 0
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
subst δ; rewrite addn0 in FQT; clear LE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : nat FQT : no_carry_in t
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
move : (total_service_is_bounded_by_Δ t); rewrite leq_eqVlt; move => /orP [/eqP EQ | LT].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : nat FQT : no_carry_in t EQ : total_service t (t + Δ) = Δ
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : nat FQT : no_carry_in t EQ : total_service t (t + Δ) = Δ
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
exists (Δ .-1 ); split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : nat FQT : no_carry_in t EQ : total_service t (t + Δ) = Δ
Δ.-1 < Δ
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : nat FQT : no_carry_in t EQ : total_service t (t + Δ) = Δ
Δ.-1 < Δ
by rewrite prednK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : nat FQT : no_carry_in t EQ : total_service t (t + Δ) = Δ
no_carry_in (t.+1 + Δ.-1 )
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : nat FQT : no_carry_in t EQ : total_service t (t + Δ) = Δ
no_carry_in (t.+1 + Δ.-1 )
by rewrite addSn -subn1 -addn1 -addnA subnK; first apply completion_of_all_jobs_implies_no_carry_in.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : nat FQT : no_carry_in t LT : total_service t (t + Δ) < Δ
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δt : nat FQT : no_carry_in t LT : total_service t (t + Δ) < Δ
exists δ : nat, δ < Δ /\ no_carry_in (t.+1 + δ)
by apply low_total_service_implies_existence_of_time_with_no_carry_in.
}
Qed .
End ProcessorIsNotTooBusy .
(** Consider an arbitrary job [j] with positive cost. *)
Variable j : Job.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** We show that there must exist a busy interval <<[t1, t2)>> that
contains the arrival time of [j]. *)
Corollary exists_busy_interval_from_total_workload_bound :
exists t1 t2 ,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\
busy_interval arr_seq sched j t1 t2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j
exists t1 t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j
exists t1 t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
rename H_from_arrival_sequence into ARR, H_job_cost_positive into POS.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j
exists t1 t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
edestruct (exists_busy_interval_prefix
arr_seq H_arrival_times_are_consistent
sched j ARR H_priority_is_reflexive (job_arrival j))
as [t1 [PREFIX GE]]; first by apply job_pending_at_arrival; auto .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE : t1 <= job_arrival j <= job_arrival j
exists t1 t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
move : GE => /andP [GE1 _].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j
exists t1 t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
exists t1 ; move : (processor_is_not_too_busy t1.+1 ) => [δ [LE QT]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : no_carry_in (t1.+1 + δ)
exists t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
apply no_carry_in_implies_quiet_time with (j := j) in QT.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ)
exists t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
have EX: exists t2 , ((t1 < t2 <= t1.+1 + δ) && quiet_time_dec arr_seq sched j t2).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ)
exists t2 : nat,
(t1 < t2 <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j t2
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ)
exists t2 : nat,
(t1 < t2 <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j t2
exists (t1 .+1 + δ); apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ)
t1 < t1.+1 + δ <= t1.+1 + δ
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ)
t1 < t1.+1 + δ <= t1.+1 + δ
by apply /andP; split ; first rewrite addSn ltnS leq_addr.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ)
quiet_time_dec arr_seq sched j (t1.+1 + δ)
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ)
quiet_time_dec arr_seq sched j (t1.+1 + δ)
by apply /quiet_time_P. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) EX : exists t2 : nat,
(t1 < t2 <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j t2
exists t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
move : (ex_minnP EX) => [t2 /andP [/andP [GTt2 LEt2] QUIET] MIN]; clear EX.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= n
exists t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
have NEQ: t1 <= job_arrival j < t2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= n
t1 <= job_arrival j < t2
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= n
t1 <= job_arrival j < t2
apply /andP; split ; first by done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= n
job_arrival j < t2
rewrite ltnNge; apply /negP; intros CONTR.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nCONTR : t2 <= job_arrival j
False
move : (PREFIX) => [_ [_ [NQT _]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nCONTR : t2 <= job_arrival j NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j t
False
move : (NQT t2); clear NQT; move => NQT.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nCONTR : t2 <= job_arrival j NQT : t1 < t2 < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j t2
False
feed NQT; first by (apply /andP; split ; [|rewrite ltnS]). Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nCONTR : t2 <= job_arrival j NQT : ~ busy_interval.quiet_time arr_seq sched j t2
False
by apply : NQT; apply /quiet_time_P.
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2
exists t2 : nat,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\ busy_interval arr_seq sched j t1 t2
exists t2 ; split ; last split ; first by done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2
t2 <= t1 + Δ
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2
t2 <= t1 + Δ
apply leq_trans with (t1.+1 + δ); [by done | by rewrite addSn ltn_add2l]. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2
busy_interval arr_seq sched j t1 t2
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant PREFIX : busy_interval_prefix arr_seq sched j t1
(job_arrival j).+1 GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2
busy_interval arr_seq sched j t1 t2
move : PREFIX => [_ [QTt1 [NQT _]]]; repeat split ; try done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : busy_interval.quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j t
forall t : nat,
t1 < t < t2 ->
~ busy_interval.quiet_time arr_seq sched j t
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : busy_interval.quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j t
forall t : nat,
t1 < t < t2 ->
~ busy_interval.quiet_time arr_seq sched j t
move => t /andP [GEt LTt] QTt.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : busy_interval.quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j tt : nat GEt : t1 < t LTt : t < t2 QTt : busy_interval.quiet_time arr_seq sched j t
False
feed (MIN t). Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : busy_interval.quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j tt : nat GEt : t1 < t LTt : t < t2 QTt : busy_interval.quiet_time arr_seq sched j t
(t1 < t <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j t
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : busy_interval.quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j tt : nat GEt : t1 < t LTt : t < t2 QTt : busy_interval.quiet_time arr_seq sched j t
(t1 < t <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j t
apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : busy_interval.quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j tt : nat GEt : t1 < t LTt : t < t2 QTt : busy_interval.quiet_time arr_seq sched j t
t1 < t <= t1.+1 + δ
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : busy_interval.quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j tt : nat GEt : t1 < t LTt : t < t2 QTt : busy_interval.quiet_time arr_seq sched j t
t1 < t <= t1.+1 + δ
by apply /andP; split ; last (apply leq_trans with t2; [apply ltnW | ]).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : busy_interval.quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j tt : nat GEt : t1 < t LTt : t < t2 QTt : busy_interval.quiet_time arr_seq sched j t
quiet_time_dec arr_seq sched j t
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : busy_interval.quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j tt : nat GEt : t1 < t LTt : t < t2 QTt : busy_interval.quiet_time arr_seq sched j t
quiet_time_dec arr_seq sched j t
by apply /quiet_time_P.
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 t : nat MIN : t2 <= t NEQ : t1 <= job_arrival j < t2 QTt1 : busy_interval.quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j tGEt : t1 < t LTt : t < t2 QTt : busy_interval.quiet_time arr_seq sched j t
False
by move : LTt; rewrite ltnNge; move => /negP LTt; apply : LTt.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : busy_interval.quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j t
busy_interval.quiet_time arr_seq sched j t2
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task 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) H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H1 : JLFP_policy Job job_pending_at := pending sched : Job -> instant -> bool job_completed_by := completed_by sched : Job -> instant -> bool arrivals_between := arrival_sequence.arrivals_between
arr_seq : instant -> instant -> seq Job no_carry_in := carry_in.no_carry_in arr_seq sched : instant -> Prop quiet_time := busy_interval.quiet_time arr_seq sched : Job -> instant -> Prop H2 : JobReady Job (processor_state Job) H_job_ready : work_bearing_readiness arr_seq sched H_work_conserving : work_conserving arr_seq sched H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq H_priority_is_reflexive : reflexive_priorities total_workload := fun t1 t2 : instant =>
workload_of_jobs predT
(arrivals_between t1 t2): instant -> instant -> nat total_service := fun t1 t2 : instant =>
service_of_jobs sched predT
(arrivals_between 0 t2) t1 t2: instant -> instant -> nat Δ : duration H_delta_positive : 0 < ΔH_workload_is_bounded : forall t : instant,
total_workload t (t + Δ) <= Δj : Job ARR : arrives_in arr_seq j POS : job_cost_positive j t1 : instant GE1 : t1 <= job_arrival j δ : nat LE : δ < Δ QT : quiet_time j (t1.+1 + δ) t2 : nat GTt2 : t1 < t2 LEt2 : t2 <= t1.+1 + δ QUIET : quiet_time_dec arr_seq sched j t2 MIN : forall n : nat,
(t1 < n <= t1.+1 + δ) &&
quiet_time_dec arr_seq sched j n ->
t2 <= nNEQ : t1 <= job_arrival j < t2 QTt1 : busy_interval.quiet_time arr_seq sched j t1 NQT : forall t : nat,
t1 < t < (job_arrival j).+1 ->
~ busy_interval.quiet_time arr_seq sched j t
busy_interval.quiet_time arr_seq sched j t2
by apply /quiet_time_P.
}
Qed .
End ExistsNoCarryIn .