Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
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]
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]
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. *)
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
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. *)
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
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. *)
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
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
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
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. *)
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
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
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
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
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
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
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
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]. *)
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
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
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
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
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
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
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. *)
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
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
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
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'
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.