Library prosa.results.edf.optimality
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.transform.edf_opt.
Require Export prosa.analysis.facts.transform.edf_wc.
Optimality of EDF on Ideal Uniprocessors
... and the basic (i.e., Liu & Layland) readiness model under which any
pending job is always ready.
For any given type of jobs, each characterized by execution
costs, an arrival time, and an absolute deadline,...
... and any valid job arrival sequence.
We observe that EDF is optimal in the sense that, if there exists
any schedule in which all jobs of arr_seq meet their deadline,
then there also exists an EDF schedule in which all deadlines are
met.
Theorem EDF_optimality:
(∃ any_sched : schedule (ideal.processor_state Job),
valid_schedule any_sched arr_seq ∧
all_deadlines_of_arrivals_met arr_seq any_sched) →
∃ edf_sched : schedule (ideal.processor_state Job),
valid_schedule edf_sched arr_seq ∧
all_deadlines_of_arrivals_met arr_seq edf_sched ∧
EDF_schedule edf_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 368)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
============================
(exists any_sched : schedule (processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\ EDF_schedule edf_sched
----------------------------------------------------------------------------- *)
Proof.
move⇒ [sched [[COME READY] DL_ARR_MET]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 399)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
============================
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\ EDF_schedule edf_sched
----------------------------------------------------------------------------- *)
have ARR := jobs_must_arrive_to_be_ready sched READY.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 410)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
============================
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\ EDF_schedule edf_sched
----------------------------------------------------------------------------- *)
have COMP := completed_jobs_are_not_ready sched READY.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 421)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
============================
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\ EDF_schedule edf_sched
----------------------------------------------------------------------------- *)
move: (all_deadlines_met_in_valid_schedule _ _ COME DL_ARR_MET) ⇒ DL_MET.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 433)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
DL_MET : all_deadlines_met sched
============================
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\ EDF_schedule edf_sched
----------------------------------------------------------------------------- *)
set sched' := edf_transform sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 438)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
DL_MET : all_deadlines_met sched
sched' := edf_transform sched : instant -> processor_state Job
============================
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\ EDF_schedule edf_sched
----------------------------------------------------------------------------- *)
∃ sched'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 440)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
DL_MET : all_deadlines_met sched
sched' := edf_transform sched : instant -> processor_state Job
============================
valid_schedule sched' arr_seq /\
all_deadlines_of_arrivals_met arr_seq sched' /\ EDF_schedule sched'
----------------------------------------------------------------------------- *)
split; last split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 442)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
DL_MET : all_deadlines_met sched
sched' := edf_transform sched : instant -> processor_state Job
============================
valid_schedule sched' arr_seq
subgoal 2 (ID 445) is:
all_deadlines_of_arrivals_met arr_seq sched'
subgoal 3 (ID 446) is:
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- by apply edf_schedule_is_valid.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 445)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
DL_MET : all_deadlines_met sched
sched' := edf_transform sched : instant -> processor_state Job
============================
all_deadlines_of_arrivals_met arr_seq sched'
subgoal 2 (ID 446) is:
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- by apply edf_schedule_meets_all_deadlines_wrt_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 446)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
DL_MET : all_deadlines_met sched
sched' := edf_transform sched : instant -> processor_state Job
============================
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- by apply edf_transform_ensures_edf.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(∃ any_sched : schedule (ideal.processor_state Job),
valid_schedule any_sched arr_seq ∧
all_deadlines_of_arrivals_met arr_seq any_sched) →
∃ edf_sched : schedule (ideal.processor_state Job),
valid_schedule edf_sched arr_seq ∧
all_deadlines_of_arrivals_met arr_seq edf_sched ∧
EDF_schedule edf_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 368)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
============================
(exists any_sched : schedule (processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\ EDF_schedule edf_sched
----------------------------------------------------------------------------- *)
Proof.
move⇒ [sched [[COME READY] DL_ARR_MET]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 399)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
============================
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\ EDF_schedule edf_sched
----------------------------------------------------------------------------- *)
have ARR := jobs_must_arrive_to_be_ready sched READY.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 410)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
============================
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\ EDF_schedule edf_sched
----------------------------------------------------------------------------- *)
have COMP := completed_jobs_are_not_ready sched READY.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 421)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
============================
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\ EDF_schedule edf_sched
----------------------------------------------------------------------------- *)
move: (all_deadlines_met_in_valid_schedule _ _ COME DL_ARR_MET) ⇒ DL_MET.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 433)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
DL_MET : all_deadlines_met sched
============================
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\ EDF_schedule edf_sched
----------------------------------------------------------------------------- *)
set sched' := edf_transform sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 438)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
DL_MET : all_deadlines_met sched
sched' := edf_transform sched : instant -> processor_state Job
============================
exists edf_sched : schedule (processor_state Job),
valid_schedule edf_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq edf_sched /\ EDF_schedule edf_sched
----------------------------------------------------------------------------- *)
∃ sched'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 440)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
DL_MET : all_deadlines_met sched
sched' := edf_transform sched : instant -> processor_state Job
============================
valid_schedule sched' arr_seq /\
all_deadlines_of_arrivals_met arr_seq sched' /\ EDF_schedule sched'
----------------------------------------------------------------------------- *)
split; last split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 442)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
DL_MET : all_deadlines_met sched
sched' := edf_transform sched : instant -> processor_state Job
============================
valid_schedule sched' arr_seq
subgoal 2 (ID 445) is:
all_deadlines_of_arrivals_met arr_seq sched'
subgoal 3 (ID 446) is:
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- by apply edf_schedule_is_valid.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 445)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
DL_MET : all_deadlines_met sched
sched' := edf_transform sched : instant -> processor_state Job
============================
all_deadlines_of_arrivals_met arr_seq sched'
subgoal 2 (ID 446) is:
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- by apply edf_schedule_meets_all_deadlines_wrt_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 446)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
ARR : jobs_must_arrive_to_execute sched
COMP : completed_jobs_dont_execute sched
DL_MET : all_deadlines_met sched
sched' := edf_transform sched : instant -> processor_state Job
============================
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- by apply edf_transform_ensures_edf.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Moreover, we note that, since EDF maintains work conservation, if there
exists a schedule in which all jobs of [arr_seq] meet their deadline,
then there also exists a work-conserving EDF in which all deadlines are
met.
Theorem EDF_WC_optimality :
(∃ any_sched : schedule (ideal.processor_state Job),
valid_schedule any_sched arr_seq ∧
all_deadlines_of_arrivals_met arr_seq any_sched) →
∃ 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 409)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
============================
(exists any_sched : schedule (processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
Proof.
move⇒ [sched [[COME READY] DL_ARR_MET]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 440)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
move: (all_deadlines_met_in_valid_schedule _ _ COME DL_ARR_MET) ⇒ DL_MET.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 452)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
set wc_sched := wc_transform arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 457)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
have wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
by apply wc_jobs_come_from_arrival_sequence.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 496)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
have wc_READY : jobs_must_be_ready_to_execute wc_sched
by apply wc_jobs_must_be_ready_to_execute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 538)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
have wc_ARR := jobs_must_arrive_to_be_ready wc_sched wc_READY.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 549)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
have wc_COMP := completed_jobs_are_not_ready wc_sched wc_READY.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 560)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 573)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
move: (all_deadlines_met_in_valid_schedule _ _ wc_COME wc_DL_ARR_MET) ⇒ wc_DL_MET.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 584)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
set sched' := edf_transform wc_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 591)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
sched' := edf_transform wc_sched : instant -> processor_state Job
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
∃ sched'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 593)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
sched' := edf_transform wc_sched : instant -> processor_state Job
============================
valid_schedule sched' arr_seq /\
all_deadlines_of_arrivals_met arr_seq sched' /\
work_conserving arr_seq sched' /\ EDF_schedule sched'
----------------------------------------------------------------------------- *)
split; last split; last split.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 595)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
sched' := edf_transform wc_sched : instant -> processor_state Job
============================
valid_schedule sched' arr_seq
subgoal 2 (ID 598) is:
all_deadlines_of_arrivals_met arr_seq sched'
subgoal 3 (ID 601) is:
work_conserving arr_seq sched'
subgoal 4 (ID 602) is:
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- by apply edf_schedule_is_valid.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 598)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
sched' := edf_transform wc_sched : instant -> processor_state Job
============================
all_deadlines_of_arrivals_met arr_seq sched'
subgoal 2 (ID 601) is:
work_conserving arr_seq sched'
subgoal 3 (ID 602) is:
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- by apply edf_schedule_meets_all_deadlines_wrt_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 601)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
sched' := edf_transform wc_sched : instant -> processor_state Job
============================
work_conserving arr_seq sched'
subgoal 2 (ID 602) is:
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- apply edf_transform_maintains_work_conservation; by [ | apply wc_is_work_conserving ].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 602)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
sched' := edf_transform wc_sched : instant -> processor_state Job
============================
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- by apply edf_transform_ensures_edf.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(∃ any_sched : schedule (ideal.processor_state Job),
valid_schedule any_sched arr_seq ∧
all_deadlines_of_arrivals_met arr_seq any_sched) →
∃ 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 409)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
============================
(exists any_sched : schedule (processor_state Job),
valid_schedule any_sched arr_seq /\
all_deadlines_of_arrivals_met arr_seq any_sched) ->
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
Proof.
move⇒ [sched [[COME READY] DL_ARR_MET]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 440)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
move: (all_deadlines_met_in_valid_schedule _ _ COME DL_ARR_MET) ⇒ DL_MET.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 452)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
set wc_sched := wc_transform arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 457)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
have wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
by apply wc_jobs_come_from_arrival_sequence.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 496)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
have wc_READY : jobs_must_be_ready_to_execute wc_sched
by apply wc_jobs_must_be_ready_to_execute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 538)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
have wc_ARR := jobs_must_arrive_to_be_ready wc_sched wc_READY.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 549)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
have wc_COMP := completed_jobs_are_not_ready wc_sched wc_READY.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 560)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 573)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
move: (all_deadlines_met_in_valid_schedule _ _ wc_COME wc_DL_ARR_MET) ⇒ wc_DL_MET.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 584)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
set sched' := edf_transform wc_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 591)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
sched' := edf_transform wc_sched : instant -> processor_state Job
============================
exists edf_wc_sched : schedule (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
----------------------------------------------------------------------------- *)
∃ sched'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 593)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
sched' := edf_transform wc_sched : instant -> processor_state Job
============================
valid_schedule sched' arr_seq /\
all_deadlines_of_arrivals_met arr_seq sched' /\
work_conserving arr_seq sched' /\ EDF_schedule sched'
----------------------------------------------------------------------------- *)
split; last split; last split.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 595)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
sched' := edf_transform wc_sched : instant -> processor_state Job
============================
valid_schedule sched' arr_seq
subgoal 2 (ID 598) is:
all_deadlines_of_arrivals_met arr_seq sched'
subgoal 3 (ID 601) is:
work_conserving arr_seq sched'
subgoal 4 (ID 602) is:
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- by apply edf_schedule_is_valid.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 598)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
sched' := edf_transform wc_sched : instant -> processor_state Job
============================
all_deadlines_of_arrivals_met arr_seq sched'
subgoal 2 (ID 601) is:
work_conserving arr_seq sched'
subgoal 3 (ID 602) is:
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- by apply edf_schedule_meets_all_deadlines_wrt_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 601)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
sched' := edf_transform wc_sched : instant -> processor_state Job
============================
work_conserving arr_seq sched'
subgoal 2 (ID 602) is:
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- apply edf_transform_maintains_work_conservation; by [ | apply wc_is_work_conserving ].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 602)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
COME : jobs_come_from_arrival_sequence sched arr_seq
READY : jobs_must_be_ready_to_execute sched
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
DL_MET : all_deadlines_met sched
wc_sched := wc_transform arr_seq sched : nat -> option_eqType Job
wc_COME : jobs_come_from_arrival_sequence wc_sched arr_seq
wc_READY : jobs_must_be_ready_to_execute wc_sched
wc_ARR : jobs_must_arrive_to_execute wc_sched
wc_COMP : completed_jobs_dont_execute wc_sched
wc_DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq wc_sched
wc_DL_MET : all_deadlines_met wc_sched
sched' := edf_transform wc_sched : instant -> processor_state Job
============================
EDF_schedule sched'
----------------------------------------------------------------------------- *)
- by apply edf_transform_ensures_edf.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Remark: [EDF_optimality] is of course an immediate corollary of
[EDF_WC_optimality]. We nonetheless have two separate proofs for historic
reasons as [EDF_optimality] predates [EDF_WC_optimality] (in Prosa).
Weak Optimality Theorem
For any given type of jobs, each characterized by execution
costs, an arrival time, and an absolute deadline,...
... if we have a well-behaved reference schedule ...
Variable any_sched: schedule (ideal.processor_state Job).
Hypothesis H_must_arrive: jobs_must_arrive_to_execute any_sched.
Hypothesis H_completed_dont_execute: completed_jobs_dont_execute any_sched.
Hypothesis H_must_arrive: jobs_must_arrive_to_execute any_sched.
Hypothesis H_completed_dont_execute: completed_jobs_dont_execute any_sched.
... in which no deadlines are missed, ...
...then there also exists an EDF schedule in which no deadlines
are missed (and in which exactly the same set of jobs is
scheduled, as ensured by the last clause).
Theorem weak_EDF_optimality:
∃ edf_sched : schedule (ideal.processor_state Job),
jobs_must_arrive_to_execute edf_sched ∧
completed_jobs_dont_execute edf_sched ∧
all_deadlines_met edf_sched ∧
EDF_schedule edf_sched ∧
∀ j,
(∃ t, scheduled_at any_sched j t) ↔
(∃ t', scheduled_at edf_sched j t').
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 380)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
============================
exists edf_sched : schedule (processor_state Job),
jobs_must_arrive_to_execute edf_sched /\
completed_jobs_dont_execute edf_sched /\
all_deadlines_met edf_sched /\
EDF_schedule edf_sched /\
(forall j : Job,
(exists t : instant, scheduled_at any_sched j t) <->
(exists t' : instant, scheduled_at edf_sched j t'))
----------------------------------------------------------------------------- *)
Proof.
set sched' := edf_transform any_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 385)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
============================
exists edf_sched : schedule (processor_state Job),
jobs_must_arrive_to_execute edf_sched /\
completed_jobs_dont_execute edf_sched /\
all_deadlines_met edf_sched /\
EDF_schedule edf_sched /\
(forall j : Job,
(exists t : instant, scheduled_at any_sched j t) <->
(exists t' : instant, scheduled_at edf_sched j t'))
----------------------------------------------------------------------------- *)
∃ sched'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 387)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
============================
jobs_must_arrive_to_execute sched' /\
completed_jobs_dont_execute sched' /\
all_deadlines_met sched' /\
EDF_schedule sched' /\
(forall j : Job,
(exists t : instant, scheduled_at any_sched j t) <->
(exists t' : instant, scheduled_at sched' j t'))
----------------------------------------------------------------------------- *)
repeat split.
(* ----------------------------------[ coqtop ]---------------------------------
6 subgoals (ID 389)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
============================
jobs_must_arrive_to_execute sched'
subgoal 2 (ID 396) is:
completed_jobs_dont_execute sched'
subgoal 3 (ID 403) is:
all_deadlines_met sched'
subgoal 4 (ID 410) is:
EDF_schedule sched'
subgoal 5 (ID 423) is:
(exists t : instant, scheduled_at any_sched j t) ->
exists t' : instant, scheduled_at sched' j t'
subgoal 6 (ID 424) is:
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
----------------------------------------------------------------------------- *)
- by apply edf_transform_jobs_must_arrive.
(* ----------------------------------[ coqtop ]---------------------------------
5 subgoals (ID 396)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
============================
completed_jobs_dont_execute sched'
subgoal 2 (ID 403) is:
all_deadlines_met sched'
subgoal 3 (ID 410) is:
EDF_schedule sched'
subgoal 4 (ID 423) is:
(exists t : instant, scheduled_at any_sched j t) ->
exists t' : instant, scheduled_at sched' j t'
subgoal 5 (ID 424) is:
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
----------------------------------------------------------------------------- *)
- by apply edf_transform_completed_jobs_dont_execute.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 403)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
============================
all_deadlines_met sched'
subgoal 2 (ID 410) is:
EDF_schedule sched'
subgoal 3 (ID 423) is:
(exists t : instant, scheduled_at any_sched j t) ->
exists t' : instant, scheduled_at sched' j t'
subgoal 4 (ID 424) is:
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
----------------------------------------------------------------------------- *)
- by apply edf_transform_deadlines_met.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 410)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
============================
EDF_schedule sched'
subgoal 2 (ID 423) is:
(exists t : instant, scheduled_at any_sched j t) ->
exists t' : instant, scheduled_at sched' j t'
subgoal 3 (ID 424) is:
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
----------------------------------------------------------------------------- *)
- by apply edf_transform_ensures_edf.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 423)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
j : Job
============================
(exists t : instant, scheduled_at any_sched j t) ->
exists t' : instant, scheduled_at sched' j t'
subgoal 2 (ID 424) is:
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
----------------------------------------------------------------------------- *)
- by move⇒ [t SCHED_j]; apply edf_transform_job_scheduled' with (t0 := t).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 424)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
j : Job
============================
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
----------------------------------------------------------------------------- *)
- by move⇒ [t SCHED_j]; apply edf_transform_job_scheduled with (t0 := t).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End WeakOptimality.
∃ edf_sched : schedule (ideal.processor_state Job),
jobs_must_arrive_to_execute edf_sched ∧
completed_jobs_dont_execute edf_sched ∧
all_deadlines_met edf_sched ∧
EDF_schedule edf_sched ∧
∀ j,
(∃ t, scheduled_at any_sched j t) ↔
(∃ t', scheduled_at edf_sched j t').
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 380)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
============================
exists edf_sched : schedule (processor_state Job),
jobs_must_arrive_to_execute edf_sched /\
completed_jobs_dont_execute edf_sched /\
all_deadlines_met edf_sched /\
EDF_schedule edf_sched /\
(forall j : Job,
(exists t : instant, scheduled_at any_sched j t) <->
(exists t' : instant, scheduled_at edf_sched j t'))
----------------------------------------------------------------------------- *)
Proof.
set sched' := edf_transform any_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 385)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
============================
exists edf_sched : schedule (processor_state Job),
jobs_must_arrive_to_execute edf_sched /\
completed_jobs_dont_execute edf_sched /\
all_deadlines_met edf_sched /\
EDF_schedule edf_sched /\
(forall j : Job,
(exists t : instant, scheduled_at any_sched j t) <->
(exists t' : instant, scheduled_at edf_sched j t'))
----------------------------------------------------------------------------- *)
∃ sched'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 387)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
============================
jobs_must_arrive_to_execute sched' /\
completed_jobs_dont_execute sched' /\
all_deadlines_met sched' /\
EDF_schedule sched' /\
(forall j : Job,
(exists t : instant, scheduled_at any_sched j t) <->
(exists t' : instant, scheduled_at sched' j t'))
----------------------------------------------------------------------------- *)
repeat split.
(* ----------------------------------[ coqtop ]---------------------------------
6 subgoals (ID 389)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
============================
jobs_must_arrive_to_execute sched'
subgoal 2 (ID 396) is:
completed_jobs_dont_execute sched'
subgoal 3 (ID 403) is:
all_deadlines_met sched'
subgoal 4 (ID 410) is:
EDF_schedule sched'
subgoal 5 (ID 423) is:
(exists t : instant, scheduled_at any_sched j t) ->
exists t' : instant, scheduled_at sched' j t'
subgoal 6 (ID 424) is:
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
----------------------------------------------------------------------------- *)
- by apply edf_transform_jobs_must_arrive.
(* ----------------------------------[ coqtop ]---------------------------------
5 subgoals (ID 396)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
============================
completed_jobs_dont_execute sched'
subgoal 2 (ID 403) is:
all_deadlines_met sched'
subgoal 3 (ID 410) is:
EDF_schedule sched'
subgoal 4 (ID 423) is:
(exists t : instant, scheduled_at any_sched j t) ->
exists t' : instant, scheduled_at sched' j t'
subgoal 5 (ID 424) is:
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
----------------------------------------------------------------------------- *)
- by apply edf_transform_completed_jobs_dont_execute.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 403)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
============================
all_deadlines_met sched'
subgoal 2 (ID 410) is:
EDF_schedule sched'
subgoal 3 (ID 423) is:
(exists t : instant, scheduled_at any_sched j t) ->
exists t' : instant, scheduled_at sched' j t'
subgoal 4 (ID 424) is:
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
----------------------------------------------------------------------------- *)
- by apply edf_transform_deadlines_met.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 410)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
============================
EDF_schedule sched'
subgoal 2 (ID 423) is:
(exists t : instant, scheduled_at any_sched j t) ->
exists t' : instant, scheduled_at sched' j t'
subgoal 3 (ID 424) is:
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
----------------------------------------------------------------------------- *)
- by apply edf_transform_ensures_edf.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 423)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
j : Job
============================
(exists t : instant, scheduled_at any_sched j t) ->
exists t' : instant, scheduled_at sched' j t'
subgoal 2 (ID 424) is:
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
----------------------------------------------------------------------------- *)
- by move⇒ [t SCHED_j]; apply edf_transform_job_scheduled' with (t0 := t).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 424)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
any_sched : schedule (processor_state Job)
H_must_arrive : jobs_must_arrive_to_execute any_sched
H_completed_dont_execute : completed_jobs_dont_execute any_sched
H_all_deadlines_met : all_deadlines_met any_sched
sched' := edf_transform any_sched : instant -> processor_state Job
j : Job
============================
(exists t' : instant, scheduled_at sched' j t') ->
exists t : instant, scheduled_at any_sched j t
----------------------------------------------------------------------------- *)
- by move⇒ [t SCHED_j]; apply edf_transform_job_scheduled with (t0 := t).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End WeakOptimality.