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:
+    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.
@@ -7,7 +17,204 @@ Require Import prosa.model.processor.ideal.
 Require Import prosa.model.readiness.basic.
 
 
-Section Optimality.
+(** 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... *)
+  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 (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.
+
+  (** 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.
+
+  (** ...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 t2 is a swap candidate returned by fsc for t1 in a schedule
+      then swapping the two instants maintains work conservation *)
+  Lemma 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.
+    move=> WC_sched. 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.
+    move=> j t ARR BL.
+     case: (boolP(t == t1)) => [/eqP EQ| /eqP NEQ].
+    - rewrite EQ. by exists j2; rewrite swap_job_scheduled_t1. (* t = t1 *)
+    - case: (boolP(t == t2)) => [/eqP EQ'| /eqP NEQ']. (* t <> t1 *)
+      + rewrite EQ' //. by exists j1; rewrite swap_job_scheduled_t2. (* t = t2 *)
+      + case: (boolP(t <= t1)) => [LEQ | GT]; last rewrite -ltnNge in GT. (* t <> t1 /\ 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]. 
+            apply /andP; split; first (apply /andP; split) => //. 
+            rewrite (service_before_swap_invariant sched t1 t2 _ t) // /t2.
+            apply fsc_range1 => //. rewrite -(swap_job_scheduled_other_times _ t1 t2 j t) //;
+            (apply /neqP; eauto). }
+          exists j_other. rewrite  (swap_job_scheduled_other_times) //; do 2! (apply /neqP; eauto).
+        - case: (boolP(t2 < t)) => [LT | GEQ]; last rewrite -leqNgt in GEQ.
+          + 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]. 
+              apply /andP; split; first (apply /andP; split) => //. 
+              rewrite (service_after_swap_invariant sched t1 t2 _ t) // /t2.
+              apply fsc_range1 => //. rewrite -(swap_job_scheduled_other_times _ t1 t2 j t) //;
+              (apply /neqP; eauto). }
+          exists j_other. rewrite  (swap_job_scheduled_other_times) //; do 2! (apply /neqP; eauto).
+          + case: (boolP(scheduled_at sched j2 t)) => Hj'.
+            - exists j2. rewrite (swap_job_scheduled_other_times _ t1 t2 j2 t) //; (apply /neqP; eauto).
+            - 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).
+                unfold jobs_come_from_arrival_sequence in H_from_arr_seq.
+                apply (H_from_arr_seq _ t2) => // /backlogged/job_ready/basic_ready_instance/pending/completed_by.
+                apply /andP; split; first (apply /andP; split) => //; last by []. 
+                rewrite /has_arrived. apply (leq_trans t2_arrival). by apply ltnW.
+                rewrite -ltnNge. apply (leq_ltn_trans) with (service sched j2 t2).
+                  by apply service_monotonic. apply H_completed_jobs_dont_execute => //. }
+              exists j_other. rewrite  (swap_job_scheduled_other_times) //; do 2! (apply /neqP; eauto).
+  Qed.
+
+
+End FSCWorkConservationLemmas.
+
+
+(** In the next setcion, 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.
+
+  (** ...and in which no scheduled job misses a deadline. *)
+  Hypothesis H_no_deadline_misses: all_deadlines_met sched.
+
+  (** We analyze [make_edf_at] applied to an arbitrary point in time,
+     which we denote [t_edf] in the following. *)
+  Variable t_edf: instant.
+
+  (** 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 a schedule is work_conserving then applying make_edf_at
+     to it at some instant t_edf maintains work conservation. *)
+  Lemma mea_maintains_work_conservation :
+    work_conserving arr_seq sched -> work_conserving arr_seq sched'.
+  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) => //.
+         apply ideal_proc_model_ensures_ideal_progress.
+         rewrite /all_deadlines_met in  (H_no_deadline_misses).
+         apply (H_no_deadline_misses s t_edf); rewrite scheduled_at_def; by 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).
+
+  (** ...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.
+
+  (** ...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_trans] denote the schedule obtained by transforming
+     [sched] up to the horizon. *)
+  Let sched_trans := edf_transform_prefix sched horizon.
+
+  (** We show that if sched is work_conserving then so is sched_trans *)
+  Lemma edf_transform_prefix_maintains_work_conservation :
+    work_conserving arr_seq sched -> work_conserving arr_seq sched_trans.
+    Proof. 
+      rewrite /sched_trans/edf_transform_prefix.
+      have [COMP [ARR DL_MET]] : completed_jobs_dont_execute sched_trans /\
+                                 jobs_must_arrive_to_execute sched_trans /\ all_deadlines_met sched_trans.
+        by apply edf_prefix_well_formedness.
+        have PREMISES : sched_arrival_premises sched arr_seq.
+        { rewrite /sched_arrival_premises; split => //; last split => //.
+          rewrite /valid_schedule; split => //; by apply basic_readiness_compliance. }
+        move=> WC_sched; apply (prefix_map_property_invariance_with_assumps arr_seq) => //.
+        move => t sched' [ARR' [[COME' READY'] MET']]; split => //; last split.
+        rewrite /valid_schedule; split => //. by apply edf_prefix_jobs_come_from_arrival_sequence.
+        apply basic_readiness_compliance;
+        repeat (apply edf_prefix_well_formedness => //;
+          try apply (jobs_must_arrive_to_be_ready sched') => //;
+          try apply (completed_jobs_are_not_ready sched') => //).
+        apply edf_prefix_well_formedness => //;
+          try apply (jobs_must_arrive_to_be_ready sched') => //;
+          apply (completed_jobs_are_not_ready sched') => //.
+        move => t sched' [ARR' [[COME' READY'] MET']]. 
+        apply mea_maintains_work_conservation => //; first by apply (jobs_must_arrive_to_be_ready sched'). 
+        by apply (completed_jobs_are_not_ready sched'). 
+    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 *)
+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}.
@@ -17,14 +224,63 @@ Section Optimality.
   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 corresponds to the given arrival sequence. *)
+  Hypothesis H_sched_valid: valid_schedule sched arr_seq.
 
-  (* do we need to specify predicates for the schedule (e.g. valid) or for the arrival sequence? *)
+  (** ...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 :
-    forall sched : schedule (ideal.processor_state Job),
-      work_conserving arr_seq sched -> work_conserving arr_seq (edf_transform sched).
-  Proof. Admitted.
+      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 (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'. 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}.
 
-  Theorem EDF_WC_optimality :
+
+  (** ... 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) ->
@@ -38,7 +294,6 @@ Section Optimality.
     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.
@@ -49,15 +304,12 @@ Section Optimality.
     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. 
-    - by apply edf_transform_maintains_work_conservation; apply wc_is_work_conserving.
+    - apply edf_transform_maintains_work_conservation; by [ | apply wc_is_work_conserving ].
     - by apply edf_transform_ensures_edf. 
   Qed.
 
-
-
-End Optimality.
+End WorkConservingEDFOptimality.