Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.transform.swap .[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.behavior.completion.
(** In this file, we make a few simple observations about schedules with
replacements. *)
Section ReplaceAtFacts .
(** For any given type of jobs... *)
Context {Job : JobType}.
(** ... and any given type of processor states, ... *)
Context {PState : ProcessorState Job}.
(** ...consider any given reference schedule. *)
Variable sched : schedule PState.
(** Suppose we are given a specific time [t'] ... *)
Variable t' : instant.
(** ...and a replacement state [state]. *)
Variable nstate : PState.
(** In the following, let [sched'] denote the schedule with replacement at time
t'. *)
Let sched' := replace_at sched t' nstate.
(** We begin with the trivial observation that [replace_at sched t' nstate]
indeed returns [nstate] at time [t']. *)
Lemma replace_at_def :
sched' t' = nstate.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState
sched' t' = nstate
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState
sched' t' = nstate
rewrite /sched' /replace_at.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState
(if t' == t' then nstate else sched t') = nstate
now apply ifT.
Qed .
(** Equally trivially, the schedule doesn't change at other times. *)
Lemma rest_of_schedule_invariant :
forall t , t <> t' -> sched' t = sched t.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState
forall t : instant, t <> t' -> sched' t = sched t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState
forall t : instant, t <> t' -> sched' t = sched t
move => t DIFF.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState t : instant DIFF : t <> t'
sched' t = sched t
rewrite /sched' /replace_at.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState t : instant DIFF : t <> t'
(if t' == t then nstate else sched t) = sched t
case (t' == t) eqn :TT => [|//].Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState t : instant DIFF : t <> t' TT : (t' == t) = true
nstate = sched t
by move /eqP in TT; rewrite TT in DIFF; contradiction .
Qed .
(** As a result, the service in intervals that do not intersect with
[t'] is invariant, too. *)
Lemma service_at_other_times_invariant :
forall t1 t2 ,
t2 <= t' \/ t' < t1 ->
forall j ,
service_during sched j t1 t2
=
service_during sched' j t1 t2.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState
forall t1 t2 : nat,
t2 <= t' \/ t' < t1 ->
forall j : Job,
service_during sched j t1 t2 =
service_during sched' j t1 t2
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState
forall t1 t2 : nat,
t2 <= t' \/ t' < t1 ->
forall j : Job,
service_during sched j t1 t2 =
service_during sched' j t1 t2
move => t1 t2 SWAP_EXCLUDED j.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState t1, t2 : nat SWAP_EXCLUDED : t2 <= t' \/ t' < t1 j : Job
service_during sched j t1 t2 =
service_during sched' j t1 t2
rewrite /service_during /service_at.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState t1, t2 : nat SWAP_EXCLUDED : t2 <= t' \/ t' < t1 j : Job
\sum_(t1 <= t < t2) service_in j (sched t) =
\sum_(t1 <= t < t2) service_in j (sched' t)
apply eq_big_nat => t /andP [le_t1t lt_tt2].Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState t1, t2 : nat SWAP_EXCLUDED : t2 <= t' \/ t' < t1 j : Job t : nat le_t1t : t1 <= t lt_tt2 : t < t2
service_in j (sched t) = service_in j (sched' t)
rewrite rest_of_schedule_invariant//.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState t1, t2 : nat SWAP_EXCLUDED : t2 <= t' \/ t' < t1 j : Job t : nat le_t1t : t1 <= t lt_tt2 : t < t2
t <> t'
eapply point_not_in_interval; eauto .Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState t1, t2 : nat SWAP_EXCLUDED : t2 <= t' \/ t' < t1 j : Job t : nat le_t1t : t1 <= t lt_tt2 : t < t2
t1 <= t < t2
apply /andP; by split .
Qed .
(** Next, we consider the amount of service received in intervals
that do span across the replacement point. We can relate the
service received in the original and the new schedules by adding
the service in the respective "missing" state... *)
Lemma service_delta :
forall t1 t2 ,
t1 <= t' < t2 ->
forall j ,
service_during sched j t1 t2 + service_at sched' j t'
=
service_during sched' j t1 t2 + service_at sched j t'.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState
forall t1 t2 : nat,
t1 <= t' < t2 ->
forall j : Job,
service_during sched j t1 t2 + service_at sched' j t' =
service_during sched' j t1 t2 + service_at sched j t'
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState
forall t1 t2 : nat,
t1 <= t' < t2 ->
forall j : Job,
service_during sched j t1 t2 + service_at sched' j t' =
service_during sched' j t1 t2 + service_at sched j t'
move => t1 t2 TIMES j.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState t1, t2 : nat TIMES : t1 <= t' < t2 j : Job
service_during sched j t1 t2 + service_at sched' j t' =
service_during sched' j t1 t2 + service_at sched j t'
rewrite -(service_split_at_point sched _ _ t' _) //
-(service_split_at_point sched' _ _ t' _) //.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState t1, t2 : nat TIMES : t1 <= t' < t2 j : Job
service_during sched j t1 t' + service_at sched j t' +
service_during sched j t'.+1 t2 +
service_at sched' j t' =
service_during sched' j t1 t' + service_at sched' j t' +
service_during sched' j t'.+1 t2 +
service_at sched j t'
by rewrite !service_at_other_times_invariant -/sched'; [ring | right | left ].
Qed .
(** ...which we can also rewrite as follows. *)
Corollary service_in_replaced :
forall t1 t2 ,
t1 <= t' < t2 ->
forall j ,
service_during sched' j t1 t2
=
service_during sched j t1 t2 + service_at sched' j t' - service_at sched j t'.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState
forall t1 t2 : nat,
t1 <= t' < t2 ->
forall j : Job,
service_during sched' j t1 t2 =
service_during sched j t1 t2 + service_at sched' j t' -
service_at sched j t'
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState
forall t1 t2 : nat,
t1 <= t' < t2 ->
forall j : Job,
service_during sched' j t1 t2 =
service_during sched j t1 t2 + service_at sched' j t' -
service_at sched j t'
move => t1 t2 ORDER j.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState t1, t2 : nat ORDER : t1 <= t' < t2 j : Job
service_during sched' j t1 t2 =
service_during sched j t1 t2 + service_at sched' j t' -
service_at sched j t'
by rewrite service_delta// addnK. Qed .
(** As another simple invariant (useful for case analysis), we
observe that if a job is scheduled neither in the replaced nor
in the new state, then at any time it receives exactly the same
amount of service in the new schedule with replacements as in
the original schedule. *)
Lemma service_at_of_others_invariant (j : Job):
~~ scheduled_in j (sched' t') ->
~~ scheduled_in j (sched t') ->
forall t ,
service_at sched j t = service_at sched' j t.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState j : Job
~~ scheduled_in j (sched' t') ->
~~ scheduled_in j (sched t') ->
forall t : instant,
service_at sched j t = service_at sched' j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState j : Job
~~ scheduled_in j (sched' t') ->
~~ scheduled_in j (sched t') ->
forall t : instant,
service_at sched j t = service_at sched' j t
move => NOT_IN_NEW NOT_IN_OLD t.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState j : Job NOT_IN_NEW : ~~ scheduled_in j (sched' t') NOT_IN_OLD : ~~ scheduled_in j (sched t') t : instant
service_at sched j t = service_at sched' j t
rewrite /service_at.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState j : Job NOT_IN_NEW : ~~ scheduled_in j (sched' t') NOT_IN_OLD : ~~ scheduled_in j (sched t') t : instant
service_in j (sched t) = service_in j (sched' t)
case : (boolP (t == t')) => /eqP TT.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState j : Job NOT_IN_NEW : ~~ scheduled_in j (sched' t') NOT_IN_OLD : ~~ scheduled_in j (sched t') t : instant TT : t = t'
service_in j (sched t) = service_in j (sched' t)
- Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState j : Job NOT_IN_NEW : ~~ scheduled_in j (sched' t') NOT_IN_OLD : ~~ scheduled_in j (sched t') t : instant TT : t = t'
service_in j (sched t) = service_in j (sched' t)
by rewrite !TT !service_in_implies_scheduled_in //; apply negbTE.
- Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState j : Job NOT_IN_NEW : ~~ scheduled_in j (sched' t') NOT_IN_OLD : ~~ scheduled_in j (sched t') t : instant TT : t <> t'
service_in j (sched t) = service_in j (sched' t)
rewrite rest_of_schedule_invariant//.
Qed .
(** Based on the previous observation, we can trivially lift the
invariant that jobs not involved in the replacement receive
equal service to the cumulative service received in any
interval. *)
Corollary service_during_of_others_invariant (j : Job):
~~ scheduled_in j (sched' t') ->
~~ scheduled_in j (sched t') ->
forall t1 t2 ,
service_during sched j t1 t2 = service_during sched' j t1 t2.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState j : Job
~~ scheduled_in j (sched' t') ->
~~ scheduled_in j (sched t') ->
forall t1 t2 : instant,
service_during sched j t1 t2 =
service_during sched' j t1 t2
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState j : Job
~~ scheduled_in j (sched' t') ->
~~ scheduled_in j (sched t') ->
forall t1 t2 : instant,
service_during sched j t1 t2 =
service_during sched' j t1 t2
move => NOT_IN_NEW NOT_IN_OLD t1 t2.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState j : Job NOT_IN_NEW : ~~ scheduled_in j (sched' t') NOT_IN_OLD : ~~ scheduled_in j (sched t') t1, t2 : instant
service_during sched j t1 t2 =
service_during sched' j t1 t2
rewrite /service_during.Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState j : Job NOT_IN_NEW : ~~ scheduled_in j (sched' t') NOT_IN_OLD : ~~ scheduled_in j (sched t') t1, t2 : instant
\sum_(t1 <= t < t2) service_at sched j t =
\sum_(t1 <= t < t2) service_at sched' j t
apply eq_big_nat => t /andP [le_t1t lt_tt2].Job : JobType PState : ProcessorState Job sched : schedule PState t' : instant nstate : PState sched' := replace_at sched t' nstate : schedule PState j : Job NOT_IN_NEW : ~~ scheduled_in j (sched' t') NOT_IN_OLD : ~~ scheduled_in j (sched t') t1, t2 : instant t : nat le_t1t : t1 <= t lt_tt2 : t < t2
service_at sched j t = service_at sched' j t
rewrite service_at_of_others_invariant //.
Qed .
End ReplaceAtFacts .