Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.model.aggregate.workload.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.model.aggregate.service_of_jobs.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.busy_interval.quiet_time.
(** * 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 : ProcessorState Job}.
(** ... 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 .
(** In the following, we consider an arbitrary sequence of jobs [jobs]. *)
Variable jobs : seq Job.
(** Also, consider an interval <<[t1, t2)>>... *)
Variable t1 t2 : instant.
(** ...and two additional predicates [P1] and [P2]. *)
Variable P1 P2 : pred Job.
(** For brevity, in the following comments we denote a subset of [jobs]
satisfying a predicate [P] by [{jobs | P}]. *)
(** First, we prove that the service received by [{jobs | P1}] can be split
into: (1) the service received by [{jobs | P1 ∧ P2}] and (2) the service
received by the a subset [{jobs | P1 ∧ ¬ P2}]. *)
Lemma service_of_jobs_case_on_pred :
service_of_jobs sched P1 jobs t1 t2 =
service_of_jobs sched (fun j => P1 j && P2 j) jobs t1 t2
+ service_of_jobs sched (fun j => P1 j && ~~ P2 j) jobs t1 t2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
service_of_jobs sched P1 jobs t1 t2 =
service_of_jobs sched (fun j : Job => P1 j && P2 j)
jobs t1 t2 +
service_of_jobs sched (fun j : Job => P1 j && ~~ P2 j)
jobs t1 t2
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
service_of_jobs sched P1 jobs t1 t2 =
service_of_jobs sched (fun j : Job => P1 j && P2 j)
jobs t1 t2 +
service_of_jobs sched (fun j : Job => P1 j && ~~ P2 j)
jobs t1 t2
rewrite /service_of_jobs big_mkcond //=.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
\sum_(i <- jobs)
(if P1 i then service_during sched i t1 t2 else 0 ) =
\sum_(j <- jobs | P1 j && P2 j)
service_during sched j t1 t2 +
\sum_(j <- jobs | P1 j && ~~ P2 j)
service_during sched j t1 t2
rewrite [in X in _ = X + _]big_mkcond //=.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
\sum_(i <- jobs)
(if P1 i then service_during sched i t1 t2 else 0 ) =
\sum_(i <- jobs)
(if P1 i && P2 i
then service_during sched i t1 t2
else 0 ) +
\sum_(j <- jobs | P1 j && ~~ P2 j)
service_during sched j t1 t2
rewrite [in X in _ = _ + X]big_mkcond //=.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
\sum_(i <- jobs)
(if P1 i then service_during sched i t1 t2 else 0 ) =
\sum_(i <- jobs)
(if P1 i && P2 i
then service_during sched i t1 t2
else 0 ) +
\sum_(i <- jobs)
(if P1 i && ~~ P2 i
then service_during sched i t1 t2
else 0 )
rewrite -big_split; apply eq_big_seq; intros j IN.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job j : Job IN : j \in jobs
(if P1 j then service_during sched j t1 t2 else 0 ) =
ssrnat_addn__canonical__Monoid_ComLaw
(if P1 j && P2 j
then service_during sched j t1 t2
else 0 )
(if P1 j && ~~ P2 j
then service_during sched j t1 t2
else 0 )
by destruct (P1 _), (P2 _); simpl ; lia .
Qed .
(** We show that the service received by [{jobs | P}] is equal to the
difference between the total service received by [jobs] and the service
of [{jobs | ¬ P}]. *)
Lemma service_of_jobs_negate_pred :
service_of_jobs sched P jobs t1 t2 =
total_service_of_jobs_in sched jobs t1 t2 - service_of_jobs sched (fun j => ~~ P j) jobs t1 t2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
service_of_jobs sched P jobs t1 t2 =
total_service_of_jobs_in sched jobs t1 t2 -
service_of_jobs sched (fun j : Job => ~~ P j) jobs t1
t2
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
service_of_jobs sched P jobs t1 t2 =
total_service_of_jobs_in sched jobs t1 t2 -
service_of_jobs sched (fun j : Job => ~~ P j) jobs t1
t2
rewrite /total_service_of_jobs_in /service_of_jobs.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
\sum_(j <- jobs | P j) service_during sched j t1 t2 =
\sum_(j <- jobs | predT j)
service_during sched j t1 t2 -
\sum_(j <- jobs | ~~ P j) service_during sched j t1 t2
rewrite big_mkcond [in X in _ = X - _]big_mkcond [in X in _ = _ - X]big_mkcond //=.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
\sum_(i <- jobs)
(if P i then service_during sched i t1 t2 else 0 ) =
\sum_(i <- jobs) service_during sched i t1 t2 -
\sum_(i <- jobs)
(if ~~ P i then service_during sched i t1 t2 else 0 )
rewrite -sumnB; last by move => j _; case : (P j).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
\sum_(i <- jobs)
(if P i then service_during sched i t1 t2 else 0 ) =
\sum_(i <- jobs)
(service_during sched i t1 t2 -
(if ~~ P i
then service_during sched i t1 t2
else 0 ))
apply : eq_big_seq => j IN.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job j : Job IN : j \in jobs
(if P j then service_during sched j t1 t2 else 0 ) =
service_during sched j t1 t2 -
(if ~~ P j then service_during sched j t1 t2 else 0 )
by case : (P j) => //=; lia .
Qed .
(** We show that [service_of_jobs] is monotone with respect to the
predicate. That is, given the fact [∀ j ∈ jobs: P1 j ==> P2 j], we show
that the service of [{jobs | P1}] is bounded by the service of [{jobs | P2}]. *)
Lemma service_of_jobs_pred_impl :
(forall j : Job, j \in jobs -> P1 j -> P2 j) ->
service_of_jobs sched P1 jobs t1 t2 <= service_of_jobs sched P2 jobs t1 t2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
(forall j : Job, j \in jobs -> P1 j -> P2 j) ->
service_of_jobs sched P1 jobs t1 t2 <=
service_of_jobs sched P2 jobs t1 t2
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
(forall j : Job, j \in jobs -> P1 j -> P2 j) ->
service_of_jobs sched P1 jobs t1 t2 <=
service_of_jobs sched P2 jobs t1 t2
by intros IMPL; apply leq_sum_seq_pred; eauto . Qed .
(** Similarly, we show that if [P1] is equivalent to [P2], then the service
of [{jobs | P1}] is equal to the service of [{jobs | P2}]. *)
Lemma service_of_jobs_equiv_pred :
{in jobs, P1 =1 P2} ->
service_of_jobs sched P1 jobs t1 t2 = service_of_jobs sched P2 jobs t1 t2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
{in jobs, P1 =1 P2} ->
service_of_jobs sched P1 jobs t1 t2 =
service_of_jobs sched P2 jobs t1 t2
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
{in jobs, P1 =1 P2} ->
service_of_jobs sched P1 jobs t1 t2 =
service_of_jobs sched P2 jobs t1 t2
intros * EQUIV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job EQUIV : {in jobs, P1 =1 P2}
service_of_jobs sched P1 jobs t1 t2 =
service_of_jobs sched P2 jobs t1 t2
rewrite /service_of_jobs !big_mkcond [in X in _ = X]big_mkcond //=; apply : eq_big_seq.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job EQUIV : {in jobs, P1 =1 P2}
{in jobs,
(fun i : Job =>
if P1 i then service_during sched i t1 t2 else 0 ) =1
(fun i : Job =>
if P2 i then service_during sched i t1 t2 else 0 )}
intros j IN; specialize (EQUIV j IN); simpl in EQUIV; rewrite EQUIV; clear EQUIV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job j : Job IN : j \in jobs
(if P2 j then service_during sched j t1 t2 else 0 ) =
(if P2 j then service_during sched j t1 t2 else 0 )
by case : (P2 j) => //.
Qed .
(** Next, we show an auxiliary lemma that allows us to change the order of
summation.
Recall that [service_of_jobs] is defined as a sum over all jobs in
[jobs] of <<[service_during j [t1,t2)]>>. We show that [service_of_jobs]
over an interval <<[t1,t2)>> is equal to the sum over individual time
instances (in <<[t1,t2)>>) of [service_of_jobs_at].
In other words, we show that <<[∑_{j ∈ jobs} ∑_{t \in [t1,t2)} service
of j at t]>> is equal to <<[∑_{t \in [t1,t2)} ∑_{j ∈ jobs} service of j
at t]>>. *)
Lemma service_of_jobs_sum_over_time_interval :
service_of_jobs sched P jobs t1 t2
= \sum_(t1 <= t < t2) service_of_jobs_at sched P jobs t.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
service_of_jobs sched P jobs t1 t2 =
\sum_(t1 <= t < t2) service_of_jobs_at sched P jobs t
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
service_of_jobs sched P jobs t1 t2 =
\sum_(t1 <= t < t2) service_of_jobs_at sched P jobs t
by apply exchange_big. Qed .
(** We show that service of [{jobs | false}] is equal to 0. *)
Lemma service_of_jobs_pred0 :
service_of_jobs sched pred0 jobs t1 t2 = 0 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
service_of_jobs sched pred0 jobs t1 t2 = 0
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
service_of_jobs sched pred0 jobs t1 t2 = 0
by apply big_pred0. Qed .
(** More generally, if none of the jobs inside [jobs] is scheduled
at time [t] or satisfies [P], then total service of [jobs] at
time [t] is equal to 0. *)
Lemma service_of_jobs_nsched_or_unsat :
forall (t : instant),
(forall j , j \in jobs -> ~~ (P j && scheduled_at sched j t)) ->
service_of_jobs_at sched P jobs t = 0 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
forall t : instant,
(forall j : Job,
j \in jobs -> ~~ (P j && scheduled_at sched j t)) ->
service_of_jobs_at sched P jobs t = 0
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job
forall t : instant,
(forall j : Job,
j \in jobs -> ~~ (P j && scheduled_at sched j t)) ->
service_of_jobs_at sched P jobs t = 0
intros ? ALL.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant ALL : forall j : Job,
j \in jobs -> ~~ (P j && scheduled_at sched j t)
service_of_jobs_at sched P jobs t = 0
elim : jobs ALL => [|a l IHl] ALL.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant ALL : forall j : Job,
j \in [::] -> ~~ (P j && scheduled_at sched j t)
service_of_jobs_at sched P [::] t = 0
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant ALL : forall j : Job,
j \in [::] -> ~~ (P j && scheduled_at sched j t)
service_of_jobs_at sched P [::] t = 0
by rewrite /service_of_jobs_at big_nil.
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant a : Job l : seq Job IHl : (forall j : Job,
j \in l -> ~~ (P j && scheduled_at sched j t)) ->
service_of_jobs_at sched P l t = 0 ALL : forall j : Job,
j \in a :: l ->
~~ (P j && scheduled_at sched j t)
service_of_jobs_at sched P (a :: l) t = 0
feed IHl. Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant a : Job l : seq Job IHl : (forall j : Job,
j \in l -> ~~ (P j && scheduled_at sched j t)) ->
service_of_jobs_at sched P l t = 0 ALL : forall j : Job,
j \in a :: l ->
~~ (P j && scheduled_at sched j t)
forall j : Job,
j \in l -> ~~ (P j && scheduled_at sched j t)
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant a : Job l : seq Job IHl : (forall j : Job,
j \in l -> ~~ (P j && scheduled_at sched j t)) ->
service_of_jobs_at sched P l t = 0 ALL : forall j : Job,
j \in a :: l ->
~~ (P j && scheduled_at sched j t)
forall j : Job,
j \in l -> ~~ (P j && scheduled_at sched j t)
by intros j' IN; apply ALL; rewrite in_cons; apply /orP; right . } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant a : Job l : seq Job IHl : service_of_jobs_at sched P l t = 0 ALL : forall j : Job,
j \in a :: l ->
~~ (P j && scheduled_at sched j t)
service_of_jobs_at sched P (a :: l) t = 0
rewrite /service_of_jobs_at big_cons; rewrite /service_of_jobs_at in IHl.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant a : Job l : seq Job ALL : forall j : Job,
j \in a :: l ->
~~ (P j && scheduled_at sched j t)IHl : \sum_(j <- l | P j) service_at sched j t = 0
(if P a
then
service_at sched a t +
\sum_(j <- l | P j) service_at sched j t
else \sum_(j <- l | P j) service_at sched j t) = 0
destruct (P a) eqn : Pa => [|//].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant a : Job l : seq Job ALL : forall j : Job,
j \in a :: l ->
~~ (P j && scheduled_at sched j t)IHl : \sum_(j <- l | P j) service_at sched j t = 0 Pa : P a = true
service_at sched a t +
\sum_(j <- l | P j) service_at sched j t = 0
rewrite IHl addn0.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant a : Job l : seq Job ALL : forall j : Job,
j \in a :: l ->
~~ (P j && scheduled_at sched j t)IHl : \sum_(j <- l | P j) service_at sched j t = 0 Pa : P a = true
service_at sched a t = 0
specialize (ALL a); feed ALL.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant a : Job l : seq Job ALL : a \in a :: l ->
~~ (P a && scheduled_at sched a t) IHl : \sum_(j <- l | P j) service_at sched j t = 0 Pa : P a = true
a \in a :: l
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant a : Job l : seq Job ALL : a \in a :: l ->
~~ (P a && scheduled_at sched a t) IHl : \sum_(j <- l | P j) service_at sched j t = 0 Pa : P a = true
a \in a :: l
by rewrite in_cons; apply /orP; left . } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant a : Job l : seq Job ALL : ~~ (P a && scheduled_at sched a t) IHl : \sum_(j <- l | P j) service_at sched j t = 0 Pa : P a = true
service_at sched a t = 0
rewrite Pa Bool.andb_true_l in ALL.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 jobs : seq Job t1, t2 : instant P1, P2 : pred Job t : instant a : Job l : seq Job IHl : \sum_(j <- l | P j) service_at sched j t = 0 Pa : P a = true ALL : ~~ scheduled_at sched a t
service_at sched a t = 0
by apply not_scheduled_implies_no_service.
Qed .
End GenericModelLemmas .
(** In this section, we prove a lemma about the sum of service with
different predicates over a fixed time interval. *)
Section HEPService .
(** Consider any type of jobs. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor state model, ... *)
Context {PState : ProcessorState Job}.
(** ... any valid arrival sequence, .... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any schedule of this arrival sequence ... *)
Variable sched : schedule PState.
(** ... where jobs do not execute before their arrival. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
(** Consider a JLFP policy that indicates a higher-or-equal priority
relation and assume that the relation is reflexive. *)
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
(** Consider an interval <<[t1, t2)>> ... *)
Variables t1 t2 : instant.
(** ... and a job [j] arriving no earlier than [t1]. *)
Variable j : Job.
Hypothesis H_arrives : arrives_in arr_seq j.
Hypothesis H_t1_le_j_arr : t1 <= job_arrival j.
(** We prove that the sum of the service during <<[t1, t2)>> of job
[j] and the service of higher-or-equal priority jobs distinct
from [j] during <<[t1, t2)>> is equal to the service of
higher-or-equal priority jobs in <<[t1, t2)>>. *)
Lemma service_plus_ahep_eq_service_hep :
service_during sched j t1 t2 + service_of_other_hep_jobs arr_seq sched j t1 t2
= service_of_hep_jobs arr_seq sched j t1 t2.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j
service_during sched j t1 t2 +
service_of_other_hep_jobs arr_seq sched j t1 t2 =
service_of_hep_jobs arr_seq sched j t1 t2
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j
service_during sched j t1 t2 +
service_of_other_hep_jobs arr_seq sched j t1 t2 =
service_of_hep_jobs arr_seq sched j t1 t2
have EQ: forall a b c , b <= c -> a = c - b -> a + b = c by lia .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j EQ : forall a b c : nat,
b <= c -> a = c - b -> a + b = c
service_during sched j t1 t2 +
service_of_other_hep_jobs arr_seq sched j t1 t2 =
service_of_hep_jobs arr_seq sched j t1 t2
apply : EQ; first by apply service_of_jobs_pred_impl => s IN2 /andP [AHEP _].Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j
service_during sched j t1 t2 =
service_of_hep_jobs arr_seq sched j t1 t2 -
service_of_other_hep_jobs arr_seq sched j t1 t2
rewrite /service_of_other_hep_jobs /service_of_hep_jobs.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j
service_during sched j t1 t2 =
service_of_jobs sched (hep_job^~ j)
(arrivals_between arr_seq t1 t2) t1 t2 -
service_of_jobs sched (another_hep_job^~ j)
(arrivals_between arr_seq t1 t2) t1 t2
erewrite service_of_jobs_case_on_pred with (P2 := fun jhp => jhp == j).Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j
service_during sched j t1 t2 =
service_of_jobs sched
(fun j0 : Job => hep_job j0 j && (j0 == j))
(arrivals_between arr_seq t1 t2) t1 t2 +
service_of_jobs sched
(fun j0 : Job => hep_job j0 j && (j0 != j))
(arrivals_between arr_seq t1 t2) t1 t2 -
service_of_jobs sched (another_hep_job^~ j)
(arrivals_between arr_seq t1 t2) t1 t2
have -> : forall a b , a + b - b = a by lia .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j
service_during sched j t1 t2 =
service_of_jobs sched
(fun j0 : Job => hep_job j0 j && (j0 == j))
(arrivals_between arr_seq t1 t2) t1 t2
have [LE|LT] := leqP t2 (job_arrival j).Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LE : t2 <= job_arrival j
service_during sched j t1 t2 =
service_of_jobs sched
(fun j0 : Job => hep_job j0 j && (j0 == j))
(arrivals_between arr_seq t1 t2) t1 t2
{ Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LE : t2 <= job_arrival j
service_during sched j t1 t2 =
service_of_jobs sched
(fun j0 : Job => hep_job j0 j && (j0 == j))
(arrivals_between arr_seq t1 t2) t1 t2
apply eq_trans with 0 ; last symmetry .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LE : t2 <= job_arrival j
service_during sched j t1 t2 = 0
{ Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LE : t2 <= job_arrival j
service_during sched j t1 t2 = 0
by apply : cumulative_service_before_job_arrival_zero => //. } Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LE : t2 <= job_arrival j
service_of_jobs sched
(fun j0 : Job => hep_job j0 j && (j0 == j))
(arrivals_between arr_seq t1 t2) t1 t2 = 0
{ Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LE : t2 <= job_arrival j
service_of_jobs sched
(fun j0 : Job => hep_job j0 j && (j0 == j))
(arrivals_between arr_seq t1 t2) t1 t2 = 0
rewrite /service_of_jobs // big1_seq // => s /andP [/andP [_ /eqP EQ] IN]; subst s.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LE : t2 <= job_arrival j IN : j \in arrivals_between arr_seq t1 t2
service_during sched j t1 t2 = 0
by apply : cumulative_service_before_job_arrival_zero => //. }
} Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LT : job_arrival j < t2
service_during sched j t1 t2 =
service_of_jobs sched
(fun j0 : Job => hep_job j0 j && (j0 == j))
(arrivals_between arr_seq t1 t2) t1 t2
{ Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LT : job_arrival j < t2
service_during sched j t1 t2 =
service_of_jobs sched
(fun j0 : Job => hep_job j0 j && (j0 == j))
(arrivals_between arr_seq t1 t2) t1 t2
rewrite /service_of_jobs; erewrite big_pred1_seq => //.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LT : job_arrival j < t2
(fun j0 : Job => hep_job j0 j && (j0 == j)) =1 pred1 j
{ Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LT : job_arrival j < t2
(fun j0 : Job => hep_job j0 j && (j0 == j)) =1 pred1 j
move => j'; rewrite /pred1 //=.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LT : job_arrival j < t2 j' : Job
hep_job j' j && (j' == j) = (j' == j)
have [A|B] := eqVneq j' j; last by rewrite andbF.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched JLFP : JLFP_policy Job H_priority_is_reflexive : reflexive_job_priorities
JLFP t1, t2 : instant j : Job H_arrives : arrives_in arr_seq j H_t1_le_j_arr : t1 <= job_arrival j LT : job_arrival j < t2 j' : Job A : j' = j
hep_job j' j && true = true
by rewrite andbT; subst ; apply H_priority_is_reflexive.
}
}
Qed .
End HEPService .
(** 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 : ProcessorState Job}.
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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 => [|//].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 move => a b; 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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
apply : eq_leq; have /esym/eqP := EQ; rewrite eq_sum_leq_seq.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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
all
(fun x : Job =>
service_during sched x t1 t_compl == job_cost x)
[seq x <- arrivals_between arr_seq t1 t2 | P x] ->
job_cost j = service_during sched j t1 t_compl
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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
all
(fun x : Job =>
service_during sched x t1 t_compl == job_cost x)
[seq x <- arrivals_between arr_seq t1 t2 | P x] ->
job_cost j = service_during sched j t1 t_compl
move => /allP/(_ j) + /ltac :(apply /esym/eqP); apply .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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
j \in [seq x <- arrivals_between arr_seq t1 t2 | P x]
by rewrite mem_filter Pj. } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 i : Job,
i \in arrivals_between arr_seq t1 t2 ->
P i -> service_during sched i t1 t_compl <= job_cost i
by intros ; apply cumulative_service_le_job_cost; eauto .
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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 => [|//].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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) => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job}.
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 , service_of_jobs_at sched P jobs t <= 1 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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,
service_of_jobs_at sched P jobs t <= 1
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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,
service_of_jobs_at sched P jobs t <= 1
intros t.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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
service_of_jobs_at sched P jobs t <= 1
eapply leq_trans.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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
service_of_jobs_at sched P jobs t <= ?n
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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
service_of_jobs_at sched P jobs 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 : ProcessorState Job 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 ; elim : jobs H_no_duplicate_jobs => [|j js IHjs] uniq_js.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 uniq_js : uniq [::]
\sum_(i <- [::]) service_at sched i t <= 1
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 uniq_js : uniq [::]
\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 : ProcessorState Job 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 j : Job js : seq Job IHjs : uniq js ->
\sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js)
\sum_(i <- (j :: js)) service_at sched i t <= 1
feed IHjs; first by move : uniq_js; rewrite cons_uniq => /andP [_ U]. Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 j : Job js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js)
\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 : ProcessorState Job 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 j : Job js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js)
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 : ProcessorState Job 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 j : Job js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js) 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 : ProcessorState Job 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 j : Job js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js) 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 : ProcessorState Job 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 j : Job js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js) 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 : ProcessorState Job 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 j : Job js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js) 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 : ProcessorState Job 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 j : Job js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js) 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 : ProcessorState Job 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 j : Job js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js) 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 : ProcessorState Job 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 j : Job js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js) 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 : ProcessorState Job 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 j : Job js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js) 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 : ProcessorState Job 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 j : Job js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js) 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 : ProcessorState Job 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 j : Job js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js) 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 : ProcessorState Job 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 : seq Job H_no_duplicate_jobs : uniq jobs t : instant js : seq Job IHjs : \sum_(i <- js) service_at sched i t <= 1 uniq_js : uniq (j :: js) O : service_at sched j t = 1 POS, SCHED : scheduled_at sched j t IN : j \in js
False
by move : uniq_js; 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 : ProcessorState Job 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 : ProcessorState Job 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 + Δ) <= Δ
move => t Δ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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
move => t1 t2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : ProcessorState Job 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 : service_of_jobs_at sched P jobs 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 : ProcessorState Job 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 : service_of_jobs_at sched P jobs t' <= 1
\sum_(i <- jobs | P i) service_at sched i t' <=
service_of_jobs_at sched P jobs t'
by rewrite leq_sum.
Qed .
End ServiceOfJobsIsBoundedByLength .
(** In this section, we prove a relation between a predicate defined
on a set of jobs and the total service of these jobs. *)
Section PredServedEqService .
(** Assume that the arrival sequence does not contain duplicate
arrivals. *)
Hypothesis H_arrival_sequence_is_a_set : arrival_sequence_uniq arr_seq.
(** Consider a JLFP-policy that indicates a higher-or-equal
priority relation. *)
Context {JLFP : JLFP_policy Job}.
(** Consider a job [j]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
(** We consider an arbitrary time interval <<[t1, t)>> that starts
with a quiet time. *)
Variable t1 t : instant.
Hypothesis H_quiet_time : quiet_time arr_seq sched j t1.
(** We prove that the number of points in the interval that
satisfy the predicate [exists j ∈ served jobs: P j] is equal to the
total service of all jobs that satisfy [P].
Note that this lemma uses [served_jobs_at] instead of its
uniprocessor variant [served_job_at]. This is done on purpose
so that this lemma fits better with abstract functions and
predicates defined in [/analysis/abstract/...] since such
functions are usually defined on a general (not necessarily
uniprocessor) class of processor models. *)
Lemma cumulative_pred_served_eq_service :
(forall j' , P j' -> hep_job j' j) ->
\sum_(t1 <= t' < t) has P (served_jobs_at arr_seq sched t')
= service_of_jobs sched P (arrivals_between arr_seq t1 t) t1 t.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1
(forall j' : Job, P j' -> hep_job j' j) ->
\sum_(t1 <= t' < t)
has P (served_jobs_at arr_seq sched t') =
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t1 t
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1
(forall j' : Job, P j' -> hep_job j' j) ->
\sum_(t1 <= t' < t)
has P (served_jobs_at arr_seq sched t') =
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t1 t
move => Phep.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' j
\sum_(t1 <= t' < t)
has P (served_jobs_at arr_seq sched t') =
service_of_jobs sched P
(arrivals_between arr_seq t1 t) t1 t
rewrite [RHS]exchange_big /=; apply : eq_big_nat => x /andP[t1lex xltt].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t
has P (served_jobs_at arr_seq sched x) =
\sum_(i <- arrivals_between arr_seq t1 t | P i)
service_at sched i x
have L (js : seq Job) (UNIQ : uniq js):
\sum_(i <- js | P i) service_at sched i x
= has (fun j => (P j) && (receives_service_at sched j x)) js.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t js : seq Job UNIQ : uniq js
\sum_(i <- js | P i) service_at sched i x =
has
(fun j : Job => P j && receives_service_at sched j x)
js
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t js : seq Job UNIQ : uniq js
\sum_(i <- js | P i) service_at sched i x =
has
(fun j : Job => P j && receives_service_at sched j x)
js
clear xltt t1lex Phep.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 x : nat js : seq Job UNIQ : uniq js
\sum_(i <- js | P i) service_at sched i x =
has
(fun j : Job => P j && receives_service_at sched j x)
js
have L : forall (n : nat) (b : bool), (b -> n = 1 ) -> (~~ b -> n = 0 ) -> (n = b)
by clear ; move => n [] A B; [rewrite A | rewrite B].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 x : nat js : seq Job UNIQ : uniq js L : forall (n : nat) (b : bool),
(b -> n = 1 ) -> (~~ b -> n = 0 ) -> n = b
\sum_(i <- js | P i) service_at sched i x =
has
(fun j : Job => P j && receives_service_at sched j x)
js
apply : L.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 x : nat js : seq Job UNIQ : uniq js
has
(fun j : Job => P j && receives_service_at sched j x)
js -> \sum_(i <- js | P i) service_at sched i x = 1
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 x : nat js : seq Job UNIQ : uniq js
has
(fun j : Job => P j && receives_service_at sched j x)
js -> \sum_(i <- js | P i) service_at sched i x = 1
move => /hasP [jo IN /andP [Pjo SERVjo]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 x : nat js : seq Job UNIQ : uniq js jo : Job IN : jo \in js Pjo : P jo SERVjo : receives_service_at sched jo x
\sum_(i <- js | P i) service_at sched i x = 1
apply /eqP; rewrite eqn_leq; apply /andP; split .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 x : nat js : seq Job UNIQ : uniq js jo : Job IN : jo \in js Pjo : P jo SERVjo : receives_service_at sched jo x
\sum_(i <- js | P i) service_at sched i x <= 1
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 x : nat js : seq Job UNIQ : uniq js jo : Job IN : jo \in js Pjo : P jo SERVjo : receives_service_at sched jo x
\sum_(i <- js | P i) service_at sched i x <= 1
by apply service_of_jobs_le_1 => //.
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 x : nat js : seq Job UNIQ : uniq js jo : Job IN : jo \in js Pjo : P jo SERVjo : receives_service_at sched jo x
0 < \sum_(i <- js | P i) service_at sched i x
by rewrite sum_nat_gt0; apply /hasP; exists jo => //; rewrite mem_filter IN Pjo. } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 x : nat js : seq Job UNIQ : uniq js
~~
has
(fun j : Job => P j && receives_service_at sched j x)
js -> \sum_(i <- js | P i) service_at sched i x = 0
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 x : nat js : seq Job UNIQ : uniq js
~~
has
(fun j : Job => P j && receives_service_at sched j x)
js -> \sum_(i <- js | P i) service_at sched i x = 0
move => /hasPn ALL; rewrite big1_seq // => jo /andP [Pjo IN].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 x : nat js : seq Job UNIQ : uniq js ALL : {in js,
forall x0 : Job,
~~ (P x0 && receives_service_at sched x0 x)} jo : Job Pjo : P jo IN : jo \in js
service_at sched jo x = 0
move : (ALL _ IN); rewrite negb_and => /orP [A | B]; first by rewrite Pjo in A.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 x : nat js : seq Job UNIQ : uniq js ALL : {in js,
forall x0 : Job,
~~ (P x0 && receives_service_at sched x0 x)} jo : Job Pjo : P jo IN : jo \in js B : ~~ receives_service_at sched jo x
service_at sched jo x = 0
by move : B; rewrite /receives_service_at -leqNgt leqn0 => /eqP ->. } } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t L : forall js : seq Job,
uniq js ->
\sum_(i <- js | P i) service_at sched i x =
has
(fun j : Job =>
P j && receives_service_at sched j x) js
has P (served_jobs_at arr_seq sched x) =
\sum_(i <- arrivals_between arr_seq t1 t | P i)
service_at sched i x
rewrite L; clear L; last by apply arrivals_uniq.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t
has P (served_jobs_at arr_seq sched x) =
has
(fun j : Job => P j && receives_service_at sched j x)
(arrivals_between arr_seq t1 t)
have L :
forall (X : Type ) (P Q : pred X) (xs : seq X),
has (fun x => P x && Q x) xs = has P ([ seq x <- xs | Q x]).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t
forall (X : Type ) (P Q : pred X) (xs : seq X),
has (fun x : X => P x && Q x) xs =
has P [seq x <- xs | Q x]
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t
forall (X : Type ) (P Q : pred X) (xs : seq X),
has (fun x : X => P x && Q x) xs =
has P [seq x <- xs | Q x]
clear .forall (X : Type ) (P Q : pred X) (xs : seq X),
has (fun x : X => P x && Q x) xs =
has P [seq x <- xs | Q x]
move => X P Q xs; induction xs as [ | x xs IHxs]; first by done .X : Type P, Q : pred X x : X xs : seq X IHxs : has (fun x : X => P x && Q x) xs =
has P [seq x <- xs | Q x]
has (fun x : X => P x && Q x) (x :: xs) =
has P [seq x <- x :: xs | Q x]
by rewrite //= IHxs; destruct (P x) eqn :Px, (Q x) eqn :Qx; rewrite //= ?Px ?Qx . } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t L : forall (X : Type ) (P Q : pred X) (xs : seq X),
has (fun x : X => P x && Q x) xs =
has P [seq x <- xs | Q x]
has P (served_jobs_at arr_seq sched x) =
has
(fun j : Job => P j && receives_service_at sched j x)
(arrivals_between arr_seq t1 t)
rewrite -L; clear L; f_equal .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t
has
(fun x0 : Job =>
P x0 && receives_service_at sched x0 x)
(arrivals_up_to arr_seq x) =
has
(fun j : Job => P j && receives_service_at sched j x)
(arrivals_between arr_seq t1 t)
rewrite /arrivals_up_to (arrivals_between_cat _ _ t1); [ | lia | lia ].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t
has
(fun x0 : Job =>
P x0 && receives_service_at sched x0 x)
(arrivals_between arr_seq 0 t1 ++
arrivals_between arr_seq t1 x.+1 ) =
has
(fun j : Job => P j && receives_service_at sched j x)
(arrivals_between arr_seq t1 t)
rewrite has_cat -[RHS]orFb; f_equal .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t
has
(fun x0 : Job =>
P x0 && receives_service_at sched x0 x)
(arrivals_between arr_seq 0 t1) = false
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t
has
(fun x0 : Job =>
P x0 && receives_service_at sched x0 x)
(arrivals_between arr_seq 0 t1) = false
apply /eqP; rewrite eqbF_neg; apply /hasPn => jo IN; apply /negP => /andP [Pjo SERV].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t jo : Job IN : jo \in arrivals_between arr_seq 0 t1 Pjo : P jo SERV : receives_service_at sched jo x
False
apply service_at_implies_scheduled_at, scheduled_implies_not_completed in SERV => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t jo : Job IN : jo \in arrivals_between arr_seq 0 t1 Pjo : P jo SERV : ~~ completed_by sched jo x
False
move : SERV => /negP SERV; apply :SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t jo : Job IN : jo \in arrivals_between arr_seq 0 t1 Pjo : P jo
completed_by sched jo x
(eapply completion_monotonic; last apply : H_quiet_time) => //. Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t jo : Job IN : jo \in arrivals_between arr_seq 0 t1 Pjo : P jo
arrives_in arr_seq jo
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t jo : Job IN : jo \in arrivals_between arr_seq 0 t1 Pjo : P jo
arrives_in arr_seq jo
by apply : in_arrivals_implies_arrived.
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t jo : Job IN : jo \in arrivals_between arr_seq 0 t1 Pjo : P jo
arrived_before jo t1
by apply : job_arrival_between_lt.
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t
has
(fun x0 : Job =>
P x0 && receives_service_at sched x0 x)
(arrivals_between arr_seq t1 x.+1 ) =
has
(fun j : Job => P j && receives_service_at sched j x)
(arrivals_between arr_seq t1 t)
rewrite [in RHS](arrivals_between_cat _ _ x.+1 ); [ | lia | lia ].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t
has
(fun x0 : Job =>
P x0 && receives_service_at sched x0 x)
(arrivals_between arr_seq t1 x.+1 ) =
has
(fun j : Job => P j && receives_service_at sched j x)
(arrivals_between arr_seq t1 x.+1 ++
arrivals_between arr_seq x.+1 t)
rewrite has_cat -[LHS]orbF; f_equal ; symmetry .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t
has
(fun j : Job => P j && receives_service_at sched j x)
(arrivals_between arr_seq x.+1 t) = false
apply /eqP; rewrite eqbF_neg; apply /hasPn => jo IN; apply /negP => /andP [Pjo SERV].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t jo : Job IN : jo \in arrivals_between arr_seq x.+1 t Pjo : P jo SERV : receives_service_at sched jo x
False
apply service_at_implies_scheduled_at in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t jo : Job IN : jo \in arrivals_between arr_seq x.+1 t Pjo : P jo SERV : scheduled_at sched jo x
False
apply H_jobs_must_arrive_to_execute in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t jo : Job IN : jo \in arrivals_between arr_seq x.+1 t Pjo : P jo SERV : has_arrived jo x
False
apply job_arrival_between_ge in IN => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job 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 H_arrival_sequence_is_a_set : arrival_sequence_uniq
arr_seq JLFP : JLFP_policy Job j : Job H_j_arrives : arrives_in arr_seq j t1, t : instant H_quiet_time : quiet_time arr_seq sched j t1 Phep : forall j' : Job, P j' -> hep_job j' jx : nat t1lex : t1 <= x xltt : x < t jo : Job IN : x < job_arrival jo Pjo : P jo SERV : has_arrived jo x
False
by move : IN SERV; rewrite /has_arrived; lia .
Qed .
End PredServedEqService .
End UnitServiceUniProcessorModelLemmas .