Library prosa.implementation.facts.generic_schedule

From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
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.
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:
      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 moveh 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.
    moveh t RANGE.
    rewrite [RHS]schedule_up_to_unfold rest_of_schedule_invariant // ⇒ EQ.
    now move: RANGE; rewrite EQ ltnn.

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.
    moveh 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).
      moveEQ. move: LT.
      now rewrite EQ ltnn. }

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 h1
        schedule_up_to policy idle_state h1 t = schedule_up_to policy idle_state h2 t.
    moveh1 h2 LEQ t BEFORE.
    elim: h2 LEQ BEFORE; first by rewrite leqn0 ⇒ /eqP →.
    movet' IH.
    rewrite leq_eqVlt ltnS ⇒ /orP [/eqP <-|LEQ] // t_H1.
    rewrite IH // schedule_up_to_widen //.
    now apply (leq_trans t_H1).

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.
    moveh t LE.
    rewrite /identical_prefix /generic_schedulet' LT.
    rewrite (schedule_up_to_prefix_inclusion t' h) //.
    by move: (leq_trans LT LE); rewrite ltnS.

End GenericScheduleProperties.