# Library prosa.implementation.definitions.generic_scheduler

# Generic Reference Scheduler

Consider any type of jobs and type of schedule.

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.

End PointwisePolicy.

Section GenericSchedule.

Consider any type of jobs and type of schedule.

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.

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

We construct the schedule step by step starting from an "empty" schedule
that is idle at all times as a base case.

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

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.