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.
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. *)SectionGenericScheduleProperties.(** For any type of jobs and type of schedule, ... *)Context {Job : JobType} {PState : Type}.Context `{ProcessorState Job PState}.(** ... any scheduling policy, and ... *)Variablepolicy : PointwisePolicy PState.(** ... any notion of idleness. *)Variableidle_state : PState.(** For notational convenience, we define [prefix t] to denote the finite prefix considered when scheduling a job at time [t]. *)Letprefixt := if t is t'.+1then 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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forallt : instant,
schedule_up_to policy idle_state t t =
policy (prefix t) t
Job: JobType PState: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forallt : instant,
schedule_up_to policy idle_state t t =
policy (prefix t) t
byelim=> [|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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forallht : instant,
schedule_up_to policy idle_state h t =
replace_at (prefix h) h (policy (prefix h) h) t
Job: JobType PState: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forallht : instant,
schedule_up_to policy idle_state h t =
replace_at (prefix h) h (policy (prefix h) h) t
bymove=> 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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forallht : nat,
t <= h ->
schedule_up_to policy idle_state h t =
schedule_up_to policy idle_state h.+1 t
Job: JobType PState: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forallht : nat,
t <= h ->
schedule_up_to policy idle_state h t =
schedule_up_to policy idle_state h.+1 t
Job: JobType PState: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : 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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : 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
nowmove: 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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forallht : nat,
h < t ->
schedule_up_to policy idle_state h t = idle_state
Job: JobType PState: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forallht : nat,
h < t ->
schedule_up_to policy idle_state h t = idle_state
h < t ->
schedule_up_to policy idle_state h t = idle_state
Job: JobType PState: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : 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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : 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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : 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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : 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
nowsubst.
Job: JobType PState: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : 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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : 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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : 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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : 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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : 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
nowrewrite 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: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forallh1h2 : nat,
h1 <= h2 ->
forallt : nat,
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state h2 t
Job: JobType PState: Type H: ProcessorState Job PState policy: PointwisePolicy PState idle_state: PState prefix:= funt : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end: nat -> schedule PState
forallh1h2 : nat,
h1 <= h2 ->
forallt : nat,
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state h2 t