Library rt.restructuring.analysis.edf.optimality

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:
    ( any_sched : schedule (ideal.processor_state Job),
        valid_schedule any_sched arr_seq
        all_deadlines_of_arrivals_met arr_seq any_sched)
     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.
     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:
     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
       j,
          ( t, scheduled_at any_sched j t)
          ( t', scheduled_at edf_sched j t').
  Proof.
    set sched' := edf_transform any_sched.
     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.