Skip to content
Snippets Groups Projects

Added edf_wc.v

Closed Added edf_wc.v
wip-edf-wc into master
Closed LailaElbeheiry requested to merge wip-edf-wc into master
Compare
and
Show latest version
5 files
+ 305
− 43
Compare changes
  • Side-by-side
  • Inline
Files
5
analysis/facts/transform/edf_wc.v
+ 239
− 39
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,199 @@ 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.
(** ...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.
(** ...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}.
@@ -17,47 +219,45 @@ 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.
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.
work_conserving arr_seq sched -> work_conserving arr_seq sched_edf.
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.
- by apply edf_transform_maintains_work_conservation; apply wc_is_work_conserving.
- by apply edf_transform_ensures_edf.
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.
End Optimality.