Library prosa.analysis.facts.edf_definitions
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.model.ideal_schedule.
Require Export prosa.analysis.facts.behavior.deadlines.
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.model.priority.edf.
Require Export prosa.model.schedule.edf.
Require Export prosa.model.schedule.priority_driven.
Equivalence of EDF Definitions
... (2) the classic Liu & Layland model of readiness without jitter and
without self-suspensions, where pending jobs are always ready, and ...
... (3) that jobs are fully preemptive.
For any given type of jobs, each characterized by an arrival time,
an execution cost, and an absolute deadline, ...
...consider a given valid job arrival sequence ...
...and a corresponding schedule.
Suppose jobs don't execute after their completion, ...
...all jobs come from the arrival sequence [arr_seq], ...
...and jobs from [arr_seq] don't miss their deadlines.
We first show that a schedule that satisfies the standalone
[EDF_schedule] predicate is also compliant with the generic notion of EDF
policy defined in Prosa, namely the [respects_policy_at_preemption_point]
predicate.
Lemma EDF_schedule_implies_respects_policy_at_preemption_point :
EDF_schedule sched →
respects_policy_at_preemption_point arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 48)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
============================
EDF_schedule sched -> respects_policy_at_preemption_point arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
move⇒ EDF j' j t ARR PREEMPTION BL SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
============================
hep_job_at t j j'
----------------------------------------------------------------------------- *)
have suff: ∃ t' : nat, t ≤ t' < job_deadline j' ∧ scheduled_at sched j' t'.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 64)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
============================
(exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t') ->
hep_job_at t j j'
subgoal 2 (ID 65) is:
((exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t') ->
hep_job_at t j j') -> hep_job_at t j j'
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
============================
(exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t') ->
hep_job_at t j j'
----------------------------------------------------------------------------- *)
move⇒ [t' [/andP [LE _] SCHED']].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 124)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
t' : nat
LE : t <= t'
SCHED' : scheduled_at sched j' t'
============================
hep_job_at t j j'
----------------------------------------------------------------------------- *)
apply: (EDF t); [done | exact LE | exact SCHED' |].
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 163)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
t' : nat
LE : t <= t'
SCHED' : scheduled_at sched j' t'
============================
job_arrival j' <= t
----------------------------------------------------------------------------- *)
by apply: (backlogged_implies_arrived sched j' t).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 65) is:
((exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t') ->
hep_job_at t j j') -> hep_job_at t j j'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 65)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
============================
((exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t') ->
hep_job_at t j j') -> hep_job_at t j j'
----------------------------------------------------------------------------- *)
apply; apply: incomplete_implies_scheduled_later;
first by apply: H_no_deadline_misses ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 250)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
============================
~~ completed_by sched j' t
----------------------------------------------------------------------------- *)
by apply: (backlogged_implies_incomplete sched j' t).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
EDF_schedule sched →
respects_policy_at_preemption_point arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 48)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
============================
EDF_schedule sched -> respects_policy_at_preemption_point arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
move⇒ EDF j' j t ARR PREEMPTION BL SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
============================
hep_job_at t j j'
----------------------------------------------------------------------------- *)
have suff: ∃ t' : nat, t ≤ t' < job_deadline j' ∧ scheduled_at sched j' t'.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 64)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
============================
(exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t') ->
hep_job_at t j j'
subgoal 2 (ID 65) is:
((exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t') ->
hep_job_at t j j') -> hep_job_at t j j'
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
============================
(exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t') ->
hep_job_at t j j'
----------------------------------------------------------------------------- *)
move⇒ [t' [/andP [LE _] SCHED']].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 124)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
t' : nat
LE : t <= t'
SCHED' : scheduled_at sched j' t'
============================
hep_job_at t j j'
----------------------------------------------------------------------------- *)
apply: (EDF t); [done | exact LE | exact SCHED' |].
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 163)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
t' : nat
LE : t <= t'
SCHED' : scheduled_at sched j' t'
============================
job_arrival j' <= t
----------------------------------------------------------------------------- *)
by apply: (backlogged_implies_arrived sched j' t).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 65) is:
((exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t') ->
hep_job_at t j j') -> hep_job_at t j j'
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 65)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
============================
((exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t') ->
hep_job_at t j j') -> hep_job_at t j j'
----------------------------------------------------------------------------- *)
apply; apply: incomplete_implies_scheduled_later;
first by apply: H_no_deadline_misses ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 250)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
EDF : EDF_schedule sched
j', j : Job
t : instant
ARR : arrives_in arr_seq j'
PREEMPTION : preemption_time sched t
BL : backlogged sched j' t
SCHED : scheduled_at sched j t
============================
~~ completed_by sched j' t
----------------------------------------------------------------------------- *)
by apply: (backlogged_implies_incomplete sched j' t).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Conversely, the reverse direction also holds: a schedule that satisfies
the [respects_policy_at_preemption_point] predicate is also an EDF
schedule in the sense of [EDF_schedule].
Lemma respects_policy_at_preemption_point_implies_EDF_schedule :
respects_policy_at_preemption_point arr_seq sched →
EDF_schedule sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
============================
respects_policy_at_preemption_point arr_seq sched -> EDF_schedule sched
----------------------------------------------------------------------------- *)
Proof.
move⇒ H_priority_driven t j_hp SCHED t' j LEQ SCHED' EARLIER_ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
============================
job_deadline j_hp <= job_deadline j
----------------------------------------------------------------------------- *)
case (boolP (j == j_hp)); first by move /eqP ⇒ EQ; subst.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 81)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
============================
j != j_hp -> job_deadline j_hp <= job_deadline j
----------------------------------------------------------------------------- *)
move /neqP ⇒ NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 154)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
job_deadline j_hp <= job_deadline j
----------------------------------------------------------------------------- *)
exploit (H_priority_driven j j_hp t) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 496)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
arrives_in arr_seq j
subgoal 2 (ID 497) is:
preemption_time sched t
subgoal 3 (ID 498) is:
backlogged sched j t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 496)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
arrives_in arr_seq j
----------------------------------------------------------------------------- *)
by apply (H_from_arr_seq _ _ SCHED').
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 497) is:
preemption_time sched t
subgoal 2 (ID 498) is:
backlogged sched j t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 497)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
preemption_time sched t
subgoal 2 (ID 498) is:
backlogged sched j t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 497)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
preemption_time sched t
----------------------------------------------------------------------------- *)
by rewrite /preemption_time; destruct (sched t).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 498) is:
backlogged sched j t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 498)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
backlogged sched j t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 498)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
backlogged sched j t
----------------------------------------------------------------------------- *)
apply /andP; split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 616)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
job_ready sched j t
subgoal 2 (ID 617) is:
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
- apply /andP; split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 688)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
~~ completed_by sched j t
subgoal 2 (ID 617) is:
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply (incompletion_monotonic _ j _ _ LEQ).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 721)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
~~ completed_by sched j t'
subgoal 2 (ID 617) is:
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply scheduled_implies_not_completed ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 727)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
ideal_progress_proc_model (processor_state Job)
subgoal 2 (ID 617) is:
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
by apply ideal_proc_model_ensures_ideal_progress.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 617)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
- apply /negP; move ⇒ SCHED''.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 776)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
SCHED'' : scheduled_at sched j t
============================
False
----------------------------------------------------------------------------- *)
by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
respects_policy_at_preemption_point arr_seq sched →
EDF_schedule sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
============================
respects_policy_at_preemption_point arr_seq sched -> EDF_schedule sched
----------------------------------------------------------------------------- *)
Proof.
move⇒ H_priority_driven t j_hp SCHED t' j LEQ SCHED' EARLIER_ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
============================
job_deadline j_hp <= job_deadline j
----------------------------------------------------------------------------- *)
case (boolP (j == j_hp)); first by move /eqP ⇒ EQ; subst.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 81)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
============================
j != j_hp -> job_deadline j_hp <= job_deadline j
----------------------------------------------------------------------------- *)
move /neqP ⇒ NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 154)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
job_deadline j_hp <= job_deadline j
----------------------------------------------------------------------------- *)
exploit (H_priority_driven j j_hp t) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 496)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
arrives_in arr_seq j
subgoal 2 (ID 497) is:
preemption_time sched t
subgoal 3 (ID 498) is:
backlogged sched j t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 496)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_arr_seq_valid : valid_arrival_sequence arr_seq
sched : schedule (processor_state Job)
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
arrives_in arr_seq j
----------------------------------------------------------------------------- *)
by apply (H_from_arr_seq _ _ SCHED').
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 497) is:
preemption_time sched t
subgoal 2 (ID 498) is:
backlogged sched j t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 497)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
preemption_time sched t
subgoal 2 (ID 498) is:
backlogged sched j t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 497)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
preemption_time sched t
----------------------------------------------------------------------------- *)
by rewrite /preemption_time; destruct (sched t).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 498) is:
backlogged sched j t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 498)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
backlogged sched j t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 498)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
backlogged sched j t
----------------------------------------------------------------------------- *)
apply /andP; split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 616)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
job_ready sched j t
subgoal 2 (ID 617) is:
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
- apply /andP; split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 688)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
~~ completed_by sched j t
subgoal 2 (ID 617) is:
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply (incompletion_monotonic _ j _ _ LEQ).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 721)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
~~ completed_by sched j t'
subgoal 2 (ID 617) is:
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply scheduled_implies_not_completed ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 727)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
ideal_progress_proc_model (processor_state Job)
subgoal 2 (ID 617) is:
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
by apply ideal_proc_model_ensures_ideal_progress.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 617)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
============================
~~ scheduled_at sched j t
----------------------------------------------------------------------------- *)
- apply /negP; move ⇒ SCHED''.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 776)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
H_priority_driven : respects_policy_at_preemption_point arr_seq sched
t : instant
j_hp : Job
SCHED : scheduled_at sched j_hp t
t' : instant
j : Job
LEQ : t <= t'
SCHED' : scheduled_at sched j t'
EARLIER_ARR : job_arrival j <= t
NEQ : j <> j_hp
SCHED'' : scheduled_at sched j t
============================
False
----------------------------------------------------------------------------- *)
by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
From the two preceding lemmas, it follows immediately that the two EDF
definitions are indeed equivalent, which we note with the following
corollary.
Corollary EDF_schedule_equiv:
EDF_schedule sched ↔ respects_policy_at_preemption_point arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
============================
EDF_schedule sched <-> respects_policy_at_preemption_point arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 82)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
============================
EDF_schedule sched -> respects_policy_at_preemption_point arr_seq sched
subgoal 2 (ID 83) is:
respects_policy_at_preemption_point arr_seq sched -> EDF_schedule sched
----------------------------------------------------------------------------- *)
- by apply EDF_schedule_implies_respects_policy_at_preemption_point.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 83)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
============================
respects_policy_at_preemption_point arr_seq sched -> EDF_schedule sched
----------------------------------------------------------------------------- *)
- by apply respects_policy_at_preemption_point_implies_EDF_schedule.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Equivalence.
EDF_schedule sched ↔ respects_policy_at_preemption_point arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
============================
EDF_schedule sched <-> respects_policy_at_preemption_point arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 82)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
============================
EDF_schedule sched -> respects_policy_at_preemption_point arr_seq sched
subgoal 2 (ID 83) is:
respects_policy_at_preemption_point arr_seq sched -> EDF_schedule sched
----------------------------------------------------------------------------- *)
- by apply EDF_schedule_implies_respects_policy_at_preemption_point.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 83)
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_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq
H_no_deadline_misses : all_deadlines_of_arrivals_met arr_seq sched
============================
respects_policy_at_preemption_point arr_seq sched -> EDF_schedule sched
----------------------------------------------------------------------------- *)
- by apply respects_policy_at_preemption_point_implies_EDF_schedule.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Equivalence.