Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.model.aggregate.workload.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.model.aggregate.service_of_jobs.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.behavior.completion.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** * 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 with H0; auto .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 ) =
addn_comoid
(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
induction 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 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 ALL : forall j : Job,
j \in a :: l ->
~~ (P j && scheduled_at sched j t)IHl : (forall j : Job,
j \in l -> ~~ (P j && scheduled_at sched j t)) ->
service_of_jobs_at sched P l t = 0
service_of_jobs_at sched P (a :: l) 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 a : Job l : seq Job ALL : forall j : Job,
j \in a :: l ->
~~ (P j && scheduled_at sched j t)IHl : (forall j : Job,
j \in l -> ~~ (P j && scheduled_at sched j t)) ->
service_of_jobs_at sched P l t = 0
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 ALL : forall j : Job,
j \in a :: l ->
~~ (P j && scheduled_at sched j t)IHl : (forall j : Job,
j \in l -> ~~ (P j && scheduled_at sched j t)) ->
service_of_jobs_at sched P l t = 0
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 ALL : forall j : Job,
j \in a :: l ->
~~ (P j && scheduled_at sched j t)IHl : (forall j : Job,
j \in l -> ~~ (P j && scheduled_at sched j t)) ->
service_of_jobs_at sched P l t = 0
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 ALL : forall j : Job,
j \in a :: l ->
~~ (P j && scheduled_at sched j t)IHl : service_of_jobs_at sched P l t = 0
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; last by done .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 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; last by done .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 intros ; destruct (a < b) eqn :EQU; apply /orP;
[by left |right ]; apply negbT in EQU; rewrite leqNgt. } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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; last by rewrite ltnW.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
- 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; last by done .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); try done .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
+ 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
- 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
+ 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
- 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 ; induction jobs as [ | j 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 [::] t : instant
\sum_(i <- [::]) service_at sched i t <= 1
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 [::] t : instant
\sum_(i <- [::]) service_at sched i t <= 1
by rewrite big_nil.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : uniq js ->
\sum_(i <- js) service_at sched i t <= 1
\sum_(i <- (j :: js)) service_at sched i t <= 1
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : uniq js ->
\sum_(i <- js) service_at sched i t <= 1
\sum_(i <- (j :: js)) service_at sched i t <= 1
feed IHjs; first by move : H_no_duplicate_jobs; rewrite cons_uniq => /andP [_ U]. Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1
\sum_(i <- (j :: js)) service_at sched i t <= 1
rewrite big_cons.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1
service_at sched j t +
\sum_(j <- js) service_at sched j t <= 1
destruct (service_is_zero_or_one H_unit_service_proc_model sched j t) as [Z | O].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 Z : service_at sched j t = 0
service_at sched j t +
\sum_(j <- js) service_at sched j t <= 1
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 Z : service_at sched j t = 0
service_at sched j t +
\sum_(j <- js) service_at sched j t <= 1
by rewrite Z (leqRW IHjs).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1
service_at sched j t +
\sum_(j <- js) service_at sched j t <= 1
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1
service_at sched j t +
\sum_(j <- js) service_at sched j t <= 1
have -> : \sum_(j <- js) service_in j (sched t) = 0 ; last by rewrite O.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1
\sum_(j <- js) service_in j (sched t) = 0
have POS: service_at sched j t > 0 by rewrite O.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS : 0 < service_at sched j t
\sum_(j <- js) service_in j (sched t) = 0
apply service_at_implies_scheduled_at in POS.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS : scheduled_at sched j t
\sum_(j <- js) service_in j (sched t) = 0
apply /eqP; rewrite big_seq big1 //; intros j' IN.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS : scheduled_at sched j t j' : Job IN : j' \in js
service_in j' (sched t) = 0
apply /eqP; rewrite -leqn0 leqNgt.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS : scheduled_at sched j t j' : Job IN : j' \in js
~~ (0 < service_in j' (sched t))
eapply contra with (b := scheduled_at sched j' t);
first apply service_at_implies_scheduled_at.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS : scheduled_at sched j t j' : Job IN : j' \in js
~~ scheduled_at sched j' t
apply /negP; intros SCHED.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 j : Job js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS : scheduled_at sched j t j' : Job IN : j' \in js SCHED : scheduled_at sched j' t
False
specialize (H_uniprocessor_model _ _ _ _ POS SCHED); subst j'.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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, js : seq Job H_no_duplicate_jobs : uniq (j :: js) t : instant IHjs : \sum_(i <- js) service_at sched i t <= 1 O : service_at sched j t = 1 POS, SCHED : scheduled_at sched j t IN : j \in js
False
by move : H_no_duplicate_jobs; rewrite cons_uniq => /andP [/negP NIN _].
Qed .
(** Next, we prove that the service received by those jobs is no larger
than their workload. *)
Corollary service_of_jobs_le_length_of_interval :
forall (t : instant) (Δ : duration),
service_of_jobs sched P jobs t (t + Δ) <= Δ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : 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 + Δ) <= Δ
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 Δ : 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
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 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 .
End UnitServiceUniProcessorModelLemmas .