restructured wc_correctness file, added some lines to FSC proof

parent f462b010
Pipeline #22002 failed with stages
in 3 minutes and 54 seconds
......@@ -15,88 +15,16 @@ Require Export rt.restructuring.model.processor.ideal.
Require Export rt.restructuring.model.readiness.basic.
Section ArrivalSequence.
Section WCCorrectnessFacts.
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
Section ArrivalSequenceMWA.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arr_seq_valid : valid_arrival_sequence arr_seq.
Variable sched: schedule (ideal.processor_state Job).
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
Variable t: instant.
Let sched' := make_wc_at arr_seq sched t.
Lemma mwa_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched' arr_seq.
Proof.
rewrite /sched' /make_wc_at.
destruct (sched t) as [j_orig|] eqn:SCHED_orig; first by done.
by apply swapped_jobs_come_from_arrival_sequence.
Qed.
End ArrivalSequenceMWA.
Section ArrivalSequencePrefix.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arr_seq_valid : valid_arrival_sequence arr_seq.
Section FSCFacts.
Variable sched: schedule (ideal.processor_state Job).
Variable horizon: instant.
Variable arr_seq: arrival_sequence Job.
Let sched' := wc_transform_prefix arr_seq sched horizon.
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
Lemma wc_prefix_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched' arr_seq.
Proof.
rewrite /sched' /wc_transform_prefix.
apply prefix_map_property_invariance; last by done.
move => schedX t ARR.
by apply mwa_jobs_come_from_arrival_sequence.
Qed.
End ArrivalSequencePrefix.
End ArrivalSequence.
Section JobsMustBeReady.
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
Section JobsMustBeReadyFSC.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arr_seq_valid : valid_arrival_sequence arr_seq.
Variable sched: schedule (ideal.processor_state Job).
Section JobsMustBeReadyFSC.
Hypothesis H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched.
......@@ -125,35 +53,57 @@ Section JobsMustBeReady.
Admitted.
End JobsMustBeReadyFSC.
Section JobsMustBeReadyMWA.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arr_seq_valid : valid_arrival_sequence arr_seq.
End FSCFacts.
Section MWAFacts.
Variable sched: schedule (ideal.processor_state Job).
Hypothesis H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched.
Variable t: instant.
Let sched' := make_wc_at arr_seq sched t.
Section ArrivalSequenceMWA.
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
Variable t: instant.
Lemma mwa_jobs_must_be_ready_to_execute:
jobs_must_be_ready_to_execute sched'.
Proof.
rewrite /sched' /make_wc_at.
destruct (sched t) as [j_orig|] eqn:SCHED_orig; first by done.
by apply fsc_jobs_must_be_ready_to_execute.
Qed.
Let sched' := make_wc_at arr_seq sched t.
Lemma mwa_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched' arr_seq.
Proof.
rewrite /sched' /make_wc_at.
destruct (sched t) as [j_orig|] eqn:SCHED_orig; first by done.
by apply swapped_jobs_come_from_arrival_sequence.
Qed.
End ArrivalSequenceMWA.
Section JobsMustBeReadyMWA.
Hypothesis H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched.
Variable t: instant.
Let sched' := make_wc_at arr_seq sched t.
Lemma mwa_jobs_must_be_ready_to_execute:
jobs_must_be_ready_to_execute sched'.
Proof.
rewrite /sched' /make_wc_at.
destruct (sched t) as [j_orig|] eqn:SCHED_orig; first by done.
by apply fsc_jobs_must_be_ready_to_execute.
Qed.
End JobsMustBeReadyMWA.
End JobsMustBeReadyMWA.
Section PrefixInclusion.
End MWAFacts.
Section PrefixFacts.
Variable sched: schedule (ideal.processor_state Job).
Variable horizon: instant.
Variable arr_seq: arrival_sequence Job.
Section PrefixInclusion.
Variable h1 h2 : instant.
......@@ -168,7 +118,7 @@ Section JobsMustBeReady.
i (max_deadline_for_jobs_arrived_before arr_seq i))
as [n|] eqn:search_result; last by done.
apply search_arg_in_range in search_result.
by move:search_result => /andP [LEQ LMAX].
by move:search_result => /andP [LEQ LMAX].
Qed.
Hypothesis H_horizon_order: h1 <= h2.
......@@ -183,44 +133,56 @@ Section JobsMustBeReady.
rewrite /sched1 /sched2.
induction h2; first by move: (ltn_leq_trans before_horizon H_horizon_order).
move: H_horizon_order. rewrite leq_eqVlt => /orP [/eqP ->|LT]; first by done.
move: LT. rewrite ltnS => H_horizon_order_lt.
rewrite [RHS]/wc_transform_prefix /prefix_map -/prefix_map IHi //.
rewrite {1}/make_wc_at.
destruct (prefix_map sched (make_wc_at arr_seq) i i) as [j|] eqn:SCHED; first by done.
rewrite -(swap_before_invariant _ i (find_swap_candidate arr_seq (wc_transform_prefix arr_seq sched i) i));
last by apply ltn_leq_trans with (n := h1).
rewrite //.
by apply swap_candidate_is_in_future.
move: LT. rewrite ltnS => H_horizon_order_lt.
rewrite [RHS]/wc_transform_prefix /prefix_map -/prefix_map IHi //.
rewrite {1}/make_wc_at.
destruct (prefix_map sched (make_wc_at arr_seq) i i) as [j|] eqn:SCHED; first by done.
rewrite -(swap_before_invariant _ i (find_swap_candidate arr_seq (wc_transform_prefix arr_seq sched i) i));
last by apply ltn_leq_trans with (n := h1).
rewrite //.
by apply swap_candidate_is_in_future.
Qed.
End PrefixInclusion.
Section ArrivalSequencePrefix.
End PrefixInclusion.
Let sched' := wc_transform_prefix arr_seq sched horizon.
Section JobsMustBeReadyPrefix.
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
Variable sched: schedule (ideal.processor_state Job).
Lemma wc_prefix_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched' arr_seq.
Proof.
rewrite /sched' /wc_transform_prefix.
apply prefix_map_property_invariance; last by done.
move => schedX t ARR.
by apply mwa_jobs_come_from_arrival_sequence.
Qed.
End ArrivalSequencePrefix.
Variable horizon: instant.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
Let sched' := wc_transform_prefix arr_seq sched horizon.
Section JobsMustBeReadyPrefix.
Let sched' := wc_transform_prefix arr_seq sched horizon.
Hypothesis H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched.
Hypothesis H_jobs_must_be_ready: jobs_must_be_ready_to_execute sched.
Lemma wc_prefix_jobs_must_be_ready_to_execute:
jobs_must_be_ready_to_execute sched'.
rewrite /sched' /wc_transform_prefix.
apply prefix_map_property_invariance; last by done.
move=> schedX t ARR.
by apply mwa_jobs_must_be_ready_to_execute.
Qed.
End JobsMustBeReadyPrefix.
Lemma wc_prefix_jobs_must_be_ready_to_execute:
jobs_must_be_ready_to_execute sched'.
rewrite /sched' /wc_transform_prefix.
apply prefix_map_property_invariance; last by done.
move=> schedX t ARR.
by apply mwa_jobs_must_be_ready_to_execute.
Qed.
End JobsMustBeReadyPrefix.
End PrefixFacts.
End JobsMustBeReady.
End WCCorrectnessFacts.
Section Correctness.
Section WCCorrectness.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
......@@ -249,7 +211,7 @@ Section Correctness.
rewrite /sched_wc /wc_transform.
move=> j t.
rewrite /scheduled_at -/(scheduled_at _ j t).
by apply (wc_prefix_jobs_come_from_arrival_sequence sched t.+1 arr_seq H_from_arr_seq).
by apply (wc_prefix_jobs_come_from_arrival_sequence arr_seq sched t.+1 H_from_arr_seq).
Qed.
Lemma sched_wc_def:
......@@ -298,7 +260,7 @@ Section Correctness.
-apply wc_is_work_conserving.
Qed.
End Correctness.
End WCCorrectness.
(*
Section Optimality.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment