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.
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import prosa.model.readiness.basic.
+
+(** We start by showing that [swapped] a function used by the inner-most level of [edf_transform]
+    maintains work conservation if the two instants being swapped are not idle. *)
+Section NonIdleSwapWorkConservationLemmas.
+
+  (** 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.
+
+  (** ...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.
+
+  (** ...suppose we are given two specific times [t1] and [t2],... *)
+  Variables t1 t2 : instant.
+
+  (** ...where, to avoid dealing with symmetric cases, assume in the following
+     that t1 and t2 are ordered,... *)
+  Hypothesis H_well_ordered: t1 <= t2.
+
+  (** ...and two jobs [j1] and [j2],... *)
+  Variables j1 j2 : Job.
+
+  (** ...such that [j2] arrives before time [t1],... *)
+  Hypothesis H_arrival_j2 : job_arrival j2 <= t1.
+
+  (** ...and that [j1] is scheduled at [t1],... *)
+  Hypothesis H_t1_not_idle : scheduled_at sched j1 t1.
+
+  (** ...and [j2] is scheduled at [t2]. *)
+  Hypothesis H_t2_not_idle : scheduled_at sched j2 t2.
+
+  (** We let [swap_sched] denote the schedule in which the allocations at
+      [t1] and [t2] have been swapped. *)
+  Let swap_sched := swapped sched t1 t2.
+
+  (** Now consider an arbitrary job [j],... *)
+  Variable j : Job.
+
+  (** ...and arbitrary instant [t],... *)
+  Variable t : instant.
+
+  (** ...such that [j] arrives in [arr_seq],... *)
+  Hypothesis H_arrival_j : arrives_in arr_seq j.
+
+  (** ...and [j] is backlogged in [swap_sched] at instant [t] *)
+  Hypothesis H_backlogged_j_t : backlogged swap_sched j t.
+
+  (** We first show that if [t] equals [t1] then swap_sched maintains work conservation.
+      That is, there exists some job that's scheduled in [swap_sched] at instant [t] *)
+  Lemma non_idle_swap_maintains_work_conservation_t1 :
+    work_conserving arr_seq sched ->
+    t = t1 -> exists j_other, scheduled_at swap_sched j_other t.
+  Proof.
+    move=> _ EQ; rewrite EQ; by exists j2; rewrite swap_job_scheduled_t1.
+  Qed.
+
+  (** Similarly, if [t] equals [t2] then then swap_sched maintains work conservation. *)
+  Lemma non_idle_swap_maintains_work_conservation_t2 :
+    work_conserving arr_seq sched ->
+    t = t2 -> exists j_other, scheduled_at swap_sched j_other t.
+  Proof.
+    move=> _ EQ; rewrite EQ; by exists j1; rewrite swap_job_scheduled_t2.
+  Qed.
+
+  (** If [t] is less than or equal to [t1] then then then swap_sched maintains work conservation. *)
+  Lemma non_idle_swap_maintains_work_conservation_LEQ_t1 :
+    work_conserving arr_seq sched ->
+    t <= t1 -> exists j_other, scheduled_at swap_sched j_other t.
+  Proof.
+    move=> WC_sched LEQ.
+    case: (boolP(t == t1)) => [/eqP EQ| /eqP NEQ]; first by apply non_idle_swap_maintains_work_conservation_t1.
+    case: (boolP(t == t2)) => [/eqP EQ'| /eqP NEQ']; first by apply non_idle_swap_maintains_work_conservation_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 :H_backlogged_j_t.
+      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) => //.
+      + by rewrite (service_before_swap_invariant sched t1 t2 _ t). 
+      + 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).
+  Qed.
+
+  (** Similarly, if [t] is greater than [t2] then then then swap_sched maintains work conservation. *)
+  Lemma non_idle_swap_maintains_work_conservation_GT_t2 :
+    work_conserving arr_seq sched ->
+    t2 < t -> exists j_other, scheduled_at swap_sched j_other t.
+  Proof.
+    move=> WC_sched GT.
+    case: (boolP(t == t1)) => [/eqP EQ| /eqP NEQ]; first by apply non_idle_swap_maintains_work_conservation_t1.
+    case: (boolP(t == t2)) => [/eqP EQ'| /eqP NEQ']; first by apply non_idle_swap_maintains_work_conservation_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 :H_backlogged_j_t.
+      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) => //.
+      + 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).
+  Qed.
+
+  (* Lastly, we show that if [t] lies between [t1] and [t2] then work conservation is still maintained. *)
+  Lemma non_idle_swap_maintains_work_conservation_BET_t1_t2 :
+    work_conserving arr_seq sched ->
+    t1 < t <= t2 -> exists j_other, scheduled_at swap_sched j_other t.
+  Proof.
+    move=> WC_sched H_range.
+    case: (boolP(t == t1)) => [/eqP EQ| /eqP NEQ]; first by apply non_idle_swap_maintains_work_conservation_t1.
+    case: (boolP(t == t2)) => [/eqP EQ'| /eqP NEQ']; first by apply non_idle_swap_maintains_work_conservation_t2.
+    move: H_range. move /andP => [LT GE].
+    case: (boolP(scheduled_at sched j2 t)) => Hj'.
+    - exists j2; by 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).
+        - 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 H_arrival_j2); 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.
+
+End NonIdleSwapWorkConservationLemmas.
+
+
+(** Now, we show 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.
+
+  (** ...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.
+
+  (** 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.
+    have H_range : t1 <= t2 by apply fsc_range1.
+    move=> WC_sched j t ARR BL.
+    case: (boolP(t == t1)) => [/eqP EQ| /eqP NEQ].
+    - by apply (non_idle_swap_maintains_work_conservation_t1 arr_seq _ _ _ j2).
+    - case: (boolP(t == t2)) => [/eqP EQ'| /eqP NEQ'].
+      + by apply (non_idle_swap_maintains_work_conservation_t2 arr_seq _ _ _ j1).
+      + case: (boolP((t <= t1) || (t2 < t))) => [NOT_BET | BET]. (* t <> t2 *)
+        * move: NOT_BET; move/orP => [] => NOT_BET.
+          { by apply (non_idle_swap_maintains_work_conservation_LEQ_t1 arr_seq _ _ _ H_range _ _ H_not_idle t2_not_idle j).  }
+          { by apply (non_idle_swap_maintains_work_conservation_GT_t2 arr_seq _ _ _ H_range _ _ H_not_idle t2_not_idle j). }
+        * move: BET; rewrite negb_or. move /andP. case; rewrite <- ltnNge => range1; rewrite <- leqNgt => range2.
+          have BET: (t1 < t) && (t <= t2) by apply /andP.
+          now apply (non_idle_swap_maintains_work_conservation_BET_t1_t2 arr_seq _ H_completed_jobs_dont_execute H_from_arr_seq _ _ _ _ t2_arrival H_not_idle t2_not_idle ).
+  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.
+
+  (** ...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 an arbitrary 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) => //.
+           + 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 *)
+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).
+
+  (** ...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.
+
+  (** ...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 /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.  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 done.
+    move: ARR BL'. by apply edf_transform_prefix_maintains_work_conservation.
+  Qed.
+
+End EDFTransformWorkConservationLemmas.
+