add EDF optimality argument

This patch adds the classic EDF optimality argument: by swapping
allocations, any schedule in which no job misses a deadline can be
transformed into an EDF schedule in which also no job misses a deadline.

restructuring/analysis/edf/optimality.v

+From rt.restructuring.model Require Export schedule.edf.
+From rt.restructuring.analysis Require Import schedulability transform.facts.edf_opt.
+
+(** This file contains the theorem that states the famous EDF
+    optimality result: if there is any way to meet all deadlines
+    (assuming an ideal uniprocessor), then there is also an EDF
+    schedule in which all deadlines are met. *)
+
+Section Optimality.
+  (* For any given type of jobs... *)
+  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+  
+  (* ... and any valid job arrival sequence. *)
+  Variable arr_seq: arrival_sequence Job.
+  Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
+
+  (* We observe that EDF is optimal in the sense that, if there exists
+     any schedule in which all jobs of arr_seq meet their deadline,
+     then there also exists an EDF schedule in which all deadlines are
+     met. *)
+  Theorem EDF_optimality:
+    (exists any_sched : schedule (ideal.processor_state Job),
+        valid_schedule any_sched arr_seq /\
+        all_deadlines_of_arrivals_met arr_seq any_sched) ->
+    exists edf_sched : schedule (ideal.processor_state Job),
+        valid_schedule edf_sched arr_seq /\
+        all_deadlines_of_arrivals_met arr_seq edf_sched /\
+        is_EDF_schedule edf_sched.
+  Proof.
+    move=> [sched [[COME [ARR COMP]] DL_ARR_MET]].
+    move: (all_deadlines_met_in_valid_schedule _ _ COME DL_ARR_MET) => DL_MET.
+    set sched' := edf_transform sched.
+    exists sched'. split; last split.
+    - by apply edf_schedule_is_valid.
+    - by apply edf_schedule_meets_all_deadlines_wrt_arrivals.
+    - by apply edf_transform_ensures_edf.
+  Qed.
+
+End Optimality.
+
+(** We further state a weaker notion of the above optimality claim
+    that avoids a dependency on a given arrival sequence. *)
+Section WeakOptimality.
+
+  (* For any given type of jobs,... *)
+  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+
+  (* ...if we have a well-behaved schedule in which no deadlines are missed,... *)
+  Variable any_sched: schedule (ideal.processor_state Job).
+  Hypothesis H_must_arrive: jobs_must_arrive_to_execute any_sched.
+  Hypothesis H_completed_dont_execute: completed_jobs_dont_execute any_sched.
+  Hypothesis H_all_deadlines_met: all_deadlines_met any_sched.
+
+  (* ...then there also exists a corresponding EDF schedule in which
+     no deadlines are missed (and in which exactly the same set of
+     jobs is scheduled, as ensured by the last clause). *)
+  Theorem weak_EDF_optimality:
+    exists edf_sched : schedule (ideal.processor_state Job),
+      jobs_must_arrive_to_execute edf_sched /\
+      completed_jobs_dont_execute edf_sched /\
+      all_deadlines_met edf_sched /\
+      is_EDF_schedule edf_sched /\
+      forall j,
+          (exists t,  scheduled_at any_sched j t) <->
+          (exists t', scheduled_at edf_sched j t').
+  Proof.
+    set sched' := edf_transform any_sched.
+    exists sched'. repeat split.
+    - by apply edf_transform_jobs_must_arrive.
+    - by apply edf_transform_completed_jobs_dont_execute.
+    - by apply edf_transform_deadlines_met.
+    - by apply edf_transform_ensures_edf.
+    - by move=> [t SCHED_j]; apply edf_transform_job_scheduled' with (t0 := t).
+    - by move=> [t SCHED_j]; apply edf_transform_job_scheduled with (t0 := t).
+  Qed.
+
+End WeakOptimality.

restructuring/analysis/transform/edf_trans.v

+From rt.restructuring.analysis.transform Require Export prefix swap.
+From rt.util Require Export search_arg.
+
+(** In this file we define the "EDF-ification" of a schedule, the
+    operation at the core of the EDF optimality proof. *)
+
+Section EDFTransformation.
+  (* Consider any given type of jobs... *)
+  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+
+  (* ... and ideal uniprocessor schedules. *)
+  Let PState := ideal.processor_state Job.
+  Let SchedType := schedule (PState).
+
+  (* We say that a state s1 "has an earlier or equal deadline" than a
+     state s2 if the job scheduled in state s1 has has an earlier or
+     equal deadline than the job scheduled in state s2. This function
+     is never used on idle states, so the default values are
+     irrelevant. *)
+  Definition earlier_deadline (s1 s2: PState) :=
+    (oapp job_deadline 0 s1) <= (oapp job_deadline 0 s2).
+
+  (* 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
+    | None => false
+    | Some j' => job_arrival j' <= reference_time
+    end.
+
+  (* Next, we define a central element of the "EDF-ification"
+     procedure: given a job scheduled at a time t1, find a later time
+     t2 before the job's deadlineat which a job with an
+     earlier-or-equal deadline is scheduled. In other words, find a
+     job that causes the [EDF_at] property to be violated at time
+     t1. *)
+  Definition find_swap_candidate (sched: SchedType) (t1: instant) (j: Job) :=
+    if search_arg sched (relevant_pstate t1) earlier_deadline t1 (job_deadline j) is Some t
+    then t
+    else 0.
+
+  (* The point-wise EDF-ification procedure: given a schedule and a
+     time t1, ensure that the schedule satisfies [EDF_at] at time
+     t1. *)
+  Definition make_edf_at (sched: SchedType) (t1: instant): SchedType :=
+    match sched t1 with
+    | None => sched (* leave idle instants alone *)
+    | Some j =>
+      let
+        t2 := find_swap_candidate sched t1 j
+      in swapped sched t1 t2
+    end.
+
+  (* To transform a finite prefix of a given reference schedule, apply
+     [make_edf_at] to every point up to the given finite horizon. *)
+  Definition edf_transform_prefix (sched: SchedType) (horizon: instant): SchedType :=
+    prefix_map sched make_edf_at horizon.
+
+  (* Finally, a full EDF schedule (i.e., one that satisfies [EDF_at]
+     at any time) is obtained by first computing an EDF prefix up to
+     and including the requested time t, and by then looking at the
+     last point of the prefix. *)
+  Definition edf_transform (sched: SchedType) (t: instant): ideal.processor_state Job :=
+    let
+      edf_prefix := edf_transform_prefix sched t.+1
+    in edf_prefix t.
+
+End EDFTransformation.
+

restructuring/model/schedule/edf.v

+From mathcomp Require Import ssrnat ssrbool fintype.
+From rt.restructuring.behavior Require Export schedule.
+
+(** In this file, we define what it means to be an "EDF schedule". *)
+Section DefinitionOfEDF.
+
+  (* For any given type of jobs... *)
+  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+
+  (* ... any given type of processor states: *)
+  Context {PState: eqType}.
+  Context `{ProcessorState Job PState}.
+
+  (* We say that a schedule is locally an EDF schedule at a point in
+     time [t] if the job scheduled at time [t] has a deadline that is
+     earlier than or equal to the deadline of any other job that could
+     be scheduled at time t but is scheduled later.
+
+     Note that this simple definition is (intentionally) oblivious to
+     (i.e., not compatible with) issues such as non-preemptive regions
+     or self-suspensions. *)
+  Definition EDF_at (sched: schedule PState) (t: instant) :=
+    forall (j: Job),
+      scheduled_at sched j t ->
+      forall (t': instant) (j': Job),
+        t <= t' ->
+        scheduled_at sched j' t' ->
+        job_arrival j' <= t ->
+        job_deadline j <= job_deadline j'.
+
+  (* A schedule is an EDF schedule if it is locally EDF at every point in time. *)
+  Definition is_EDF_schedule (sched: schedule PState) := forall t, EDF_at sched t.
+
+End DefinitionOfEDF.
+
+
+
+
+
+
+