Commit ed836827 authored by Marco Maida's avatar Marco Maida 🌱
Browse files

Polished wc_trans

parent 81fb5183
Pipeline #23231 failed with stages
in 3 minutes and 35 seconds
From prosa.analysis.transform Require Export prefix swap.
From prosa.util Require Export search_arg.
From prosa.model.processor Require Export ideal.
Require Export prosa.analysis.facts.transform.swaps.
Require Export prosa.analysis.transform.prefix.
Require Export prosa.util.search_arg.
Require Export prosa.model.processor.ideal.
Require Export prosa.util.list.
(** In this file we define the transformation from any schedule into
a work conserving one. The procedure is to patch the idle allocations
with future job allocations. Note that a job cannot be allocated before
its arrival, therefore there could still exist idle instants between two
jobs allocation.
jobs allocation. *)
Section WCTransformation.
(** Consider any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(** ... and ideal uniprocessor schedules. *)
(** Consider any type of jobs... *)
Context {Job : JobType}.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
Context `{JobArrival Job}.
(** ... an ideal uniprocessor schedule... *)
Let PState := ideal.processor_state Job.
Let SchedType := schedule (PState).
(** ... any valid job arrival sequence. *)
(** ... and any valid job arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arr_seq_valid : valid_arrival_sequence arr_seq.
(** We say that a state is relevant (for the purpose of the
transformation) if it is not idle and if the job scheduled in it
has arrived prior to some given reference time. *)
Definition relevant_pstate (reference_time: instant) (s: PState) :=
match s with
Definition relevant_pstate reference_time pstate :=
match pstate with
| None => false
| Some j => job_arrival j <= reference_time
......@@ -35,14 +36,14 @@ Section WCTransformation.
(** In order to patch an idle allocation, we look in the future for another allocation
that could be moved there. The limit of the search should be the maximum deadline of
every job arrived before the given moment. *)
Definition max_deadline_for_jobs_arrived_before (arrived_before : instant) :=
Definition max_deadline_for_jobs_arrived_before arrived_before :=
let deadlines := map job_deadline (arrivals_up_to arr_seq arrived_before)
in max0 deadlines.
(** Next, we define a central element of the work-conserving transformation
procedure: given an idle allocation at [t], find a job allocation in the future
to swap with. *)
Definition find_swap_candidate (sched : SchedType) (t : instant) :=
Definition find_swap_candidate sched t :=
let order _ _ := false (* always take the first result *)
let max_dl := max_deadline_for_jobs_arrived_before t
......@@ -56,7 +57,7 @@ Section WCTransformation.
(** The point-wise transformation procedure: given a schedule and a
time [t1], ensure that the schedule satisfies [wc_at] at time
[t1]. *)
Definition make_wc_at (sched : SchedType) (t1 : instant) : SchedType :=
Definition make_wc_at sched t1 :=
match sched t1 with
| Some j => sched (* leave working instants alone *)
| None =>
......@@ -67,14 +68,14 @@ Section WCTransformation.
(** To transform a finite prefix of a given reference schedule, apply
[make_wc_at] to every point up to the given finite horizon. *)
Definition wc_transform_prefix (sched : SchedType) (horizon : instant) : SchedType :=
Definition wc_transform_prefix sched horizon :=
prefix_map sched make_wc_at horizon.
(** Finally, a full work conserving schedule (i.e., one that satisfies [wc_at]
at any time) is obtained by first computing a wc prefix up to
and including the requested time [t], and by then looking at the
last point of the prefix. *)
Definition wc_transform (sched : SchedType) (t : instant) : ideal.processor_state Job :=
Definition wc_transform sched t :=
wc_prefix := wc_transform_prefix sched t.+1
in wc_prefix t.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment