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.analysis.facts.behavior.deadlines.
 Require Export prosa.util.exists_extensionality.
 
+
 (** * Optimality of Work-Conserving EDF on Ideal Uniprocessors *)
 
 (** This file builds on the EDF optimality theorem:
@@ -15,21 +17,113 @@ Require Import prosa.model.processor.ideal.
 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.
+(** We start by showing that work conservation is maintained by the inner-most level
+    of [edf_transform] which is [find_swap_candidate]. *)
+Section FSCWorkConservationLemmas.
 
-  (** For any given type of jobs, each characterized by execution
-      costs, an arrival time, and an absolute deadline,... *)
+  (** 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.
 
-  (** Consider an ideal uniprocessor schedule... *)
+  (** ...consider an ideal uniprocessor schedule... *)
+  Variable sched: schedule (ideal.processor_state Job).
+
+  (** ...that is well-behaved (i.e., in which jobs execute only after
+     having arrived and only if they are not yet complete). *)
+  Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
+
+
+  (** ...if all jobs in the original schedule come from the arrival sequence,... *)
+  Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
+
+ (** We start by showing that if [t1] and [t2] are two non-idle instants in [sched],
+     whose jobs arrive before [t1] then swapping them maintains work_conservation *)
+  Lemma non_idle_swap_maintains_work_conservation :
+    forall t1 t2 j1 j2, scheduled_at sched j1 t1 -> scheduled_at sched j2 t2 -> t1 <= t2 -> job_arrival j2 <= t1 ->
+                   work_conserving arr_seq sched ->
+                   work_conserving arr_seq (swapped sched t1 t2).
+  Proof.
+    move=> t1 t2 j1 j2 t1_not_idle t2_not_idle t1_lte_t2 j2_arrival WC_sched.
+    move=> j t ARR BL. 
+    case: (boolP(t == t1)) => [/eqP EQ| /eqP NEQ].
+    - rewrite EQ. exists j2; by rewrite swap_job_scheduled_t1. (* t = t1 *)
+    - case: (boolP(t == t2)) => [/eqP EQ'| /eqP NEQ']. (* t <> t1 *)
+      + rewrite EQ' //. exists j1; by rewrite swap_job_scheduled_t2. (* t = t2 *)
+      + case: (boolP((t <= t1) || (t2 < t))) => [NOT_BET | BET]. (* t <> t2 *)
+        * have [j_other j_other_scheduled] : exists j_other, scheduled_at sched j_other t.
+          { rewrite /work_conserving in WC_sched. apply (WC_sched j) => //; move :BL.
+            rewrite /backlogged/job_ready/basic_ready_instance/pending/completed_by.
+            move /andP => [ARR_INCOMP scheduled]; move :ARR_INCOMP; move /andP => [arrive not_comp]. 
+            move: NOT_BET; move/orP => [] => NOT_BET; (apply /andP; split; first (apply /andP; split) => //).
+            + by rewrite (service_before_swap_invariant sched t1 t2 _ t). 
+            + by rewrite -(swap_job_scheduled_other_times _ t1 t2 j t) //; (apply /neqP; eauto).
+            + by rewrite (service_after_swap_invariant sched t1 t2 _ t) // /t2; apply fsc_range1.
+            + by rewrite -(swap_job_scheduled_other_times _ t1 t2 j t) //; (apply /neqP; eauto).
+          }
+          exists j_other; by rewrite  (swap_job_scheduled_other_times) //; do 2! (apply /neqP; eauto).
+        * case: (boolP(scheduled_at sched j2 t)) => Hj'.
+          { by exists j2; rewrite (swap_job_scheduled_other_times _ t1 t2 j2 t) //; (apply /neqP; eauto). }
+          { move: BET; rewrite negb_or; move /andP; case; rewrite <- ltnNge => range1; rewrite <- leqNgt => range2.
+            have [j_other j_other_scheduled] : exists j_other, scheduled_at sched j_other t. 
+            { rewrite /work_conserving in WC_sched. apply (WC_sched j2).
+              + by unfold jobs_come_from_arrival_sequence in H_from_arr_seq; apply (H_from_arr_seq _ t2) => //.
+              + rewrite/backlogged/job_ready/basic_ready_instance/pending/completed_by.
+                apply /andP; split; first (apply /andP; split) => //; last by done.
+                * by rewrite /has_arrived; apply (leq_trans j2_arrival); apply ltnW. 
+                * rewrite -ltnNge. apply (leq_ltn_trans) with (service sched j2 t2). 
+                  - by apply service_monotonic. 
+                  - by apply H_completed_jobs_dont_execute. } 
+            exists j_other. now rewrite  (swap_job_scheduled_other_times) //; (apply /neqP; eauto). }
+Qed.
+
+  (** Suppose we are given a job [j1]... *)
+  Variable j1: Job.
+
+  (** ...and a point in time [t1]... *)
+  Variable t1: instant.
+
+  (** ...at which [j1] is scheduled... *)
+  Hypothesis H_not_idle: scheduled_at sched j1 t1.
+
+  (** ...and that is before its deadline. *)
+  Hypothesis H_deadline_not_missed: t1 < job_deadline j1.
+
+
+ (** We now show that if [t2] is a swap candidate returned by [find_swap_candidate] for [t1]
+     then swapping the two instants maintains work conservation *)
+  Corollary fsc_swap_maintains_work_conservation :
+    work_conserving arr_seq sched ->
+    work_conserving arr_seq (swapped sched t1 (edf_trans.find_swap_candidate sched t1 j1)).
+  Proof.
+    set t2 := edf_trans.find_swap_candidate sched t1 j1. 
+    have [j2 [t2_not_idle t2_arrival]] : exists j2, scheduled_at sched j2 t2 /\ job_arrival j2 <= t1
+        by apply fsc_not_idle.
+    now apply (non_idle_swap_maintains_work_conservation t1 t2 j1 j2) => //; apply fsc_range1 => //.
+Qed.
+
+End FSCWorkConservationLemmas.
+
+(** In the next section, we show that that work conservation is maintained by the
+    next level of [edf_transform] which is [make_edf_at]. *)
+Section MakeEDFWorkConservationLemmas.
+
+  (** 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.
+
+  (** ...consider an ideal uniprocessor schedule... *)
   Variable sched: schedule (ideal.processor_state Job).
 
+  (** ...if all jobs in the original schedule come from the arrival sequence,... *)
+  Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
+
   (** ...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.
@@ -37,22 +131,83 @@ Section EDFPrefixWorkConservationLemmas.
   (** ...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.
+  (** We analyze [make_edf_at] applied to an arbitrary point in time,
+     which we denote [t_edf] in the following. *)
+  Variable t_edf: instant.
 
-  (** ...let [sched'] denote the schedule obtained by transforming
-     [sched] up to the horizon. *)
-  Let sched' := edf_transform_prefix sched horizon.
+  (** For brevity, let [sched'] denote the schedule obtained from
+      [make_edf_at] applied to [sched] at time [t_edf]. *)
+  Let sched' := make_edf_at sched t_edf.
 
-  (** We show that if sched is work_conserving then so is sched' *)
-  Lemma edf_transform_prefix_maintains_work_conservation :
+  (* We show that if a schedule is work_conserving then applying [make_edf_at]
+     to it at an arbitrary instant [t_edf] maintains work conservation. *)
+  Lemma mea_maintains_work_conservation :
     work_conserving arr_seq sched -> work_conserving arr_seq sched'.
-    Proof. Admitted.
+  Proof. rewrite /sched'/make_edf_at => WC_sched. destruct (sched t_edf) eqn:E => //.
+         apply fsc_swap_maintains_work_conservation => //.
+         -  by rewrite scheduled_at_def; apply /eqP => //.
+         - apply (scheduled_at_implies_later_deadline sched) => //.
+           + by apply ideal_proc_model_ensures_ideal_progress.
+           + rewrite /all_deadlines_met in  (H_no_deadline_misses).
+             now apply (H_no_deadline_misses s t_edf); rewrite scheduled_at_def; apply /eqP.
+           + by rewrite scheduled_at_def; apply/eqP => //.
+  Qed.
+
+End MakeEDFWorkConservationLemmas.
+
+(** On to the next layer, we prove 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).
+
+  Variable horizon: instant.
+
+  (** ...let [sched_trans] denote the schedule obtained by transforming
+      [sched] up to the horizon. *)
+  Let sched_trans := edf_transform_prefix sched horizon.
+
+  (* Let [schedule_behavior_premises] define the premise that a schedule is:
+     1) well-behaved
+     2) has all jobs coming from the arrival sequence [arr_seq]
+     3) in which no scheduled job misses its deadline *)
+  Definition scheduled_behavior_premises (sched : schedule (processor_state Job)) :=
+    jobs_must_arrive_to_execute sched /\ completed_jobs_dont_execute sched /\
+    jobs_come_from_arrival_sequence sched arr_seq /\ all_deadlines_met sched.
+
+  (* Let [P] denote the predicate that a schedule satisfies [scheduled_behavior_premises]
+     and is work-conserving *)
+  Let P (sched : schedule (processor_state Job)) :=
+    scheduled_behavior_premises sched /\ work_conserving arr_seq sched.
+
+  (** We show that if [sched] is work-conserving then so is [sched_trans] *)
+  Lemma edf_transform_prefix_maintains_work_conservation:
+    P sched -> P sched_trans.
+  Proof.
+    rewrite/sched_trans/edf_transform_prefix. apply (prefix_map_property_invariance ). rewrite /P.
+    move=> sched' t  [[H_ARR [H_COMPLETED [H_COME H_all_deadlines_met]]] H_wc_sched].
+    rewrite/scheduled_behavior_premises/valid_schedule; split; first split. 
+    - by apply mea_jobs_must_arrive.
+    - split; last split.
+      + by apply mea_completed_jobs.
+      + by apply mea_jobs_come_from_arrival_sequence.
+      + by apply mea_no_deadline_misses.
+    - by apply mea_maintains_work_conservation.
+  Qed.
 
 End EDFPrefixWorkConservationLemmas.
 
-(** Now that we proved that edf_transform_prefix maintains work_conservation,
- we go ahead and prove that edf_transform maintains work_conservation *)
+(** 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
@@ -67,6 +222,12 @@ Section EDFTransformWorkConservationLemmas.
   (** Consider an ideal uniprocessor schedule... *)
   Variable sched: schedule (ideal.processor_state Job).
 
+  (** ...if all jobs in the original schedule come from the arrival sequence,... *)
+  Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... that corresponds to the given arrival sequence. *)
+  Hypothesis H_sched_valid: valid_schedule sched arr_seq.
+
   (** ...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.
@@ -78,74 +239,25 @@ Section EDFTransformWorkConservationLemmas.
      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 *)
+  (** 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.
+    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 =
+    rewrite /backlogged/job_ready/basic_ready_instance/pending/completed_by/service/service_during.
+    have ->: \sum_(0 <= t0 < t) service_at sched_edf 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.
+    { apply eq_big_nat.  move => t' /andP [_ LT_t].
+      rewrite /sched_edf/edf_transform/service_at (edf_prefix_inclusion _ _ _ _ t'.+1 t.+1) => //.
+      now apply ltn_trans with (n := t). }
+    rewrite /sched_edf/edf_transform 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 [].
+    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 done.
+    move: ARR BL'. by apply edf_transform_prefix_maintains_work_conservation.
   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.