Library prosa.implementation.definitions.generic_scheduler

Require Export prosa.analysis.transform.swap.

Generic Reference Scheduler

In this file, we provide a generic procedure that produces a schedule by making a decision on what to schedule at each point in time.
To begin with, we define the notion of a pointwise scheduling policy that makes a decision at a given time t based on given prefix up to time t.-1.
Section PointwisePolicy.
Consider any type of jobs and type of schedule.
  Context {Job : JobType}.
  Variable PState : ProcessorState Job.

A pointwise scheduling policy is a function that, given a schedule prefix that is valid up to time t - 1, decides what to schedule at time t.
  Definition PointwisePolicy := schedule PState → instant → PState.
End PointwisePolicy.

Section GenericSchedule.
Consider any type of jobs and type of schedule.
  Context {Job : JobType} {PState : ProcessorState Job}.

Suppose we are given a policy function that, given a schedule prefix that is valid up to time t - 1, decides what to schedule at time t.
  Variable policy : PointwisePolicy PState.

Let idle_state denote the processor state that indicates that the entire system is idle.
  Variable idle_state : PState.

We construct the schedule step by step starting from an "empty" schedule that is idle at all times as a base case.
  Definition empty_schedule: schedule PState := fun _ ⇒ idle_state.

Next, we define a function that computes a schedule prefix up to a given time horizon h.
  Fixpoint schedule_up_to (h : instant) :=
    let
      prefix := if h is h'.+1 then schedule_up_to h' else empty_schedule
    in
      replace_at prefix h (policy prefix h).

Finally, we define the generic schedule as follows: for a given point in time t, we compute the finite prefix up to and including t, namely schedule_up_to t, and then return the job scheduled at time t in that prefix.
  Definition generic_schedule (t : instant) : PState :=
    schedule_up_to t t.

End GenericSchedule.