Built with
Alectryon , running Coq+SerAPI v8.14.0+0.14.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.model.aggregate.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.model.aggregate.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]
Require Export prosa.analysis.facts.behavior.completion.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_schedule.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 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]
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.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]
(** * Lemmas about Service Received by Sets of Jobs *)
(** In this file, we establish basic facts about the service received by _sets_ of jobs. *)
(** To begin with, we provide some basic properties of service
of a set of jobs in case of a generic scheduling model. *)
Section GenericModelLemmas .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor state model, ... *)
Context {PState : Type }.
Context `{ProcessorState Job PState}.
(** ... any job arrival sequence with consistent arrivals, .... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** ... and any schedule of this arrival sequence ... *)
Variable sched : schedule PState.
(** ... 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.
(** Let P be any predicate over jobs. *)
Variable P : pred Job.
(** We show that the total service of jobs released in a time interval <<[t1,t2)>>
during <<[t1,t2)>> is equal to the sum of:
(1) the total service of jobs released in time interval <<[t1, t)>> during time <<[t1, t)>>
(2) the total service of jobs released in time interval <<[t1, t)>> during time <<[t, t2)>>
and (3) the total service of jobs released in time interval <<[t, t2)>> during time <<[t, t2)>>. *)
Lemma service_of_jobs_cat_scheduling_interval :
forall t1 t2 t ,
t1 <= t <= t2 ->
service_of_jobs sched P (arrivals_between arr_seq t1 t2) t1 t2
= service_of_jobs sched P (arrivals_between arr_seq t1 t) t1 t
+ service_of_jobs sched P (arrivals_between arr_seq t1 t) t t2
+ service_of_jobs sched P (arrivals_between arr_seq t t2) t t2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job
forall t1 t2 t : nat,
t1 <= t <= t2 ->
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t2 =
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t1 t +
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t t2 +
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job
forall t1 t2 t : nat,
t1 <= t <= t2 ->
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t2 =
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t1 t +
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t t2 +
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2
move => t1 t2 t /andP [GEt LEt].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t2 =
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t1 t +
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t t2 +
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2
rewrite (arrivals_between_cat _ _ t) //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2
service_of_jobs sched P
(arrivals_between arr_seq t1 t ++
arrivals_between arr_seq t t2) t1 t2 =
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t1 t +
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t t2 +
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2
rewrite {1 }/service_of_jobs big_cat //=.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2
\sum_(i <- arrivals_between arr_seq t1 t | P i)
service_during sched i t1 t2 +
\sum_(i <- arrivals_between arr_seq t t2 | P i)
service_during sched i t1 t2 =
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t1 t +
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t t2 +
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2
rewrite exchange_big //= (@big_cat_nat _ _ _ t) //=;
rewrite [in X in X + _ + _]exchange_big //= [in X in _ + X + _]exchange_big //=.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2
\sum_(j <- arrivals_between arr_seq t1 t | P j)
\sum_(t1 <= i < t) service_at sched j i +
\sum_(j <- arrivals_between arr_seq t1 t | P j)
\sum_(t <= i < t2) service_at sched j i +
\sum_(i <- arrivals_between arr_seq t t2 | P i)
service_during sched i t1 t2 =
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t1 t +
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t t2 +
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2
apply /eqP; rewrite -!addnA eqn_add2l eqn_add2l.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2
\sum_(i <- arrivals_between arr_seq t t2 | P i)
service_during sched i t1 t2 ==
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2
rewrite exchange_big //= (@big_cat_nat _ _ _ t) //= [in X in _ + X]exchange_big //=.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2
\sum_(t1 <= i < t)
\sum_(i0 <- arrivals_between arr_seq t t2 | P i0)
service_at sched i0 i +
\sum_(j <- arrivals_between arr_seq t t2 | P j)
\sum_(t <= i < t2) service_at sched j i ==
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2
rewrite -[service_of_jobs _ _ _ _ _]add0n /service_of_jobs eqn_add2r.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2
\sum_(t1 <= i < t)
\sum_(i0 <- arrivals_between arr_seq t t2 | P i0)
service_at sched i0 i == 0
rewrite big_nat_cond big1 //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2
forall i : nat,
(t1 <= i < t) && true ->
\sum_(i0 <- arrivals_between arr_seq t t2 | P i0)
service_at sched i0 i = 0
move => x /andP [/andP [GEi LTi] _].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2 x : nat GEi : t1 <= x LTi : x < t
\sum_(i <- arrivals_between arr_seq t t2 | P i)
service_at sched i x = 0
rewrite big_seq_cond big1 //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2 x : nat GEi : t1 <= x LTi : x < t
forall i : Job,
(i \in arrivals_between arr_seq t t2) && P i ->
service_at sched i x = 0
move => j /andP [ARR Ps].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2 x : nat GEi : t1 <= x LTi : x < t j : Job ARR : j \in arrivals_between arr_seq t t2 Ps : P j
service_at sched j x = 0
apply service_before_job_arrival_zero with H0; auto .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2 x : nat GEi : t1 <= x LTi : x < t j : Job ARR : j \in arrivals_between arr_seq t t2 Ps : P j
x < job_arrival j
eapply in_arrivals_implies_arrived_between in ARR; eauto 2 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2 x : nat GEi : t1 <= x LTi : x < t j : Job ARR : arrived_between j t t2 Ps : P j
x < job_arrival j
by move : ARR => /andP [N1 N2]; apply leq_trans with t.
Qed .
(** We show that the total service of jobs released in a time interval <<[t1, t2)>>
during <<[t, t2)>> is equal to the sum of:
(1) the total service of jobs released in a time interval <<[t1, t)>> during <<[t, t2)>>
and (2) the total service of jobs released in a time interval <<[t, t2)>> during <<[t, t2)>>. *)
Lemma service_of_jobs_cat_arrival_interval :
forall t1 t2 t ,
t1 <= t <= t2 ->
service_of_jobs sched P (arrivals_between arr_seq t1 t2) t t2 =
service_of_jobs sched P (arrivals_between arr_seq t1 t) t t2 +
service_of_jobs sched P (arrivals_between arr_seq t t2) t t2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job
forall t1 t2 t : nat,
t1 <= t <= t2 ->
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t t2 =
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t t2 +
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job
forall t1 t2 t : nat,
t1 <= t <= t2 ->
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t t2 =
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t t2 +
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2
move => t1 t2 t /andP [GEt LEt].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t t2 =
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t t2 +
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2
apply /eqP;rewrite eq_sym; apply /eqP.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t t2 +
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2 =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t t2
rewrite [in X in _ = X](arrivals_between_cat _ _ t) //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2, t : nat GEt : t1 <= t LEt : t <= t2
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t t2 +
service_of_jobs sched P
(arrivals_between arr_seq t t2) t t2 =
service_of_jobs sched P
(arrivals_between arr_seq t1 t ++
arrivals_between arr_seq t t2) t t2
by rewrite {3 }/service_of_jobs -big_cat //=.
Qed .
End GenericModelLemmas .
(** In this section, we prove some properties about service
of sets of jobs for unit-service processor models. *)
Section UnitServiceModelLemmas .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of unit-service processor state model. *)
Context {PState : Type }.
Context `{ProcessorState Job PState}.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
(** 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 unit-service schedule of this arrival sequence ... *)
Variable sched : schedule PState.
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.
(** Let P be any predicate over jobs. *)
Variable P : pred Job.
(** First, we prove that the service received by any set of jobs is
upper-bounded by the corresponding workload. *)
Lemma service_of_jobs_le_workload :
forall (jobs : seq Job) (t1 t2 : instant),
service_of_jobs sched P jobs t1 t2 <= workload_of_jobs P jobs.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job
forall (jobs : seq Job) (t1 t2 : instant),
service_of_jobs sched P jobs t1 t2 <=
workload_of_jobs P jobs
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job
forall (jobs : seq Job) (t1 t2 : instant),
service_of_jobs sched P jobs t1 t2 <=
workload_of_jobs P jobs
intros jobs t1 t2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job t1, t2 : instant
service_of_jobs sched P jobs t1 t2 <=
workload_of_jobs P jobs
apply leq_sum; intros j _.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job t1, t2 : instant j : Job
service_during sched j t1 t2 <= job_cost j
by apply cumulative_service_le_job_cost.
Qed .
(** In this section, we introduce a connection between the cumulative
service, cumulative workload, and completion of jobs. *)
Section WorkloadServiceAndCompletion .
(** Consider an arbitrary time interval <<[t1, t2)>>. *)
Variables t1 t2 : instant.
(** Let jobs be a set of all jobs arrived during <<[t1, t2)>>. *)
Let jobs := arrivals_between arr_seq t1 t2.
(** Next, we consider some time instant [t_compl]. *)
Variable t_compl : instant.
(** And state the proposition that all jobs are completed by time
[t_compl]. Next we show that this proposition is equivalent to
the fact that [workload of jobs = service of jobs]. *)
Let all_jobs_completed_by t_compl :=
forall j , j \in jobs -> P j -> completed_by sched j t_compl.
(** First, we prove that if the workload of [jobs] is equal to the
service of [jobs], then any job in [jobs] is completed by time
[t_compl]. *)
Lemma workload_eq_service_impl_all_jobs_have_completed :
workload_of_jobs P jobs = service_of_jobs sched P jobs t1 t_compl ->
all_jobs_completed_by t_compl.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl ->
all_jobs_completed_by t_compl
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl ->
all_jobs_completed_by t_compl
unfold jobs; intros EQ j ARR Pj; move : (ARR) => ARR2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : workload_of_jobs P
(arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl j : Job ARR : j \in jobs Pj : P j ARR2 : j \in jobs
completed_by sched j t_compl
apply in_arrivals_implies_arrived_between in ARR; last by done .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : workload_of_jobs P
(arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl j : Job ARR : arrived_between j t1 t2 Pj : P j ARR2 : j \in jobs
completed_by sched j t_compl
move : ARR => /andP [T1 T2].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : workload_of_jobs P
(arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2
completed_by sched j t_compl
have F1: forall a b , (a < b) || (a >= b).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : workload_of_jobs P
(arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2
forall a b : nat, (a < b) || (b <= a)
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : workload_of_jobs P
(arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2
forall a b : nat, (a < b) || (b <= a)
by intros ; destruct (a < b) eqn :EQU; apply /orP;
[by left |right ]; apply negbT in EQU; rewrite leqNgt. } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : workload_of_jobs P
(arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)
completed_by sched j t_compl
move : (F1 t_compl t1) => /orP [LT | GT].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : workload_of_jobs P
(arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)LT : t_compl < t1
completed_by sched j t_compl
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : workload_of_jobs P
(arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)LT : t_compl < t1
completed_by sched j t_compl
rewrite /service_of_jobs /service_during in EQ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)LT : t_compl < t1 EQ : workload_of_jobs P
(arrivals_between arr_seq t1 t2) =
\sum_(j <- arrivals_between arr_seq t1 t2 |
P j)
\sum_(t1 <= t < t_compl) service_at sched j t
completed_by sched j t_compl
rewrite exchange_big big_geq //= in EQ; last by rewrite ltnW.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)LT : t_compl < t1 EQ : workload_of_jobs P
(arrivals_between arr_seq t1 t2) = 0
completed_by sched j t_compl
rewrite /workload_of_jobs in EQ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)LT : t_compl < t1 EQ : \sum_(j <- arrivals_between arr_seq t1 t2 |
P j) job_cost j = 0
completed_by sched j t_compl
rewrite (big_rem j) ?Pj //= in EQ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)LT : t_compl < t1 EQ : job_cost j +
\sum_(y <- rem (T:=Job) j
(arrivals_between arr_seq t1 t2) |
P y) job_cost y = 0
completed_by sched j t_compl
move : EQ => /eqP; rewrite addn_eq0; move => /andP [CZ _].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)LT : t_compl < t1 CZ : job_cost j == 0
completed_by sched j t_compl
unfold completed_by, service.completed_by.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)LT : t_compl < t1 CZ : job_cost j == 0
job_cost j <= service sched j t_compl
by move : CZ => /eqP CZ; rewrite CZ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : workload_of_jobs P
(arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)GT : t1 <= t_compl
completed_by sched j t_compl
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : workload_of_jobs P
(arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)GT : t1 <= t_compl
completed_by sched j t_compl
unfold workload_of_jobs, service_of_jobs in EQ; unfold completed_by, service.completed_by.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : \sum_(j <- arrivals_between arr_seq t1 t2 |
P j) job_cost j =
\sum_(j <- arrivals_between arr_seq t1 t2 |
P j) service_during sched j t1 t_compl j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)GT : t1 <= t_compl
job_cost j <= service sched j t_compl
rewrite /service -(service_during_cat _ _ _ t1); last by apply /andP; split .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : \sum_(j <- arrivals_between arr_seq t1 t2 |
P j) job_cost j =
\sum_(j <- arrivals_between arr_seq t1 t2 |
P j) service_during sched j t1 t_compl j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)GT : t1 <= t_compl
job_cost j <=
service_during sched j 0 t1 +
service_during sched j t1 t_compl
rewrite cumulative_service_before_job_arrival_zero // add0n.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : \sum_(j <- arrivals_between arr_seq t1 t2 |
P j) job_cost j =
\sum_(j <- arrivals_between arr_seq t1 t2 |
P j) service_during sched j t1 t_compl j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)GT : t1 <= t_compl
job_cost j <= service_during sched j t1 t_compl
rewrite <- sum_majorant_eqn with (E1 := fun j => service_during sched j t1 t_compl)
(xs := arrivals_between arr_seq t1 t2) (P := P); try done .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop EQ : \sum_(j <- arrivals_between arr_seq t1 t2 |
P j) job_cost j =
\sum_(j <- arrivals_between arr_seq t1 t2 |
P j) service_during sched j t1 t_compl j : Job Pj : P j ARR2 : j \in jobs T1 : t1 <= job_arrival j T2 : job_arrival j < t2 F1 : forall a b : nat, (a < b) || (b <= a)GT : t1 <= t_compl
forall x : Job,
x \in arrivals_between arr_seq t1 t2 ->
P x -> service_during sched x t1 t_compl <= job_cost x
by intros ; apply cumulative_service_le_job_cost; auto using ideal_proc_model_provides_unit_service.
Qed .
(** And vice versa, the fact that any job in [jobs] is completed by time [t_compl]
implies that the workload of [jobs] is equal to the service of [jobs]. *)
Lemma all_jobs_have_completed_impl_workload_eq_service :
all_jobs_completed_by t_compl ->
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop
all_jobs_completed_by t_compl ->
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop
all_jobs_completed_by t_compl ->
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl
unfold jobs; intros COMPL.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl
have F: forall j t , t <= t1 -> j \in arrivals_between arr_seq t1 t2 -> service_during sched j 0 t = 0 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl
forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl
forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0
intros j t LE ARR.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl j : Job t : nat LE : t <= t1 ARR : j \in arrivals_between arr_seq t1 t2
service_during sched j 0 t = 0
eapply in_arrivals_implies_arrived_between in ARR; eauto 2 ; move : ARR => /andP [GE LT].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl j : Job t : nat LE : t <= t1 GE : t1 <= job_arrival j LT : job_arrival j < t2
service_during sched j 0 t = 0
eapply cumulative_service_before_job_arrival_zero; eauto 2 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl j : Job t : nat LE : t <= t1 GE : t1 <= job_arrival j LT : job_arrival j < t2
t <= job_arrival j
by apply leq_trans with t1.
} Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl
destruct (t_compl <= t1) eqn :EQ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl
unfold service_of_jobs.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
\sum_(j <- arrivals_between arr_seq t1 t2 | P j)
service_during sched j t1 t_compl
unfold service_during.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
\sum_(j <- arrivals_between arr_seq t1 t2 | P j)
\sum_(t1 <= t < t_compl) service_at sched j t
rewrite exchange_big //=.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
\sum_(t1 <= j < t_compl)
\sum_(i <- arrivals_between arr_seq t1 t2 | P i)
service_at sched i j
rewrite big_geq; last by done .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
0
rewrite /workload_of_jobs big1_seq //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true
forall i : Job,
P i && (i \in arrivals_between arr_seq t1 t2) ->
job_cost i = 0
move => j /andP [Pj ARR].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true j : Job Pj : P j ARR : j \in arrivals_between arr_seq t1 t2
job_cost j = 0
specialize (COMPL _ ARR Pj).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job COMPL : completed_by sched j t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true Pj : P j ARR : j \in arrivals_between arr_seq t1 t2
job_cost j = 0
rewrite <- F with (j := j) (t := t_compl); try done .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job COMPL : completed_by sched j t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true Pj : P j ARR : j \in arrivals_between arr_seq t1 t2
job_cost j = service_during sched j 0 t_compl
apply /eqP; rewrite eqn_leq; apply /andP; split .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job COMPL : completed_by sched j t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true Pj : P j ARR : j \in arrivals_between arr_seq t1 t2
job_cost j <= service_during sched j 0 t_compl
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job COMPL : completed_by sched j t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true Pj : P j ARR : j \in arrivals_between arr_seq t1 t2
job_cost j <= service_during sched j 0 t_compl
by apply COMPL.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job COMPL : completed_by sched j t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true Pj : P j ARR : j \in arrivals_between arr_seq t1 t2
service_during sched j 0 t_compl <= job_cost j
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job COMPL : completed_by sched j t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = true Pj : P j ARR : j \in arrivals_between arr_seq t1 t2
service_during sched j 0 t_compl <= job_cost j
by apply service_at_most_cost.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = false
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = false
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl
apply /eqP; rewrite eqn_leq; apply /andP; split ; first last .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = false
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl <=
workload_of_jobs P (arrivals_between arr_seq t1 t2)
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = false
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl <=
workload_of_jobs P (arrivals_between arr_seq t1 t2)
by apply service_of_jobs_le_workload.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = false
workload_of_jobs P (arrivals_between arr_seq t1 t2) <=
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = false
workload_of_jobs P (arrivals_between arr_seq t1 t2) <=
service_of_jobs sched P
(arrivals_between arr_seq t1 t2) t1 t_compl
rewrite /workload_of_jobs big_seq_cond [X in _ <= X]big_seq_cond.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = false
\sum_(i <- arrivals_between arr_seq t1 t2 | (i
\in
arrivals_between
arr_seq
t1 t2) &&
P i)
job_cost i <=
\sum_(i <- arrivals_between arr_seq t1 t2 | (i
\in
arrivals_between
arr_seq
t1 t2) &&
P i)
service_during sched i t1 t_compl
rewrite leq_sum // => j /andP [ARR Pj].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop COMPL : all_jobs_completed_by t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = false j : Job ARR : j \in arrivals_between arr_seq t1 t2 Pj : P j
job_cost j <= service_during sched j t1 t_compl
specialize (COMPL _ ARR Pj).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job COMPL : completed_by sched j t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = false ARR : j \in arrivals_between arr_seq t1 t2 Pj : P j
job_cost j <= service_during sched j t1 t_compl
rewrite -[service_during _ _ _ _ ]add0n -(F j t1) //= -(big_cat_nat) //=.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job COMPL : completed_by sched j t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 EQ : (t_compl <= t1) = false ARR : j \in arrivals_between arr_seq t1 t2 Pj : P j
t1 <= t_compl
move : EQ =>/negP /negP; rewrite -ltnNge => EQ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop j : Job COMPL : completed_by sched j t_compl F : forall (j : Job) (t : nat),
t <= t1 ->
j \in arrivals_between arr_seq t1 t2 ->
service_during sched j 0 t = 0 ARR : j \in arrivals_between arr_seq t1 t2 Pj : P j EQ : t1 < t_compl
t1 <= t_compl
by apply ltnW.
Qed .
(** Using the lemmas above, we prove the equivalence. *)
Corollary all_jobs_have_completed_equiv_workload_eq_service :
all_jobs_completed_by t_compl <->
workload_of_jobs P jobs = service_of_jobs sched P jobs t1 t_compl.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop
all_jobs_completed_by t_compl <->
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop
all_jobs_completed_by t_compl <->
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl
split .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop
all_jobs_completed_by t_compl ->
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop
all_jobs_completed_by t_compl ->
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl
by apply all_jobs_have_completed_impl_workload_eq_service.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl ->
all_jobs_completed_by t_compl
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job t1, t2 : instant jobs := arrivals_between arr_seq t1 t2 : seq Job t_compl : instant all_jobs_completed_by := fun t_compl : instant =>
forall j : Job,
j \in jobs ->
P j ->
completed_by sched j t_compl: instant -> Prop
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl ->
all_jobs_completed_by t_compl
by apply workload_eq_service_impl_all_jobs_have_completed.
Qed .
End WorkloadServiceAndCompletion .
End UnitServiceModelLemmas .
(** In this section, we prove some properties about service
of sets of jobs for unit-service uniprocessor models. *)
Section UnitServiceUniProcessorModelLemmas .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of unit-service uniprocessor state model. *)
Context {PState : Type }.
Context `{ProcessorState Job PState}.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
Hypothesis H_uniprocessor_model : uniprocessor_model PState.
(** 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 unit-service uni-processor schedule of this arrival sequence ... *)
Variable sched : schedule PState.
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.
(** Let [P] be any predicate over jobs. *)
Variable P : pred Job.
(** In this section, we prove that the service received by any set of jobs
is upper-bounded by the corresponding interval length. *)
Section ServiceOfJobsIsBoundedByLength .
(** Let [jobs] denote any set of jobs. *)
Variable jobs : seq Job.
Hypothesis H_no_duplicate_jobs : uniq jobs.
(** We prove that the overall service of [jobs] at a single time instant is at most [1]. *)
Lemma service_of_jobs_le_1 :
forall t , \sum_(j <- jobs | P j) service_at sched j t <= 1 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs
forall t : instant,
\sum_(j <- jobs | P j) service_at sched j t <= 1
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs
forall t : instant,
\sum_(j <- jobs | P j) service_at sched j t <= 1
intros t.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t : instant
\sum_(j <- jobs | P j) service_at sched j t <= 1
eapply leq_trans.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t : instant
\sum_(j <- jobs | P j) service_at sched j t <= ?n
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t : instant
\sum_(j <- jobs | P j) service_at sched j t <= ?n
by apply leq_sum_seq_pred with (P2 := predT); intros . } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t : instant
\sum_(i <- jobs | predT i) ((service_at sched)^~ t) i <=
1
simpl ; induction jobs as [ | j js].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq [::] t : instant
\sum_(i <- [::]) service_at sched i t <= 1
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq [::] t : instant
\sum_(i <- [::]) service_at sched i t <= 1
by rewrite big_nil.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : uniq js ->
\sum_(i <- js) service_at sched i t <= 1
\sum_(i <- (j :: js)) service_at sched i t <= 1
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : uniq js ->
\sum_(i <- js) service_at sched i t <= 1
\sum_(i <- (j :: js)) service_at sched i t <= 1
feed IHjs; first by move : H_no_duplicate_jobs; rewrite cons_uniq => /andP [_ U]. Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1
\sum_(i <- (j :: js)) service_at sched i t <= 1
rewrite big_cons.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1
service_at sched j t +
\sum_(j <- js) service_at sched j t <= 1
destruct (service_is_zero_or_one H_unit_service_proc_model sched j t) as [Z | O].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 Z : service_at sched j t = 0
service_at sched j t +
\sum_(j <- js) service_at sched j t <= 1
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 Z : service_at sched j t = 0
service_at sched j t +
\sum_(j <- js) service_at sched j t <= 1
by rewrite Z (leqRW IHjs).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1
service_at sched j t +
\sum_(j <- js) service_at sched j t <= 1
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1
service_at sched j t +
\sum_(j <- js) service_at sched j t <= 1
have -> : \sum_(j <- js) service_in j (sched t) = 0 ; last by rewrite O.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1
\sum_(j <- js) service_in j (sched t) = 0
have POS: service_at sched j t > 0 by rewrite O.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS : 0 < service_at sched j t
\sum_(j <- js) service_in j (sched t) = 0
apply service_at_implies_scheduled_at in POS.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS : scheduled_at sched j t
\sum_(j <- js) service_in j (sched t) = 0
apply /eqP; rewrite big_seq big1 //; intros j' IN.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS : scheduled_at sched j t j' : Job IN : j' \in js
service_in j' (sched t) = 0
apply /eqP; rewrite -leqn0 leqNgt.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS : scheduled_at sched j t j' : Job IN : j' \in js
~~ (0 < service_in j' (sched t))
eapply contra with (b := scheduled_at sched j' t);
first apply service_at_implies_scheduled_at.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS : scheduled_at sched j t j' : Job IN : j' \in js
~~ scheduled_at sched j' t
apply /negP; intros SCHED.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS : scheduled_at sched j t j' : Job IN : j' \in js SCHED : scheduled_at sched j' t
False
specialize (H_uniprocessor_model _ _ _ _ POS SCHED); subst j'.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState j : Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs, js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS, SCHED : scheduled_at sched j t IN : j \in js
False
by move : H_no_duplicate_jobs; rewrite cons_uniq => /andP [/negP NIN _].
Qed .
(** Next, we prove that the service received by those jobs is no larger
than their workload. *)
Corollary service_of_jobs_le_length_of_interval :
forall (t : instant) (Δ : duration),
service_of_jobs sched P jobs t (t + Δ) <= Δ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs
forall (t : instant) (Δ : duration),
service_of_jobs sched P jobs t (t + Δ) <= Δ
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs
forall (t : instant) (Δ : duration),
service_of_jobs sched P jobs t (t + Δ) <= Δ
intros .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t : instant Δ : duration
service_of_jobs sched P jobs t (t + Δ) <= Δ
have EQ: \sum_(t <= x < t + Δ) 1 = Δ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t : instant Δ : duration
\sum_(t <= x < t + Δ) 1 = Δ
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t : instant Δ : duration
\sum_(t <= x < t + Δ) 1 = Δ
by rewrite big_const_nat iter_addn mul1n addn0 -{2 }[t]addn0 subnDl subn0. } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t : instant Δ : duration EQ : \sum_(t <= x < t + Δ) 1 = Δ
service_of_jobs sched P jobs t (t + Δ) <= Δ
rewrite -{2 }EQ {EQ}.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t : instant Δ : duration
service_of_jobs sched P jobs t (t + Δ) <=
\sum_(t <= x < t + Δ) 1
rewrite /service_of_jobs/service_during/service_at exchange_big //=.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t : instant Δ : duration
\sum_(t <= j < t + Δ)
\sum_(i <- jobs | P i) service_in i (sched j) <=
\sum_(t <= x < t + Δ) 1
rewrite leq_sum //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t : instant Δ : duration
forall i : nat,
true ->
\sum_(i0 <- jobs | P i0) service_in i0 (sched i) <= 1
move => t' _.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t : instant Δ : duration t' : nat
\sum_(i <- jobs | P i) service_in i (sched t') <= 1
by apply service_of_jobs_le_1.
Qed .
(** The same holds for two time instants. *)
Corollary service_of_jobs_le_length_of_interval' :
forall (t1 t2 : instant),
service_of_jobs sched P jobs t1 t2 <= t2 - t1.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs
forall t1 t2 : instant,
service_of_jobs sched P jobs t1 t2 <= t2 - t1
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs
forall t1 t2 : instant,
service_of_jobs sched P jobs t1 t2 <= t2 - t1
intros .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t1, t2 : instant
service_of_jobs sched P jobs t1 t2 <= t2 - t1
have <-: \sum_(t1 <= x < t2) 1 = t2 - t1.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t1, t2 : instant
\sum_(t1 <= x < t2) 1 = t2 - t1
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t1, t2 : instant
\sum_(t1 <= x < t2) 1 = t2 - t1
by rewrite big_const_nat iter_addn mul1n addn0. } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t1, t2 : instant
service_of_jobs sched P jobs t1 t2 <=
\sum_(t1 <= x < t2) 1
rewrite /service_of_jobs exchange_big //=.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t1, t2 : instant
\sum_(t1 <= j < t2)
\sum_(i <- jobs | P i) service_at sched i j <=
\sum_(t1 <= x < t2) 1
rewrite leq_sum //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t1, t2 : instant
forall i : nat,
true ->
\sum_(i0 <- jobs | P i0) service_at sched i0 i <= 1
move => t' _.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t1, t2 : instant t' : nat
\sum_(i <- jobs | P i) service_at sched i t' <= 1
have SE := service_of_jobs_le_1 t'.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t1, t2 : instant t' : nat SE : \sum_(j <- jobs | P j) service_at sched j t' <= 1
\sum_(i <- jobs | P i) service_at sched i t' <= 1
eapply leq_trans; last by eassumption .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : Type H2 : ProcessorState Job PState H_unit_service_proc_model : unit_service_proc_model
PState H_uniprocessor_model : uniprocessor_model PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState 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 P : pred Job jobs : seq Job H_no_duplicate_jobs : uniq jobs t1, t2 : instant t' : nat SE : \sum_(j <- jobs | P j) service_at sched j t' <= 1
\sum_(i <- jobs | P i) service_at sched i t' <=
\sum_(j <- jobs | P j) service_at sched j t'
by rewrite leq_sum.
Qed .
End ServiceOfJobsIsBoundedByLength .
End UnitServiceUniProcessorModelLemmas .
(** In this section, we prove some properties about service
of sets of jobs for ideal uni-processor model. *)
Section IdealModelLemmas .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** Next, consider any ideal uni-processor 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.
(** Let [P] be any predicate over jobs. *)
Variable P : pred Job.
(** We prove that if the total service within some time interval <<[t1,t2)>>
is smaller than <<t2 - t1>>, then there is an idle time instant [t ∈ [t1,t2)]. *)
Lemma low_service_implies_existence_of_idle_time :
forall t1 t2 ,
service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t , t1 <= t < t2 /\ is_idle sched t.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job
forall t1 t2 : instant,
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t : nat, t1 <= t < t2 /\ is_idle sched t
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job
forall t1 t2 : instant,
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t : nat, t1 <= t < t2 /\ is_idle sched t
intros ? ? SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
exists t : nat, t1 <= t < t2 /\ is_idle sched t
destruct (t1 <= t2) eqn :LE; last first .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = false
exists t : nat, t1 <= t < t2 /\ is_idle sched t
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = false
exists t : nat, t1 <= t < t2 /\ is_idle sched t
move : LE => /negP/negP; rewrite -ltnNge.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
t2 < t1 ->
exists t : nat, t1 <= t < t2 /\ is_idle sched t
move => LT; apply ltnW in LT; rewrite -subn_eq0 in LT.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LT : t2 - t1 == 0
exists t : nat, t1 <= t < t2 /\ is_idle sched t
by move : LT => /eqP -> in SERV; rewrite ltn0 in SERV.
} Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = true
exists t : nat, t1 <= t < t2 /\ is_idle sched t
have EX: exists δ , t2 = t1 + δ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = true
exists δ : nat, t2 = t1 + δ
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = true
exists δ : nat, t2 = t1 + δ
by exists (t2 - t1); rewrite subnKC // ltnW. } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = true EX : exists δ : nat, t2 = t1 + δ
exists t : nat, t1 <= t < t2 /\ is_idle sched t
move : EX => [δ EQ]; subst t2; clear LE.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ : nat SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 (t1 + δ)) t1
(t1 + δ) <
t1 + δ - t1
exists t : nat, t1 <= t < t1 + δ /\ is_idle sched t
rewrite {3 }[t1 + δ]addnC -addnBA // subnn addn0 in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ : nat SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 (t1 + δ)) t1
(t1 + δ) < δ
exists t : nat, t1 <= t < t1 + δ /\ is_idle sched t
rewrite /service_of_jobs exchange_big //= in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ : nat SERV : \sum_(t1 <= j <
t1 + δ)
\sum_(i <-
arrivals_between arr_seq 0
(t1 + δ))
(sched j == Some i) < δ
exists t : nat, t1 <= t < t1 + δ /\ is_idle sched t
apply sum_le_summation_range in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ : nat SERV : exists x : nat,
t1 <= x < t1 + δ /\
\sum_(i <-
arrivals_between arr_seq 0
(t1 + δ))
(sched x == Some i) = 0
exists t : nat, t1 <= t < t1 + δ /\ is_idle sched t
move : SERV => [x [/andP [GEx LEx] L]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : \sum_(i <- arrivals_between arr_seq 0 (t1 + δ))
(sched x == Some i) = 0
exists t : nat, t1 <= t < t1 + δ /\ is_idle sched t
exists x ; split ; first by apply /andP; split .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : \sum_(i <- arrivals_between arr_seq 0 (t1 + δ))
(sched x == Some i) = 0
is_idle sched x
apply /negPn; apply /negP; intros NIDLE.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : \sum_(i <- arrivals_between arr_seq 0 (t1 + δ))
(sched x == Some i) = 0 NIDLE : ~~ is_idle sched x
False
unfold is_idle in NIDLE.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : \sum_(i <- arrivals_between arr_seq 0 (t1 + δ))
(sched x == Some i) = 0 NIDLE : sched x != None
False
destruct (sched x) eqn :SCHED; last by done .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ s : Job SCHED : sched x = Some s L : \sum_(i <- arrivals_between arr_seq 0 (t1 + δ))
(Some s == Some i) = 0 NIDLE : Some s != None
False
move : SCHED => /eqP SCHED; clear NIDLE; rewrite -scheduled_at_def/= in SCHED.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ s : Job L : \sum_(i <- arrivals_between arr_seq 0 (t1 + δ))
(Some s == Some i) = 0 SCHED : scheduled_at sched s x
False
move : L => /eqP; rewrite -sum_nat_eq0_nat; move => /allP L.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ s : Job SCHED : scheduled_at sched s x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x : Job, (Some s == Some x) == 0 }
False
specialize (L s); feed L.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ s : Job SCHED : scheduled_at sched s x L : s \in arrivals_between arr_seq 0 (t1 + δ) ->
(fun x : Job => is_true ((Some s == Some x) == 0 ))
s
s \in arrivals_between arr_seq 0 (t1 + δ)
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ s : Job SCHED : scheduled_at sched s x L : s \in arrivals_between arr_seq 0 (t1 + δ) ->
(fun x : Job => is_true ((Some s == Some x) == 0 ))
s
s \in arrivals_between arr_seq 0 (t1 + δ)
unfold arrivals_between.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ s : Job SCHED : scheduled_at sched s x L : s \in arrivals_between arr_seq 0 (t1 + δ) ->
(fun x : Job => is_true ((Some s == Some x) == 0 ))
s
s \in \cat_(0 <=t<t1 + δ)arrivals_at arr_seq t
eapply arrived_between_implies_in_arrivals; eauto 2 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ s : Job SCHED : scheduled_at sched s x L : s \in arrivals_between arr_seq 0 (t1 + δ) ->
(fun x : Job => is_true ((Some s == Some x) == 0 ))
s
arrived_between s 0 (t1 + δ)
by apply H_jobs_must_arrive_to_execute in SCHED; apply leq_ltn_trans with x.
} Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : 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 P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ s : Job SCHED : scheduled_at sched s x L : (fun x : Job => is_true ((Some s == Some x) == 0 ))
s
False
by move : L; simpl ;rewrite eqb0; move => /eqP EQ.
Qed .
End IdealModelLemmas .