Commit 34c14244 authored by Björn Brandenburg's avatar Björn Brandenburg

fix definition change fallout in EDF transformation analysis

parent 37e9bdac
......@@ -9,7 +9,7 @@ From rt.restructuring.analysis Require Import schedulability transform.facts.edf
Section Optimality.
(* 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.
......@@ -27,7 +27,9 @@ Section Optimality.
all_deadlines_of_arrivals_met arr_seq edf_sched /\
is_EDF_schedule edf_sched.
Proof.
move=> [sched [[COME [ARR COMP]] DL_ARR_MET]].
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 sched' := edf_transform sched.
exists sched'. split; last split.
......
From mathcomp Require Import ssrnat ssrbool fintype.
From rt.restructuring.behavior Require Import schedule.ideal facts.all.
From rt.restructuring.behavior Require Export facts.all.
From rt.restructuring.model Require Export schedule.edf.
From rt.restructuring.analysis Require Export schedulability transform.edf_trans transform.facts.swaps.
......@@ -11,6 +11,10 @@ From rt.util Require Import tactics nat.
the proofs of individual properties of the obtained EDF
schedule. *)
(* Throughout this file, we assume ideal uniprocessor schedules. *)
From rt.restructuring.behavior Require Export schedule.ideal.
(* Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
From rt.restructuring.model.readiness Require Export basic.
(** We start by analyzing the helper function [find_swap_candidate],
which is a problem-specific wrapper around [search_arg]. *)
......@@ -210,6 +214,8 @@ Section MakeEDFAtFacts.
Lemma mea_completed_jobs:
completed_jobs_dont_execute sched'.
Proof.
have IDEAL := @ideal_proc_model_ensures_ideal_progress Job.
have UNIT := @ideal_proc_model_provides_unit_service Job.
rewrite /sched' /make_edf_at.
destruct (sched t_edf) as [j_orig|] eqn:SCHED; last by done.
have SCHED': scheduled_at sched j_orig t_edf
......@@ -871,9 +877,12 @@ Section Optimality.
Theorem edf_schedule_is_valid:
valid_schedule equivalent_edf_schedule arr_seq.
Proof.
move: H_sched_valid => [COME [ARR COMP]].
rewrite /valid_schedule; split; last split.
- by apply edf_transform_jobs_come_from_arrival_sequence.
move: H_sched_valid => [COME READY].
rewrite /valid_schedule; split;
first by apply edf_transform_jobs_come_from_arrival_sequence.
have ARR := jobs_must_arrive_to_be_ready sched READY.
have COMP := completed_jobs_are_not_ready sched READY.
apply basic_readiness_compliance.
- by apply edf_transform_jobs_must_arrive.
- by apply edf_transform_completed_jobs_dont_execute.
Qed.
......@@ -882,7 +891,9 @@ Section Optimality.
Theorem edf_schedule_meets_all_deadlines:
all_deadlines_met equivalent_edf_schedule.
Proof.
move: H_sched_valid => [COME [ARR COMP]].
move: H_sched_valid => [COME READY].
have ARR := jobs_must_arrive_to_be_ready sched READY.
have COMP := completed_jobs_are_not_ready sched READY.
by apply edf_transform_deadlines_met.
Qed.
......@@ -903,7 +914,9 @@ Section Optimality.
all_deadlines_of_arrivals_met arr_seq equivalent_edf_schedule.
Proof.
move=> j ARR_j.
move: H_sched_valid => [COME [ARR COMP]].
move: H_sched_valid => [COME READY].
have ARR := jobs_must_arrive_to_be_ready sched READY.
have COMP := completed_jobs_are_not_ready sched READY.
destruct (job_cost j == 0) eqn:COST.
- move: COST => /eqP COST.
rewrite /job_meets_deadline /completed_by COST.
......
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