From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
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]
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.implementation.definitions.generic_scheduler.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.transform.replace_at.
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]

(** * Properties of the Generic Reference Scheduler *)

(** This file establishes some facts about the generic reference scheduler that
    constructs a schedule via pointwise scheduling decisions based on a given
    policy and the preceding prefix. *)

Section GenericScheduleProperties.
  (** For any type of jobs and type of schedule, ... *)
  Context {Job : JobType} {PState : ProcessorState Job}.

  (** ... any scheduling policy, and ... *)
  Variable policy : PointwisePolicy PState.

  (** ... any notion of idleness. *)
  Variable idle_state : PState.

  (** For notational convenience, we define [prefix t] to denote the finite
      prefix considered when scheduling a job at time [t]. *)
  Let prefix t := if t is t'.+1 then schedule_up_to policy idle_state  t' else empty_schedule idle_state.

  (** To begin with, we establish two simple rewriting lemmas for unrolling
      [schedule_up_to]. First, we observe that the allocation is indeed
      determined by the policy based on the preceding prefix. *)
  Lemma schedule_up_to_def:
    forall t,
      schedule_up_to policy idle_state t t = policy (prefix t) t.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forall t : instant,
schedule_up_to policy idle_state t t =
policy (prefix t) t
  Proof.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forall t : instant,
schedule_up_to policy idle_state t t =
policy (prefix t) t by elim=> [|n IH]; rewrite [LHS]/schedule_up_to -/(schedule_up_to _) /replace_at; apply ifT. Qed.

  (** Second, we note how to replace [schedule_up_to] in the general case with
      its definition. *)
  Lemma schedule_up_to_unfold:
    forall h t,
      schedule_up_to policy idle_state h t = replace_at (prefix h) h (policy (prefix h) h) t.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forall h t : instant,
schedule_up_to policy idle_state h t =
replace_at (prefix h) h (policy (prefix h) h) t
  Proof.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forall h t : instant,
schedule_up_to policy idle_state h t =
replace_at (prefix h) h (policy (prefix h) h) t by move=> h t; rewrite [LHS]/schedule_up_to /prefix; elim: h. Qed.

  (** Next, we observe that we can increase a prefix's horizon by one
        time unit without changing any allocations in the prefix. *)
  Lemma schedule_up_to_widen:
    forall h t,
      t <= h ->
      schedule_up_to policy idle_state h t = schedule_up_to policy idle_state h.+1 t.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forall h t : nat,
t <= h ->
schedule_up_to policy idle_state h t =
schedule_up_to policy idle_state h.+1 t
  Proof.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forall h t : nat,
t <= h ->
schedule_up_to policy idle_state h t =
schedule_up_to policy idle_state h.+1 t
    move=> h t RANGE.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
h, t: nat
RANGE: t <= h
schedule_up_to policy idle_state h t =
schedule_up_to policy idle_state h.+1 t
    rewrite [RHS]schedule_up_to_unfold rest_of_schedule_invariant // => EQ.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
h, t: nat
RANGE: t <= h
EQ: t = h.+1
False
    now move: RANGE; rewrite EQ ltnn.
  Qed.

  (** After the horizon of a prefix, the schedule is still "empty", meaning
        that all instants are idle. *)
  Lemma schedule_up_to_empty:
    forall h t,
      h < t ->
      schedule_up_to policy idle_state h t = idle_state.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forall h t : nat,
h < t ->
schedule_up_to policy idle_state h t = idle_state
  Proof.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forall h t : nat,
h < t ->
schedule_up_to policy idle_state h t = idle_state
    move=> h t.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
h, t: nat
h < t ->
schedule_up_to policy idle_state h t = idle_state
    elim: h => [LT|h IH LT].
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
t: nat
LT: 0 < t
schedule_up_to policy idle_state 0 t = idle_state
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
t, h: nat
IH: h < t ->
schedule_up_to policy idle_state h t = idle_state
LT: h.+1 < t
schedule_up_to policy idle_state h.+1 t = idle_state
    {
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
t: nat
LT: 0 < t
schedule_up_to policy idle_state 0 t = idle_state rewrite /schedule_up_to rest_of_schedule_invariant // => ZERO.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
t: nat
LT: 0 < t
ZERO: t = 0
False
      now subst. }
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
t, h: nat
IH: h < t ->
schedule_up_to policy idle_state h t = idle_state
LT: h.+1 < t
schedule_up_to policy idle_state h.+1 t = idle_state
    {
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
t, h: nat
IH: h < t ->
schedule_up_to policy idle_state h t = idle_state
LT: h.+1 < t
schedule_up_to policy idle_state h.+1 t = idle_state rewrite /schedule_up_to rest_of_schedule_invariant -/(schedule_up_to _ _ h t);
        first by apply IH => //; apply ltn_trans with (n := h.+1).
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
t, h: nat
IH: h < t ->
schedule_up_to policy idle_state h t = idle_state
LT: h.+1 < t
t <> h.+1
      move=> EQ.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
t, h: nat
IH: h < t ->
schedule_up_to policy idle_state h t = idle_state
LT: h.+1 < t
EQ: t = h.+1
False move: LT.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
t, h: nat
IH: h < t ->
schedule_up_to policy idle_state h t = idle_state
EQ: t = h.+1
h.+1 < t -> False
      now rewrite EQ ltnn. }
  Qed.

  (** A crucial fact is that a prefix up to horizon [h1] is identical to a
      prefix up to a later horizon [h2] at times up to [h1]. *)
  Lemma schedule_up_to_prefix_inclusion:
    forall h1 h2,
      h1 <= h2 ->
      forall t,
        t <= h1 ->
        schedule_up_to policy idle_state h1 t = schedule_up_to policy idle_state h2 t.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forall h1 h2 : nat,
h1 <= h2 ->
forall t : nat,
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state h2 t
  Proof.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forall h1 h2 : nat,
h1 <= h2 ->
forall t : nat,
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state h2 t
    move=> h1 h2 LEQ t BEFORE.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
h1, h2: nat
LEQ: h1 <= h2
t: nat
BEFORE: t <= h1
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state h2 t
    elim: h2 LEQ BEFORE; first by rewrite leqn0 => /eqP ->.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
h1, t: nat
forall n : nat,
(h1 <= n ->
 t <= h1 ->
 schedule_up_to policy idle_state h1 t =
 schedule_up_to policy idle_state n t) ->
h1 <= n.+1 ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state n.+1 t
    move=> t' IH.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
h1, t, t': nat
IH: h1 <= t' ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state t' t
h1 <= t'.+1 ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state t'.+1 t
    rewrite leq_eqVlt ltnS => /orP [/eqP <-|LEQ] // t_H1.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
h1, t, t': nat
IH: h1 <= t' ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state t' t
LEQ: h1 <= t'
t_H1: t <= h1
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state t'.+1 t
    rewrite IH // schedule_up_to_widen //.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
h1, t, t': nat
IH: h1 <= t' ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state t' t
LEQ: h1 <= t'
t_H1: t <= h1
t <= t'
    now apply (leq_trans t_H1).
  Qed.

  (** It follows that [generic_schedule] and [schedule_up_to] for a given
      horizon [h] share an identical prefix. *)
  Corollary schedule_up_to_identical_prefix:
    forall h t,
      t <= h.+1 ->
      identical_prefix (schedule_up_to policy idle_state h) (generic_schedule policy idle_state) t.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forall h t : nat,
t <= h.+1 ->
identical_prefix (schedule_up_to policy idle_state h)
  (generic_schedule policy idle_state) t
  Proof.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forall h t : nat,
t <= h.+1 ->
identical_prefix (schedule_up_to policy idle_state h)
  (generic_schedule policy idle_state) t
    move=> h t LE.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
h, t: nat
LE: t <= h.+1
identical_prefix (schedule_up_to policy idle_state h)
  (generic_schedule policy idle_state) t
    rewrite /identical_prefix /generic_schedule => t' LT.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
h, t: nat
LE: t <= h.+1
t': nat
LT: t' < t
schedule_up_to policy idle_state h t' =
schedule_up_to policy idle_state t' t'
    rewrite (schedule_up_to_prefix_inclusion t' h) //.
Job: JobType
PState: ProcessorState Job
policy: PointwisePolicy PState
idle_state: PState
prefix:= fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
h, t: nat
LE: t <= h.+1
t': nat
LT: t' < t
t' <= h
    by move: (leq_trans LT LE); rewrite ltnS.
  Qed.

End GenericScheduleProperties.