Library prosa.implementation.definitions.ideal_uni_scheduler

Ideal Uniprocessor Reference Scheduler

In this file, we provide a generic priority-aware scheduler that produces an ideal uniprocessor schedule for a given arrival sequence. The scheduler respects nonpreemptive sections and arbitrary readiness models.
Consider any type of jobs with costs and arrival times, ...
  Context {Job : JobType} {JC : JobCost Job} {JA : JobArrival Job}.

.. in the context of an ideal uniprocessor model.
Suppose we are given a consistent arrival sequence of such jobs ...
... and a non-clairvoyant readiness model.

Preemption-Aware Scheduler

First, we define the notion of a generic uniprocessor scheduler that is cognizant of non-preemptive sections, so consider any preemption model.
  Context `{JobPreemptable Job}.

  Section NonPreemptiveSectionAware.

Suppose we are given a scheduling policy that applies when jobs are preemptive: given a set of jobs ready at time t, select which to run (if any) at time t.
    Variable choose_job : instant seq Job option Job.

The next job is then chosen either by policy (if the current job is preemptive or the processor is idle) or a non-preemptively executing job continues to execute.
    Section JobAllocation.

Consider a finite schedule prefix ...
      Variable sched_prefix : schedule (ideal.processor_state Job).

... that is valid up to time t - 1.
      Variable t : instant.

We define a predicate that tests whether the job scheduled at the previous instant (if t > 0) is nonpreemptive (and hence needs to be continued to be scheduled).
      Definition prev_job_nonpreemptive : bool :=
        match t with
        | 0 ⇒ false
        | S t'if sched_prefix t' is Some j then
                   job_ready sched_prefix j t &&
                   ~~job_preemptable j (service sched_prefix j t)

Based on the prev_job_nonpreemptive predicate, either the previous job continues to be scheduled or the given policy chooses what to run instead.
      Definition allocation_at : option Job :=
        if prev_job_nonpreemptive then
          sched_prefix t.-1
          choose_job t (jobs_backlogged_at arr_seq sched_prefix t).
    End JobAllocation.

A preemption-model-compliant ideal uniprocessor schedule is then produced when using allocation_at as the policy for the generic scheduler.

Priority-Aware Scheduler

Building on the preemption-model aware scheduler, we next define a simple priority-aware scheduler.
  Section PriorityAware.

Given any JLDP priority policy...
    Context `{JLDP_policy Job}.

...always choose the highest-priority job when making a scheduling decision...
... to obtain a priority- and preemption-model-aware ideal uniprocessor schedule.