Library prosa.analysis.transform.wc_trans

Require Export prosa.analysis.transform.swap.
Require Export prosa.analysis.transform.prefix.
Require Export prosa.util.search_arg.
Require Export prosa.util.list.
Require Export prosa.model.processor.ideal.

In this file we define the transformation from any ideal uniprocessor 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 any two job allocations.
Section WCTransformation.

We assume ideal uni-processor schedules.
  #[local] Existing Instance ideal.processor_state.

Consider any type of jobs with arrival times, costs, and deadlines...
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  Context `{JobDeadline Job}.

...an ideal uniprocessor schedule...
...and any valid job arrival sequence.
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 pstate :=
    match pstate with
    | Nonefalse
    | Some jjob_arrival j reference_time
    end.

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 is the maximum deadline of every job arrived before the given moment.
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 t :=
    let order _ _ := false (* always take the first result *)
    in
    let max_dl := max_deadline_for_jobs_arrived_before t
    in
    let search_result := search_arg sched (relevant_pstate t) order t max_dl
    in
    if search_result is Some t_swap
    then t_swap
    else t. (* if nothing is found, swap with yourself *)

The point-wise transformation procedure: given a schedule and a time t1, ensure that the schedule is work-conserving at time t1.
  Definition make_wc_at sched t1 : schedule PState :=
    match sched t1 with
    | Some jsched (* leave working instants alone *)
    | None
      let
        t2 := find_swap_candidate sched t1
      in swapped sched t1 t2
    end.

To transform a finite prefix of a given reference schedule, apply make_wc_at to every point up to the given finite horizon.
Finally, a fully work-conserving schedule (i.e., one that is work-conserving at any time) is obtained by first computing a work-conserving prefix up to and including the requested time t, and by then looking at the last point of the prefix.
  Definition wc_transform sched t :=
    let
      wc_prefix := wc_transform_prefix sched t.+1
    in wc_prefix t.

End WCTransformation.