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.

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.

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

  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.

End GenericScheduleProperties.