Built with
Alectryon , running Coq+SerAPI v8.14.0+0.14.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.util.all .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.behavior.all .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.processor.platform_properties.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.definitions.schedule_prefix.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]
(** * Service *)
(** In this file, we establish basic facts about the service received by
jobs. *)
(** To begin with, we provide some simple but handy rewriting rules for
[service] and [service_during]. *)
Section Composition .
(** Consider any job type and any processor state. *)
Context {Job : JobType}.
Context {PState : Type }.
Context `{ProcessorState Job PState}.
(** For any given schedule... *)
Variable sched : schedule PState.
(** ...and any given job... *)
Variable j : Job.
(** ...we establish a number of useful rewriting rules that decompose
the service received during an interval into smaller intervals. *)
(** As a trivial base case, no job receives any service during an empty
interval. *)
Lemma service_during_geq :
forall t1 t2 ,
t1 >= t2 -> service_during sched j t1 t2 = 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : nat,
t2 <= t1 -> service_during sched j t1 t2 = 0
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : nat,
t2 <= t1 -> service_during sched j t1 t2 = 0
move => t1 t2 t1t2.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : nat t1t2 : t2 <= t1
service_during sched j t1 t2 = 0
by rewrite /service_during big_geq //.
Qed .
(** Equally trivially, no job has received service prior to time zero. *)
Corollary service0 :
service sched j 0 = 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
service sched j 0 = 0
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
service sched j 0 = 0
by rewrite /service service_during_geq //.
Qed .
(** Trivially, an interval consisting of one time unit is equivalent to
[service_at]. *)
Lemma service_during_instant :
forall t ,
service_during sched j t t.+1 = service_at sched j t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
service_during sched j t t.+1 = service_at sched j t
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
service_during sched j t t.+1 = service_at sched j t
move => t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t : instant
service_during sched j t t.+1 = service_at sched j t
by rewrite /service_during big_nat_recr ?big_geq //.
Qed .
(** Next, we observe that we can look at the service received during an
interval <<[t1, t3)>> as the sum of the service during [t1, t2) and [t2, t3)
for any t2 \in [t1, t3]. (The "_cat" suffix denotes the concatenation of
the two intervals.) *)
Lemma service_during_cat :
forall t1 t2 t3 ,
t1 <= t2 <= t3 ->
(service_during sched j t1 t2) + (service_during sched j t2 t3)
= service_during sched j t1 t3.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 t3 : nat,
t1 <= t2 <= t3 ->
service_during sched j t1 t2 +
service_during sched j t2 t3 =
service_during sched j t1 t3
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 t3 : nat,
t1 <= t2 <= t3 ->
service_during sched j t1 t2 +
service_during sched j t2 t3 =
service_during sched j t1 t3
move => t1 t2 t3 /andP [t1t2 t2t3].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2, t3 : nat t1t2 : t1 <= t2 t2t3 : t2 <= t3
service_during sched j t1 t2 +
service_during sched j t2 t3 =
service_during sched j t1 t3
by rewrite /service_during -big_cat_nat /=.
Qed .
(** Since [service] is just a special case of [service_during], the same holds
for [service]. *)
Lemma service_cat :
forall t1 t2 ,
t1 <= t2 ->
(service sched j t1) + (service_during sched j t1 t2)
= service sched j t2.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : nat,
t1 <= t2 ->
service sched j t1 + service_during sched j t1 t2 =
service sched j t2
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : nat,
t1 <= t2 ->
service sched j t1 + service_during sched j t1 t2 =
service sched j t2
move => t1 t2 t1t2.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : nat t1t2 : t1 <= t2
service sched j t1 + service_during sched j t1 t2 =
service sched j t2
by rewrite /service service_during_cat //.
Qed .
(** As a special case, we observe that the service during an interval can be
decomposed into the first instant and the rest of the interval. *)
Lemma service_during_first_plus_later :
forall t1 t2 ,
t1 < t2 ->
(service_at sched j t1) + (service_during sched j t1.+1 t2)
= service_during sched j t1 t2.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : nat,
t1 < t2 ->
service_at sched j t1 +
service_during sched j t1.+1 t2 =
service_during sched j t1 t2
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : nat,
t1 < t2 ->
service_at sched j t1 +
service_during sched j t1.+1 t2 =
service_during sched j t1 t2
move => t1 t2 t1t2.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : nat t1t2 : t1 < t2
service_at sched j t1 +
service_during sched j t1.+1 t2 =
service_during sched j t1 t2
have TIMES: t1 <= t1.+1 <= t2 by rewrite /(_ && _) ifT //.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : nat t1t2 : t1 < t2 TIMES : t1 <= t1.+1 <= t2
service_at sched j t1 +
service_during sched j t1.+1 t2 =
service_during sched j t1 t2
have SPLIT := service_during_cat t1 t1.+1 t2 TIMES.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : nat t1t2 : t1 < t2 TIMES : t1 <= t1.+1 <= t2 SPLIT : service_during sched j t1 t1.+1 +
service_during sched j t1.+1 t2 =
service_during sched j t1 t2
service_at sched j t1 +
service_during sched j t1.+1 t2 =
service_during sched j t1 t2
by rewrite -service_during_instant //.
Qed .
(** Symmetrically, we have the same for the end of the interval. *)
Lemma service_during_last_plus_before :
forall t1 t2 ,
t1 <= t2 ->
(service_during sched j t1 t2) + (service_at sched j t2)
= service_during sched j t1 t2.+1 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : nat,
t1 <= t2 ->
service_during sched j t1 t2 + service_at sched j t2 =
service_during sched j t1 t2.+1
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : nat,
t1 <= t2 ->
service_during sched j t1 t2 + service_at sched j t2 =
service_during sched j t1 t2.+1
move => t1 t2 t1t2.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : nat t1t2 : t1 <= t2
service_during sched j t1 t2 + service_at sched j t2 =
service_during sched j t1 t2.+1
rewrite -(service_during_cat t1 t2 t2.+1 ); last by rewrite /(_ && _) ifT //.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : nat t1t2 : t1 <= t2
service_during sched j t1 t2 + service_at sched j t2 =
service_during sched j t1 t2 +
service_during sched j t2 t2.+1
by rewrite service_during_instant //.
Qed .
(** And hence also for [service]. *)
Corollary service_last_plus_before :
forall t ,
(service sched j t) + (service_at sched j t)
= service sched j t.+1 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
service sched j t + service_at sched j t =
service sched j t.+1
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
service sched j t + service_at sched j t =
service sched j t.+1
move => t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t : instant
service sched j t + service_at sched j t =
service sched j t.+1
by rewrite /service -service_during_last_plus_before //.
Qed .
(** Finally, we deconstruct the service received during an interval <<[t1, t3)>>
into the service at a midpoint t2 and the service in the intervals before
and after. *)
Lemma service_split_at_point :
forall t1 t2 t3 ,
t1 <= t2 < t3 ->
(service_during sched j t1 t2) + (service_at sched j t2) + (service_during sched j t2.+1 t3)
= service_during sched j t1 t3.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 t3 : nat,
t1 <= t2 < t3 ->
service_during sched j t1 t2 + service_at sched j t2 +
service_during sched j t2.+1 t3 =
service_during sched j t1 t3
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 t3 : nat,
t1 <= t2 < t3 ->
service_during sched j t1 t2 + service_at sched j t2 +
service_during sched j t2.+1 t3 =
service_during sched j t1 t3
move => t1 t2 t3 /andP [t1t2 t2t3].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2, t3 : nat t1t2 : t1 <= t2 t2t3 : t2 < t3
service_during sched j t1 t2 + service_at sched j t2 +
service_during sched j t2.+1 t3 =
service_during sched j t1 t3
rewrite -addnA service_during_first_plus_later// service_during_cat// /(_ && _) ifT//.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2, t3 : nat t1t2 : t1 <= t2 t2t3 : t2 < t3
t2 <= t3
by exact : ltnW.
Qed .
End Composition .
(** As a common special case, we establish facts about schedules in which a
job receives either 1 or 0 service units at all times. *)
Section UnitService .
(** Consider any job type and any processor state. *)
Context {Job : JobType}.
Context {PState : Type }.
Context `{ProcessorState Job PState}.
(** Let's consider a unit-service model... *)
Hypothesis H_unit_service : unit_service_proc_model PState.
(** ...and a given schedule. *)
Variable sched : schedule PState.
(** Let [j] be any job that is to be scheduled. *)
Variable j : Job.
(** First, we prove that the instantaneous service cannot be greater than 1, ... *)
Lemma service_at_most_one :
forall t , service_at sched j t <= 1 .Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall t : instant, service_at sched j t <= 1
Proof .Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall t : instant, service_at sched j t <= 1
by move => t; rewrite /service_at.
Qed .
(** ... which implies that the instantaneous service always equals to 0 or 1. *)
Corollary service_is_zero_or_one :
forall t , service_at sched j t = 0 \/ service_at sched j t = 1 .Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall t : instant,
service_at sched j t = 0 \/ service_at sched j t = 1
Proof .Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall t : instant,
service_at sched j t = 0 \/ service_at sched j t = 1
intros .Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant
service_at sched j t = 0 \/ service_at sched j t = 1
have Lewf := service_at_most_one t.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant Lewf : service_at sched j t <= 1
service_at sched j t = 0 \/ service_at sched j t = 1
remember (service_at sched j t) as ρ.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant ρ : work Heqρ : ρ = service_at sched j t Lewf : ρ <= 1
ρ = 0 \/ ρ = 1
by destruct ρ; last destruct ρ; [left | right | exfalso ].
Qed .
(** Next we prove that the cumulative service received by job [j] in
any interval of length [delta] is at most [delta]. *)
Lemma cumulative_service_le_delta :
forall t delta , service_during sched j t (t + delta) <= delta.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall (t : instant) (delta : nat),
service_during sched j t (t + delta) <= delta
Proof .Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall (t : instant) (delta : nat),
service_during sched j t (t + delta) <= delta
unfold service_during; intros t delta.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat
\sum_(t <= t < t + delta) service_at sched j t <=
delta
apply leq_trans with (n := \sum_(t <= t0 < t + delta) 1 );
last by rewrite sum_of_ones.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat
\sum_(t <= t < t + delta) service_at sched j t <=
\sum_(t <= t0 < t + delta) 1
by apply : leq_sum => t' _; apply : service_at_most_one.
Qed .
(** Conversely, we prove that if the cumulative service received by
job [j] in an interval of length [delta] is greater than or
equal to [ρ], then [ρ ≤ delta]. *)
Lemma cumulative_service_ge_delta :
forall t delta ρ ,
ρ <= service_during sched j t (t + delta) ->
ρ <= delta.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall (t : instant) (delta ρ : nat),
ρ <= service_during sched j t (t + delta) ->
ρ <= delta
Proof .Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
forall (t : instant) (delta ρ : nat),
ρ <= service_during sched j t (t + delta) ->
ρ <= delta
induction delta; intros ? LE.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant ρ : nat LE : ρ <= service_during sched j t (t + 0 )
ρ <= 0
- Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant ρ : nat LE : ρ <= service_during sched j t (t + 0 )
ρ <= 0
by rewrite service_during_geq in LE; ssrlia.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat IHdelta : forall ρ : nat,
ρ <= service_during sched j t (t + delta) ->
ρ <= deltaρ : nat LE : ρ <= service_during sched j t (t + delta.+1 )
ρ <= delta.+1
- Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat IHdelta : forall ρ : nat,
ρ <= service_during sched j t (t + delta) ->
ρ <= deltaρ : nat LE : ρ <= service_during sched j t (t + delta.+1 )
ρ <= delta.+1
rewrite addnS -service_during_last_plus_before in LE; last by ssrlia.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat IHdelta : forall ρ : nat,
ρ <= service_during sched j t (t + delta) ->
ρ <= deltaρ : nat LE : ρ <=
service_during sched j t (t + delta) +
service_at sched j (t + delta)
ρ <= delta.+1
destruct (service_is_zero_or_one (t + delta)) as [EQ|EQ]; rewrite EQ in LE.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat IHdelta : forall ρ : nat,
ρ <= service_during sched j t (t + delta) ->
ρ <= deltaρ : nat EQ : service_at sched j (t + delta) = 0 LE : ρ <= service_during sched j t (t + delta) + 0
ρ <= delta.+1
+ Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat IHdelta : forall ρ : nat,
ρ <= service_during sched j t (t + delta) ->
ρ <= deltaρ : nat EQ : service_at sched j (t + delta) = 0 LE : ρ <= service_during sched j t (t + delta) + 0
ρ <= delta.+1
rewrite addn0 in LE.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat IHdelta : forall ρ : nat,
ρ <= service_during sched j t (t + delta) ->
ρ <= deltaρ : nat EQ : service_at sched j (t + delta) = 0 LE : ρ <= service_during sched j t (t + delta)
ρ <= delta.+1
by apply IHdelta in LE; rewrite (leqRW LE).Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat IHdelta : forall ρ : nat,
ρ <= service_during sched j t (t + delta) ->
ρ <= deltaρ : nat EQ : service_at sched j (t + delta) = 1 LE : ρ <= service_during sched j t (t + delta) + 1
ρ <= delta.+1
+ Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat IHdelta : forall ρ : nat,
ρ <= service_during sched j t (t + delta) ->
ρ <= deltaρ : nat EQ : service_at sched j (t + delta) = 1 LE : ρ <= service_during sched j t (t + delta) + 1
ρ <= delta.+1
rewrite addn1 in LE.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat IHdelta : forall ρ : nat,
ρ <= service_during sched j t (t + delta) ->
ρ <= deltaρ : nat EQ : service_at sched j (t + delta) = 1 LE : ρ <= (service_during sched j t (t + delta)).+1
ρ <= delta.+1
destruct ρ; first by done .Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant delta : nat IHdelta : forall ρ : nat,
ρ <= service_during sched j t (t + delta) ->
ρ <= deltaρ : nat EQ : service_at sched j (t + delta) = 1 LE : ρ < (service_during sched j t (t + delta)).+1
ρ < delta.+1
by rewrite ltnS in LE; apply IHdelta in LE; rewrite (leqRW LE).
Qed .
Section ServiceIsUnitGrowthFunction .
(** We show that the service received by any job [j] is a unit growth function. *)
Lemma service_is_unit_growth_function :
unit_growth_function (service sched j).Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
unit_growth_function (service sched j)
Proof .Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job
unit_growth_function (service sched j)
rewrite /unit_growth_function => t.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : nat
service sched j (t + 1 ) <= service sched j t + 1
rewrite addn1 -service_last_plus_before leq_add2l.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : nat
service_at sched j t <= 1
by apply service_at_most_one.
Qed .
(** Next, consider any time [t]... *)
Variable t : instant.
(** ...and let [s] be any value less than the service received
by job [j] by time [t]. *)
Variable s : duration.
Hypothesis H_less_than_s : s < service sched j t.
(** Then, we show that there exists an earlier time [t'] where job
[j] had [s] units of service. *)
Corollary exists_intermediate_service :
exists t' ,
t' < t /\
service sched j t' = s.Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant s : duration H_less_than_s : s < service sched j t
exists t' : nat, t' < t /\ service sched j t' = s
Proof .Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant s : duration H_less_than_s : s < service sched j t
exists t' : nat, t' < t /\ service sched j t' = s
feed (exists_intermediate_point (service sched j));
[by apply service_is_unit_growth_function | intros EX]. Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant s : duration H_less_than_s : s < service sched j t EX : forall x1 x2 : nat,
x1 <= x2 ->
forall y : nat,
service sched j x1 <= y < service sched j x2 ->
exists x_mid : nat,
x1 <= x_mid < x2 /\ service sched j x_mid = y
exists t' : nat, t' < t /\ service sched j t' = s
feed (EX 0 t); first by done . Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant s : duration H_less_than_s : s < service sched j t EX : forall y : nat,
service sched j 0 <= y < service sched j t ->
exists x_mid : nat,
0 <= x_mid < t /\ service sched j x_mid = y
exists t' : nat, t' < t /\ service sched j t' = s
feed (EX s); first by rewrite /service /service_during big_geq //. Job : JobType PState : Type H : ProcessorState Job PState H_unit_service : unit_service_proc_model PState sched : schedule PState j : Job t : instant s : duration H_less_than_s : s < service sched j t EX : exists x_mid : nat,
0 <= x_mid < t /\ service sched j x_mid = s
exists t' : nat, t' < t /\ service sched j t' = s
by move : EX => /= [x_mid EX]; exists x_mid .
Qed .
End ServiceIsUnitGrowthFunction .
End UnitService .
(** We establish a basic fact about the monotonicity of service. *)
Section Monotonicity .
(** Consider any job type and any processor model. *)
Context {Job : JobType}.
Context {PState : Type }.
Context `{ProcessorState Job PState}.
(** Consider any given schedule... *)
Variable sched : schedule PState.
(** ...and a given job that is to be scheduled. *)
Variable j : Job.
(** We observe that the amount of service received is monotonic by definition. *)
Lemma service_monotonic :
forall t1 t2 ,
t1 <= t2 ->
service sched j t1 <= service sched j t2.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : nat,
t1 <= t2 -> service sched j t1 <= service sched j t2
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : nat,
t1 <= t2 -> service sched j t1 <= service sched j t2
move => t1 t2 let 1 t2 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : nat let1t2 : t1 <= t2
service sched j t1 <= service sched j t2
by rewrite -(service_cat sched j t1 t2 let 1 t2 ); apply : leq_addr.
Qed .
End Monotonicity .
(** Consider any job type and any processor model. *)
Section RelationToScheduled .
Context {Job : JobType}.
Context {PState : Type }.
Context `{ProcessorState Job PState}.
(** Consider any given schedule... *)
Variable sched : schedule PState.
(** ...and a given job that is to be scheduled. *)
Variable j : Job.
(** We observe that a job that isn't scheduled cannot possibly receive service. *)
Lemma not_scheduled_implies_no_service :
forall t ,
~~ scheduled_at sched j t -> service_at sched j t = 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
~~ scheduled_at sched j t -> service_at sched j t = 0
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
~~ scheduled_at sched j t -> service_at sched j t = 0
rewrite /service_at /scheduled_at.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
~~ scheduled_in j (sched t) ->
service_in j (sched t) = 0
move => t NOT_SCHED.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t : instant NOT_SCHED : ~~ scheduled_in j (sched t)
service_in j (sched t) = 0
by rewrite service_implies_scheduled //.
Qed .
(** Conversely, if a job receives service, then it must be scheduled. *)
Lemma service_at_implies_scheduled_at :
forall t ,
service_at sched j t > 0 -> scheduled_at sched j t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
0 < service_at sched j t -> scheduled_at sched j t
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
0 < service_at sched j t -> scheduled_at sched j t
move => t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t : instant
0 < service_at sched j t -> scheduled_at sched j t
destruct (scheduled_at sched j t) eqn :SCHEDULED; first trivial .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t : instant SCHEDULED : scheduled_at sched j t = false
0 < service_at sched j t -> false
by rewrite not_scheduled_implies_no_service // negbT //.
Qed .
(** Thus, if the cumulative amount of service changes, then it must be
scheduled, too. *)
Lemma service_delta_implies_scheduled :
forall t ,
service sched j t < service sched j t.+1 -> scheduled_at sched j t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
service sched j t < service sched j t.+1 ->
scheduled_at sched j t
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
service sched j t < service sched j t.+1 ->
scheduled_at sched j t
move => t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t : instant
service sched j t < service sched j t.+1 ->
scheduled_at sched j t
rewrite -service_last_plus_before -{1 }(addn0 (service sched j t)) ltn_add2l.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t : instant
0 < service_at sched j t -> scheduled_at sched j t
by apply : service_at_implies_scheduled_at.
Qed .
(** We observe that a job receives cumulative service during some interval iff
it receives services at some specific time in the interval. *)
Lemma service_during_service_at :
forall t1 t2 ,
service_during sched j t1 t2 > 0
<->
exists t ,
t1 <= t < t2 /\
service_at sched j t > 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : instant,
0 < service_during sched j t1 t2 <->
(exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t)
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : instant,
0 < service_during sched j t1 t2 <->
(exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t)
split .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant
0 < service_during sched j t1 t2 ->
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
{ Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant
0 < service_during sched j t1 t2 ->
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
move => NONZERO.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant NONZERO : 0 < service_during sched j t1 t2
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
case (boolP([exists t : 'I_t2,
(t >= t1) && (service_at sched j t > 0 )])) => [EX | ALL].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant NONZERO : 0 < service_during sched j t1 t2EX : [exists t ,
(t1 <= t) && (0 < service_at sched j t)]
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
- Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant NONZERO : 0 < service_during sched j t1 t2EX : [exists t ,
(t1 <= t) && (0 < service_at sched j t)]
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
move : EX => /existsP [x /andP [GE SERV]].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant NONZERO : 0 < service_during sched j t1 t2x : ordinal_finType t2 GE : t1 <= x SERV : 0 < service_at sched j x
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
exists x ; split => //.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant NONZERO : 0 < service_during sched j t1 t2x : ordinal_finType t2 GE : t1 <= x SERV : 0 < service_at sched j x
t1 <= x < t2
apply /andP; by split .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant NONZERO : 0 < service_during sched j t1 t2ALL : ~~
[exists t ,
(t1 <= t) && (0 < service_at sched j t)]
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
- Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant NONZERO : 0 < service_during sched j t1 t2ALL : ~~
[exists t ,
(t1 <= t) && (0 < service_at sched j t)]
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
rewrite negb_exists in ALL; move : ALL => /forallP ALL.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant NONZERO : 0 < service_during sched j t1 t2ALL : forall x : ordinal_finType t2,
~~ ((t1 <= x) && (0 < service_at sched j x))
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
rewrite /service_during big_nat_cond in NONZERO.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant ALL : forall x : ordinal_finType t2,
~~ ((t1 <= x) && (0 < service_at sched j x))NONZERO : 0 <
\sum_(t1 <= i < t2 | (t1 <= i < t2) && true)
service_at sched j i
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
rewrite big1 ?ltn0 // in NONZERO => i.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant ALL : forall x : ordinal_finType t2,
~~ ((t1 <= x) && (0 < service_at sched j x))i : nat
(t1 <= i < t2) && true -> service_at sched j i = 0
rewrite andbT; move => /andP [GT LT].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant ALL : forall x : ordinal_finType t2,
~~ ((t1 <= x) && (0 < service_at sched j x))i : nat GT : t1 <= i LT : i < t2
service_at sched j i = 0
specialize (ALL (Ordinal LT)); simpl in ALL.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant i : nat LT : i < t2 ALL : ~~ ((t1 <= i) && (0 < service_at sched j i)) GT : t1 <= i
service_at sched j i = 0
rewrite GT andTb -eqn0Ngt in ALL.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant i : nat LT : i < t2 GT : t1 <= i ALL : service_at sched j i == 0
service_at sched j i = 0
by apply /eqP => //.
} Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant
(exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t) ->
0 < service_during sched j t1 t2
{ Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant
(exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t) ->
0 < service_during sched j t1 t2
move => [t [TT SERVICE]].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant t : nat TT : t1 <= t < t2 SERVICE : 0 < service_at sched j t
0 < service_during sched j t1 t2
case (boolP (0 < service_during sched j t1 t2)) => // NZ.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant t : nat TT : t1 <= t < t2 SERVICE : 0 < service_at sched j tNZ : ~~ (0 < service_during sched j t1 t2)
0 < service_during sched j t1 t2
exfalso .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant t : nat TT : t1 <= t < t2 SERVICE : 0 < service_at sched j tNZ : ~~ (0 < service_during sched j t1 t2)
False
rewrite -eqn0Ngt in NZ.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant t : nat TT : t1 <= t < t2 SERVICE : 0 < service_at sched j tNZ : service_during sched j t1 t2 == 0
False
move /eqP: NZ.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant t : nat TT : t1 <= t < t2 SERVICE : 0 < service_at sched j t
service_during sched j t1 t2 = 0 -> False
rewrite big_nat_eq0 => IS_ZERO.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant t : nat TT : t1 <= t < t2 SERVICE : 0 < service_at sched j tIS_ZERO : forall i : nat,
t1 <= i < t2 -> service_at sched j i = 0
False
have NO_SERVICE := IS_ZERO t TT.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant t : nat TT : t1 <= t < t2 SERVICE : 0 < service_at sched j tIS_ZERO : forall i : nat,
t1 <= i < t2 -> service_at sched j i = 0 NO_SERVICE : service_at sched j t = 0
False
apply lt0n_neq0 in SERVICE.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant t : nat TT : t1 <= t < t2 SERVICE : service_at sched j t != 0 IS_ZERO : forall i : nat,
t1 <= i < t2 -> service_at sched j i = 0 NO_SERVICE : service_at sched j t = 0
False
by move /neqP in SERVICE; contradiction .
}
Qed .
(** Thus, any job that receives some service during an interval must be
scheduled at some point during the interval... *)
Corollary cumulative_service_implies_scheduled :
forall t1 t2 ,
service_during sched j t1 t2 > 0 ->
exists t ,
t1 <= t < t2 /\
scheduled_at sched j t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : instant,
0 < service_during sched j t1 t2 ->
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t1 t2 : instant,
0 < service_during sched j t1 t2 ->
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t
move => t1 t2.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant
0 < service_during sched j t1 t2 ->
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t
rewrite service_during_service_at.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant
(exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t) ->
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t
move => [t' [TIMES SERVICED]].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant t' : nat TIMES : t1 <= t' < t2 SERVICED : 0 < service_at sched j t'
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t
exists t' ; split => //.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant t' : nat TIMES : t1 <= t' < t2 SERVICED : 0 < service_at sched j t'
scheduled_at sched j t'
by apply : service_at_implies_scheduled_at.
Qed .
(** ...which implies that any job with positive cumulative service must have
been scheduled at some point. *)
Corollary positive_service_implies_scheduled_before :
forall t ,
service sched j t > 0 -> exists t' , (t' < t /\ scheduled_at sched j t').Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
0 < service sched j t ->
exists t' : nat, t' < t /\ scheduled_at sched j t'
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
0 < service sched j t ->
exists t' : nat, t' < t /\ scheduled_at sched j t'
move => t2.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t2 : instant
0 < service sched j t2 ->
exists t' : nat, t' < t2 /\ scheduled_at sched j t'
rewrite /service => NONZERO.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t2 : instant NONZERO : 0 < service_during sched j 0 t2
exists t' : nat, t' < t2 /\ scheduled_at sched j t'
have EX_SCHED := cumulative_service_implies_scheduled 0 t2 NONZERO.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t2 : instant NONZERO : 0 < service_during sched j 0 t2EX_SCHED : exists t : nat,
0 <= t < t2 /\ scheduled_at sched j t
exists t' : nat, t' < t2 /\ scheduled_at sched j t'
by move : EX_SCHED => [t [TIMES SCHED_AT]]; exists t ; split .
Qed .
(** If we can assume that a scheduled job always receives service,
we can further prove the converse. *)
Section GuaranteedService .
(** Assume [j] always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced : ideal_progress_proc_model PState.
(** In other words, not being scheduled is equivalent to receiving zero
service. *)
Lemma no_service_not_scheduled :
forall t ,
~~ scheduled_at sched j t <-> service_at sched j t = 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : instant,
~~ scheduled_at sched j t <-> service_at sched j t = 0
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : instant,
~~ scheduled_at sched j t <-> service_at sched j t = 0
move => t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant
~~ scheduled_at sched j t <-> service_at sched j t = 0
rewrite /scheduled_at /service_at.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant
~~ scheduled_in j (sched t) <->
service_in j (sched t) = 0
split => [NOT_SCHED | NO_SERVICE].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant NOT_SCHED : ~~ scheduled_in j (sched t)
service_in j (sched t) = 0
- Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant NOT_SCHED : ~~ scheduled_in j (sched t)
service_in j (sched t) = 0
by rewrite service_implies_scheduled //.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant NO_SERVICE : service_in j (sched t) = 0
~~ scheduled_in j (sched t)
- Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant NO_SERVICE : service_in j (sched t) = 0
~~ scheduled_in j (sched t)
apply (contra (H_scheduled_implies_serviced j (sched t))).Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant NO_SERVICE : service_in j (sched t) = 0
~~ (0 < service_in j (sched t))
by rewrite -eqn0Ngt; apply /eqP => //.
Qed .
(** Then, if a job does not receive any service during an interval, it
is not scheduled. *)
Lemma no_service_during_implies_not_scheduled :
forall t1 t2 ,
service_during sched j t1 t2 = 0 ->
forall t ,
t1 <= t < t2 -> ~~ scheduled_at sched j t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t1 t2 : instant,
service_during sched j t1 t2 = 0 ->
forall t : nat,
t1 <= t < t2 -> ~~ scheduled_at sched j t
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t1 t2 : instant,
service_during sched j t1 t2 = 0 ->
forall t : nat,
t1 <= t < t2 -> ~~ scheduled_at sched j t
move => t1 t2 ZERO_SUM t /andP [GT_t1 LT_t2].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2 : instant ZERO_SUM : service_during sched j t1 t2 = 0 t : nat GT_t1 : t1 <= t LT_t2 : t < t2
~~ scheduled_at sched j t
rewrite no_service_not_scheduled.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2 : instant ZERO_SUM : service_during sched j t1 t2 = 0 t : nat GT_t1 : t1 <= t LT_t2 : t < t2
service_at sched j t = 0
move : ZERO_SUM.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2 : instant t : nat GT_t1 : t1 <= t LT_t2 : t < t2
service_during sched j t1 t2 = 0 ->
service_at sched j t = 0
rewrite /service_during big_nat_eq0 => IS_ZERO.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2 : instant t : nat GT_t1 : t1 <= t LT_t2 : t < t2 IS_ZERO : forall i : nat,
t1 <= i < t2 -> service_at sched j i = 0
service_at sched j t = 0
by apply (IS_ZERO t); apply /andP; split => //.
Qed .
(** Conversely, if a job is not scheduled during an interval, then
it does not receive any service in that interval *)
Lemma not_scheduled_during_implies_zero_service :
forall t1 t2 ,
(forall t , t1 <= t < t2 -> ~~ scheduled_at sched j t) ->
service_during sched j t1 t2 = 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t1 t2 : nat,
(forall t : nat,
t1 <= t < t2 -> ~~ scheduled_at sched j t) ->
service_during sched j t1 t2 = 0
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t1 t2 : nat,
(forall t : nat,
t1 <= t < t2 -> ~~ scheduled_at sched j t) ->
service_during sched j t1 t2 = 0
intros t1 t2 NSCHED.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2 : nat NSCHED : forall t : nat,
t1 <= t < t2 -> ~~ scheduled_at sched j t
service_during sched j t1 t2 = 0
apply big_nat_eq0; move => t NEQ.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2 : nat NSCHED : forall t : nat,
t1 <= t < t2 -> ~~ scheduled_at sched j tt : nat NEQ : t1 <= t < t2
service_at sched j t = 0
by apply no_service_not_scheduled, NSCHED.
Qed .
(** If a job is scheduled at some point in an interval, it receives
positive cumulative service during the interval... *)
Lemma scheduled_implies_cumulative_service :
forall t1 t2 ,
(exists t ,
t1 <= t < t2 /\
scheduled_at sched j t) ->
service_during sched j t1 t2 > 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t1 t2 : nat,
(exists t : nat,
t1 <= t < t2 /\ scheduled_at sched j t) ->
0 < service_during sched j t1 t2
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t1 t2 : nat,
(exists t : nat,
t1 <= t < t2 /\ scheduled_at sched j t) ->
0 < service_during sched j t1 t2
move => t1 t2 [t' [TIMES SCHED]].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2, t' : nat TIMES : t1 <= t' < t2 SCHED : scheduled_at sched j t'
0 < service_during sched j t1 t2
rewrite service_during_service_at.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2, t' : nat TIMES : t1 <= t' < t2 SCHED : scheduled_at sched j t'
exists t : nat,
t1 <= t < t2 /\ 0 < service_at sched j t
exists t' ; split => //.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2, t' : nat TIMES : t1 <= t' < t2 SCHED : scheduled_at sched j t'
0 < service_at sched j t'
move : SCHED.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2, t' : nat TIMES : t1 <= t' < t2
scheduled_at sched j t' -> 0 < service_at sched j t'
rewrite /scheduled_at /service_at.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t1, t2, t' : nat TIMES : t1 <= t' < t2
scheduled_in j (sched t') ->
0 < service_in j (sched t')
by apply (H_scheduled_implies_serviced j (sched t')).
Qed .
(** ...which again applies to total service, too. *)
Corollary scheduled_implies_nonzero_service :
forall t ,
(exists t' ,
t' < t /\
scheduled_at sched j t') ->
service sched j t > 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : nat,
(exists t' : nat, t' < t /\ scheduled_at sched j t') ->
0 < service sched j t
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : nat,
(exists t' : nat, t' < t /\ scheduled_at sched j t') ->
0 < service sched j t
move => t [t' [TT SCHED]].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t, t' : nat TT : t' < t SCHED : scheduled_at sched j t'
0 < service sched j t
rewrite /service.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t, t' : nat TT : t' < t SCHED : scheduled_at sched j t'
0 < service_during sched j 0 t
apply scheduled_implies_cumulative_service.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H_scheduled_implies_serviced : ideal_progress_proc_model
PState t, t' : nat TT : t' < t SCHED : scheduled_at sched j t'
exists t0 : nat,
0 <= t0 < t /\ scheduled_at sched j t0
by exists t' ; split => //.
Qed .
End GuaranteedService .
(** Furthermore, if we know that jobs are not released early, then we can
narrow the interval during which they must have been scheduled. *)
Section AfterArrival .
Context `{JobArrival Job}.
(** Assume that jobs must arrive to execute. *)
Hypothesis H_jobs_must_arrive :
jobs_must_arrive_to_execute sched.
(** We prove that any job with positive cumulative service at time [t] must
have been scheduled some time since its arrival and before time [t]. *)
Lemma positive_service_implies_scheduled_since_arrival :
forall t ,
service sched j t > 0 ->
exists t' , (job_arrival j <= t' < t /\ scheduled_at sched j t').Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : instant,
0 < service sched j t ->
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : instant,
0 < service sched j t ->
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
move => t SERVICE.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant SERVICE : 0 < service sched j t
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
have EX_SCHED := positive_service_implies_scheduled_before t SERVICE.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant SERVICE : 0 < service sched j tEX_SCHED : exists t' : nat,
t' < t /\ scheduled_at sched j t'
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
inversion EX_SCHED as [t'' [TIMES SCHED_AT]].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant SERVICE : 0 < service sched j tEX_SCHED : exists t' : nat,
t' < t /\ scheduled_at sched j t't'' : nat TIMES : t'' < t SCHED_AT : scheduled_at sched j t''
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
exists t'' ; split ; last by done .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant SERVICE : 0 < service sched j tEX_SCHED : exists t' : nat,
t' < t /\ scheduled_at sched j t't'' : nat TIMES : t'' < t SCHED_AT : scheduled_at sched j t''
job_arrival j <= t'' < t
rewrite /(_ && _) ifT //.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant SERVICE : 0 < service sched j tEX_SCHED : exists t' : nat,
t' < t /\ scheduled_at sched j t't'' : nat TIMES : t'' < t SCHED_AT : scheduled_at sched j t''
job_arrival j <= t''
move : H_jobs_must_arrive.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant SERVICE : 0 < service sched j tEX_SCHED : exists t' : nat,
t' < t /\ scheduled_at sched j t't'' : nat TIMES : t'' < t SCHED_AT : scheduled_at sched j t''
jobs_must_arrive_to_execute sched ->
job_arrival j <= t''
rewrite /jobs_must_arrive_to_execute /has_arrived => ARR.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant SERVICE : 0 < service sched j tEX_SCHED : exists t' : nat,
t' < t /\ scheduled_at sched j t't'' : nat TIMES : t'' < t SCHED_AT : scheduled_at sched j t'' ARR : forall (j : Job) (t : instant),
scheduled_at sched j t -> job_arrival j <= t
job_arrival j <= t''
by apply : ARR.
Qed .
Lemma not_scheduled_before_arrival :
forall t , t < job_arrival j -> ~~ scheduled_at sched j t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : nat,
t < job_arrival j -> ~~ scheduled_at sched j t
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : nat,
t < job_arrival j -> ~~ scheduled_at sched j t
move => t EARLY.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : nat EARLY : t < job_arrival j
~~ scheduled_at sched j t
apply : (contra (H_jobs_must_arrive j t)).Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : nat EARLY : t < job_arrival j
~~ has_arrived j t
by rewrite /has_arrived -ltnNge //.
Qed .
(** We show that job [j] does not receive service at any time [t] prior to its
arrival. *)
Lemma service_before_job_arrival_zero :
forall t ,
t < job_arrival j ->
service_at sched j t = 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : nat,
t < job_arrival j -> service_at sched j t = 0
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : nat,
t < job_arrival j -> service_at sched j t = 0
move => t NOT_ARR.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : nat NOT_ARR : t < job_arrival j
service_at sched j t = 0
by rewrite not_scheduled_implies_no_service // not_scheduled_before_arrival //.
Qed .
(** Note that the same property applies to the cumulative service. *)
Lemma cumulative_service_before_job_arrival_zero :
forall t1 t2 : instant,
t2 <= job_arrival j ->
service_during sched j t1 t2 = 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t1 t2 : instant,
t2 <= job_arrival j ->
service_during sched j t1 t2 = 0
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t1 t2 : instant,
t2 <= job_arrival j ->
service_during sched j t1 t2 = 0
move => t1 t2 EARLY.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : instant EARLY : t2 <= job_arrival j
service_during sched j t1 t2 = 0
rewrite /service_during.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : instant EARLY : t2 <= job_arrival j
\sum_(t1 <= t < t2) service_at sched j t = 0
have ZERO_SUM: \sum_(t1 <= t < t2) service_at sched j t = \sum_(t1 <= t < t2) 0 ;
last by rewrite ZERO_SUM sum0.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : instant EARLY : t2 <= job_arrival j
\sum_(t1 <= t < t2) service_at sched j t =
\sum_(t1 <= t < t2) 0
rewrite big_nat_cond [in RHS]big_nat_cond.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : instant EARLY : t2 <= job_arrival j
\sum_(t1 <= i < t2 | (t1 <= i < t2) && true)
service_at sched j i =
\sum_(t1 <= i < t2 | (t1 <= i < t2) && true) 0
apply : eq_bigr => i /andP [TIMES _].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : instant EARLY : t2 <= job_arrival j i : nat TIMES : t1 <= i < t2
service_at sched j i = 0
move : TIMES => /andP [le_t1_i lt_i_t2].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : instant EARLY : t2 <= job_arrival j i : nat le_t1_i : t1 <= i lt_i_t2 : i < t2
service_at sched j i = 0
apply (service_before_job_arrival_zero i).Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : instant EARLY : t2 <= job_arrival j i : nat le_t1_i : t1 <= i lt_i_t2 : i < t2
i < job_arrival j
by apply leq_trans with (n := t2); auto .
Qed .
(** Hence, one can ignore the service received by a job before its arrival
time... *)
Lemma ignore_service_before_arrival :
forall t1 t2 ,
t1 <= job_arrival j ->
t2 >= job_arrival j ->
service_during sched j t1 t2 = service_during sched j (job_arrival j) t2.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t1 t2 : nat,
t1 <= job_arrival j ->
job_arrival j <= t2 ->
service_during sched j t1 t2 =
service_during sched j (job_arrival j) t2
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t1 t2 : nat,
t1 <= job_arrival j ->
job_arrival j <= t2 ->
service_during sched j t1 t2 =
service_during sched j (job_arrival j) t2
move => t1 t2 le_t1 le_t2.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : nat le_t1 : t1 <= job_arrival j le_t2 : job_arrival j <= t2
service_during sched j t1 t2 =
service_during sched j (job_arrival j) t2
rewrite -(service_during_cat sched j t1 (job_arrival j) t2).Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : nat le_t1 : t1 <= job_arrival j le_t2 : job_arrival j <= t2
service_during sched j t1 (job_arrival j) +
service_during sched j (job_arrival j) t2 =
service_during sched j (job_arrival j) t2
rewrite cumulative_service_before_job_arrival_zero //.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t1, t2 : nat le_t1 : t1 <= job_arrival j le_t2 : job_arrival j <= t2
t1 <= job_arrival j <= t2
by apply /andP; split .
Qed .
(** ... which we can also state in terms of cumulative service. *)
Corollary no_service_before_arrival :
forall t ,
t <= job_arrival j -> service sched j t = 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : nat,
t <= job_arrival j -> service sched j t = 0
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : nat,
t <= job_arrival j -> service sched j t = 0
move => t EARLY.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job H0 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : nat EARLY : t <= job_arrival j
service sched j t = 0
by rewrite /service cumulative_service_before_job_arrival_zero //.
Qed .
End AfterArrival .
(** In this section, we prove some lemmas about time instants with same
service. *)
Section TimesWithSameService .
(** Consider any time instants [t1] and [t2]... *)
Variable t1 t2 : instant.
(** ...where [t1] is no later than [t2]... *)
Hypothesis H_t1_le_t2 : t1 <= t2.
(** ...and where job [j] has received the same amount of service. *)
Hypothesis H_same_service : service sched j t1 = service sched j t2.
(** First, we observe that this means that the job receives no service
during <<[t1, t2)>>... *)
Lemma constant_service_implies_no_service_during :
service_during sched j t1 t2 = 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
service_during sched j t1 t2 = 0
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
service_during sched j t1 t2 = 0
move : H_same_service.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
service sched j t1 = service sched j t2 ->
service_during sched j t1 t2 = 0
rewrite -(service_cat sched j t1 t2) // -[service sched j t1 in LHS]addn0 => /eqP.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
service sched j t1 + 0 ==
service sched j t1 + service_during sched j t1 t2 ->
service_during sched j t1 t2 = 0
by rewrite eqn_add2l => /eqP //.
Qed .
(** ...which of course implies that it does not receive service at any
point, either. *)
Lemma constant_service_implies_not_scheduled :
forall t ,
t1 <= t < t2 -> service_at sched j t = 0 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
forall t : nat,
t1 <= t < t2 -> service_at sched j t = 0
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
forall t : nat,
t1 <= t < t2 -> service_at sched j t = 0
move => t /andP [GE_t1 LT_t2].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : nat GE_t1 : t1 <= t LT_t2 : t < t2
service_at sched j t = 0
move : constant_service_implies_no_service_during.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : nat GE_t1 : t1 <= t LT_t2 : t < t2
service_during sched j t1 t2 = 0 ->
service_at sched j t = 0
rewrite /service_during big_nat_eq0 => IS_ZERO.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : nat GE_t1 : t1 <= t LT_t2 : t < t2 IS_ZERO : forall i : nat,
t1 <= i < t2 -> service_at sched j i = 0
service_at sched j t = 0
by apply IS_ZERO; apply /andP; split => //.
Qed .
(** We show that job [j] receives service at some point [t < t1]
iff [j] receives service at some point [t' < t2]. *)
Lemma same_service_implies_serviced_at_earlier_times :
[exists t : 'I_t1, service_at sched j t > 0 ] =
[exists t' : 'I_t2, service_at sched j t' > 0 ].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
[exists t , 0 < service_at sched j t] =
[exists t' , 0 < service_at sched j t']
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2
[exists t , 0 < service_at sched j t] =
[exists t' , 0 < service_at sched j t']
apply /idP/idP => /existsP [t SERVICED].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : ordinal_finType t1 SERVICED : 0 < service_at sched j t
[exists t' , 0 < service_at sched j t']
{ Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : ordinal_finType t1 SERVICED : 0 < service_at sched j t
[exists t' , 0 < service_at sched j t']
have LE: t < t2 by apply : (leq_trans _ H_t1_le_t2) => //.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : ordinal_finType t1 SERVICED : 0 < service_at sched j tLE : t < t2
[exists t' , 0 < service_at sched j t']
by apply /existsP; exists (Ordinal LE ).
} Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : ordinal_finType t2 SERVICED : 0 < service_at sched j t
[exists t , 0 < service_at sched j t]
{ Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : ordinal_finType t2 SERVICED : 0 < service_at sched j t
[exists t , 0 < service_at sched j t]
case (boolP (t < t1)) => LE.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : ordinal_finType t2 SERVICED : 0 < service_at sched j tLE : t < t1
[exists t , 0 < service_at sched j t]
- Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : ordinal_finType t2 SERVICED : 0 < service_at sched j tLE : t < t1
[exists t , 0 < service_at sched j t]
by apply /existsP; exists (Ordinal LE ).Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : ordinal_finType t2 SERVICED : 0 < service_at sched j tLE : ~~ (t < t1)
[exists t , 0 < service_at sched j t]
- Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : ordinal_finType t2 SERVICED : 0 < service_at sched j tLE : ~~ (t < t1)
[exists t , 0 < service_at sched j t]
exfalso .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : ordinal_finType t2 SERVICED : 0 < service_at sched j tLE : ~~ (t < t1)
False
have TIMES: t1 <= t < t2
by apply /andP; split => //; rewrite leqNgt //.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : ordinal_finType t2 SERVICED : 0 < service_at sched j tLE : ~~ (t < t1) TIMES : t1 <= t < t2
False
have NO_SERVICE := constant_service_implies_not_scheduled t TIMES.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 t : ordinal_finType t2 SERVICED : 0 < service_at sched j tLE : ~~ (t < t1) TIMES : t1 <= t < t2 NO_SERVICE : service_at sched j t = 0
False
by rewrite NO_SERVICE in SERVICED.
}
Qed .
(** Then, under the assumption that scheduled jobs receives service,
we can translate this into a claim about scheduled_at. *)
(** Assume [j] always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced : ideal_progress_proc_model PState.
(** We show that job [j] is scheduled at some point [t < t1] iff [j] is scheduled
at some point [t' < t2]. *)
Lemma same_service_implies_scheduled_at_earlier_times :
[exists t : 'I_t1, scheduled_at sched j t] =
[exists t' : 'I_t2, scheduled_at sched j t'].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState
[exists t , scheduled_at sched j t] =
[exists t' , scheduled_at sched j t']
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState
[exists t , scheduled_at sched j t] =
[exists t' , scheduled_at sched j t']
have CONV: forall B , [exists b : 'I_B, scheduled_at sched j b]
= [exists b : 'I_B, service_at sched j b > 0 ].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall B : nat,
[exists b , scheduled_at sched j b] =
[exists b , 0 < service_at sched j b]
{ Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall B : nat,
[exists b , scheduled_at sched j b] =
[exists b , 0 < service_at sched j b]
move => B.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState B : nat
[exists b , scheduled_at sched j b] =
[exists b , 0 < service_at sched j b]
apply /idP/idP => /existsP [b P]; apply /existsP; exists b .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState B : nat b : ordinal_finType B P : scheduled_at sched j b
0 < service_at sched j b
- Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState B : nat b : ordinal_finType B P : scheduled_at sched j b
0 < service_at sched j b
by move : P; rewrite /scheduled_at /service_at;
apply (H_scheduled_implies_serviced j (sched b)).Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState B : nat b : ordinal_finType B P : 0 < service_at sched j b
scheduled_at sched j b
- Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState B : nat b : ordinal_finType B P : 0 < service_at sched j b
scheduled_at sched j b
by apply service_at_implies_scheduled_at.
} Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState CONV : forall B : nat,
[exists b , scheduled_at sched j b] =
[exists b , 0 < service_at sched j b]
[exists t , scheduled_at sched j t] =
[exists t' , scheduled_at sched j t']
rewrite !CONV.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState j : Job t1, t2 : instant H_t1_le_t2 : t1 <= t2 H_same_service : service sched j t1 =
service sched j t2 H_scheduled_implies_serviced : ideal_progress_proc_model
PState CONV : forall B : nat,
[exists b , scheduled_at sched j b] =
[exists b , 0 < service_at sched j b]
[exists b , 0 < service_at sched j b] =
[exists b , 0 < service_at sched j b]
by apply same_service_implies_serviced_at_earlier_times.
Qed .
End TimesWithSameService .
End RelationToScheduled .
Section ServiceInTwoSchedules .
(** Consider any job type and any processor model. *)
Context {Job : JobType}.
Context {PState : Type }.
Context `{ProcessorState Job PState}.
(** Consider any two given schedules... *)
Variable sched1 sched2 : schedule PState.
(** Given an interval in which the schedules provide the same service
to a job at each instant, we can prove that the cumulative service
received during the interval has to be the same. *)
Section ServiceDuringEquivalentInterval .
(** Consider two time instants... *)
Variable t1 t2 : instant.
(** ...and a given job that is to be scheduled. *)
Variable j : Job.
(** Assume that, in any instant between [t1] and [t2] the service
provided to [j] from the two schedules is the same. *)
Hypothesis H_sched1_sched2_same_service_at :
forall t , t1 <= t < t2 ->
service_at sched1 j t = service_at sched2 j t.
(** It follows that the service provided during [t1] and [t2]
is also the same. *)
Lemma same_service_during :
service_during sched1 j t1 t2 = service_during sched2 j t1 t2.Job : JobType PState : Type H : ProcessorState Job PState sched1, sched2 : schedule PState t1, t2 : instant j : Job H_sched1_sched2_same_service_at : forall t : nat,
t1 <= t < t2 ->
service_at sched1 j
t =
service_at sched2 j
t
service_during sched1 j t1 t2 =
service_during sched2 j t1 t2
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched1, sched2 : schedule PState t1, t2 : instant j : Job H_sched1_sched2_same_service_at : forall t : nat,
t1 <= t < t2 ->
service_at sched1 j
t =
service_at sched2 j
t
service_during sched1 j t1 t2 =
service_during sched2 j t1 t2
rewrite /service_during.Job : JobType PState : Type H : ProcessorState Job PState sched1, sched2 : schedule PState t1, t2 : instant j : Job H_sched1_sched2_same_service_at : forall t : nat,
t1 <= t < t2 ->
service_at sched1 j
t =
service_at sched2 j
t
\sum_(t1 <= t < t2) service_at sched1 j t =
\sum_(t1 <= t < t2) service_at sched2 j t
apply eq_big_nat.Job : JobType PState : Type H : ProcessorState Job PState sched1, sched2 : schedule PState t1, t2 : instant j : Job H_sched1_sched2_same_service_at : forall t : nat,
t1 <= t < t2 ->
service_at sched1 j
t =
service_at sched2 j
t
forall i : nat,
t1 <= i < t2 ->
service_at sched1 j i = service_at sched2 j i
by apply H_sched1_sched2_same_service_at.
Qed .
End ServiceDuringEquivalentInterval .
(** We can leverage the previous lemma to conclude that two schedules
that match in a given interval will also have the same cumulative
service across the interval. *)
Corollary equal_prefix_implies_same_service_during :
forall t1 t2 ,
(forall t , t1 <= t < t2 -> sched1 t = sched2 t) ->
forall j , service_during sched1 j t1 t2 = service_during sched2 j t1 t2.Job : JobType PState : Type H : ProcessorState Job PState sched1, sched2 : schedule PState
forall t1 t2 : nat,
(forall t : nat, t1 <= t < t2 -> sched1 t = sched2 t) ->
forall j : Job,
service_during sched1 j t1 t2 =
service_during sched2 j t1 t2
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched1, sched2 : schedule PState
forall t1 t2 : nat,
(forall t : nat, t1 <= t < t2 -> sched1 t = sched2 t) ->
forall j : Job,
service_during sched1 j t1 t2 =
service_during sched2 j t1 t2
move => t1 t2 SCHED_EQ j.Job : JobType PState : Type H : ProcessorState Job PState sched1, sched2 : schedule PState t1, t2 : nat SCHED_EQ : forall t : nat,
t1 <= t < t2 -> sched1 t = sched2 tj : Job
service_during sched1 j t1 t2 =
service_during sched2 j t1 t2
apply same_service_during => t' RANGE.Job : JobType PState : Type H : ProcessorState Job PState sched1, sched2 : schedule PState t1, t2 : nat SCHED_EQ : forall t : nat,
t1 <= t < t2 -> sched1 t = sched2 tj : Job t' : nat RANGE : t1 <= t' < t2
service_at sched1 j t' = service_at sched2 j t'
by rewrite /service_at SCHED_EQ.
Qed .
(** For convenience, we restate the corollary also at the level of
[service] for identical prefixes. *)
Corollary identical_prefix_service :
forall h ,
identical_prefix sched1 sched2 h ->
forall j , service sched1 j h = service sched2 j h.Job : JobType PState : Type H : ProcessorState Job PState sched1, sched2 : schedule PState
forall h : instant,
identical_prefix sched1 sched2 h ->
forall j : Job,
service sched1 j h = service sched2 j h
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched1, sched2 : schedule PState
forall h : instant,
identical_prefix sched1 sched2 h ->
forall j : Job,
service sched1 j h = service sched2 j h
by move => h IDENT j; apply equal_prefix_implies_same_service_during.
Qed .
End ServiceInTwoSchedules .