Library prosa.analysis.facts.transform.edf_wc
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.transform.edf_opt.
Require Export prosa.analysis.facts.transform.wc_correctness.
Require Export prosa.analysis.facts.behavior.deadlines.
Require Export prosa.analysis.facts.readiness.backlogged.
Optimality of Work-Conserving EDF on Ideal Uniprocessors
Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model.
Non-Idle Swaps
For any given type of jobs...
... and any valid job arrival sequence.
...consider an ideal uniprocessor schedule...
...that is well-behaved (i.e., in which jobs execute only after having
arrived and only if they are not yet complete, and in which all jobs come
from the arrival sequence).
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
Suppose we are given two specific times [t1] and [t2],...
...which we assume to be ordered (to avoid dealing with symmetric cases),...
...and two jobs [j1] and [j2]...
...such that [j2] arrives before time [t1],...
...[j1] is scheduled at time [t1], and...
...[j2] is scheduled at time [t2].
We let [swap_sched] denote the schedule in which the allocations at
[t1] and [t2] have been swapped.
Now consider an arbitrary job [j]...
...and an arbitrary instant [t]...
...such that [j] arrives in [arr_seq]...
...and is backlogged in [swap_sched] at instant [t].
We proceed by case analysis. We first show that, if [t] equals [t1], then
[swap_sched] maintains work conservation. That is, there exists some job
that's scheduled in [swap_sched] at instant [t]
Lemma non_idle_swap_maintains_work_conservation_t1 :
work_conserving arr_seq sched →
t = t1 →
∃ j_other, scheduled_at swap_sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1567)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
============================
work_conserving arr_seq sched ->
t = t1 -> exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
Proof.
move⇒ _ EQ; rewrite EQ; by ∃ j2; rewrite swap_job_scheduled_t1.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
work_conserving arr_seq sched →
t = t1 →
∃ j_other, scheduled_at swap_sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1567)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
============================
work_conserving arr_seq sched ->
t = t1 -> exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
Proof.
move⇒ _ EQ; rewrite EQ; by ∃ j2; rewrite swap_job_scheduled_t1.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Similarly, if [t] equals [t2] then then [swap_sched] maintains work conservation.
Lemma non_idle_swap_maintains_work_conservation_t2 :
work_conserving arr_seq sched →
t = t2 →
∃ j_other, scheduled_at swap_sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1582)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
============================
work_conserving arr_seq sched ->
t = t2 -> exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
Proof.
move⇒ _ EQ; rewrite EQ; by ∃ j1; rewrite swap_job_scheduled_t2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
work_conserving arr_seq sched →
t = t2 →
∃ j_other, scheduled_at swap_sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1582)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
============================
work_conserving arr_seq sched ->
t = t2 -> exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
Proof.
move⇒ _ EQ; rewrite EQ; by ∃ j1; rewrite swap_job_scheduled_t2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
If [t] is less than or equal to [t1] then then then [swap_sched] maintains work conservation.
Lemma non_idle_swap_maintains_work_conservation_LEQ_t1 :
work_conserving arr_seq sched →
t ≤ t1 →
∃ j_other, scheduled_at swap_sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1595)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
============================
work_conserving arr_seq sched ->
t <= t1 -> exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
Proof.
move⇒ WC_sched LEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1597)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
LEQ : t <= t1
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t1)) ⇒ [/eqP EQ| /eqP NEQ]; first by apply non_idle_swap_maintains_work_conservation_t1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1685)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
LEQ : t <= t1
NEQ : t <> t1
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t2)) ⇒ [/eqP EQ'| /eqP NEQ']; first by apply non_idle_swap_maintains_work_conservation_t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1775)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
have [j_other j_other_scheduled] : ∃ j_other, scheduled_at sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1784)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at sched j_other t
subgoal 2 (ID 1796) is:
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1784)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at sched j_other t
----------------------------------------------------------------------------- *)
rewrite /work_conserving in WC_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1843)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
exists j_other : Job, scheduled_at sched j_other t
----------------------------------------------------------------------------- *)
apply (WC_sched j) ⇒ //; move :H_backlogged_j_t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1870)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
backlogged swap_sched j t -> backlogged sched j t
----------------------------------------------------------------------------- *)
rewrite /backlogged/job_ready/basic_ready_instance/pending/completed_by.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1921)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
has_arrived j t && ~~ (job_cost j <= service swap_sched j t) &&
~~ scheduled_at swap_sched j t ->
has_arrived j t && ~~ (job_cost j <= service sched j t) &&
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
move /andP ⇒ [ARR_INCOMP scheduled]; move :ARR_INCOMP; move /andP ⇒ [arrive not_comp].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2005)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
scheduled : ~~ scheduled_at swap_sched j t
arrive : has_arrived j t
not_comp : ~~ (job_cost j <= service swap_sched j t)
============================
has_arrived j t && ~~ (job_cost j <= service sched j t) &&
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply /andP; split; first (apply /andP; split) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2059)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
scheduled : ~~ scheduled_at swap_sched j t
arrive : has_arrived j t
not_comp : ~~ (job_cost j <= service swap_sched j t)
============================
~~ (job_cost j <= service sched j t)
subgoal 2 (ID 2032) is:
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
+ by rewrite (service_before_swap_invariant sched t1 t2 _ t).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2032)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
scheduled : ~~ scheduled_at swap_sched j t
arrive : has_arrived j t
not_comp : ~~ (job_cost j <= service swap_sched j t)
============================
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
+ by rewrite -(swap_job_scheduled_other_times _ t1 t2 j t) //; (apply /neqP; eauto).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1796)
subgoal 1 (ID 1796) is:
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1796)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
j_other : Job
j_other_scheduled : scheduled_at sched j_other t
============================
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
∃ j_other; by rewrite (swap_job_scheduled_other_times) //; do 2! (apply /neqP; eauto).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
work_conserving arr_seq sched →
t ≤ t1 →
∃ j_other, scheduled_at swap_sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1595)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
============================
work_conserving arr_seq sched ->
t <= t1 -> exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
Proof.
move⇒ WC_sched LEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1597)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
LEQ : t <= t1
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t1)) ⇒ [/eqP EQ| /eqP NEQ]; first by apply non_idle_swap_maintains_work_conservation_t1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1685)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
LEQ : t <= t1
NEQ : t <> t1
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t2)) ⇒ [/eqP EQ'| /eqP NEQ']; first by apply non_idle_swap_maintains_work_conservation_t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1775)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
have [j_other j_other_scheduled] : ∃ j_other, scheduled_at sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1784)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at sched j_other t
subgoal 2 (ID 1796) is:
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1784)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at sched j_other t
----------------------------------------------------------------------------- *)
rewrite /work_conserving in WC_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1843)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
exists j_other : Job, scheduled_at sched j_other t
----------------------------------------------------------------------------- *)
apply (WC_sched j) ⇒ //; move :H_backlogged_j_t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1870)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
backlogged swap_sched j t -> backlogged sched j t
----------------------------------------------------------------------------- *)
rewrite /backlogged/job_ready/basic_ready_instance/pending/completed_by.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1921)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
has_arrived j t && ~~ (job_cost j <= service swap_sched j t) &&
~~ scheduled_at swap_sched j t ->
has_arrived j t && ~~ (job_cost j <= service sched j t) &&
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
move /andP ⇒ [ARR_INCOMP scheduled]; move :ARR_INCOMP; move /andP ⇒ [arrive not_comp].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2005)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
scheduled : ~~ scheduled_at swap_sched j t
arrive : has_arrived j t
not_comp : ~~ (job_cost j <= service swap_sched j t)
============================
has_arrived j t && ~~ (job_cost j <= service sched j t) &&
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply /andP; split; first (apply /andP; split) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2059)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
scheduled : ~~ scheduled_at swap_sched j t
arrive : has_arrived j t
not_comp : ~~ (job_cost j <= service swap_sched j t)
============================
~~ (job_cost j <= service sched j t)
subgoal 2 (ID 2032) is:
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
+ by rewrite (service_before_swap_invariant sched t1 t2 _ t).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2032)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
scheduled : ~~ scheduled_at swap_sched j t
arrive : has_arrived j t
not_comp : ~~ (job_cost j <= service swap_sched j t)
============================
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
+ by rewrite -(swap_job_scheduled_other_times _ t1 t2 j t) //; (apply /neqP; eauto).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1796)
subgoal 1 (ID 1796) is:
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1796)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
LEQ : t <= t1
NEQ : t <> t1
NEQ' : t <> t2
j_other : Job
j_other_scheduled : scheduled_at sched j_other t
============================
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
∃ j_other; by rewrite (swap_job_scheduled_other_times) //; do 2! (apply /neqP; eauto).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Similarly, if [t] is greater than [t2] then then then [swap_sched] maintains work conservation.
Lemma non_idle_swap_maintains_work_conservation_GT_t2 :
work_conserving arr_seq sched →
t2 < t →
∃ j_other, scheduled_at swap_sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1608)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
============================
work_conserving arr_seq sched ->
t2 < t -> exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
Proof.
move⇒ WC_sched GT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1610)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
GT : t2 < t
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t1)) ⇒ [/eqP EQ| /eqP NEQ]; first by apply non_idle_swap_maintains_work_conservation_t1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1698)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
GT : t2 < t
NEQ : t <> t1
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t2)) ⇒ [/eqP EQ'| /eqP NEQ']; first by apply non_idle_swap_maintains_work_conservation_t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1788)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
have [j_other j_other_scheduled] : ∃ j_other, scheduled_at sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1797)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at sched j_other t
subgoal 2 (ID 1809) is:
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1797)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at sched j_other t
----------------------------------------------------------------------------- *)
rewrite /work_conserving in WC_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1856)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
exists j_other : Job, scheduled_at sched j_other t
----------------------------------------------------------------------------- *)
apply (WC_sched j) ⇒ //; move :H_backlogged_j_t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1883)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
backlogged swap_sched j t -> backlogged sched j t
----------------------------------------------------------------------------- *)
rewrite /backlogged/job_ready/basic_ready_instance/pending/completed_by.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1934)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
has_arrived j t && ~~ (job_cost j <= service swap_sched j t) &&
~~ scheduled_at swap_sched j t ->
has_arrived j t && ~~ (job_cost j <= service sched j t) &&
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
move /andP ⇒ [ARR_INCOMP scheduled]; move :ARR_INCOMP; move /andP ⇒ [arrive not_comp].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2018)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
scheduled : ~~ scheduled_at swap_sched j t
arrive : has_arrived j t
not_comp : ~~ (job_cost j <= service swap_sched j t)
============================
has_arrived j t && ~~ (job_cost j <= service sched j t) &&
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply /andP; split; first (apply /andP; split) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2072)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
scheduled : ~~ scheduled_at swap_sched j t
arrive : has_arrived j t
not_comp : ~~ (job_cost j <= service swap_sched j t)
============================
~~ (job_cost j <= service sched j t)
subgoal 2 (ID 2045) is:
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
+ by rewrite (service_after_swap_invariant sched t1 t2 _ t) // /t2; apply fsc_range1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2045)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
scheduled : ~~ scheduled_at swap_sched j t
arrive : has_arrived j t
not_comp : ~~ (job_cost j <= service swap_sched j t)
============================
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
+ by rewrite -(swap_job_scheduled_other_times _ t1 t2 j t) //; (apply /neqP; eauto).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1809)
subgoal 1 (ID 1809) is:
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1809)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
j_other : Job
j_other_scheduled : scheduled_at sched j_other t
============================
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
∃ j_other; by rewrite (swap_job_scheduled_other_times) //; do 2! (apply /neqP; eauto).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
work_conserving arr_seq sched →
t2 < t →
∃ j_other, scheduled_at swap_sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1608)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
============================
work_conserving arr_seq sched ->
t2 < t -> exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
Proof.
move⇒ WC_sched GT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1610)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
GT : t2 < t
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t1)) ⇒ [/eqP EQ| /eqP NEQ]; first by apply non_idle_swap_maintains_work_conservation_t1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1698)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
GT : t2 < t
NEQ : t <> t1
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t2)) ⇒ [/eqP EQ'| /eqP NEQ']; first by apply non_idle_swap_maintains_work_conservation_t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1788)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
have [j_other j_other_scheduled] : ∃ j_other, scheduled_at sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1797)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at sched j_other t
subgoal 2 (ID 1809) is:
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1797)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at sched j_other t
----------------------------------------------------------------------------- *)
rewrite /work_conserving in WC_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1856)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
exists j_other : Job, scheduled_at sched j_other t
----------------------------------------------------------------------------- *)
apply (WC_sched j) ⇒ //; move :H_backlogged_j_t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1883)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
backlogged swap_sched j t -> backlogged sched j t
----------------------------------------------------------------------------- *)
rewrite /backlogged/job_ready/basic_ready_instance/pending/completed_by.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1934)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
has_arrived j t && ~~ (job_cost j <= service swap_sched j t) &&
~~ scheduled_at swap_sched j t ->
has_arrived j t && ~~ (job_cost j <= service sched j t) &&
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
move /andP ⇒ [ARR_INCOMP scheduled]; move :ARR_INCOMP; move /andP ⇒ [arrive not_comp].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2018)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
scheduled : ~~ scheduled_at swap_sched j t
arrive : has_arrived j t
not_comp : ~~ (job_cost j <= service swap_sched j t)
============================
has_arrived j t && ~~ (job_cost j <= service sched j t) &&
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply /andP; split; first (apply /andP; split) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2072)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
scheduled : ~~ scheduled_at swap_sched j t
arrive : has_arrived j t
not_comp : ~~ (job_cost j <= service swap_sched j t)
============================
~~ (job_cost j <= service sched j t)
subgoal 2 (ID 2045) is:
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
+ by rewrite (service_after_swap_invariant sched t1 t2 _ t) // /t2; apply fsc_range1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2045)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
scheduled : ~~ scheduled_at swap_sched j t
arrive : has_arrived j t
not_comp : ~~ (job_cost j <= service swap_sched j t)
============================
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
+ by rewrite -(swap_job_scheduled_other_times _ t1 t2 j t) //; (apply /neqP; eauto).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1809)
subgoal 1 (ID 1809) is:
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1809)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
GT : t2 < t
NEQ : t <> t1
NEQ' : t <> t2
j_other : Job
j_other_scheduled : scheduled_at sched j_other t
============================
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
∃ j_other; by rewrite (swap_job_scheduled_other_times) //; do 2! (apply /neqP; eauto).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lastly, we show that if [t] lies between [t1] and [t2] then work conservation is still maintained.
Lemma non_idle_swap_maintains_work_conservation_BET_t1_t2 :
work_conserving arr_seq sched →
t1 < t ≤ t2 →
∃ j_other, scheduled_at swap_sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1621)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
============================
work_conserving arr_seq sched ->
t1 < t <= t2 -> exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
Proof.
move⇒ WC_sched H_range.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1623)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
H_range : t1 < t <= t2
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t1)) ⇒ [/eqP EQ| /eqP NEQ]; first by apply non_idle_swap_maintains_work_conservation_t1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1711)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
H_range : t1 < t <= t2
NEQ : t <> t1
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t2)) ⇒ [/eqP EQ'| /eqP NEQ']; first by apply non_idle_swap_maintains_work_conservation_t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1801)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
H_range : t1 < t <= t2
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
move: H_range.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1805)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
============================
t1 < t <= t2 -> exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
move /andP ⇒ [LT GE].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1846)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(scheduled_at sched j2 t)) ⇒ Hj'.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1867)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : scheduled_at sched j2 t
============================
exists j_other : Job, scheduled_at swap_sched j_other t
subgoal 2 (ID 1868) is:
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
- ∃ j2; by rewrite (swap_job_scheduled_other_times _ t1 t2 j2 t) //; (apply /neqP; eauto).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1868)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
- have [j_other j_other_scheduled] : ∃ j_other, scheduled_at sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1997)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
============================
exists j_other : Job, scheduled_at sched j_other t
subgoal 2 (ID 2009) is:
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1997)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
============================
exists j_other : Job, scheduled_at sched j_other t
----------------------------------------------------------------------------- *)
rewrite /work_conserving in WC_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2058)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
exists j_other : Job, scheduled_at sched j_other t
----------------------------------------------------------------------------- *)
apply (WC_sched j2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2059)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
arrives_in arr_seq j2
subgoal 2 (ID 2060) is:
backlogged sched j2 t
----------------------------------------------------------------------------- *)
- by unfold jobs_come_from_arrival_sequence in H_from_arr_seq; apply (H_from_arr_seq _ t2) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2060)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
backlogged sched j2 t
----------------------------------------------------------------------------- *)
- rewrite/backlogged/job_ready/basic_ready_instance/pending/completed_by.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2115)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
has_arrived j2 t && ~~ (job_cost j2 <= service sched j2 t) &&
~~ scheduled_at sched j2 t
----------------------------------------------------------------------------- *)
apply /andP; split; first (apply /andP; split) ⇒ //; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2168)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
has_arrived j2 t
subgoal 2 (ID 2169) is:
~~ (job_cost j2 <= service sched j2 t)
----------------------------------------------------------------------------- *)
+ by rewrite /has_arrived; apply (leq_trans H_arrival_j2); apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2169)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
~~ (job_cost j2 <= service sched j2 t)
----------------------------------------------------------------------------- *)
+ rewrite -ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2231)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
service sched j2 t < job_cost j2
----------------------------------------------------------------------------- *)
apply (leq_ltn_trans) with (service sched j2 t2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2235)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
service sched j2 t <= service sched j2 t2
subgoal 2 (ID 2236) is:
service sched j2 t2 < job_cost j2
----------------------------------------------------------------------------- *)
× by apply service_monotonic.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2236)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
service sched j2 t2 < job_cost j2
----------------------------------------------------------------------------- *)
× by apply H_completed_jobs_dont_execute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2009)
subgoal 1 (ID 2009) is:
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2009)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
j_other : Job
j_other_scheduled : scheduled_at sched j_other t
============================
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
∃ j_other.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2243)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
j_other : Job
j_other_scheduled : scheduled_at sched j_other t
============================
scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
now rewrite (swap_job_scheduled_other_times) //; (apply /neqP; eauto).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End NonIdleSwapWorkConservationLemmas.
work_conserving arr_seq sched →
t1 < t ≤ t2 →
∃ j_other, scheduled_at swap_sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1621)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
============================
work_conserving arr_seq sched ->
t1 < t <= t2 -> exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
Proof.
move⇒ WC_sched H_range.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1623)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
H_range : t1 < t <= t2
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t1)) ⇒ [/eqP EQ| /eqP NEQ]; first by apply non_idle_swap_maintains_work_conservation_t1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1711)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
H_range : t1 < t <= t2
NEQ : t <> t1
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t2)) ⇒ [/eqP EQ'| /eqP NEQ']; first by apply non_idle_swap_maintains_work_conservation_t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1801)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
H_range : t1 < t <= t2
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
move: H_range.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1805)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
============================
t1 < t <= t2 -> exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
move /andP ⇒ [LT GE].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1846)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
case: (boolP(scheduled_at sched j2 t)) ⇒ Hj'.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1867)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : scheduled_at sched j2 t
============================
exists j_other : Job, scheduled_at swap_sched j_other t
subgoal 2 (ID 1868) is:
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
- ∃ j2; by rewrite (swap_job_scheduled_other_times _ t1 t2 j2 t) //; (apply /neqP; eauto).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1868)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
============================
exists j_other : Job, scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
- have [j_other j_other_scheduled] : ∃ j_other, scheduled_at sched j_other t.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1997)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
============================
exists j_other : Job, scheduled_at sched j_other t
subgoal 2 (ID 2009) is:
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1997)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
============================
exists j_other : Job, scheduled_at sched j_other t
----------------------------------------------------------------------------- *)
rewrite /work_conserving in WC_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2058)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
exists j_other : Job, scheduled_at sched j_other t
----------------------------------------------------------------------------- *)
apply (WC_sched j2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2059)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
arrives_in arr_seq j2
subgoal 2 (ID 2060) is:
backlogged sched j2 t
----------------------------------------------------------------------------- *)
- by unfold jobs_come_from_arrival_sequence in H_from_arr_seq; apply (H_from_arr_seq _ t2) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2060)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
backlogged sched j2 t
----------------------------------------------------------------------------- *)
- rewrite/backlogged/job_ready/basic_ready_instance/pending/completed_by.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2115)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
has_arrived j2 t && ~~ (job_cost j2 <= service sched j2 t) &&
~~ scheduled_at sched j2 t
----------------------------------------------------------------------------- *)
apply /andP; split; first (apply /andP; split) ⇒ //; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2168)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
has_arrived j2 t
subgoal 2 (ID 2169) is:
~~ (job_cost j2 <= service sched j2 t)
----------------------------------------------------------------------------- *)
+ by rewrite /has_arrived; apply (leq_trans H_arrival_j2); apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2169)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
~~ (job_cost j2 <= service sched j2 t)
----------------------------------------------------------------------------- *)
+ rewrite -ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2231)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
service sched j2 t < job_cost j2
----------------------------------------------------------------------------- *)
apply (leq_ltn_trans) with (service sched j2 t2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2235)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
service sched j2 t <= service sched j2 t2
subgoal 2 (ID 2236) is:
service sched j2 t2 < job_cost j2
----------------------------------------------------------------------------- *)
× by apply service_monotonic.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2236)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
WC_sched : forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
exists j_other : Job, scheduled_at sched j_other t
============================
service sched j2 t2 < job_cost j2
----------------------------------------------------------------------------- *)
× by apply H_completed_jobs_dont_execute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2009)
subgoal 1 (ID 2009) is:
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2009)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
j_other : Job
j_other_scheduled : scheduled_at sched j_other t
============================
exists j_other0 : Job, scheduled_at swap_sched j_other0 t
----------------------------------------------------------------------------- *)
∃ j_other.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2243)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
t1, t2 : instant
H_well_ordered : t1 <= t2
j1, j2 : Job
H_arrival_j2 : job_arrival j2 <= t1
H_t1_not_idle : scheduled_at sched j1 t1
H_t2_not_idle : scheduled_at sched j2 t2
swap_sched := swapped sched t1 t2 : schedule (processor_state Job)
j : Job
t : instant
H_arrival_j : arrives_in arr_seq j
H_backlogged_j_t : backlogged swap_sched j t
WC_sched : work_conserving arr_seq sched
NEQ : t <> t1
NEQ' : t <> t2
LT : t1 < t
GE : t <= t2
Hj' : ~~ scheduled_at sched j2 t
j_other : Job
j_other_scheduled : scheduled_at sched j_other t
============================
scheduled_at swap_sched j_other t
----------------------------------------------------------------------------- *)
now rewrite (swap_job_scheduled_other_times) //; (apply /neqP; eauto).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End NonIdleSwapWorkConservationLemmas.
Work-Conserving Swap Candidates
For any given type of jobs...
...and any valid job arrival sequence,...
...consider an ideal uniprocessor schedule...
...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.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
...and in which all jobs come from the arrival sequence.
Suppose we are given a job [j1]...
...and a point in time [t1]...
...at which [j1] is scheduled...
...and that is before [j1]'s deadline.
We now show that, if [t2] is a swap candidate returned by
[find_swap_candidate] for [t1], then swapping the processor allocations at
the two instants maintains work conservation.
Corollary fsc_swap_maintains_work_conservation :
work_conserving arr_seq sched →
work_conserving arr_seq (swapped sched t1 (edf_trans.find_swap_candidate sched t1 j1)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1558)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
============================
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1563)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
============================
work_conserving arr_seq sched ->
work_conserving arr_seq (swapped sched t1 t2)
----------------------------------------------------------------------------- *)
have [j2 [t2_not_idle t2_arrival]] : ∃ j2, scheduled_at sched j2 t2 ∧ job_arrival j2 ≤ t1
by apply fsc_not_idle.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1601)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
============================
work_conserving arr_seq sched ->
work_conserving arr_seq (swapped sched t1 t2)
----------------------------------------------------------------------------- *)
have H_range : t1 ≤ t2 by apply fsc_range1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1610)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
============================
work_conserving arr_seq sched ->
work_conserving arr_seq (swapped sched t1 t2)
----------------------------------------------------------------------------- *)
move⇒ WC_sched j t ARR BL.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1616)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t1)) ⇒ [/eqP EQ| /eqP NEQ].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1703)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
EQ : t = t1
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 2 (ID 1704) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
- by apply (non_idle_swap_maintains_work_conservation_t1 arr_seq _ _ _ j2).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1704)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
- case: (boolP(t == t2)) ⇒ [/eqP EQ'| /eqP NEQ'].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1803)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
EQ' : t = t2
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 2 (ID 1804) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
+ by apply (non_idle_swap_maintains_work_conservation_t2 arr_seq _ _ _ j1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1804)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
+ case: (boolP((t ≤ t1) || (t2 < t))) ⇒ [NOT_BET | BET].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1827)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
NOT_BET : (t <= t1) || (t2 < t)
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 2 (ID 1828) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
(* t <> t2 *)
× move: NOT_BET; move/orP ⇒ [] ⇒ NOT_BET.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1874)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
NOT_BET : t <= t1
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 2 (ID 1875) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 3 (ID 1828) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1874)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
NOT_BET : t <= t1
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
by apply (non_idle_swap_maintains_work_conservation_LEQ_t1 arr_seq _ _ _ H_range _ _ H_not_idle t2_not_idle j).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1875)
subgoal 1 (ID 1875) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 2 (ID 1828) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1875)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
NOT_BET : t2 < t
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 2 (ID 1828) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1875)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
NOT_BET : t2 < t
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
by apply (non_idle_swap_maintains_work_conservation_GT_t2 arr_seq _ _ _ H_range _ _ H_not_idle t2_not_idle j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1828)
subgoal 1 (ID 1828) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1828)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
BET : ~~ ((t <= t1) || (t2 < t))
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
× move: BET; rewrite negb_or.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1915)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
============================
~~ (t <= t1) && ~~ (t2 < t) ->
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
move /andP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1945)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
============================
~~ (t <= t1) /\ ~~ (t2 < t) ->
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
case; rewrite <- ltnNge ⇒ range1; rewrite <- leqNgt ⇒ range2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1958)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
range1 : t1 < t
range2 : t <= t2
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
have BET: (t1 < t) && (t ≤ t2) by apply /andP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2013)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
range1 : t1 < t
range2 : t <= t2
BET : t1 < t <= t2
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
now apply (non_idle_swap_maintains_work_conservation_BET_t1_t2 arr_seq _ H_completed_jobs_dont_execute H_from_arr_seq _ _ _ _ t2_arrival H_not_idle t2_not_idle ).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FSCWorkConservationLemmas.
work_conserving arr_seq sched →
work_conserving arr_seq (swapped sched t1 (edf_trans.find_swap_candidate sched t1 j1)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1558)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
============================
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1563)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
============================
work_conserving arr_seq sched ->
work_conserving arr_seq (swapped sched t1 t2)
----------------------------------------------------------------------------- *)
have [j2 [t2_not_idle t2_arrival]] : ∃ j2, scheduled_at sched j2 t2 ∧ job_arrival j2 ≤ t1
by apply fsc_not_idle.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1601)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
============================
work_conserving arr_seq sched ->
work_conserving arr_seq (swapped sched t1 t2)
----------------------------------------------------------------------------- *)
have H_range : t1 ≤ t2 by apply fsc_range1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1610)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
============================
work_conserving arr_seq sched ->
work_conserving arr_seq (swapped sched t1 t2)
----------------------------------------------------------------------------- *)
move⇒ WC_sched j t ARR BL.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1616)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
case: (boolP(t == t1)) ⇒ [/eqP EQ| /eqP NEQ].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1703)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
EQ : t = t1
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 2 (ID 1704) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
- by apply (non_idle_swap_maintains_work_conservation_t1 arr_seq _ _ _ j2).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1704)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
- case: (boolP(t == t2)) ⇒ [/eqP EQ'| /eqP NEQ'].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1803)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
EQ' : t = t2
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 2 (ID 1804) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
+ by apply (non_idle_swap_maintains_work_conservation_t2 arr_seq _ _ _ j1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1804)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
+ case: (boolP((t ≤ t1) || (t2 < t))) ⇒ [NOT_BET | BET].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1827)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
NOT_BET : (t <= t1) || (t2 < t)
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 2 (ID 1828) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
(* t <> t2 *)
× move: NOT_BET; move/orP ⇒ [] ⇒ NOT_BET.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1874)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
NOT_BET : t <= t1
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 2 (ID 1875) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 3 (ID 1828) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1874)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
NOT_BET : t <= t1
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
by apply (non_idle_swap_maintains_work_conservation_LEQ_t1 arr_seq _ _ _ H_range _ _ H_not_idle t2_not_idle j).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1875)
subgoal 1 (ID 1875) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 2 (ID 1828) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1875)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
NOT_BET : t2 < t
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
subgoal 2 (ID 1828) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1875)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
NOT_BET : t2 < t
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
by apply (non_idle_swap_maintains_work_conservation_GT_t2 arr_seq _ _ _ H_range _ _ H_not_idle t2_not_idle j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1828)
subgoal 1 (ID 1828) is:
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1828)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
BET : ~~ ((t <= t1) || (t2 < t))
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
× move: BET; rewrite negb_or.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1915)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
============================
~~ (t <= t1) && ~~ (t2 < t) ->
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
move /andP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1945)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
============================
~~ (t <= t1) /\ ~~ (t2 < t) ->
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
case; rewrite <- ltnNge ⇒ range1; rewrite <- leqNgt ⇒ range2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1958)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
range1 : t1 < t
range2 : t <= t2
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
have BET: (t1 < t) && (t ≤ t2) by apply /andP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2013)
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)
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
j1 : Job
t1 : instant
H_not_idle : scheduled_at sched j1 t1
H_deadline_not_missed : t1 < job_deadline j1
t2 := edf_trans.find_swap_candidate sched t1 j1 : nat
j2 : Job
t2_not_idle : scheduled_at sched j2 t2
t2_arrival : job_arrival j2 <= t1
H_range : t1 <= t2
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
BL : backlogged (swapped sched t1 t2) j t
NEQ : t <> t1
NEQ' : t <> t2
range1 : t1 < t
range2 : t <= t2
BET : t1 < t <= t2
============================
exists j_other : Job, scheduled_at (swapped sched t1 t2) j_other t
----------------------------------------------------------------------------- *)
now apply (non_idle_swap_maintains_work_conservation_BET_t1_t2 arr_seq _ H_completed_jobs_dont_execute H_from_arr_seq _ _ _ _ t2_arrival H_not_idle t2_not_idle ).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FSCWorkConservationLemmas.
Work-Conservation of the Point-Wise EDF Transformation
For any given type of jobs...
... and any valid job arrival sequence, ...
... consider an ideal uniprocessor schedule ...
... in which all jobs come from 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.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
...and in which no scheduled job misses a deadline.
We analyze [make_edf_at] applied to an arbitrary point in time,
which we denote [t_edf] in the following.
For brevity, let [sched'] denote the schedule obtained from
[make_edf_at] applied to [sched] at time [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'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1558)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
============================
work_conserving arr_seq sched -> work_conserving arr_seq sched'
----------------------------------------------------------------------------- *)
Proof. rewrite /sched'/make_edf_at ⇒ WC_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1567)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
============================
work_conserving arr_seq
match sched t_edf with
| Some j =>
swapped sched t_edf (edf_trans.find_swap_candidate sched t_edf j)
| None => sched
end
----------------------------------------------------------------------------- *)
destruct (sched t_edf) eqn:E ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1580)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
============================
work_conserving arr_seq
(swapped sched t_edf (edf_trans.find_swap_candidate sched t_edf s))
----------------------------------------------------------------------------- *)
apply fsc_swap_maintains_work_conservation ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1620)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
============================
scheduled_at sched s t_edf
subgoal 2 (ID 1621) is:
t_edf < job_deadline s
----------------------------------------------------------------------------- *)
- by rewrite scheduled_at_def; apply /eqP ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1621)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
============================
t_edf < job_deadline s
----------------------------------------------------------------------------- *)
- apply (scheduled_at_implies_later_deadline sched) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1709)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
============================
ideal_progress_proc_model (option_eqType Job)
subgoal 2 (ID 1710) is:
job_meets_deadline sched s
subgoal 3 (ID 1711) is:
scheduled_at sched s t_edf
----------------------------------------------------------------------------- *)
+ by apply ideal_proc_model_ensures_ideal_progress.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1710)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
============================
job_meets_deadline sched s
subgoal 2 (ID 1711) is:
scheduled_at sched s t_edf
----------------------------------------------------------------------------- *)
+ rewrite /all_deadlines_met in (H_no_deadline_misses).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1815)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
H_no_deadline_misses : forall (j : Job) (t : instant),
scheduled_at sched j t -> job_meets_deadline sched j
============================
job_meets_deadline sched s
subgoal 2 (ID 1711) is:
scheduled_at sched s t_edf
----------------------------------------------------------------------------- *)
now apply (H_no_deadline_misses s t_edf); rewrite scheduled_at_def; apply /eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1711)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
============================
scheduled_at sched s t_edf
----------------------------------------------------------------------------- *)
+ by rewrite scheduled_at_def; apply/eqP ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End MakeEDFWorkConservationLemmas.
work_conserving arr_seq sched → work_conserving arr_seq sched'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1558)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
============================
work_conserving arr_seq sched -> work_conserving arr_seq sched'
----------------------------------------------------------------------------- *)
Proof. rewrite /sched'/make_edf_at ⇒ WC_sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1567)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
============================
work_conserving arr_seq
match sched t_edf with
| Some j =>
swapped sched t_edf (edf_trans.find_swap_candidate sched t_edf j)
| None => sched
end
----------------------------------------------------------------------------- *)
destruct (sched t_edf) eqn:E ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1580)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
============================
work_conserving arr_seq
(swapped sched t_edf (edf_trans.find_swap_candidate sched t_edf s))
----------------------------------------------------------------------------- *)
apply fsc_swap_maintains_work_conservation ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1620)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
============================
scheduled_at sched s t_edf
subgoal 2 (ID 1621) is:
t_edf < job_deadline s
----------------------------------------------------------------------------- *)
- by rewrite scheduled_at_def; apply /eqP ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1621)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
============================
t_edf < job_deadline s
----------------------------------------------------------------------------- *)
- apply (scheduled_at_implies_later_deadline sched) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1709)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
============================
ideal_progress_proc_model (option_eqType Job)
subgoal 2 (ID 1710) is:
job_meets_deadline sched s
subgoal 3 (ID 1711) is:
scheduled_at sched s t_edf
----------------------------------------------------------------------------- *)
+ by apply ideal_proc_model_ensures_ideal_progress.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1710)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
============================
job_meets_deadline sched s
subgoal 2 (ID 1711) is:
scheduled_at sched s t_edf
----------------------------------------------------------------------------- *)
+ rewrite /all_deadlines_met in (H_no_deadline_misses).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1815)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
H_no_deadline_misses : forall (j : Job) (t : instant),
scheduled_at sched j t -> job_meets_deadline sched j
============================
job_meets_deadline sched s
subgoal 2 (ID 1711) is:
scheduled_at sched s t_edf
----------------------------------------------------------------------------- *)
now apply (H_no_deadline_misses s t_edf); rewrite scheduled_at_def; apply /eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1711)
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)
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_no_deadline_misses : all_deadlines_met sched
t_edf : instant
sched' := make_edf_at sched t_edf : schedule (processor_state Job)
WC_sched : work_conserving arr_seq sched
s : Job
E : sched t_edf = Some s
============================
scheduled_at sched s t_edf
----------------------------------------------------------------------------- *)
+ by rewrite scheduled_at_def; apply/eqP ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End MakeEDFWorkConservationLemmas.
Work-Conserving EDF Prefix
For any given type of jobs, each characterized by execution
costs, an arrival time, and an absolute deadline,...
... and any valid job arrival sequence, ...
... consider an ideal uniprocessor schedule,...
... an arbitrary finite [horizon], and ...
...let [sched_trans] denote the schedule obtained by transforming
[sched] up to the horizon.
Let [schedule_behavior_premises] define the premise that a schedule is:
1) well-behaved,
2) has all jobs coming from the arrival sequence [arr_seq], and
3) in which no scheduled job misses its deadline
Definition scheduled_behavior_premises (sched : schedule (processor_state Job)) :=
jobs_must_arrive_to_execute sched
∧ completed_jobs_dont_execute sched
∧ jobs_come_from_arrival_sequence sched arr_seq
∧ all_deadlines_met sched.
jobs_must_arrive_to_execute sched
∧ completed_jobs_dont_execute sched
∧ jobs_come_from_arrival_sequence sched arr_seq
∧ all_deadlines_met sched.
For brevity, let [P] denote the predicate that a schedule satisfies
[scheduled_behavior_premises] and is work-conserving.
Let P (sched : schedule (processor_state Job)) :=
scheduled_behavior_premises sched ∧ work_conserving arr_seq sched.
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1552)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
============================
P sched -> P sched_trans
----------------------------------------------------------------------------- *)
Proof.
rewrite/sched_trans/edf_transform_prefix.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1560)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
============================
P sched -> P (prefix_map sched make_edf_at horizon)
----------------------------------------------------------------------------- *)
apply (prefix_map_property_invariance ).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1562)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
============================
forall (sched0 : schedule (option_eqType Job)) (t : instant),
P sched0 -> P (make_edf_at sched0 t)
----------------------------------------------------------------------------- *)
rewrite /P.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1563)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
============================
forall (sched0 : schedule (option_eqType Job)) (t : instant),
scheduled_behavior_premises sched0 /\ work_conserving arr_seq sched0 ->
scheduled_behavior_premises (make_edf_at sched0 t) /\
work_conserving arr_seq (make_edf_at sched0 t)
----------------------------------------------------------------------------- *)
move⇒ sched' t [[H_ARR [H_COMPLETED [H_COME H_all_deadlines_met]]] H_wc_sched].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1606)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
scheduled_behavior_premises (make_edf_at sched' t) /\
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
rewrite/scheduled_behavior_premises/valid_schedule; split; first split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1619)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
jobs_must_arrive_to_execute (make_edf_at sched' t)
subgoal 2 (ID 1620) is:
completed_jobs_dont_execute (make_edf_at sched' t) /\
jobs_come_from_arrival_sequence (make_edf_at sched' t) arr_seq /\
all_deadlines_met (make_edf_at sched' t)
subgoal 3 (ID 1617) is:
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
- by apply mea_jobs_must_arrive.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1620)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
completed_jobs_dont_execute (make_edf_at sched' t) /\
jobs_come_from_arrival_sequence (make_edf_at sched' t) arr_seq /\
all_deadlines_met (make_edf_at sched' t)
subgoal 2 (ID 1617) is:
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
- split; last split.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 1629)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
completed_jobs_dont_execute (make_edf_at sched' t)
subgoal 2 (ID 1632) is:
jobs_come_from_arrival_sequence (make_edf_at sched' t) arr_seq
subgoal 3 (ID 1633) is:
all_deadlines_met (make_edf_at sched' t)
subgoal 4 (ID 1617) is:
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
+ by apply mea_completed_jobs.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1632)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
jobs_come_from_arrival_sequence (make_edf_at sched' t) arr_seq
subgoal 2 (ID 1633) is:
all_deadlines_met (make_edf_at sched' t)
subgoal 3 (ID 1617) is:
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
+ by apply mea_jobs_come_from_arrival_sequence.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1633)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
all_deadlines_met (make_edf_at sched' t)
subgoal 2 (ID 1617) is:
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
+ by apply mea_no_deadline_misses.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1617)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
- by apply mea_maintains_work_conservation.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End EDFPrefixWorkConservationLemmas.
P sched → P sched_trans.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1552)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
============================
P sched -> P sched_trans
----------------------------------------------------------------------------- *)
Proof.
rewrite/sched_trans/edf_transform_prefix.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1560)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
============================
P sched -> P (prefix_map sched make_edf_at horizon)
----------------------------------------------------------------------------- *)
apply (prefix_map_property_invariance ).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1562)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
============================
forall (sched0 : schedule (option_eqType Job)) (t : instant),
P sched0 -> P (make_edf_at sched0 t)
----------------------------------------------------------------------------- *)
rewrite /P.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1563)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
============================
forall (sched0 : schedule (option_eqType Job)) (t : instant),
scheduled_behavior_premises sched0 /\ work_conserving arr_seq sched0 ->
scheduled_behavior_premises (make_edf_at sched0 t) /\
work_conserving arr_seq (make_edf_at sched0 t)
----------------------------------------------------------------------------- *)
move⇒ sched' t [[H_ARR [H_COMPLETED [H_COME H_all_deadlines_met]]] H_wc_sched].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1606)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
scheduled_behavior_premises (make_edf_at sched' t) /\
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
rewrite/scheduled_behavior_premises/valid_schedule; split; first split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1619)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
jobs_must_arrive_to_execute (make_edf_at sched' t)
subgoal 2 (ID 1620) is:
completed_jobs_dont_execute (make_edf_at sched' t) /\
jobs_come_from_arrival_sequence (make_edf_at sched' t) arr_seq /\
all_deadlines_met (make_edf_at sched' t)
subgoal 3 (ID 1617) is:
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
- by apply mea_jobs_must_arrive.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1620)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
completed_jobs_dont_execute (make_edf_at sched' t) /\
jobs_come_from_arrival_sequence (make_edf_at sched' t) arr_seq /\
all_deadlines_met (make_edf_at sched' t)
subgoal 2 (ID 1617) is:
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
- split; last split.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 1629)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
completed_jobs_dont_execute (make_edf_at sched' t)
subgoal 2 (ID 1632) is:
jobs_come_from_arrival_sequence (make_edf_at sched' t) arr_seq
subgoal 3 (ID 1633) is:
all_deadlines_met (make_edf_at sched' t)
subgoal 4 (ID 1617) is:
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
+ by apply mea_completed_jobs.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1632)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
jobs_come_from_arrival_sequence (make_edf_at sched' t) arr_seq
subgoal 2 (ID 1633) is:
all_deadlines_met (make_edf_at sched' t)
subgoal 3 (ID 1617) is:
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
+ by apply mea_jobs_come_from_arrival_sequence.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1633)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
all_deadlines_met (make_edf_at sched' t)
subgoal 2 (ID 1617) is:
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
+ by apply mea_no_deadline_misses.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1617)
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)
horizon : instant
sched_trans := edf_transform_prefix sched horizon
: schedule (processor_state Job)
P := fun sched : schedule (processor_state Job) =>
scheduled_behavior_premises sched /\ work_conserving arr_seq sched
: schedule (processor_state Job) -> Prop
sched' : schedule (option_eqType Job)
t : instant
H_ARR : jobs_must_arrive_to_execute sched'
H_COMPLETED : completed_jobs_dont_execute sched'
H_COME : jobs_come_from_arrival_sequence sched' arr_seq
H_all_deadlines_met : all_deadlines_met sched'
H_wc_sched : work_conserving arr_seq sched'
============================
work_conserving arr_seq (make_edf_at sched' t)
----------------------------------------------------------------------------- *)
- by apply mea_maintains_work_conservation.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End EDFPrefixWorkConservationLemmas.
Work-Conservation of the EDF Transformation
For any given type of jobs, each characterized by execution
costs, an arrival time, and an absolute deadline,...
... and any valid job arrival sequence, ...
... consider a valid ideal uniprocessor schedule ...
Variable sched: schedule (ideal.processor_state Job).
Hypothesis H_sched_valid: valid_schedule sched arr_seq.
Hypothesis H_sched_valid: valid_schedule sched arr_seq.
...and in which no scheduled job misses a deadline.
We first note that [sched] satisfies [scheduled_behavior_premises].
Lemma sched_satisfies_behavior_premises : scheduled_behavior_premises arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1543)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
============================
scheduled_behavior_premises arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split; [ apply (jobs_must_arrive_to_be_ready sched) | split; [ apply (completed_jobs_are_not_ready sched) | split]].
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 1553)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
============================
jobs_must_be_ready_to_execute sched
subgoal 2 (ID 1563) is:
jobs_must_be_ready_to_execute sched
subgoal 3 (ID 1565) is:
jobs_come_from_arrival_sequence sched arr_seq
subgoal 4 (ID 1566) is:
all_deadlines_met sched
----------------------------------------------------------------------------- *)
all: by try apply H_sched_valid.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1543)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
============================
scheduled_behavior_premises arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split; [ apply (jobs_must_arrive_to_be_ready sched) | split; [ apply (completed_jobs_are_not_ready sched) | split]].
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 1553)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
============================
jobs_must_be_ready_to_execute sched
subgoal 2 (ID 1563) is:
jobs_must_be_ready_to_execute sched
subgoal 3 (ID 1565) is:
jobs_come_from_arrival_sequence sched arr_seq
subgoal 4 (ID 1566) is:
all_deadlines_met sched
----------------------------------------------------------------------------- *)
all: by try apply H_sched_valid.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We prove that, if the given schedule [sched] is work-conserving, then the
schedule that results from transforming it into an EDF schedule is also
work-conserving.
Lemma edf_transform_maintains_work_conservation :
work_conserving arr_seq sched → work_conserving arr_seq (edf_transform sched).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1559)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
============================
work_conserving arr_seq sched ->
work_conserving arr_seq (edf_transform sched)
----------------------------------------------------------------------------- *)
Proof.
move⇒ WC_sched j t ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1564)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
============================
backlogged (edf_transform sched) j t ->
exists j_other : Job, scheduled_at (edf_transform sched) j_other t
----------------------------------------------------------------------------- *)
set sched_edf := edf_transform sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1569)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
sched_edf := edf_transform sched : instant -> processor_state Job
============================
backlogged sched_edf j t ->
exists j_other : Job, scheduled_at sched_edf j_other t
----------------------------------------------------------------------------- *)
have IDENT: identical_prefix sched_edf (edf_transform_prefix sched t.+1) t.+1
by rewrite /sched_edf/edf_transform ⇒ t' LE_t; apply (edf_prefix_inclusion) ⇒ //; apply sched_satisfies_behavior_premises.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1672)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
sched_edf := edf_transform sched : instant -> processor_state Job
IDENT : identical_prefix sched_edf (edf_transform_prefix sched (succn t))
(succn t)
============================
backlogged sched_edf j t ->
exists j_other : Job, scheduled_at sched_edf j_other t
----------------------------------------------------------------------------- *)
rewrite (backlogged_prefix_invariance _ _ (edf_transform_prefix sched t.+1) t.+1) // ⇒ BL;
last by apply basic_readiness_nonclairvoyance.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1766)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
sched_edf := edf_transform sched : instant -> processor_state Job
IDENT : identical_prefix sched_edf (edf_transform_prefix sched (succn t))
(succn t)
BL : backlogged (edf_transform_prefix sched (succn t)) j t
============================
exists j_other : Job, scheduled_at sched_edf j_other t
----------------------------------------------------------------------------- *)
have WC_trans: work_conserving arr_seq (edf_transform_prefix sched (succn t))
by apply edf_transform_prefix_maintains_work_conservation; split ⇒ //; apply sched_satisfies_behavior_premises.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1970)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
sched_edf := edf_transform sched : instant -> processor_state Job
IDENT : identical_prefix sched_edf (edf_transform_prefix sched (succn t))
(succn t)
BL : backlogged (edf_transform_prefix sched (succn t)) j t
WC_trans : work_conserving arr_seq (edf_transform_prefix sched (succn t))
============================
exists j_other : Job, scheduled_at sched_edf j_other t
----------------------------------------------------------------------------- *)
move: (WC_trans _ _ ARR BL) ⇒ [j_other SCHED_AT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1986)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
sched_edf := edf_transform sched : instant -> processor_state Job
IDENT : identical_prefix sched_edf (edf_transform_prefix sched (succn t))
(succn t)
BL : backlogged (edf_transform_prefix sched (succn t)) j t
WC_trans : work_conserving arr_seq (edf_transform_prefix sched (succn t))
j_other : Job
SCHED_AT : scheduled_at (edf_transform_prefix sched (succn t)) j_other t
============================
exists j_other0 : Job, scheduled_at sched_edf j_other0 t
----------------------------------------------------------------------------- *)
∃ j_other.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1988)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
sched_edf := edf_transform sched : instant -> processor_state Job
IDENT : identical_prefix sched_edf (edf_transform_prefix sched (succn t))
(succn t)
BL : backlogged (edf_transform_prefix sched (succn t)) j t
WC_trans : work_conserving arr_seq (edf_transform_prefix sched (succn t))
j_other : Job
SCHED_AT : scheduled_at (edf_transform_prefix sched (succn t)) j_other t
============================
scheduled_at sched_edf j_other t
----------------------------------------------------------------------------- *)
now rewrite (identical_prefix_scheduled_at _ (edf_transform_prefix sched t.+1) t.+1) //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End EDFTransformWorkConservationLemmas.
work_conserving arr_seq sched → work_conserving arr_seq (edf_transform sched).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1559)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
============================
work_conserving arr_seq sched ->
work_conserving arr_seq (edf_transform sched)
----------------------------------------------------------------------------- *)
Proof.
move⇒ WC_sched j t ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1564)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
============================
backlogged (edf_transform sched) j t ->
exists j_other : Job, scheduled_at (edf_transform sched) j_other t
----------------------------------------------------------------------------- *)
set sched_edf := edf_transform sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1569)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
sched_edf := edf_transform sched : instant -> processor_state Job
============================
backlogged sched_edf j t ->
exists j_other : Job, scheduled_at sched_edf j_other t
----------------------------------------------------------------------------- *)
have IDENT: identical_prefix sched_edf (edf_transform_prefix sched t.+1) t.+1
by rewrite /sched_edf/edf_transform ⇒ t' LE_t; apply (edf_prefix_inclusion) ⇒ //; apply sched_satisfies_behavior_premises.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1672)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
sched_edf := edf_transform sched : instant -> processor_state Job
IDENT : identical_prefix sched_edf (edf_transform_prefix sched (succn t))
(succn t)
============================
backlogged sched_edf j t ->
exists j_other : Job, scheduled_at sched_edf j_other t
----------------------------------------------------------------------------- *)
rewrite (backlogged_prefix_invariance _ _ (edf_transform_prefix sched t.+1) t.+1) // ⇒ BL;
last by apply basic_readiness_nonclairvoyance.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1766)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
sched_edf := edf_transform sched : instant -> processor_state Job
IDENT : identical_prefix sched_edf (edf_transform_prefix sched (succn t))
(succn t)
BL : backlogged (edf_transform_prefix sched (succn t)) j t
============================
exists j_other : Job, scheduled_at sched_edf j_other t
----------------------------------------------------------------------------- *)
have WC_trans: work_conserving arr_seq (edf_transform_prefix sched (succn t))
by apply edf_transform_prefix_maintains_work_conservation; split ⇒ //; apply sched_satisfies_behavior_premises.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1970)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
sched_edf := edf_transform sched : instant -> processor_state Job
IDENT : identical_prefix sched_edf (edf_transform_prefix sched (succn t))
(succn t)
BL : backlogged (edf_transform_prefix sched (succn t)) j t
WC_trans : work_conserving arr_seq (edf_transform_prefix sched (succn t))
============================
exists j_other : Job, scheduled_at sched_edf j_other t
----------------------------------------------------------------------------- *)
move: (WC_trans _ _ ARR BL) ⇒ [j_other SCHED_AT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1986)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
sched_edf := edf_transform sched : instant -> processor_state Job
IDENT : identical_prefix sched_edf (edf_transform_prefix sched (succn t))
(succn t)
BL : backlogged (edf_transform_prefix sched (succn t)) j t
WC_trans : work_conserving arr_seq (edf_transform_prefix sched (succn t))
j_other : Job
SCHED_AT : scheduled_at (edf_transform_prefix sched (succn t)) j_other t
============================
exists j_other0 : Job, scheduled_at sched_edf j_other0 t
----------------------------------------------------------------------------- *)
∃ j_other.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1988)
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)
H_sched_valid : valid_schedule sched arr_seq
H_no_deadline_misses : all_deadlines_met sched
WC_sched : work_conserving arr_seq sched
j : Job
t : instant
ARR : arrives_in arr_seq j
sched_edf := edf_transform sched : instant -> processor_state Job
IDENT : identical_prefix sched_edf (edf_transform_prefix sched (succn t))
(succn t)
BL : backlogged (edf_transform_prefix sched (succn t)) j t
WC_trans : work_conserving arr_seq (edf_transform_prefix sched (succn t))
j_other : Job
SCHED_AT : scheduled_at (edf_transform_prefix sched (succn t)) j_other t
============================
scheduled_at sched_edf j_other t
----------------------------------------------------------------------------- *)
now rewrite (identical_prefix_scheduled_at _ (edf_transform_prefix sched t.+1) t.+1) //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End EDFTransformWorkConservationLemmas.