Library prosa.results.edf.optimality

Require Export prosa.analysis.facts.transform.edf_opt.

Optimality of EDF on Ideal Uniprocessors

This module provides the famous EDF optimality theorem: if there is any way to meet all deadlines (assuming an ideal uniprocessor schedule), then there is also an (ideal) EDF schedule in which all deadlines are met.
The following results assume ideal uniprocessor schedules...
Require prosa.model.processor.ideal.
... and the basic (i.e., Liu & Layland) readiness model under which any pending job is always ready.
Require prosa.model.readiness.basic.

Optimality Theorem


Section Optimality.
For any given type of jobs, each characterized by execution costs, an arrival time, and an absolute deadline,...
  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 ∧
        EDF_schedule edf_sched.

End Optimality.

Weak Optimality Theorem

We further state a weaker notion of the above optimality result that avoids a dependency on a given arrival sequence. Specifically, it establishes that, given a reference schedule without deadline misses, there exists an EDF schedule of the same jobs in which no deadlines are missed.
Section WeakOptimality.

For any given type of jobs, each characterized by execution costs, an arrival time, and an absolute deadline,...
  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.

... if we have a well-behaved reference schedule ...
  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.

... in which no deadlines are missed, ...
  Hypothesis H_all_deadlines_met: all_deadlines_met any_sched.

...then there also exists an 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 ∧
      EDF_schedule edf_sched ∧
      ∀ j,
          (∃ t, scheduled_at any_sched j t) ↔
          (∃ t', scheduled_at edf_sched j t').

End WeakOptimality.