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.analysis.facts.readiness.backlogged.
+
+
+(** * Optimality of Work-Conserving EDF on Ideal Uniprocessors *)
+
+(** In this file, we establish the foundation needed to connect the EDF and
+    work-conservation optimality theorems: if there is any work-conserving 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.
+
+(** ** Non-Idle Swaps *)
+
+(** We start by showing that [swapped], a function used in 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, and in which all jobs come
+     from the arrival sequence). *)
+  Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
+  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.
+
+  (** ...which we assume to be ordered (to avoid dealing with symmetric cases),... *)
+  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.
+
+  (** ...[j1] is scheduled at time [t1], and... *)
+  Hypothesis H_t1_not_idle : scheduled_at sched j1 t1.
+
+  (** ...[j2] is scheduled at time [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 an arbitrary instant [t]... *)
+  Variable t : instant.
+
+  (** ...such that [j] arrives in [arr_seq]... *)
+  Hypothesis H_arrival_j : arrives_in arr_seq j.
+
+  (** ...and is backlogged in [swap_sched] at instant [t]. *)
+  Hypothesis H_backlogged_j_t : backlogged swap_sched j t.
+
+  (** We proceed by case analysis. 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.
+
+(** ** Work-Conserving Swap Candidates *)
+
+(** 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.
+
+  (** ...and in which all jobs 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 [j1]'s 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 processor allocations at
+     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.
+
+(** ** Work-Conservation of the Point-Wise EDF Transformation *)
+
+(** In the following section, we show 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).
+
+  (** ... in which all jobs 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.
+
+(** ** Work-Conserving EDF Prefix *)
+
+(** 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).
+
+  (** ... an arbitrary finite [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.
+
+  (** 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], and
+      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.
+
+  (** For brevity, 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.
+
+(** ** Work-Conservation of the EDF Transformation *)
+
+(** Finally, having established that [edf_transform_prefix] maintains work
+    conservation, we go ahead and prove that [edf_transform] maintains work
+    conservation, too. *)
+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 a valid ideal uniprocessor schedule ... *)
+  Variable sched: schedule (ideal.processor_state Job).
+  Hypothesis H_sched_valid: valid_schedule sched arr_seq.
+
+  (** ...and in which no scheduled job misses a deadline. *)
+  Hypothesis H_no_deadline_misses: all_deadlines_met sched.
+
+  (** We first note that [sched] satisfies [scheduled_behavior_premises]. *)
+  Lemma sched_satisfies_behavior_premises : scheduled_behavior_premises arr_seq sched.
+  Proof.
+    split; [ apply (jobs_must_arrive_to_be_ready sched) | split; [ apply (completed_jobs_are_not_ready sched) | split]].
+    all: by try apply H_sched_valid.
+  Qed.
+
+  (** We prove that, if the given schedule [sched] is work-conserving, then the
+      schedule that results from transforming it into an EDF schedule is also
+      work-conserving. *)
+  Lemma edf_transform_maintains_work_conservation :
+    work_conserving arr_seq sched -> work_conserving arr_seq (edf_transform sched).
+  Proof.
+    move=> WC_sched j t ARR.
+    set sched_edf := edf_transform sched.
+    have IDENT:  identical_prefix sched_edf (edf_transform_prefix sched t.+1) t.+1
+      by rewrite /sched_edf/edf_transform => t' LE_t; apply (edf_prefix_inclusion) => //; apply sched_satisfies_behavior_premises.
+    rewrite (backlogged_prefix_invariance _ _ (edf_transform_prefix sched t.+1) t.+1) // => BL;
+            last by apply basic_readiness_nonclairvoyance.
+    have WC_trans: work_conserving arr_seq  (edf_transform_prefix sched (succn t))
+      by apply edf_transform_prefix_maintains_work_conservation; split => //; apply sched_satisfies_behavior_premises.
+    move: (WC_trans _ _ ARR BL) => [j_other SCHED_AT].
+    exists j_other.
+    now rewrite (identical_prefix_scheduled_at _ (edf_transform_prefix sched t.+1) t.+1) //.
+  Qed.
+
+End EDFTransformWorkConservationLemmas.
+