Commit 89e03467 authored by Björn Brandenburg's avatar Björn Brandenburg

add implementation of ideal uniprocessor scheduler

parent c6b775a9
Pipeline #27372 passed with stages
in 13 minutes and 25 seconds
Require Export prosa.behavior.all.
Require Export prosa.model.priority.classes.
Require Export prosa.util.supremum.
Require Export prosa.model.preemption.parameter.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.model.processor.ideal.
Require Export prosa.analysis.facts.readiness.backlogged.
Require Export prosa.analysis.transform.swap.
(** * Generic Ideal Uniprocessor 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. *)
Require prosa.model.processor.ideal.
Section UniprocessorSchedule.
Context {Job : JobType}.
Context `{JobCost Job}.
Context `{JobArrival Job}.
(** Consider any type of jobs with costs and arrival times, ... *)
Context {Job : JobType} {JC: JobCost Job} {JA: JobArrival Job}.
(** ... any readiness model, ... *)
Context `{@JobReady Job (ideal.processor_state Job) (ideal.pstate_instance Job) JC JA}.
(** ... any preemption model, and ... *)
Context `{JobPreemptable Job}.
(** ... and any JLDP priority policy. *)
Context `{JLDP_policy Job}.
Context {Task : eqType}.
Context `{JobReady Job (ideal.processor_state Job)}.
(** Suppose we are given an arrival sequence of such jobs. *)
Variable arr_seq : arrival_sequence Job.
(** In the following section, we define how the next job to be scheduled is
selected based on a finite schedule prefix. *)
Section JobAllocation.
(** Consider a finite schedule prefix ... *)
Variable sched_prefix : schedule (ideal.processor_state Job).
Definition prev_job_nonpreemptive (t : instant) : bool:=
(** ... 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
......@@ -31,29 +51,33 @@ Section UniprocessorSchedule.
(** Given an arrival sequence, a prefix schedule [[0, t-1]], computes
which job has to be scheduled at [t] **)
Definition allocation_at (t : instant): option Job :=
if prev_job_nonpreemptive t then
(** Based on the [prev_job_nonpreemptive] predicate, either the previous
job is continued to be scheduled or (one of) the highest-priority
backlogged (= pending and ready) jobs is selected. *)
Definition allocation_at: option Job :=
if prev_job_nonpreemptive then
sched_prefix t.-1
supremum (hep_job_at t) (jobs_backlogged_at arr_seq sched_prefix t).
End JobAllocation.
(** 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 (ideal.processor_state Job) := fun _ => None.
(** Given an arrival sequence, computes a schedule up to time [h] **)
(** Next, we define a function that computes a fine schedule prefix up to a
given time horizon [h]. *)
Fixpoint schedule_up_to (h : instant) : schedule (ideal.processor_state Job) :=
prefix := if h is S h' then schedule_up_to h' else empty_schedule
fun t =>
if t == h then
allocation_at prefix t
prefix t.
replace_at prefix h (allocation_at prefix h).
(** Finally, we define the ideal uniprocessor 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 uni_schedule (t : instant) : ideal.processor_state Job :=
schedule_up_to t t.
This diff is collapsed.
......@@ -50,3 +50,4 @@ TODO
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment