Library prosa.implementation.definitions.ideal_uni_scheduler


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


Require Export prosa.implementation.definitions.generic_scheduler.

Require Export prosa.model.preemption.parameter.
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.readiness.backlogged.
Require Export prosa.analysis.transform.swap.

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.
The following definitions assume ideal uniprocessor schedules.
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_preemptable j (service sched_prefix j t)
                  else
                    false
        end.

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
        else
          choose_job t (jobs_backlogged_at arr_seq sched_prefix t).
    End JobAllocation.

    (* A preemption-policy-aware ideal uniprocessor schedule is then produced
       when using [allocation_at] as the policy for the generic scheduler. *)

    Definition np_uni_schedule : schedule PState := generic_schedule allocation_at idle_state.

  End NonPreemptiveSectionAware.

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...
    Definition choose_highest_prio_job t jobs := supremum (hep_job_at t) jobs.

... to obtain a priority- and preemption-model-aware ideal uniprocessor schedule.