Added edf_wc.v

analysis/facts/transform/edf_wc.v

+Require Export prosa.analysis.facts.transform.edf_opt.
+Require Export prosa.analysis.facts.transform.wc_correctness.
+Require Export prosa.util.exists_extensionality.
+
+(** * Optimality of Work-Conserving EDF on Ideal Uniprocessors *)
+
+(** This file builds on the 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 that is work-conserving
+    in which all deadlines are met. *)
+
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import prosa.model.processor.ideal.
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import prosa.model.readiness.basic.
+
+
+(** We start by proving that the transform_prefix function at the core of the
+ edf transformation maintains work conservation *)
+Section EDFPrefixWorkConservationLemmas.
+
+  (** 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.
+
+  (** Consider an ideal uniprocessor schedule... *)
+  Variable sched: schedule (ideal.processor_state Job).
+
+  (** ...that is well-behaved...  *)
+  Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
+
+  (** ...and in which no scheduled job misses a deadline. *)
+  Hypothesis H_no_deadline_misses: all_deadlines_met sched.
+
+  (** Consider any point in time, denoted [horizon], and ... *)
+  Variable horizon: instant.
+
+  (** ...let [sched'] denote the schedule obtained by transforming
+     [sched] up to the horizon. *)
+  Let sched' := edf_transform_prefix sched horizon.
+
+  (** We show that if sched is work_conserving then so is sched' *)
+  Lemma edf_transform_prefix_maintains_work_conservation :
+    work_conserving arr_seq sched -> work_conserving arr_seq sched'.
+    Proof. Admitted.
+
+End EDFPrefixWorkConservationLemmas.
+
+(** Now that we proved that edf_transform_prefix maintains work_conservation,
+ we go ahead and prove that edf_transform maintains work_conservation *)
+Section EDFTransformWorkConservationLemmas.
+
+  (** 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.
+
+  (** Consider an ideal uniprocessor schedule... *)
+  Variable sched: schedule (ideal.processor_state Job).
+
+  (** ...that is well-behaved...  *)
+  Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
+
+  (** ...and in which no scheduled job misses a deadline. *)
+  Hypothesis H_no_deadline_misses: all_deadlines_met sched.
+
+  (** In the following, let [sched_edf] denote the EDF schedule obtained by
+     transforming the given reference schedule. *)
+  Let sched_edf := edf_transform sched.
+
+  (** We prove that transforming any work conserving schedule to an EDF schedule maintains work conservation *)
+  Lemma edf_transform_maintains_work_conservation :
+      work_conserving arr_seq sched -> work_conserving arr_seq sched_edf.
+  Proof.
+    move=> WC_sched j t ARR.
+    rewrite /sched_edf/edf_transform/backlogged/job_ready/basic_ready_instance/pending/completed_by/service/service_during.
+    have ->: \sum_(0 <= t0 < t) service_at (fun t1 : instant => edf_transform_prefix sched t1.+1 t1) j t0 =
+    \sum_(0 <= t0 < t) service_at (edf_transform_prefix sched t.+1) j t0.
+    {
+      apply eq_big_nat => t' /andP [_ LT_t].
+      rewrite /service_at.
+      rewrite (edf_prefix_inclusion _ _ _ _ t'.+1 t.+1) => //.
+      by apply ltn_trans with (n := t).
+    }
+    rewrite scheduled_at_def -scheduled_at_def =>BL.
+    have sched_at_def (s : schedule (processor_state Job)) t (j : Job) := scheduled_at_def s j t.
+    apply (exists_extensionality (sched_at_def (fun t0 : instant => edf_transform_prefix sched t0.+1 t0)  t)).
+    apply (exists_extensionality (sched_at_def _  t)).
+    have BL' : backlogged (edf_transform_prefix sched t.+1) j t by [].
+    move: ARR BL'. apply edf_transform_prefix_maintains_work_conservation; by [].
+  Qed.
+
+End EDFTransformWorkConservationLemmas.
+
+(** Finally, we state the theorems that jointly make up the work-conserving EDF optimality claim. *)
+Section WorkConservingEDFOptimality.
+  (** 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.
+
+  (** Now we can show that if there exists any schedule in which
+      all jobs of arr_seq meet their deadline, then there also exists
+      a work-conserving EDF in which all deadlines are met. *)
+  Theorem edf_wc_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_wc_sched : schedule (ideal.processor_state Job),
+      valid_schedule edf_wc_sched arr_seq /\
+      all_deadlines_of_arrivals_met arr_seq edf_wc_sched /\
+      work_conserving arr_seq edf_wc_sched /\
+      EDF_schedule edf_wc_sched.
+  Proof.
+    move=> [sched [[COME READY] DL_ARR_MET]].
+    have ARR  := jobs_must_arrive_to_be_ready sched READY.
+    have COMP := completed_jobs_are_not_ready sched READY.
+    move: (all_deadlines_met_in_valid_schedule _ _ COME DL_ARR_MET) => DL_MET.
+    set wc_sched := wc_transform arr_seq sched.
+    have wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
+      by apply wc_jobs_come_from_arrival_sequence.
+    have wc_READY : jobs_must_be_ready_to_execute wc_sched
+      by apply wc_jobs_must_be_ready_to_execute.
+    have wc_ARR := jobs_must_arrive_to_be_ready wc_sched wc_READY.
+    have wc_COMP := completed_jobs_are_not_ready wc_sched wc_READY.
+    have wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
+      by apply wc_all_deadlines_of_arrivals_met; apply DL_ARR_MET.
+    move: (all_deadlines_met_in_valid_schedule _ _ wc_COME wc_DL_ARR_MET) => wc_DL_MET.
+    set sched' := edf_transform wc_sched.
+    exists sched'. split; last split; last split.
+    - by apply edf_schedule_is_valid.
+    - by apply edf_schedule_meets_all_deadlines_wrt_arrivals. 
+    - apply edf_transform_maintains_work_conservation; by [ | apply wc_is_work_conserving ].
+    - by apply edf_transform_ensures_edf. 
+  Qed.
+
+End WorkConservingEDFOptimality.