# Library prosa.implementation.facts.generic_schedule

Require Export prosa.implementation.definitions.generic_scheduler.
Require Export prosa.analysis.facts.transform.replace_at.

# 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 :
∀ t,
schedule_up_to policy idle_state t t = policy (prefix t) t.
Proof. 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 :
∀ h t,
schedule_up_to policy idle_state h t = replace_at (prefix h) h (policy (prefix h) h) t.
Proof. 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 :
∀ h t,
t ≤ h →
schedule_up_to policy idle_state h t = schedule_up_to policy idle_state h.+1 t.
Proof.
move⇒ h t RANGE.
rewrite [RHS]schedule_up_to_unfold rest_of_schedule_invariant // ⇒ EQ.
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 :
∀ h t,
h < t →
schedule_up_to policy idle_state h t = idle_state.
Proof.
move⇒ h t.
elim: h ⇒ [LT|h IH LT].
{ rewrite /schedule_up_to rest_of_schedule_invariant // ⇒ ZERO.
now subst. }
{ rewrite /schedule_up_to rest_of_schedule_invariant -/(schedule_up_to _ _ h t);
first by apply IH ⇒ //; apply ltn_trans with (n := h.+1).
move⇒ EQ. move: LT.
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 :
∀ h1 h2,
h1 ≤ h2 →
∀ t,
t ≤ h1 →
schedule_up_to policy idle_state h1 t = schedule_up_to policy idle_state h2 t.
Proof.
move⇒ h1 h2 LEQ t BEFORE.
elim: h2 LEQ BEFORE; first by rewrite leqn0 ⇒ /eqP →.
move⇒ t' IH.
rewrite leq_eqVlt ltnS ⇒ /orP [/eqP <-|LEQ] // t_H1.
rewrite IH // schedule_up_to_widen //.
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 :
∀ h t,
t ≤ h.+1 →
identical_prefix (schedule_up_to policy idle_state h) (generic_schedule policy idle_state) t.
Proof.
move⇒ h t LE.
rewrite /identical_prefix /generic_schedule ⇒ t' LT.
rewrite (schedule_up_to_prefix_inclusion t' h) //.
by move: (leq_trans LT LE); rewrite ltnS.
Qed.
End GenericScheduleProperties.