Library prosa.results.edf.optimality


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


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...
... and the basic (i.e., Liu & Layland) readiness model under which any pending job is always ready.

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.
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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 68)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arr_seq_valid : valid_arrival_sequence arr_seq
  ============================
  (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 /\ EDF_schedule edf_sched

----------------------------------------------------------------------------- *)


  Proof.
    move⇒ [sched [[COME READY] DL_ARR_MET]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 99)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arr_seq_valid : valid_arrival_sequence arr_seq
  sched : schedule (ideal.processor_state Job)
  COME : jobs_come_from_arrival_sequence sched arr_seq
  READY : jobs_must_be_ready_to_execute sched
  DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
  ============================
  exists 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

----------------------------------------------------------------------------- *)


    have ARR := jobs_must_arrive_to_be_ready sched READY.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 110)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arr_seq_valid : valid_arrival_sequence arr_seq
  sched : schedule (ideal.processor_state Job)
  COME : jobs_come_from_arrival_sequence sched arr_seq
  READY : jobs_must_be_ready_to_execute sched
  DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
  ARR : jobs_must_arrive_to_execute sched
  ============================
  exists 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

----------------------------------------------------------------------------- *)


    have COMP := completed_jobs_are_not_ready sched READY.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 121)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arr_seq_valid : valid_arrival_sequence arr_seq
  sched : schedule (ideal.processor_state Job)
  COME : jobs_come_from_arrival_sequence sched arr_seq
  READY : jobs_must_be_ready_to_execute sched
  DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
  ARR : jobs_must_arrive_to_execute sched
  COMP : completed_jobs_dont_execute sched
  ============================
  exists 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

----------------------------------------------------------------------------- *)


    move: (all_deadlines_met_in_valid_schedule _ _ COME DL_ARR_MET) ⇒ DL_MET.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 133)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arr_seq_valid : valid_arrival_sequence arr_seq
  sched : schedule (ideal.processor_state Job)
  COME : jobs_come_from_arrival_sequence sched arr_seq
  READY : jobs_must_be_ready_to_execute sched
  DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
  ARR : jobs_must_arrive_to_execute sched
  COMP : completed_jobs_dont_execute sched
  DL_MET : all_deadlines_met sched
  ============================
  exists 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

----------------------------------------------------------------------------- *)


    set sched' := edf_transform sched.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 138)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arr_seq_valid : valid_arrival_sequence arr_seq
  sched : schedule (ideal.processor_state Job)
  COME : jobs_come_from_arrival_sequence sched arr_seq
  READY : jobs_must_be_ready_to_execute sched
  DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
  ARR : jobs_must_arrive_to_execute sched
  COMP : completed_jobs_dont_execute sched
  DL_MET : all_deadlines_met sched
  sched' := edf_transform sched : instant -> ideal.processor_state Job
  ============================
  exists 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

----------------------------------------------------------------------------- *)


     sched'.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 140)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arr_seq_valid : valid_arrival_sequence arr_seq
  sched : schedule (ideal.processor_state Job)
  COME : jobs_come_from_arrival_sequence sched arr_seq
  READY : jobs_must_be_ready_to_execute sched
  DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
  ARR : jobs_must_arrive_to_execute sched
  COMP : completed_jobs_dont_execute sched
  DL_MET : all_deadlines_met sched
  sched' := edf_transform sched : instant -> ideal.processor_state Job
  ============================
  valid_schedule sched' arr_seq /\
  all_deadlines_of_arrivals_met arr_seq sched' /\ EDF_schedule sched'

----------------------------------------------------------------------------- *)


split; last split.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 142)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arr_seq_valid : valid_arrival_sequence arr_seq
  sched : schedule (ideal.processor_state Job)
  COME : jobs_come_from_arrival_sequence sched arr_seq
  READY : jobs_must_be_ready_to_execute sched
  DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
  ARR : jobs_must_arrive_to_execute sched
  COMP : completed_jobs_dont_execute sched
  DL_MET : all_deadlines_met sched
  sched' := edf_transform sched : instant -> ideal.processor_state Job
  ============================
  valid_schedule sched' arr_seq

subgoal 2 (ID 145) is:
 all_deadlines_of_arrivals_met arr_seq sched'
subgoal 3 (ID 146) is:
 EDF_schedule sched'

----------------------------------------------------------------------------- *)


    - by apply edf_schedule_is_valid.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 145)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arr_seq_valid : valid_arrival_sequence arr_seq
  sched : schedule (ideal.processor_state Job)
  COME : jobs_come_from_arrival_sequence sched arr_seq
  READY : jobs_must_be_ready_to_execute sched
  DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
  ARR : jobs_must_arrive_to_execute sched
  COMP : completed_jobs_dont_execute sched
  DL_MET : all_deadlines_met sched
  sched' := edf_transform sched : instant -> ideal.processor_state Job
  ============================
  all_deadlines_of_arrivals_met arr_seq sched'

subgoal 2 (ID 146) is:
 EDF_schedule sched'

----------------------------------------------------------------------------- *)


    - by apply edf_schedule_meets_all_deadlines_wrt_arrivals.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 146)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arr_seq_valid : valid_arrival_sequence arr_seq
  sched : schedule (ideal.processor_state Job)
  COME : jobs_come_from_arrival_sequence sched arr_seq
  READY : jobs_must_be_ready_to_execute sched
  DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
  ARR : jobs_must_arrive_to_execute sched
  COMP : completed_jobs_dont_execute sched
  DL_MET : all_deadlines_met sched
  sched' := edf_transform sched : instant -> ideal.processor_state Job
  ============================
  EDF_schedule sched'

----------------------------------------------------------------------------- *)


    - by apply edf_transform_ensures_edf.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

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 ...
... in which no deadlines are missed, ...
...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').

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 80)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  any_sched : schedule (ideal.processor_state Job)
  H_must_arrive : jobs_must_arrive_to_execute any_sched
  H_completed_dont_execute : completed_jobs_dont_execute any_sched
  H_all_deadlines_met : all_deadlines_met any_sched
  ============================
  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 /\
    EDF_schedule edf_sched /\
    (forall j : Job,
     (exists t : instant, scheduled_at any_sched j t) <->
     (exists t' : instant, scheduled_at edf_sched j t'))

----------------------------------------------------------------------------- *)


  Proof.
    set sched' := edf_transform any_sched.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 85)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  any_sched : schedule (ideal.processor_state Job)
  H_must_arrive : jobs_must_arrive_to_execute any_sched
  H_completed_dont_execute : completed_jobs_dont_execute any_sched
  H_all_deadlines_met : all_deadlines_met any_sched
  sched' := edf_transform any_sched : instant -> ideal.processor_state Job
  ============================
  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 /\
    EDF_schedule edf_sched /\
    (forall j : Job,
     (exists t : instant, scheduled_at any_sched j t) <->
     (exists t' : instant, scheduled_at edf_sched j t'))

----------------------------------------------------------------------------- *)


     sched'.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 87)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  any_sched : schedule (ideal.processor_state Job)
  H_must_arrive : jobs_must_arrive_to_execute any_sched
  H_completed_dont_execute : completed_jobs_dont_execute any_sched
  H_all_deadlines_met : all_deadlines_met any_sched
  sched' := edf_transform any_sched : instant -> ideal.processor_state Job
  ============================
  jobs_must_arrive_to_execute sched' /\
  completed_jobs_dont_execute sched' /\
  all_deadlines_met sched' /\
  EDF_schedule sched' /\
  (forall j : Job,
   (exists t : instant, scheduled_at any_sched j t) <->
   (exists t' : instant, scheduled_at sched' j t'))

----------------------------------------------------------------------------- *)


repeat split.

(* ----------------------------------[ coqtop ]---------------------------------

6 subgoals (ID 89)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  any_sched : schedule (ideal.processor_state Job)
  H_must_arrive : jobs_must_arrive_to_execute any_sched
  H_completed_dont_execute : completed_jobs_dont_execute any_sched
  H_all_deadlines_met : all_deadlines_met any_sched
  sched' := edf_transform any_sched : instant -> ideal.processor_state Job
  ============================
  jobs_must_arrive_to_execute sched'

subgoal 2 (ID 96) is:
 completed_jobs_dont_execute sched'
subgoal 3 (ID 103) is:
 all_deadlines_met sched'
subgoal 4 (ID 110) is:
 EDF_schedule sched'
subgoal 5 (ID 123) is:
 (exists t : instant, scheduled_at any_sched j t) ->
 exists t' : instant, scheduled_at sched' j t'
subgoal 6 (ID 124) is:
 (exists t' : instant, scheduled_at sched' j t') ->
 exists t : instant, scheduled_at any_sched j t

----------------------------------------------------------------------------- *)


    - by apply edf_transform_jobs_must_arrive.

(* ----------------------------------[ coqtop ]---------------------------------

5 subgoals (ID 96)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  any_sched : schedule (ideal.processor_state Job)
  H_must_arrive : jobs_must_arrive_to_execute any_sched
  H_completed_dont_execute : completed_jobs_dont_execute any_sched
  H_all_deadlines_met : all_deadlines_met any_sched
  sched' := edf_transform any_sched : instant -> ideal.processor_state Job
  ============================
  completed_jobs_dont_execute sched'

subgoal 2 (ID 103) is:
 all_deadlines_met sched'
subgoal 3 (ID 110) is:
 EDF_schedule sched'
subgoal 4 (ID 123) is:
 (exists t : instant, scheduled_at any_sched j t) ->
 exists t' : instant, scheduled_at sched' j t'
subgoal 5 (ID 124) is:
 (exists t' : instant, scheduled_at sched' j t') ->
 exists t : instant, scheduled_at any_sched j t

----------------------------------------------------------------------------- *)


    - by apply edf_transform_completed_jobs_dont_execute.

(* ----------------------------------[ coqtop ]---------------------------------

4 subgoals (ID 103)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  any_sched : schedule (ideal.processor_state Job)
  H_must_arrive : jobs_must_arrive_to_execute any_sched
  H_completed_dont_execute : completed_jobs_dont_execute any_sched
  H_all_deadlines_met : all_deadlines_met any_sched
  sched' := edf_transform any_sched : instant -> ideal.processor_state Job
  ============================
  all_deadlines_met sched'

subgoal 2 (ID 110) is:
 EDF_schedule sched'
subgoal 3 (ID 123) is:
 (exists t : instant, scheduled_at any_sched j t) ->
 exists t' : instant, scheduled_at sched' j t'
subgoal 4 (ID 124) is:
 (exists t' : instant, scheduled_at sched' j t') ->
 exists t : instant, scheduled_at any_sched j t

----------------------------------------------------------------------------- *)


    - by apply edf_transform_deadlines_met.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 110)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  any_sched : schedule (ideal.processor_state Job)
  H_must_arrive : jobs_must_arrive_to_execute any_sched
  H_completed_dont_execute : completed_jobs_dont_execute any_sched
  H_all_deadlines_met : all_deadlines_met any_sched
  sched' := edf_transform any_sched : instant -> ideal.processor_state Job
  ============================
  EDF_schedule sched'

subgoal 2 (ID 123) is:
 (exists t : instant, scheduled_at any_sched j t) ->
 exists t' : instant, scheduled_at sched' j t'
subgoal 3 (ID 124) is:
 (exists t' : instant, scheduled_at sched' j t') ->
 exists t : instant, scheduled_at any_sched j t

----------------------------------------------------------------------------- *)


    - by apply edf_transform_ensures_edf.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 123)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  any_sched : schedule (ideal.processor_state Job)
  H_must_arrive : jobs_must_arrive_to_execute any_sched
  H_completed_dont_execute : completed_jobs_dont_execute any_sched
  H_all_deadlines_met : all_deadlines_met any_sched
  sched' := edf_transform any_sched : instant -> ideal.processor_state Job
  j : Job
  ============================
  (exists t : instant, scheduled_at any_sched j t) ->
  exists t' : instant, scheduled_at sched' j t'

subgoal 2 (ID 124) is:
 (exists t' : instant, scheduled_at sched' j t') ->
 exists t : instant, scheduled_at any_sched j t

----------------------------------------------------------------------------- *)


    - by move⇒ [t SCHED_j]; apply edf_transform_job_scheduled' with (t0 := t).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 124)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  H1 : JobArrival Job
  any_sched : schedule (ideal.processor_state Job)
  H_must_arrive : jobs_must_arrive_to_execute any_sched
  H_completed_dont_execute : completed_jobs_dont_execute any_sched
  H_all_deadlines_met : all_deadlines_met any_sched
  sched' := edf_transform any_sched : instant -> ideal.processor_state Job
  j : Job
  ============================
  (exists t' : instant, scheduled_at sched' j t') ->
  exists t : instant, scheduled_at any_sched j t

----------------------------------------------------------------------------- *)


    - by move⇒ [t SCHED_j]; apply edf_transform_job_scheduled with (t0 := t).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

End WeakOptimality.