Library prosa.implementation.facts.generic_schedule

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.
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.

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.

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.

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.
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.

It follows that generic_schedule and schedule_up_to for a given horizon h share an identical prefix.