Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Import prosa.model.readiness.basic.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.model.schedule.edf.
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.analysis.transform.edf_trans.
Require Export prosa.analysis.facts.transform.swaps.
Require Export prosa.analysis.facts.readiness.basic.
(** This file contains the main argument of the EDF optimality proof,
starting with an analysis of the individual functions that drive
the piece-wise transformation of a given reference schedule in an
EDF schedule, and ending with proofs of individual properties of
the obtained EDF schedule. *)
(** We start by analyzing the helper function [find_swap_candidate],
which is a problem-specific wrapper around [search_arg]. *)
Section FindSwapCandidateFacts .
(** We assume the classic (i.e., Liu & Layland) model of readiness
without jitter or self-suspensions, wherein pending jobs are
always ready. *)
#[local] Existing Instance basic_ready_instance .
(** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(** ...consider an ideal uniprocessor schedule... *)
Variable sched : schedule (ideal.processor_state Job).
(** ...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.
(** Suppose we are given a job [j1]... *)
Variable j1 : Job.
(** ...and a point in time [t1]... *)
Variable t1 : instant.
(** ...at which [j1] is scheduled... *)
Hypothesis H_not_idle : scheduled_at sched j1 t1.
(** ...and that is before its deadline. *)
Hypothesis H_deadline_not_missed : t1 < job_deadline j1.
(** First, we observe that under these assumptions the processor
state at time [t1] is "relevant" according to the notion of
relevance underlying the EDF transformation, namely
[relevant_pstate]. *)
Lemma t1_relevant : relevant_pstate t1 (sched t1).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
relevant_pstate t1 (sched t1)
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
relevant_pstate t1 (sched t1)
move : H_not_idle.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
scheduled_at sched j1 t1 ->
relevant_pstate t1 (sched t1)
rewrite scheduled_at_def => /eqP ->.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
relevant_pstate t1 (Some j1)
rewrite /relevant_pstate -/(has_arrived j1 t1).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
has_arrived j1 t1
move : (H_jobs_must_arrive_to_execute j1 t1) => SCHED_ARR.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 SCHED_ARR : scheduled_at sched j1 t1 ->
has_arrived j1 t1
has_arrived j1 t1
now apply SCHED_ARR.
Qed .
(** Since [t1] is relevant, we conclude that a search for a relevant
state succeeds (if nothing else, it finds [t1]). *)
Lemma fsc_search_successful :
exists t , search_arg sched (relevant_pstate t1) earlier_deadline t1 (job_deadline j1) = Some t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
exists t : nat,
search_arg sched (relevant_pstate t1)
earlier_deadline t1 (job_deadline j1) = Some t
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
exists t : nat,
search_arg sched (relevant_pstate t1)
earlier_deadline t1 (job_deadline j1) = Some t
apply search_arg_not_none.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
exists x : nat,
t1 <= x < job_deadline j1 /\
relevant_pstate t1 (sched x)
exists t1 .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
t1 <= t1 < job_deadline j1 /\
relevant_pstate t1 (sched t1)
split .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
t1 <= t1 < job_deadline j1
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
t1 <= t1 < job_deadline j1
by apply /andP; split .
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
relevant_pstate t1 (sched t1)
by apply t1_relevant.
Qed .
(** For rewriting purposes, we observe that the [search_arg]
operation within [find_swap_candidate] yields the final result of
[find_swap_candidate]. *)
Corollary fsc_search_result :
search_arg sched (relevant_pstate t1) earlier_deadline t1 (job_deadline j1) = Some (find_swap_candidate sched t1 j1).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
search_arg sched (relevant_pstate t1) earlier_deadline
t1 (job_deadline j1) =
Some (find_swap_candidate sched t1 j1)
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
search_arg sched (relevant_pstate t1) earlier_deadline
t1 (job_deadline j1) =
Some (find_swap_candidate sched t1 j1)
move : fsc_search_successful => [t FOUND].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 t : nat FOUND : search_arg sched (relevant_pstate t1)
earlier_deadline t1 (job_deadline j1) =
Some t
search_arg sched (relevant_pstate t1) earlier_deadline
t1 (job_deadline j1) =
Some (find_swap_candidate sched t1 j1)
now rewrite /find_swap_candidate FOUND.
Qed .
(** There is a job that is scheduled at the time that
[find_swap_candidate] returns, and that job arrives no later than
at time [t1]. *)
Lemma fsc_not_idle :
exists j' , (scheduled_at sched j' (find_swap_candidate sched t1 j1))
/\ job_arrival j' <= t1.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
exists j' : Job,
scheduled_at sched j'
(find_swap_candidate sched t1 j1) /\
job_arrival j' <= t1
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
exists j' : Job,
scheduled_at sched j'
(find_swap_candidate sched t1 j1) /\
job_arrival j' <= t1
move : fsc_search_successful => [t FOUND].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 t : nat FOUND : search_arg sched (relevant_pstate t1)
earlier_deadline t1 (job_deadline j1) =
Some t
exists j' : Job,
scheduled_at sched j'
(find_swap_candidate sched t1 j1) /\
job_arrival j' <= t1
move : (search_arg_pred _ _ _ _ _ _ FOUND).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 t : nat FOUND : search_arg sched (relevant_pstate t1)
earlier_deadline t1 (job_deadline j1) =
Some t
relevant_pstate t1 (sched t) ->
exists j' : Job,
scheduled_at sched j'
(find_swap_candidate sched t1 j1) /\
job_arrival j' <= t1
rewrite /relevant_pstate.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 t : nat FOUND : search_arg sched (relevant_pstate t1)
earlier_deadline t1 (job_deadline j1) =
Some t
match sched t with
| Some j' => job_arrival j' <= t1
| None => false
end ->
exists j' : Job,
scheduled_at sched j'
(find_swap_candidate sched t1 j1) /\
job_arrival j' <= t1
destruct (sched t) as [j'|] eqn :SCHED_t => // ARR_j'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 t : nat FOUND : search_arg sched (relevant_pstate t1)
earlier_deadline t1 (job_deadline j1) =
Some t j' : Job SCHED_t : sched t = Some j' ARR_j' : job_arrival j' <= t1
exists j' : Job,
scheduled_at sched j'
(find_swap_candidate sched t1 j1) /\
job_arrival j' <= t1
exists j' .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 t : nat FOUND : search_arg sched (relevant_pstate t1)
earlier_deadline t1 (job_deadline j1) =
Some t j' : Job SCHED_t : sched t = Some j' ARR_j' : job_arrival j' <= t1
scheduled_at sched j'
(find_swap_candidate sched t1 j1) /\
job_arrival j' <= t1
split => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 t : nat FOUND : search_arg sched (relevant_pstate t1)
earlier_deadline t1 (job_deadline j1) =
Some t j' : Job SCHED_t : sched t = Some j' ARR_j' : job_arrival j' <= t1
scheduled_at sched j'
(find_swap_candidate sched t1 j1)
rewrite /find_swap_candidate FOUND.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 t : nat FOUND : search_arg sched (relevant_pstate t1)
earlier_deadline t1 (job_deadline j1) =
Some t j' : Job SCHED_t : sched t = Some j' ARR_j' : job_arrival j' <= t1
scheduled_at sched j' t
rewrite scheduled_at_def //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 t : nat FOUND : search_arg sched (relevant_pstate t1)
earlier_deadline t1 (job_deadline j1) =
Some t j' : Job SCHED_t : sched t = Some j' ARR_j' : job_arrival j' <= t1
sched t == Some j'
now apply /eqP.
Qed .
(** Since we are considering a uniprocessor model, only one job is
scheduled at a time. Hence once we know that a job is scheduled
at the time that [find_swap_candidate] returns, we can conclude
that it arrives not later than at time t1. *)
Corollary fsc_found_job_arrival :
forall j2 ,
scheduled_at sched j2 (find_swap_candidate sched t1 j1) ->
job_arrival j2 <= t1.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
forall j2 : Job,
scheduled_at sched j2
(find_swap_candidate sched t1 j1) ->
job_arrival j2 <= t1
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
forall j2 : Job,
scheduled_at sched j2
(find_swap_candidate sched t1 j1) ->
job_arrival j2 <= t1
move => j2 SCHED_j2.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2 : Job SCHED_j2 : scheduled_at sched j2
(find_swap_candidate sched t1 j1)
job_arrival j2 <= t1
move : fsc_not_idle => [j' [SCHED_j' ARR]].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2 : Job SCHED_j2 : scheduled_at sched j2
(find_swap_candidate sched t1 j1) j' : Job SCHED_j' : scheduled_at sched j'
(find_swap_candidate sched t1 j1) ARR : job_arrival j' <= t1
job_arrival j2 <= t1
now rewrite -(ideal_proc_model_is_a_uniprocessor_model _ _ _ _ SCHED_j' SCHED_j2).
Qed .
(** We observe that [find_swap_candidate] returns a value within a
known finite interval. *)
Lemma fsc_range :
t1 <= find_swap_candidate sched t1 j1 < job_deadline j1.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
t1 <= find_swap_candidate sched t1 j1 <
job_deadline j1
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
t1 <= find_swap_candidate sched t1 j1 <
job_deadline j1
move : fsc_search_result.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
search_arg sched (relevant_pstate t1) earlier_deadline
t1 (job_deadline j1) =
Some (find_swap_candidate sched t1 j1) ->
t1 <= find_swap_candidate sched t1 j1 <
job_deadline j1
by apply search_arg_in_range. Qed .
(** For convenience, since we often only require the lower bound on
the interval, we re-state it as a corollary. *)
Corollary fsc_range1 :
t1 <= find_swap_candidate sched t1 j1.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
t1 <= find_swap_candidate sched t1 j1
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
t1 <= find_swap_candidate sched t1 j1
by move : fsc_range => /andP [LE _]. Qed .
(** The following lemma is a key step of the overall proof: the job
scheduled at the time found by [find_swap_candidate] has the
property that it has a deadline that is no later than that of any
other job in the window given by time [t1] and the deadline of
the job scheduled at time [t1]. *)
Lemma fsc_found_job_deadline :
forall j2 ,
scheduled_at sched j2 (find_swap_candidate sched t1 j1) ->
forall j t ,
t1 <= t < job_deadline j1 ->
scheduled_at sched j t ->
job_arrival j <= t1 ->
job_deadline j2 <= job_deadline j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
forall j2 : Job,
scheduled_at sched j2
(find_swap_candidate sched t1 j1) ->
forall (j : Job) (t : nat),
t1 <= t < job_deadline j1 ->
scheduled_at sched j t ->
job_arrival j <= t1 ->
job_deadline j2 <= job_deadline j
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
forall j2 : Job,
scheduled_at sched j2
(find_swap_candidate sched t1 j1) ->
forall (j : Job) (t : nat),
t1 <= t < job_deadline j1 ->
scheduled_at sched j t ->
job_arrival j <= t1 ->
job_deadline j2 <= job_deadline j
move => j2 SCHED_j2 j t /andP [t1_le_t t_lt_dl1] SCHED_j ARR_j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2 : Job SCHED_j2 : scheduled_at sched j2
(find_swap_candidate sched t1 j1) j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 SCHED_j : scheduled_at sched j t ARR_j : job_arrival j <= t1
job_deadline j2 <= job_deadline j
have TOTAL: total earlier_deadline
by rewrite /earlier_deadline => s1 s2; apply leq_total.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2 : Job SCHED_j2 : scheduled_at sched j2
(find_swap_candidate sched t1 j1) j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 SCHED_j : scheduled_at sched j t ARR_j : job_arrival j <= t1 TOTAL : total (T:=ideal.processor_state Job)
earlier_deadline
job_deadline j2 <= job_deadline j
have TRANS: transitive earlier_deadline
by rewrite /earlier_deadline => s1 s2 s3; apply leq_trans.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2 : Job SCHED_j2 : scheduled_at sched j2
(find_swap_candidate sched t1 j1) j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 SCHED_j : scheduled_at sched j t ARR_j : job_arrival j <= t1 TOTAL : total (T:=ideal.processor_state Job)
earlier_deadline TRANS : transitive (T:=ideal.processor_state Job)
earlier_deadline
job_deadline j2 <= job_deadline j
have REFL: reflexive earlier_deadline
by rewrite /earlier_deadline => s; apply leqnn.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2 : Job SCHED_j2 : scheduled_at sched j2
(find_swap_candidate sched t1 j1) j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 SCHED_j : scheduled_at sched j t ARR_j : job_arrival j <= t1 TOTAL : total (T:=ideal.processor_state Job)
earlier_deadline TRANS : transitive (T:=ideal.processor_state Job)
earlier_deadline REFL : reflexive (T:=ideal.processor_state Job)
earlier_deadline
job_deadline j2 <= job_deadline j
move : SCHED_j SCHED_j2.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2, j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 ARR_j : job_arrival j <= t1 TOTAL : total (T:=ideal.processor_state Job)
earlier_deadline TRANS : transitive (T:=ideal.processor_state Job)
earlier_deadline REFL : reflexive (T:=ideal.processor_state Job)
earlier_deadline
scheduled_at sched j t ->
scheduled_at sched j2
(find_swap_candidate sched t1 j1) ->
job_deadline j2 <= job_deadline j
rewrite !scheduled_at_def => /eqP SCHED_j /eqP SCHED_j2.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2, j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 ARR_j : job_arrival j <= t1 TOTAL : total (T:=ideal.processor_state Job)
earlier_deadline TRANS : transitive (T:=ideal.processor_state Job)
earlier_deadline REFL : reflexive (T:=ideal.processor_state Job)
earlier_deadline SCHED_j : sched t = Some j SCHED_j2 : sched (find_swap_candidate sched t1 j1) =
Some j2
job_deadline j2 <= job_deadline j
have ED: earlier_deadline (sched (find_swap_candidate sched t1 j1)) (sched t).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2, j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 ARR_j : job_arrival j <= t1 TOTAL : total (T:=ideal.processor_state Job)
earlier_deadline TRANS : transitive (T:=ideal.processor_state Job)
earlier_deadline REFL : reflexive (T:=ideal.processor_state Job)
earlier_deadline SCHED_j : sched t = Some j SCHED_j2 : sched (find_swap_candidate sched t1 j1) =
Some j2
earlier_deadline
(sched (find_swap_candidate sched t1 j1)) (sched t)
{ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2, j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 ARR_j : job_arrival j <= t1 TOTAL : total (T:=ideal.processor_state Job)
earlier_deadline TRANS : transitive (T:=ideal.processor_state Job)
earlier_deadline REFL : reflexive (T:=ideal.processor_state Job)
earlier_deadline SCHED_j : sched t = Some j SCHED_j2 : sched (find_swap_candidate sched t1 j1) =
Some j2
earlier_deadline
(sched (find_swap_candidate sched t1 j1)) (sched t)
move : (search_arg_extremum _ _ _ REFL TRANS TOTAL _ _ _ fsc_search_result) => MIN.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2, j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 ARR_j : job_arrival j <= t1 TOTAL : total (T:=ideal.processor_state Job)
earlier_deadline TRANS : transitive (T:=ideal.processor_state Job)
earlier_deadline REFL : reflexive (T:=ideal.processor_state Job)
earlier_deadline SCHED_j : sched t = Some j SCHED_j2 : sched (find_swap_candidate sched t1 j1) =
Some j2 MIN : forall y : nat,
t1 <= y < job_deadline j1 ->
relevant_pstate t1 (sched y) ->
earlier_deadline
(sched (find_swap_candidate sched t1 j1))
(sched y)
earlier_deadline
(sched (find_swap_candidate sched t1 j1)) (sched t)
apply (MIN t).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2, j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 ARR_j : job_arrival j <= t1 TOTAL : total (T:=ideal.processor_state Job)
earlier_deadline TRANS : transitive (T:=ideal.processor_state Job)
earlier_deadline REFL : reflexive (T:=ideal.processor_state Job)
earlier_deadline SCHED_j : sched t = Some j SCHED_j2 : sched (find_swap_candidate sched t1 j1) =
Some j2 MIN : forall y : nat,
t1 <= y < job_deadline j1 ->
relevant_pstate t1 (sched y) ->
earlier_deadline
(sched (find_swap_candidate sched t1 j1))
(sched y)
t1 <= t < job_deadline j1
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2, j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 ARR_j : job_arrival j <= t1 TOTAL : total (T:=ideal.processor_state Job)
earlier_deadline TRANS : transitive (T:=ideal.processor_state Job)
earlier_deadline REFL : reflexive (T:=ideal.processor_state Job)
earlier_deadline SCHED_j : sched t = Some j SCHED_j2 : sched (find_swap_candidate sched t1 j1) =
Some j2 MIN : forall y : nat,
t1 <= y < job_deadline j1 ->
relevant_pstate t1 (sched y) ->
earlier_deadline
(sched (find_swap_candidate sched t1 j1))
(sched y)
t1 <= t < job_deadline j1
by apply /andP; split .
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2, j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 ARR_j : job_arrival j <= t1 TOTAL : total (T:=ideal.processor_state Job)
earlier_deadline TRANS : transitive (T:=ideal.processor_state Job)
earlier_deadline REFL : reflexive (T:=ideal.processor_state Job)
earlier_deadline SCHED_j : sched t = Some j SCHED_j2 : sched (find_swap_candidate sched t1 j1) =
Some j2 MIN : forall y : nat,
t1 <= y < job_deadline j1 ->
relevant_pstate t1 (sched y) ->
earlier_deadline
(sched (find_swap_candidate sched t1 j1))
(sched y)
relevant_pstate t1 (sched t)
by rewrite /relevant_pstate SCHED_j.
} Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2, j : Job t : nat t1_le_t : t1 <= t t_lt_dl1 : t < job_deadline j1 ARR_j : job_arrival j <= t1 TOTAL : total (T:=ideal.processor_state Job)
earlier_deadline TRANS : transitive (T:=ideal.processor_state Job)
earlier_deadline REFL : reflexive (T:=ideal.processor_state Job)
earlier_deadline SCHED_j : sched t = Some j SCHED_j2 : sched (find_swap_candidate sched t1 j1) =
Some j2 ED : earlier_deadline
(sched (find_swap_candidate sched t1 j1))
(sched t)
job_deadline j2 <= job_deadline j
now move : ED; rewrite /earlier_deadline /oapp SCHED_j SCHED_j2.
Qed .
(** As a special case of the above lemma, we observe that the job
scheduled at the time given by [find_swap_candidate] in
particular has a deadline no later than the job scheduled at time
[t1]. *)
Corollary fsc_no_later_deadline :
forall j2 ,
scheduled_at sched j2 (find_swap_candidate sched t1 j1) ->
job_deadline j2 <= job_deadline j1.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
forall j2 : Job,
scheduled_at sched j2
(find_swap_candidate sched t1 j1) ->
job_deadline j2 <= job_deadline j1
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1
forall j2 : Job,
scheduled_at sched j2
(find_swap_candidate sched t1 j1) ->
job_deadline j2 <= job_deadline j1
move => j2 SCHED_j2.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2 : Job SCHED_j2 : scheduled_at sched j2
(find_swap_candidate sched t1 j1)
job_deadline j2 <= job_deadline j1
apply fsc_found_job_deadline with (t := t1) => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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 j1 : Job t1 : instant H_not_idle : scheduled_at sched j1 t1 H_deadline_not_missed : t1 < job_deadline j1 j2 : Job SCHED_j2 : scheduled_at sched j2
(find_swap_candidate sched t1 j1)
t1 <= t1 < job_deadline j1
by apply /andP; split .
Qed .
End FindSwapCandidateFacts .
(** In the next section, we analyze properties of [make_edf_at], which
we abbreviate as "[mea]" in the following. *)
Section MakeEDFAtFacts .
(** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(** ...consider an ideal uniprocessor schedule... *)
Variable sched : schedule (ideal.processor_state Job).
(** ...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.
(** ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses : all_deadlines_met sched.
(** Since we will require this fact repeatedly, we briefly observe
that, since no scheduled job misses its deadline, if a job is
scheduled at some time [t], then its deadline is later than
[t]. *)
Fact scheduled_job_in_sched_has_later_deadline :
forall j t ,
scheduled_at sched j t ->
job_deadline j > t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched
forall (j : Job) (t : instant),
scheduled_at sched j t -> t < job_deadline j
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched
forall (j : Job) (t : instant),
scheduled_at sched j t -> t < job_deadline j
by move => j t SCHED; apply : (scheduled_at_implies_later_deadline sched).
Qed .
(** We analyze [make_edf_at] applied to an arbitrary point in time,
which we denote [t_edf] in the following. *)
Variable t_edf : instant.
(** For brevity, let [sched'] denote the schedule obtained from
[make_edf_at] applied to [sched] at time [t_edf]. *)
Let sched' := make_edf_at sched t_edf.
(** First, we observe that in [sched'] jobs still don't execute past
completion. *)
Lemma mea_completed_jobs :
completed_jobs_dont_execute sched'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
completed_jobs_dont_execute sched'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
completed_jobs_dont_execute sched'
have IDEAL := @ideal_proc_model_ensures_ideal_progress Job.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) IDEAL : ideal_progress_proc_model
(ideal.processor_state Job)
completed_jobs_dont_execute sched'
have UNIT := @ideal_proc_model_provides_unit_service Job.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) IDEAL : ideal_progress_proc_model
(ideal.processor_state Job) UNIT : unit_service_proc_model
(ideal.processor_state Job)
completed_jobs_dont_execute sched'
rewrite /sched' /make_edf_at.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) IDEAL : ideal_progress_proc_model
(ideal.processor_state Job) UNIT : unit_service_proc_model
(ideal.processor_state Job)
completed_jobs_dont_execute
match sched t_edf with
| Some j =>
swapped sched t_edf
(find_swap_candidate sched t_edf j)
| None => sched
end
destruct (sched t_edf) as [j_orig|] eqn :SCHED => [|//].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) IDEAL : ideal_progress_proc_model
(ideal.processor_state Job) UNIT : unit_service_proc_model
(ideal.processor_state Job) j_orig : Job SCHED : sched t_edf = Some j_orig
completed_jobs_dont_execute
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig))
have SCHED': scheduled_at sched j_orig t_edf
by rewrite scheduled_at_def; apply /eqP.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) IDEAL : ideal_progress_proc_model
(ideal.processor_state Job) UNIT : unit_service_proc_model
(ideal.processor_state Job) j_orig : Job SCHED : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf
completed_jobs_dont_execute
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig))
apply swapped_completed_jobs_dont_execute => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) IDEAL : ideal_progress_proc_model
(ideal.processor_state Job) UNIT : unit_service_proc_model
(ideal.processor_state Job) j_orig : Job SCHED : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf
t_edf <= find_swap_candidate sched t_edf j_orig
apply fsc_range1 => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) IDEAL : ideal_progress_proc_model
(ideal.processor_state Job) UNIT : unit_service_proc_model
(ideal.processor_state Job) j_orig : Job SCHED : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf
t_edf < job_deadline j_orig
now apply scheduled_job_in_sched_has_later_deadline.
Qed .
(** Importantly, [make_edf_at] does not introduce any deadline
misses, which is a crucial step in the EDF optimality
argument. *)
Lemma mea_no_deadline_misses :
all_deadlines_met sched'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
all_deadlines_met sched'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
all_deadlines_met sched'
move => j t SCHED.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t
job_meets_deadline sched' j
rewrite /sched' /make_edf_at.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t
job_meets_deadline
match sched t_edf with
| Some j =>
swapped sched t_edf
(find_swap_candidate sched t_edf j)
| None => sched
end j
destruct (sched t_edf) as [j_orig|] eqn :SCHED_orig; last first .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t SCHED_orig : sched t_edf = None
job_meets_deadline sched j
{ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t SCHED_orig : sched t_edf = None
job_meets_deadline sched j
apply (H_no_deadline_misses _ t).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t SCHED_orig : sched t_edf = None
scheduled_at sched j t
move : SCHED.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED_orig : sched t_edf = None
scheduled_at sched' j t -> scheduled_at sched j t
now rewrite /sched' /make_edf_at SCHED_orig.
} Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig
job_meets_deadline
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j
{ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig
job_meets_deadline
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j
have SCHED': scheduled_at sched j_orig t_edf
by rewrite scheduled_at_def; apply /eqP.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf
job_meets_deadline
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j
move : (scheduled_job_in_sched_has_later_deadline _ _ SCHED') => DL_orig.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig
job_meets_deadline
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j
apply edf_swap_no_deadline_misses_introduced => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig
t_edf <= find_swap_candidate sched t_edf j_orig
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig
t_edf <= find_swap_candidate sched t_edf j_orig
by apply fsc_range1 => //.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig
forall j1 j2 : Job,
scheduled_at sched j1 t_edf ->
scheduled_at sched j2
(find_swap_candidate sched t_edf j_orig) ->
job_deadline j2 <= job_deadline j1
move => j1 j2 SCHED_j1 SCHED_j2.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig j1, j2 : Job SCHED_j1 : scheduled_at sched j1 t_edf SCHED_j2 : scheduled_at sched j2
(find_swap_candidate sched t_edf j_orig)
job_deadline j2 <= job_deadline j1
apply : (fsc_found_job_deadline sched _ j_orig t_edf _ _ _ _ _ t_edf) => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig j1, j2 : Job SCHED_j1 : scheduled_at sched j1 t_edf SCHED_j2 : scheduled_at sched j2
(find_swap_candidate sched t_edf j_orig)
t_edf <= t_edf < job_deadline j_orig
by apply /andP; split .
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig
forall j1 : Job,
scheduled_at sched j1 t_edf ->
exists j2 : Job,
scheduled_at sched j2
(find_swap_candidate sched t_edf j_orig) /\
find_swap_candidate sched t_edf j_orig <
job_deadline j2
move => j1 SCHED_j1.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig j1 : Job SCHED_j1 : scheduled_at sched j1 t_edf
exists j2 : Job,
scheduled_at sched j2
(find_swap_candidate sched t_edf j_orig) /\
find_swap_candidate sched t_edf j_orig <
job_deadline j2
move : (fsc_not_idle sched H_jobs_must_arrive_to_execute j_orig t_edf SCHED' DL_orig) => [j' [SCHED_j' ARR_j']].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig j1 : Job SCHED_j1 : scheduled_at sched j1 t_edf j' : Job SCHED_j' : scheduled_at sched j'
(find_swap_candidate sched t_edf j_orig) ARR_j' : job_arrival j' <= t_edf
exists j2 : Job,
scheduled_at sched j2
(find_swap_candidate sched t_edf j_orig) /\
find_swap_candidate sched t_edf j_orig <
job_deadline j2
exists j' .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig j1 : Job SCHED_j1 : scheduled_at sched j1 t_edf j' : Job SCHED_j' : scheduled_at sched j'
(find_swap_candidate sched t_edf j_orig) ARR_j' : job_arrival j' <= t_edf
scheduled_at sched j'
(find_swap_candidate sched t_edf j_orig) /\
find_swap_candidate sched t_edf j_orig <
job_deadline j'
split => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig j1 : Job SCHED_j1 : scheduled_at sched j1 t_edf j' : Job SCHED_j' : scheduled_at sched j'
(find_swap_candidate sched t_edf j_orig) ARR_j' : job_arrival j' <= t_edf
find_swap_candidate sched t_edf j_orig <
job_deadline j'
now apply scheduled_job_in_sched_has_later_deadline.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig
job_meets_deadline sched j
have EX: (exists t' , scheduled_at sched j t').Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig
exists t' : instant, scheduled_at sched j t'
{ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig
exists t' : instant, scheduled_at sched j t'
apply swap_job_scheduled with (t1 := t_edf) (t2 := find_swap_candidate sched t_edf j_orig) (t := t).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j t
now move : SCHED; rewrite /sched' /make_edf_at SCHED_orig.
} Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig EX : exists t' : instant, scheduled_at sched j t'
job_meets_deadline sched j
move : EX => [t' SCHED_t'].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig t' : instant SCHED_t' : scheduled_at sched j t'
job_meets_deadline sched j
now apply H_no_deadline_misses with (t := t').
}
Qed .
(** As a result, we may conclude that any job scheduled at a time t has a deadline later than t. *)
Corollary mea_scheduled_job_has_later_deadline :
forall j t ,
scheduled_at sched' j t ->
job_deadline j > t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at sched' j t -> t < job_deadline j
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at sched' j t -> t < job_deadline j
move => j t SCHED.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t
t < job_deadline j
apply (scheduled_at_implies_later_deadline sched') => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t
completed_jobs_dont_execute sched'
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t
completed_jobs_dont_execute sched'
by apply mea_completed_jobs.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t
job_meets_deadline sched' j
by apply mea_no_deadline_misses with (t := t).
Qed .
(** Next comes a big step in the optimality proof: we observe that
[make_edf_at] indeed ensures that [EDF_at] holds at time [t_edf] in
[sched']. As this is a larger argument, we proceed by case analysis and
first establish a couple of helper lemmas in the following section. *)
Section GuaranteeCaseAnalysis .
(** Let [j_orig] denote the job scheduled in [sched] at time
[t_edf], let [j_edf] denote the job scheduled in [sched'] at
time [t_edf], and let [j'] denote any job scheduled in
[sched'] at some time [t'] after [t_edf]... *)
Variable j_orig j_edf j' : Job.
Variable t' : instant.
Hypothesis H_t_edf_le_t' : t_edf <= t'.
Hypothesis H_sched_orig : scheduled_at sched j_orig t_edf.
Hypothesis H_sched_edf : scheduled_at sched' j_edf t_edf.
Hypothesis H_sched' : scheduled_at sched' j' t'.
(** ... and that arrives before time [t_edf]. *)
Hypothesis H_arrival_j' : job_arrival j' <= t_edf.
(** We begin by observing three simple facts that will be used repeatedly in
the case analysis. *)
(** First, the deadline of [j_orig] is later than [t_edf]. *)
Fact mea_guarantee_dl_orig : t_edf < job_deadline j_orig.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
t_edf < job_deadline j_orig
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
t_edf < job_deadline j_orig
by apply (scheduled_job_in_sched_has_later_deadline j_orig t_edf H_sched_orig). Qed .
(** Second, by the definition of [sched'], [j_edf] is scheduled in
[sched] at the time returned by [find_swap_candidate]. *)
Fact mea_guarantee_fsc_is_j_edf : sched (find_swap_candidate sched t_edf j_orig) = Some j_edf.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
move : (H_sched_orig).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
scheduled_at sched j_orig t_edf ->
sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
rewrite scheduled_at_def => /eqP SCHED.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig
sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
move : (H_sched_edf).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig
scheduled_at sched' j_edf t_edf ->
sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
rewrite /sched' /make_edf_at /swapped /replace_at {1 }SCHED //=.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig
scheduled_at
(fun t : instant =>
if find_swap_candidate sched t_edf j_orig == t
then sched t_edf
else
if t_edf == t
then
sched (find_swap_candidate sched t_edf j_orig)
else sched t) j_edf t_edf ->
sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
rewrite scheduled_at_def.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig
(if find_swap_candidate sched t_edf j_orig == t_edf
then sched t_edf
else
if t_edf == t_edf
then sched (find_swap_candidate sched t_edf j_orig)
else sched t_edf) == Some j_edf ->
sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
destruct (find_swap_candidate sched t_edf j_orig == t_edf) eqn :FSC.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig FSC : (find_swap_candidate sched t_edf j_orig == t_edf) =
true
sched t_edf == Some j_edf ->
sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig FSC : (find_swap_candidate sched t_edf j_orig == t_edf) =
true
sched t_edf == Some j_edf ->
sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
by move : FSC => /eqP -> /eqP.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig FSC : (find_swap_candidate sched t_edf j_orig == t_edf) =
false
(if t_edf == t_edf
then sched (find_swap_candidate sched t_edf j_orig)
else sched t_edf) == Some j_edf ->
sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
by rewrite ifT // => /eqP.
Qed .
(** Third, the deadline of [j_edf] is no later than the deadline
of [j_orig]. *)
Fact mea_guarantee_deadlines : job_deadline j_edf <= job_deadline j_orig.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
job_deadline j_edf <= job_deadline j_orig
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
job_deadline j_edf <= job_deadline j_orig
apply : (fsc_no_later_deadline sched _ _ t_edf) => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
t_edf < job_deadline j_orig
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
t_edf < job_deadline j_orig
by exact mea_guarantee_dl_orig.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
scheduled_at sched j_edf
(find_swap_candidate sched t_edf j_orig)
by rewrite scheduled_at_def mea_guarantee_fsc_is_j_edf //=.
Qed .
(** With the setup in place, we are now ready to begin the case analysis. *)
(** First, we consider the simpler case where [t'] is no earlier
than the deadline of [j_orig]. This case is simpler because
[t'] being no earlier than [j_orig]'s deadline implies that
[j'] has deadline no earlier than [j_orig] (since no scheduled
job in [sched] misses a deadline), which in turn has a
deadline no earlier than [j_edf]. *)
Lemma mea_guarantee_case_t'_past_deadline :
job_deadline j_orig <= t' ->
job_deadline j_edf <= job_deadline j'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
job_deadline j_orig <= t' ->
job_deadline j_edf <= job_deadline j'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
job_deadline j_orig <= t' ->
job_deadline j_edf <= job_deadline j'
move : (mea_scheduled_job_has_later_deadline j' t' H_sched') => DL_j' BOUND_t'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf DL_j' : t' < job_deadline j' BOUND_t' : job_deadline j_orig <= t'
job_deadline j_edf <= job_deadline j'
apply leq_trans with (n := job_deadline j_orig) => // ;
first by exact mea_guarantee_deadlines.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf DL_j' : t' < job_deadline j' BOUND_t' : job_deadline j_orig <= t'
job_deadline j_orig <= job_deadline j'
by apply leq_trans with (n := t').
Qed .
(** Next, we consider the more difficult case, where [t'] is
before the deadline of [j_orig]. *)
Lemma mea_guarantee_case_t'_before_deadline :
t' < job_deadline j_orig ->
job_deadline j_edf <= job_deadline j'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
t' < job_deadline j_orig ->
job_deadline j_edf <= job_deadline j'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
t' < job_deadline j_orig ->
job_deadline j_edf <= job_deadline j'
move : (H_sched_orig).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
scheduled_at sched j_orig t_edf ->
t' < job_deadline j_orig ->
job_deadline j_edf <= job_deadline j'
rewrite scheduled_at_def => /eqP SCHED BOUND_t'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig
job_deadline j_edf <= job_deadline j'
move : (mea_guarantee_fsc_is_j_edf) => FSC.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
job_deadline j_edf <= job_deadline j'
have EX: (exists x , scheduled_at sched j' x /\ t_edf <= x < job_deadline j_orig).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
exists x : instant,
scheduled_at sched j' x /\
t_edf <= x < job_deadline j_orig
{ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf
exists x : instant,
scheduled_at sched j' x /\
t_edf <= x < job_deadline j_orig
case : (boolP(t_edf == t')) => [/eqP EQ| /eqP NEQ].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf EQ : t_edf = t'
exists x : instant,
scheduled_at sched j' x /\
t_edf <= x < job_deadline j_orig
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf EQ : t_edf = t'
exists x : instant,
scheduled_at sched j' x /\
t_edf <= x < job_deadline j_orig
exists (find_swap_candidate sched t_edf j_orig ).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf EQ : t_edf = t'
scheduled_at sched j'
(find_swap_candidate sched t_edf j_orig) /\
t_edf <= find_swap_candidate sched t_edf j_orig <
job_deadline j_orig
split ; last by apply fsc_range => //; exact mea_guarantee_dl_orig.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf EQ : t_edf = t'
scheduled_at sched j'
(find_swap_candidate sched t_edf j_orig)
subst .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t' : instant j_orig : Job SCHED : sched t' = Some j_orig j' : Job H_arrival_j' : job_arrival j' <= t' sched' := make_edf_at sched t' : schedule (ideal.processor_state Job) H_sched' : scheduled_at sched' j' t' j_edf : Job H_sched_edf : scheduled_at sched' j_edf t' H_sched_orig : scheduled_at sched j_orig t' H_t_edf_le_t' : t' <= t' BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t' j_orig) =
Some j_edf
scheduled_at sched j'
(find_swap_candidate sched t' j_orig)
rewrite -(ideal_proc_model_is_a_uniprocessor_model _ _ _ _ H_sched_edf H_sched').Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t' : instant j_orig : Job SCHED : sched t' = Some j_orig j' : Job H_arrival_j' : job_arrival j' <= t' sched' := make_edf_at sched t' : schedule (ideal.processor_state Job) H_sched' : scheduled_at sched' j' t' j_edf : Job H_sched_edf : scheduled_at sched' j_edf t' H_sched_orig : scheduled_at sched j_orig t' H_t_edf_le_t' : t' <= t' BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t' j_orig) =
Some j_edf
scheduled_at sched j_edf
(find_swap_candidate sched t' j_orig)
now rewrite scheduled_at_def FSC //=.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf <> t'
exists x : instant,
scheduled_at sched j' x /\
t_edf <= x < job_deadline j_orig
case : (boolP(find_swap_candidate sched t_edf j_orig == t')) => [/eqP EQ' | /eqP NEQ'].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf <> t' EQ' : find_swap_candidate sched t_edf j_orig = t'
exists x : instant,
scheduled_at sched j' x /\
t_edf <= x < job_deadline j_orig
+ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf <> t' EQ' : find_swap_candidate sched t_edf j_orig = t'
exists x : instant,
scheduled_at sched j' x /\
t_edf <= x < job_deadline j_orig
exists t_edf .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf <> t' EQ' : find_swap_candidate sched t_edf j_orig = t'
scheduled_at sched j' t_edf /\
t_edf <= t_edf < job_deadline j_orig
split ; last by apply /andP; split => //; exact mea_guarantee_dl_orig.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf <> t' EQ' : find_swap_candidate sched t_edf j_orig = t'
scheduled_at sched j' t_edf
rewrite -(swap_job_scheduled_t2 _ _ (find_swap_candidate sched t_edf j_orig) _).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf <> t' EQ' : find_swap_candidate sched t_edf j_orig = t'
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j'
(find_swap_candidate sched t_edf j_orig)
move : H_sched'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf <> t' EQ' : find_swap_candidate sched t_edf j_orig = t'
scheduled_at sched' j' t' ->
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j'
(find_swap_candidate sched t_edf j_orig)
rewrite /sched' /make_edf_at SCHED.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf <> t' EQ' : find_swap_candidate sched t_edf j_orig = t'
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j' t' ->
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j'
(find_swap_candidate sched t_edf j_orig)
now rewrite EQ'.
+ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf <> t' NEQ' : find_swap_candidate sched t_edf j_orig <> t'
exists x : instant,
scheduled_at sched j' x /\
t_edf <= x < job_deadline j_orig
move : NEQ NEQ' => /eqP NEQ /eqP NEQ'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf != t' NEQ' : find_swap_candidate sched t_edf j_orig != t'
exists x : instant,
scheduled_at sched j' x /\
t_edf <= x < job_deadline j_orig
exists t' .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf != t' NEQ' : find_swap_candidate sched t_edf j_orig != t'
scheduled_at sched j' t' /\
t_edf <= t' < job_deadline j_orig
split ; last by apply /andP; split .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf != t' NEQ' : find_swap_candidate sched t_edf j_orig != t'
scheduled_at sched j' t'
rewrite -(swap_job_scheduled_other_times _ t_edf (find_swap_candidate sched t_edf j_orig)) //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf != t' NEQ' : find_swap_candidate sched t_edf j_orig != t'
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j' t'
move : H_sched'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf NEQ : t_edf != t' NEQ' : find_swap_candidate sched t_edf j_orig != t'
scheduled_at sched' j' t' ->
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j' t'
now rewrite /sched' /make_edf_at SCHED.
} Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf EX : exists x : instant,
scheduled_at sched j' x /\
t_edf <= x < job_deadline j_orig
job_deadline j_edf <= job_deadline j'
move : EX => [t'' [SCHED'' RANGE]].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf t'' : instant SCHED'' : scheduled_at sched j' t'' RANGE : t_edf <= t'' < job_deadline j_orig
job_deadline j_edf <= job_deadline j'
apply : (fsc_found_job_deadline sched _ j_orig t_edf _ _ _ _ _ t'') => // ;
first by exact mea_guarantee_dl_orig.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_orig, j_edf, j' : Job t' : instant H_t_edf_le_t' : t_edf <= t' H_sched_orig : scheduled_at sched j_orig t_edf H_sched_edf : scheduled_at sched' j_edf t_edf H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf SCHED : sched t_edf = Some j_orig BOUND_t' : t' < job_deadline j_orig FSC : sched (find_swap_candidate sched t_edf j_orig) =
Some j_edf t'' : instant SCHED'' : scheduled_at sched j' t'' RANGE : t_edf <= t'' < job_deadline j_orig
scheduled_at sched j_edf
(find_swap_candidate sched t_edf j_orig)
now rewrite scheduled_at_def FSC //=.
Qed .
End GuaranteeCaseAnalysis .
(** Finally, putting the preceding cases together, we obtain the
result that [make_edf_at] establishes [EDF_at] at time
[t_edf]. *)
Lemma make_edf_at_guarantee :
EDF_at sched' t_edf.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
EDF_at sched' t_edf
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
EDF_at sched' t_edf
move => j_edf H_sched_edf t' j' t_edf_le_t' H_sched' H_arrival_j'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_edf : Job H_sched_edf : scheduled_at sched' j_edf t_edf t' : instant j' : Job t_edf_le_t' : t_edf <= t' H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf
job_deadline j_edf <= job_deadline j'
destruct (sched t_edf) as [j_orig|] eqn :SCHED;
last by move : (H_sched_edf); rewrite /sched' /make_edf_at scheduled_at_def => /eqP; rewrite !SCHED.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_edf : Job H_sched_edf : scheduled_at sched' j_edf t_edf t' : instant j' : Job t_edf_le_t' : t_edf <= t' H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf j_orig : Job SCHED : sched t_edf = Some j_orig
job_deadline j_edf <= job_deadline j'
have H_sched: scheduled_at sched j_orig t_edf
by rewrite scheduled_at_def; apply /eqP.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_edf : Job H_sched_edf : scheduled_at sched' j_edf t_edf t' : instant j' : Job t_edf_le_t' : t_edf <= t' H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf j_orig : Job SCHED : sched t_edf = Some j_orig H_sched : scheduled_at sched j_orig t_edf
job_deadline j_edf <= job_deadline j'
case : (boolP (t' < job_deadline j_orig)).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_edf : Job H_sched_edf : scheduled_at sched' j_edf t_edf t' : instant j' : Job t_edf_le_t' : t_edf <= t' H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf j_orig : Job SCHED : sched t_edf = Some j_orig H_sched : scheduled_at sched j_orig t_edf
t' < job_deadline j_orig ->
job_deadline j_edf <= job_deadline j'
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_edf : Job H_sched_edf : scheduled_at sched' j_edf t_edf t' : instant j' : Job t_edf_le_t' : t_edf <= t' H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf j_orig : Job SCHED : sched t_edf = Some j_orig H_sched : scheduled_at sched j_orig t_edf
t' < job_deadline j_orig ->
job_deadline j_edf <= job_deadline j'
by apply mea_guarantee_case_t'_before_deadline.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_edf : Job H_sched_edf : scheduled_at sched' j_edf t_edf t' : instant j' : Job t_edf_le_t' : t_edf <= t' H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf j_orig : Job SCHED : sched t_edf = Some j_orig H_sched : scheduled_at sched j_orig t_edf
~~ (t' < job_deadline j_orig) ->
job_deadline j_edf <= job_deadline j'
rewrite -leqNgt => BOUND_t'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j_edf : Job H_sched_edf : scheduled_at sched' j_edf t_edf t' : instant j' : Job t_edf_le_t' : t_edf <= t' H_sched' : scheduled_at sched' j' t' H_arrival_j' : job_arrival j' <= t_edf j_orig : Job SCHED : sched t_edf = Some j_orig H_sched : scheduled_at sched j_orig t_edf BOUND_t' : job_deadline j_orig <= t'
job_deadline j_edf <= job_deadline j'
now apply : (mea_guarantee_case_t'_past_deadline j_orig j_edf j' t').
Qed .
(** We observe that [make_edf_at] maintains the property that jobs
must arrive to execute. *)
Lemma mea_jobs_must_arrive :
jobs_must_arrive_to_execute sched'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
jobs_must_arrive_to_execute sched'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
jobs_must_arrive_to_execute sched'
move => j t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant
scheduled_at sched' j t -> has_arrived j t
rewrite /has_arrived /sched' /make_edf_at.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant
scheduled_at
match sched t_edf with
| Some j =>
swapped sched t_edf
(find_swap_candidate sched t_edf j)
| None => sched
end j t -> job_arrival j <= t
destruct (sched t_edf) as [j_orig|] eqn :SCHED_orig;
last by move => SCHED; by apply H_jobs_must_arrive_to_execute.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j t ->
job_arrival j <= t
have SCHED': scheduled_at sched j_orig t_edf
by rewrite scheduled_at_def; apply /eqP.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j t ->
job_arrival j <= t
move : (scheduled_job_in_sched_has_later_deadline j_orig t_edf SCHED') => DL_orig.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j t ->
job_arrival j <= t
rewrite scheduled_at_def /swapped /replace_at.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig
(if find_swap_candidate sched t_edf j_orig == t
then sched t_edf
else
if t_edf == t
then sched (find_swap_candidate sched t_edf j_orig)
else sched t) == Some j -> job_arrival j <= t
case : (boolP((find_swap_candidate sched t_edf j_orig) == t)) => [/eqP EQ| /eqP NEQ].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig EQ : find_swap_candidate sched t_edf j_orig = t
sched t_edf == Some j -> job_arrival j <= t
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig EQ : find_swap_candidate sched t_edf j_orig = t
sched t_edf == Some j -> job_arrival j <= t
rewrite SCHED_orig => /eqP j_is_orig.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig EQ : find_swap_candidate sched t_edf j_orig = t j_is_orig : Some j_orig = Some j
job_arrival j <= t
injection j_is_orig => <-.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig EQ : find_swap_candidate sched t_edf j_orig = t j_is_orig : Some j_orig = Some j
job_arrival j_orig <= t
apply leq_trans with (n := t_edf).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig EQ : find_swap_candidate sched t_edf j_orig = t j_is_orig : Some j_orig = Some j
job_arrival j_orig <= t_edf
+ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig EQ : find_swap_candidate sched t_edf j_orig = t j_is_orig : Some j_orig = Some j
job_arrival j_orig <= t_edf
by apply H_jobs_must_arrive_to_execute.
+ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig EQ : find_swap_candidate sched t_edf j_orig = t j_is_orig : Some j_orig = Some j
t_edf <= t
by rewrite -EQ; apply fsc_range1.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig NEQ : find_swap_candidate sched t_edf j_orig <> t
(if t_edf == t
then sched (find_swap_candidate sched t_edf j_orig)
else sched t) == Some j -> job_arrival j <= t
case (boolP(t_edf == t)) => [/eqP EQ'| /eqP NEQ'].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig NEQ : find_swap_candidate sched t_edf j_orig <> t EQ' : t_edf = t
sched (find_swap_candidate sched t_edf j_orig) ==
Some j -> job_arrival j <= t
+ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig NEQ : find_swap_candidate sched t_edf j_orig <> t EQ' : t_edf = t
sched (find_swap_candidate sched t_edf j_orig) ==
Some j -> job_arrival j <= t
move => SCHED_j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig NEQ : find_swap_candidate sched t_edf j_orig <> t EQ' : t_edf = t SCHED_j : sched
(find_swap_candidate sched t_edf j_orig) ==
Some j
job_arrival j <= t
have ARR_j: job_arrival j <= t_edf by apply fsc_found_job_arrival with (sched := sched) (j1 := j_orig) => //; rewrite scheduled_at_def.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig NEQ : find_swap_candidate sched t_edf j_orig <> t EQ' : t_edf = t SCHED_j : sched
(find_swap_candidate sched t_edf j_orig) ==
Some j ARR_j : job_arrival j <= t_edf
job_arrival j <= t
now rewrite -EQ'.
+ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig NEQ : find_swap_candidate sched t_edf j_orig <> t NEQ' : t_edf <> t
sched t == Some j -> job_arrival j <= t
move => SCHED_j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED' : scheduled_at sched j_orig t_edf DL_orig : t_edf < job_deadline j_orig NEQ : find_swap_candidate sched t_edf j_orig <> t NEQ' : t_edf <> t SCHED_j : sched t == Some j
job_arrival j <= t
by apply H_jobs_must_arrive_to_execute; rewrite scheduled_at_def.
Qed .
(** We connect the fact that a job is scheduled in [sched'] to the
fact that it must be scheduled somewhere in [sched], too, since
[make_edf_at] does not introduce any new jobs. *)
Lemma mea_job_scheduled :
forall j t ,
scheduled_at sched' j t ->
exists t' , scheduled_at sched j t'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at sched' j t ->
exists t' : instant, scheduled_at sched j t'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at sched' j t ->
exists t' : instant, scheduled_at sched j t'
rewrite /sched' /make_edf_at.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at
match sched t_edf with
| Some j0 =>
swapped sched t_edf
(find_swap_candidate sched t_edf j0)
| None => sched
end j t ->
exists t' : instant, scheduled_at sched j t'
move => j t SCHED_j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED_j : scheduled_at
match sched t_edf with
| Some j =>
swapped sched t_edf
(find_swap_candidate sched t_edf j)
| None => sched
end j t
exists t' : instant, scheduled_at sched j t'
destruct (sched t_edf) as [j_orig|] eqn :SCHED_orig; last by exists t .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED_j : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig))
j t
exists t' : instant, scheduled_at sched j t'
eapply swap_job_scheduled.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant j_orig : Job SCHED_orig : sched t_edf = Some j_orig SCHED_j : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig))
j t
scheduled_at (swapped sched ?t1 ?t2 ) j ?t
now exact SCHED_j.
Qed .
(** Conversely, if a job is scheduled in [sched], it is also
scheduled somewhere in [sched'] since [make_edf_at] does not lose
any jobs. *)
Lemma mea_job_scheduled' :
forall j t ,
scheduled_at sched j t ->
exists t' , scheduled_at sched' j t'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at sched j t ->
exists t' : instant, scheduled_at sched' j t'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at sched j t ->
exists t' : instant, scheduled_at sched' j t'
move => j t SCHED_j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED_j : scheduled_at sched j t
exists t' : instant, scheduled_at sched' j t'
rewrite /sched' /make_edf_at.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED_j : scheduled_at sched j t
exists t' : instant,
scheduled_at
match sched t_edf with
| Some j =>
swapped sched t_edf
(find_swap_candidate sched t_edf j)
| None => sched
end j t'
destruct (sched t_edf) as [j_orig|] eqn :SCHED_orig;
last by exists t .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED_j : scheduled_at sched j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig
exists t' : instant,
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j t'
eapply swap_job_scheduled_original.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) j : Job t : instant SCHED_j : scheduled_at sched j t j_orig : Job SCHED_orig : sched t_edf = Some j_orig
scheduled_at sched j ?t
now exact SCHED_j.
Qed .
(** Next, we observe that if all jobs in [sched] come from a given
arrival sequence, then that's still the case in [sched'], too. *)
Section ArrivalSequence .
(** For given arrival sequence,... *)
Variable arr_seq : arrival_sequence Job.
(** ...if all jobs in [sched] come from the arrival sequence,... *)
Hypothesis H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq.
(** ...then all jobs in [sched'] do, too. *)
Lemma mea_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched' arr_seq.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq
jobs_come_from_arrival_sequence sched' arr_seq
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq
jobs_come_from_arrival_sequence sched' arr_seq
rewrite /sched' /make_edf_at.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq
jobs_come_from_arrival_sequence
match sched t_edf with
| Some j =>
swapped sched t_edf
(find_swap_candidate sched t_edf j)
| None => sched
end arr_seq
destruct (sched t_edf) as [j_orig|] eqn :SCHED_orig => [|//].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq j_orig : Job SCHED_orig : sched t_edf = Some j_orig
jobs_come_from_arrival_sequence
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) arr_seq
exact : swapped_jobs_come_from_arrival_sequence.
Qed .
End ArrivalSequence .
(** For the final claim, assume that [EDF_at] already holds
everywhere prior to time [t_edf], i.e., that [sched] consists of
an EDF prefix. *)
Hypothesis H_EDF_prefix : forall t , t < t_edf -> EDF_at sched t.
(** We establish a key property of [make_edf_at]: not only does it
ensure [EDF_at] at time [t_edf], it also maintains the fact that
the schedule has an EDF prefix prior to time [t_edf]. In other
words, it grows the EDF prefix by one time unit. *)
Lemma mea_EDF_widen :
forall t , t <= t_edf -> EDF_at sched' t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched t
forall t : nat, t <= t_edf -> EDF_at sched' t
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched t
forall t : nat, t <= t_edf -> EDF_at sched' t
move => t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat
t <= t_edf -> EDF_at sched' t
rewrite leq_eqVlt => /orP [/eqP EQ|LT] ;
first by rewrite EQ; apply make_edf_at_guarantee.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf
EDF_at sched' t
rewrite /sched' /make_edf_at.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf
EDF_at
match sched t_edf with
| Some j =>
swapped sched t_edf
(find_swap_candidate sched t_edf j)
| None => sched
end t
destruct (sched t_edf) as [j_orig|] eqn :SCHED_edf; last by apply H_EDF_prefix.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig
EDF_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) t
move => j SCHED_j t' j' LE_t_t' SCHED_j' ARR_j'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job SCHED_j : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig))
j t t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t
job_deadline j <= job_deadline j'
have SCHED_edf': scheduled_at sched j_orig t_edf
by rewrite scheduled_at_def; apply /eqP.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job SCHED_j : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig))
j t t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf
job_deadline j <= job_deadline j'
have LT_t_fsc: t < find_swap_candidate sched t_edf j_orig.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job SCHED_j : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig))
j t t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf
t < find_swap_candidate sched t_edf j_orig
{ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job SCHED_j : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig))
j t t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf
t < find_swap_candidate sched t_edf j_orig
apply leq_trans with (n := t_edf) => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job SCHED_j : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig))
j t t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf
t_edf <= find_swap_candidate sched t_edf j_orig
apply fsc_range1 => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job SCHED_j : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig))
j t t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf
t_edf < job_deadline j_orig
now apply scheduled_job_in_sched_has_later_deadline.
} Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job SCHED_j : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig))
j t t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf LT_t_fsc : t < find_swap_candidate sched t_edf j_orig
job_deadline j <= job_deadline j'
move : SCHED_j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf LT_t_fsc : t < find_swap_candidate sched t_edf j_orig
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j t ->
job_deadline j <= job_deadline j'
have ->: scheduled_at (swapped sched t_edf (find_swap_candidate sched t_edf j_orig)) j t = scheduled_at sched j t
by apply swap_job_scheduled_other_times; [move : LT | move : LT_t_fsc]; rewrite ltn_neqAle => /andP [NEQ _]; rewrite eq_sym.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf LT_t_fsc : t < find_swap_candidate sched t_edf j_orig
scheduled_at sched j t ->
job_deadline j <= job_deadline j'
move => SCHED_j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf LT_t_fsc : t < find_swap_candidate sched t_edf j_orig SCHED_j : scheduled_at sched j t
job_deadline j <= job_deadline j'
move : (H_EDF_prefix t LT).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf LT_t_fsc : t < find_swap_candidate sched t_edf j_orig SCHED_j : scheduled_at sched j t
EDF_at sched t -> job_deadline j <= job_deadline j'
rewrite /EDF_at => EDF.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf LT_t_fsc : t < find_swap_candidate sched t_edf j_orig SCHED_j : scheduled_at sched j t EDF : forall j : Job,
scheduled_at sched j t ->
forall (t' : instant) (j' : Job),
t <= t' ->
scheduled_at sched j' t' ->
job_arrival j' <= t ->
job_deadline j <= job_deadline j'
job_deadline j <= job_deadline j'
move : (SCHED_j').Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf LT_t_fsc : t < find_swap_candidate sched t_edf j_orig SCHED_j : scheduled_at sched j t EDF : forall j : Job,
scheduled_at sched j t ->
forall (t' : instant) (j' : Job),
t <= t' ->
scheduled_at sched j' t' ->
job_arrival j' <= t ->
job_deadline j <= job_deadline j'
scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf j_orig)) j' t' ->
job_deadline j <= job_deadline j'
move : (swap_job_scheduled_cases _ _ _ _ _ SCHED_j') => [->|[[EQ ->]|[EQ ->]]] SCHED_j'_orig.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf LT_t_fsc : t < find_swap_candidate sched t_edf j_orig SCHED_j : scheduled_at sched j t EDF : forall j : Job,
scheduled_at sched j t ->
forall (t' : instant) (j' : Job),
t <= t' ->
scheduled_at sched j' t' ->
job_arrival j' <= t ->
job_deadline j <= job_deadline j'SCHED_j'_orig : scheduled_at sched j' t'
job_deadline j <= job_deadline j'
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf LT_t_fsc : t < find_swap_candidate sched t_edf j_orig SCHED_j : scheduled_at sched j t EDF : forall j : Job,
scheduled_at sched j t ->
forall (t' : instant) (j' : Job),
t <= t' ->
scheduled_at sched j' t' ->
job_arrival j' <= t ->
job_deadline j <= job_deadline j'SCHED_j'_orig : scheduled_at sched j' t'
job_deadline j <= job_deadline j'
by apply EDF with (t' := t').
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf LT_t_fsc : t < find_swap_candidate sched t_edf j_orig SCHED_j : scheduled_at sched j t EDF : forall j : Job,
scheduled_at sched j t ->
forall (t' : instant) (j' : Job),
t <= t' ->
scheduled_at sched j' t' ->
job_arrival j' <= t ->
job_deadline j <= job_deadline j'EQ : t' = t_edf SCHED_j'_orig : scheduled_at sched j'
(find_swap_candidate sched t_edf
j_orig)
job_deadline j <= job_deadline j'
by apply EDF with (t' := (find_swap_candidate sched t_edf j_orig)) => //; apply ltnW.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched t_edf : instant sched' := make_edf_at sched t_edf : schedule (ideal.processor_state Job) H_EDF_prefix : forall t : nat,
t < t_edf -> EDF_at sched tt : nat LT : t < t_edf j_orig : Job SCHED_edf : sched t_edf = Some j_orig j : Job t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at
(swapped sched t_edf
(find_swap_candidate sched t_edf
j_orig)) j' t' ARR_j' : job_arrival j' <= t SCHED_edf' : scheduled_at sched j_orig t_edf LT_t_fsc : t < find_swap_candidate sched t_edf j_orig SCHED_j : scheduled_at sched j t EDF : forall j : Job,
scheduled_at sched j t ->
forall (t' : instant) (j' : Job),
t <= t' ->
scheduled_at sched j' t' ->
job_arrival j' <= t ->
job_deadline j <= job_deadline j'EQ : t' = find_swap_candidate sched t_edf j_orig SCHED_j'_orig : scheduled_at sched j' t_edf
job_deadline j <= job_deadline j'
by apply EDF with (t' := t_edf) => //; apply ltnW.
Qed .
End MakeEDFAtFacts .
(** In the following section, we establish properties of [edf_transform_prefix]. *)
Section EDFPrefixFacts .
(** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(** ...consider an ideal uniprocessor schedule... *)
Variable sched : schedule (ideal.processor_state Job).
(** ...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.
(** ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses : all_deadlines_met sched.
(** Consider any point in time, denoted [horizon], and... *)
Variable horizon : instant.
(** ...let [sched'] denote the schedule obtained by transforming
[sched] up to the horizon. *)
Let sched' := edf_transform_prefix sched horizon.
(** To start, we observe that [sched'] is still well-behaved and
without deadline misses. *)
Lemma edf_prefix_well_formedness :
completed_jobs_dont_execute sched'
/\
jobs_must_arrive_to_execute sched'
/\
all_deadlines_met sched'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
completed_jobs_dont_execute sched' /\
jobs_must_arrive_to_execute sched' /\
all_deadlines_met sched'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
completed_jobs_dont_execute sched' /\
jobs_must_arrive_to_execute sched' /\
all_deadlines_met sched'
rewrite /sched' /edf_transform_prefix.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
completed_jobs_dont_execute
(prefix_map sched make_edf_at horizon) /\
jobs_must_arrive_to_execute
(prefix_map sched make_edf_at horizon) /\
all_deadlines_met
(prefix_map sched make_edf_at horizon)
apply prefix_map_property_invariance; last by split .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
forall (sched : schedule (ideal.processor_state Job))
(t : instant),
completed_jobs_dont_execute sched /\
jobs_must_arrive_to_execute sched /\
all_deadlines_met sched ->
completed_jobs_dont_execute (make_edf_at sched t) /\
jobs_must_arrive_to_execute (make_edf_at sched t) /\
all_deadlines_met (make_edf_at sched t)
move => sched'' t [COMP [ARR DL_MET]].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) sched'' : schedule (ideal.processor_state Job) t : instant COMP : completed_jobs_dont_execute sched'' ARR : jobs_must_arrive_to_execute sched'' DL_MET : all_deadlines_met sched''
completed_jobs_dont_execute (make_edf_at sched'' t) /\
jobs_must_arrive_to_execute (make_edf_at sched'' t) /\
all_deadlines_met (make_edf_at sched'' t)
split ; last split .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) sched'' : schedule (ideal.processor_state Job) t : instant COMP : completed_jobs_dont_execute sched'' ARR : jobs_must_arrive_to_execute sched'' DL_MET : all_deadlines_met sched''
completed_jobs_dont_execute (make_edf_at sched'' t)
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) sched'' : schedule (ideal.processor_state Job) t : instant COMP : completed_jobs_dont_execute sched'' ARR : jobs_must_arrive_to_execute sched'' DL_MET : all_deadlines_met sched''
completed_jobs_dont_execute (make_edf_at sched'' t)
apply mea_completed_jobs => //.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) sched'' : schedule (ideal.processor_state Job) t : instant COMP : completed_jobs_dont_execute sched'' ARR : jobs_must_arrive_to_execute sched'' DL_MET : all_deadlines_met sched''
jobs_must_arrive_to_execute (make_edf_at sched'' t)
apply mea_jobs_must_arrive => //.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) sched'' : schedule (ideal.processor_state Job) t : instant COMP : completed_jobs_dont_execute sched'' ARR : jobs_must_arrive_to_execute sched'' DL_MET : all_deadlines_met sched''
all_deadlines_met (make_edf_at sched'' t)
apply mea_no_deadline_misses => //.
Qed .
(** Because it is needed frequently, we extract the second clause of
the above conjunction as a corollary. *)
Corollary edf_prefix_jobs_must_arrive :
jobs_must_arrive_to_execute sched'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
jobs_must_arrive_to_execute sched'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
jobs_must_arrive_to_execute sched'
by move : edf_prefix_well_formedness => [_ [ARR _]]. Qed .
(** We similarly observe that the absence of deadline misses implies
that any scheduled job must have a deadline at a time later then
when it is scheduled. *)
Corollary edf_prefix_scheduled_job_has_later_deadline :
forall j t ,
scheduled_at sched' j t ->
job_deadline j > t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at sched' j t -> t < job_deadline j
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at sched' j t -> t < job_deadline j
move => j t SCHED.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t
t < job_deadline j
move : edf_prefix_well_formedness => [COMP [ARR DL_MET]].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) j : Job t : instant SCHED : scheduled_at sched' j t COMP : completed_jobs_dont_execute sched' ARR : jobs_must_arrive_to_execute sched' DL_MET : all_deadlines_met sched'
t < job_deadline j
exact : (scheduled_at_implies_later_deadline sched').
Qed .
(** Since no jobs are lost or added to the schedule by
[edf_transform_prefix], we if a job is scheduled in the
transformed schedule, then it is also scheduled at some point in
the original schedule. *)
Lemma edf_prefix_job_scheduled :
forall j t ,
scheduled_at sched' j t ->
exists t' , scheduled_at sched j t'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at sched' j t ->
exists t' : instant, scheduled_at sched j t'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at sched' j t ->
exists t' : instant, scheduled_at sched j t'
rewrite /sched' /edf_transform_prefix.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at (prefix_map sched make_edf_at horizon) j
t -> exists t' : instant, scheduled_at sched j t'
move => j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) j : Job
forall t : instant,
scheduled_at (prefix_map sched make_edf_at horizon) j
t -> exists t' : instant, scheduled_at sched j t'
apply prefix_map_property_invariance;
last by move => t SCHED; exists t .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) j : Job
forall (sched0 : schedule (ideal.processor_state Job))
(t : instant),
(forall t0 : instant,
scheduled_at sched0 j t0 ->
exists t' : instant, scheduled_at sched j t') ->
forall t0 : instant,
scheduled_at (make_edf_at sched0 t) j t0 ->
exists t' : instant, scheduled_at sched j t'
move => sched'' t'' EX t''' SCHED_mea.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) j : Job sched'' : schedule (ideal.processor_state Job) t'' : instant EX : forall t : instant,
scheduled_at sched'' j t ->
exists t' : instant, scheduled_at sched j t't''' : instant SCHED_mea : scheduled_at (make_edf_at sched'' t'') j
t'''
exists t' : instant, scheduled_at sched j t'
move : (mea_job_scheduled _ _ _ _ SCHED_mea) => [t'''' SCHED''''].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) j : Job sched'' : schedule (ideal.processor_state Job) t'' : instant EX : forall t : instant,
scheduled_at sched'' j t ->
exists t' : instant, scheduled_at sched j t't''' : instant SCHED_mea : scheduled_at (make_edf_at sched'' t'') j
t''' t'''' : instant SCHED'''' : scheduled_at sched'' j t''''
exists t' : instant, scheduled_at sched j t'
now apply : (EX t'''' SCHED'''').
Qed .
(** Conversely, if a job is scheduled in the original schedule, it is
also scheduled at some point in the transformed schedule. *)
Lemma edf_prefix_job_scheduled' :
forall j t ,
scheduled_at sched j t ->
exists t' , scheduled_at sched' j t'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at sched j t ->
exists t' : instant, scheduled_at sched' j t'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
forall (j : Job) (t : instant),
scheduled_at sched j t ->
exists t' : instant, scheduled_at sched' j t'
move => j t SCHED_j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) j : Job t : instant SCHED_j : scheduled_at sched j t
exists t' : instant, scheduled_at sched' j t'
rewrite /sched' /edf_transform_prefix.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) j : Job t : instant SCHED_j : scheduled_at sched j t
exists t' : instant,
scheduled_at (prefix_map sched make_edf_at horizon)
j t'
apply prefix_map_property_invariance; last by exists t .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) j : Job t : instant SCHED_j : scheduled_at sched j t
forall (sched : schedule (ideal.processor_state Job))
(t : instant),
(exists t' : instant, scheduled_at sched j t') ->
exists t' : instant,
scheduled_at (make_edf_at sched t) j t'
move => schedX tx [t' SCHEDX_j].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) j : Job t : instant SCHED_j : scheduled_at sched j t schedX : schedule (ideal.processor_state Job) tx, t' : instant SCHEDX_j : scheduled_at schedX j t'
exists t' : instant,
scheduled_at (make_edf_at schedX tx) j t'
eapply mea_job_scheduled'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) j : Job t : instant SCHED_j : scheduled_at sched j t schedX : schedule (ideal.processor_state Job) tx, t' : instant SCHEDX_j : scheduled_at schedX j t'
scheduled_at schedX j ?t
now exact SCHEDX_j.
Qed .
(** Next, we note that [edf_transform_prefix] maintains the
property that all jobs stem from a given arrival sequence. *)
Section ArrivalSequence .
(** For any arrival sequence,... *)
Variable arr_seq : arrival_sequence Job.
(** ...if all jobs in the original schedule come from the arrival sequence,... *)
Hypothesis H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq.
(** ...then all jobs in the transformed schedule still come from
the same arrival sequence. *)
Lemma edf_prefix_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched' arr_seq.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq
jobs_come_from_arrival_sequence sched' arr_seq
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq
jobs_come_from_arrival_sequence sched' arr_seq
rewrite /sched' /edf_transform_prefix.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq
jobs_come_from_arrival_sequence
(prefix_map sched make_edf_at horizon) arr_seq
apply prefix_map_property_invariance => [|//].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq
forall (sched : schedule (ideal.processor_state Job))
(t : instant),
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence (make_edf_at sched t)
arr_seq
move => schedX t ARR.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq schedX : schedule (ideal.processor_state Job) t : instant ARR : jobs_come_from_arrival_sequence schedX arr_seq
jobs_come_from_arrival_sequence (make_edf_at schedX t)
arr_seq
exact : mea_jobs_come_from_arrival_sequence.
Qed .
End ArrivalSequence .
(** We establish the key property of [edf_transform_prefix]: that it indeed
ensures that the resulting schedule ensures the EDF invariant up to the
given [horizon]. *)
Lemma edf_prefix_guarantee :
forall t ,
t < horizon ->
EDF_at sched' t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
forall t : nat, t < horizon -> EDF_at sched' t
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job)
forall t : nat, t < horizon -> EDF_at sched' t
move => t IN_PREFIX.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) t : nat IN_PREFIX : t < horizon
EDF_at sched' t
rewrite /sched' /edf_transform_prefix.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) t : nat IN_PREFIX : t < horizon
EDF_at (prefix_map sched make_edf_at horizon) t
apply prefix_map_pointwise_property
with (Q := EDF_at)
(P := (fun sched => completed_jobs_dont_execute sched
/\
jobs_must_arrive_to_execute sched
/\
all_deadlines_met sched))=> //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) t : nat IN_PREFIX : t < horizon
forall (sched : schedule (ideal.processor_state Job))
(t_ref : instant),
completed_jobs_dont_execute sched /\
jobs_must_arrive_to_execute sched /\
all_deadlines_met sched ->
completed_jobs_dont_execute (make_edf_at sched t_ref) /\
jobs_must_arrive_to_execute (make_edf_at sched t_ref) /\
all_deadlines_met (make_edf_at sched t_ref)
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) t : nat IN_PREFIX : t < horizon
forall (sched : schedule (ideal.processor_state Job))
(t_ref : instant),
completed_jobs_dont_execute sched /\
jobs_must_arrive_to_execute sched /\
all_deadlines_met sched ->
completed_jobs_dont_execute (make_edf_at sched t_ref) /\
jobs_must_arrive_to_execute (make_edf_at sched t_ref) /\
all_deadlines_met (make_edf_at sched t_ref)
move => schedX t_ref [COMP [ARR DL]].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) t : nat IN_PREFIX : t < horizon schedX : schedule (ideal.processor_state Job) t_ref : instant COMP : completed_jobs_dont_execute schedX ARR : jobs_must_arrive_to_execute schedX DL : all_deadlines_met schedX
completed_jobs_dont_execute (make_edf_at schedX t_ref) /\
jobs_must_arrive_to_execute (make_edf_at schedX t_ref) /\
all_deadlines_met (make_edf_at schedX t_ref)
split ; last split .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) t : nat IN_PREFIX : t < horizon schedX : schedule (ideal.processor_state Job) t_ref : instant COMP : completed_jobs_dont_execute schedX ARR : jobs_must_arrive_to_execute schedX DL : all_deadlines_met schedX
completed_jobs_dont_execute (make_edf_at schedX t_ref)
+ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) t : nat IN_PREFIX : t < horizon schedX : schedule (ideal.processor_state Job) t_ref : instant COMP : completed_jobs_dont_execute schedX ARR : jobs_must_arrive_to_execute schedX DL : all_deadlines_met schedX
completed_jobs_dont_execute (make_edf_at schedX t_ref)
by apply mea_completed_jobs => //.
+ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) t : nat IN_PREFIX : t < horizon schedX : schedule (ideal.processor_state Job) t_ref : instant COMP : completed_jobs_dont_execute schedX ARR : jobs_must_arrive_to_execute schedX DL : all_deadlines_met schedX
jobs_must_arrive_to_execute (make_edf_at schedX t_ref)
by apply mea_jobs_must_arrive => //.
+ Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) t : nat IN_PREFIX : t < horizon schedX : schedule (ideal.processor_state Job) t_ref : instant COMP : completed_jobs_dont_execute schedX ARR : jobs_must_arrive_to_execute schedX DL : all_deadlines_met schedX
all_deadlines_met (make_edf_at schedX t_ref)
by apply mea_no_deadline_misses => //.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) t : nat IN_PREFIX : t < horizon
forall (sched : schedule (ideal.processor_state Job))
(t_ref : nat),
completed_jobs_dont_execute sched /\
jobs_must_arrive_to_execute sched /\
all_deadlines_met sched ->
(forall t' : nat, t' < t_ref -> EDF_at sched t') ->
forall t' : nat,
t' <= t_ref -> EDF_at (make_edf_at sched t_ref) t'
move => schedX t_ref [COMP [ARR DL]].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched horizon : instant sched' := edf_transform_prefix sched horizon : schedule (ideal.processor_state Job) t : nat IN_PREFIX : t < horizon schedX : schedule (ideal.processor_state Job) t_ref : nat COMP : completed_jobs_dont_execute schedX ARR : jobs_must_arrive_to_execute schedX DL : all_deadlines_met schedX
(forall t' : nat, t' < t_ref -> EDF_at schedX t') ->
forall t' : nat,
t' <= t_ref -> EDF_at (make_edf_at schedX t_ref) t'
now apply mea_EDF_widen.
Qed .
End EDFPrefixFacts .
(** Finally, we observe that [edf_transform_prefix] is prefix-stable, which
allows us to replace an earlier horizon with a later horizon. Note: this is
in a separate section because we need [edf_prefix_jobs_must_arrive]
generalized for any schedule. *)
Section EDFPrefixInclusion .
(** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(** ...consider an ideal uniprocessor schedule... *)
Variable sched : schedule (ideal.processor_state Job).
(** ...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.
(** ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses : all_deadlines_met sched.
Lemma edf_prefix_inclusion :
forall h1 h2 ,
h1 <= h2 ->
identical_prefix (edf_transform_prefix sched h1) (edf_transform_prefix sched h2) h1.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched
forall h1 h2 : nat,
h1 <= h2 ->
identical_prefix (edf_transform_prefix sched h1)
(edf_transform_prefix sched h2) h1
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched
forall h1 h2 : nat,
h1 <= h2 ->
identical_prefix (edf_transform_prefix sched h1)
(edf_transform_prefix sched h2) h1
move => h1 h2 LE_h1_h2.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, h2 : nat LE_h1_h2 : h1 <= h2
identical_prefix (edf_transform_prefix sched h1)
(edf_transform_prefix sched h2) h1
rewrite /identical_prefix => t LT_t_h1.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, h2 : nat LE_h1_h2 : h1 <= h2 t : nat LT_t_h1 : t < h1
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t
elim : h2 LE_h1_h2 => [|h2 IHh2] LE_h1_h2; first by move : (leq_trans LT_t_h1 LE_h1_h2).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, t : nat LT_t_h1 : t < h1 h2 : nat IHh2 : h1 <= h2 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t LE_h1_h2 : h1 <= h2.+1
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2.+1 t
move : LE_h1_h2; rewrite leq_eqVlt => /orP [/eqP-> //|LT].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, t : nat LT_t_h1 : t < h1 h2 : nat IHh2 : h1 <= h2 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t LT : h1 < h2.+1
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2.+1 t
move : LT.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, t : nat LT_t_h1 : t < h1 h2 : nat IHh2 : h1 <= h2 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t
h1 < h2.+1 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2.+1 t
rewrite ltnS => LE_h1_h2.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, t : nat LT_t_h1 : t < h1 h2 : nat IHh2 : h1 <= h2 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t LE_h1_h2 : h1 <= h2
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2.+1 t
rewrite [RHS]/edf_transform_prefix /prefix_map -/prefix_map IHh2 //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, t : nat LT_t_h1 : t < h1 h2 : nat IHh2 : h1 <= h2 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t LE_h1_h2 : h1 <= h2
edf_transform_prefix sched h2 t =
make_edf_at (prefix_map sched make_edf_at h2) h2 t
rewrite {1 }/make_edf_at.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, t : nat LT_t_h1 : t < h1 h2 : nat IHh2 : h1 <= h2 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t LE_h1_h2 : h1 <= h2
edf_transform_prefix sched h2 t =
match prefix_map sched make_edf_at h2 h2 with
| Some j =>
swapped (prefix_map sched make_edf_at h2) h2
(find_swap_candidate
(prefix_map sched make_edf_at h2) h2 j)
| None => prefix_map sched make_edf_at h2
end t
destruct (prefix_map sched make_edf_at h2 h2) as [j|] eqn :SCHED => [|//].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, t : nat LT_t_h1 : t < h1 h2 : nat IHh2 : h1 <= h2 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t LE_h1_h2 : h1 <= h2 j : Job SCHED : prefix_map sched make_edf_at h2 h2 = Some j
edf_transform_prefix sched h2 t =
swapped (prefix_map sched make_edf_at h2) h2
(find_swap_candidate
(prefix_map sched make_edf_at h2) h2 j) t
rewrite -(swap_before_invariant _ h2 (find_swap_candidate (edf_transform_prefix sched h2) h2 j)) // ;
last by apply leq_trans with (n := h1).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, t : nat LT_t_h1 : t < h1 h2 : nat IHh2 : h1 <= h2 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t LE_h1_h2 : h1 <= h2 j : Job SCHED : prefix_map sched make_edf_at h2 h2 = Some j
h2 <=
find_swap_candidate (edf_transform_prefix sched h2) h2
j
have SCHED_j: scheduled_at (edf_transform_prefix sched h2) j h2
by rewrite scheduled_at_def /edf_transform_prefix; apply /eqP.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, t : nat LT_t_h1 : t < h1 h2 : nat IHh2 : h1 <= h2 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t LE_h1_h2 : h1 <= h2 j : Job SCHED : prefix_map sched make_edf_at h2 h2 = Some j SCHED_j : scheduled_at (edf_transform_prefix sched h2)
j h2
h2 <=
find_swap_candidate (edf_transform_prefix sched h2) h2
j
apply fsc_range1 => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, t : nat LT_t_h1 : t < h1 h2 : nat IHh2 : h1 <= h2 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t LE_h1_h2 : h1 <= h2 j : Job SCHED : prefix_map sched make_edf_at h2 h2 = Some j SCHED_j : scheduled_at (edf_transform_prefix sched h2)
j h2
jobs_must_arrive_to_execute
(edf_transform_prefix sched h2)
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, t : nat LT_t_h1 : t < h1 h2 : nat IHh2 : h1 <= h2 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t LE_h1_h2 : h1 <= h2 j : Job SCHED : prefix_map sched make_edf_at h2 h2 = Some j SCHED_j : scheduled_at (edf_transform_prefix sched h2)
j h2
jobs_must_arrive_to_execute
(edf_transform_prefix sched h2)
by apply edf_prefix_jobs_must_arrive.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched h1, t : nat LT_t_h1 : t < h1 h2 : nat IHh2 : h1 <= h2 ->
edf_transform_prefix sched h1 t =
edf_transform_prefix sched h2 t LE_h1_h2 : h1 <= h2 j : Job SCHED : prefix_map sched make_edf_at h2 h2 = Some j SCHED_j : scheduled_at (edf_transform_prefix sched h2)
j h2
h2 < job_deadline j
apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := h2) => //.
Qed .
End EDFPrefixInclusion .
(** In the following section, we finally establish properties of the
overall EDF transformation[edf_transform]. *)
Section EDFTransformFacts .
(** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(** ...consider an ideal uniprocessor schedule... *)
Variable sched : schedule (ideal.processor_state Job).
(** ...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.
(** ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses : all_deadlines_met sched.
(** In the following, let [sched_edf] denote the EDF schedule obtained by
transforming the given reference schedule. *)
Let sched_edf := edf_transform sched.
(** We begin with a simple lemma relating [sched_edf] to its definition that
allows us to easily look at any finite prefix of the EDF-transformed
scheduled. *)
Lemma edf_finite_prefix :
forall h ,
identical_prefix sched_edf (edf_transform_prefix sched h) h.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
forall h : instant,
identical_prefix sched_edf
(edf_transform_prefix sched h) h
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
forall h : instant,
identical_prefix sched_edf
(edf_transform_prefix sched h) h
move => h.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job h : instant
identical_prefix sched_edf
(edf_transform_prefix sched h) h
rewrite /sched_edf/edf_transform /identical_prefix => t LT_h.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job h : instant t : nat LT_h : t < h
edf_transform_prefix sched t.+1 t =
edf_transform_prefix sched h t
now apply edf_prefix_inclusion.
Qed .
(** From this, we move on to the defining property of the transformation: the
resulting schedule is actually an EDF schedule. *)
Theorem edf_transform_ensures_edf :
EDF_schedule sched_edf.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
EDF_schedule sched_edf
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
EDF_schedule sched_edf
rewrite /EDF_schedule => t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job t : instant
EDF_at sched_edf t
rewrite /EDF_at //= => j SCHED_j t' j' LE_t_t' SCHED_j' ARR_j'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job t : instant j : Job SCHED_j : scheduled_at sched_edf j t t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at sched_edf j' t' ARR_j' : job_arrival j' <= t
job_deadline j <= job_deadline j'
set S := (edf_transform_prefix sched t'.+1 ).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job t : instant j : Job SCHED_j : scheduled_at sched_edf j t t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at sched_edf j' t' ARR_j' : job_arrival j' <= t S := edf_transform_prefix sched t'.+1 : schedule (ideal.processor_state Job)
job_deadline j <= job_deadline j'
have EDF: EDF_at S t by apply edf_prefix_guarantee.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job t : instant j : Job SCHED_j : scheduled_at sched_edf j t t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at sched_edf j' t' ARR_j' : job_arrival j' <= t S := edf_transform_prefix sched t'.+1 : schedule (ideal.processor_state Job) EDF : EDF_at S t
job_deadline j <= job_deadline j'
apply EDF with (t' := t') => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job t : instant j : Job SCHED_j : scheduled_at sched_edf j t t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at sched_edf j' t' ARR_j' : job_arrival j' <= t S := edf_transform_prefix sched t'.+1 : schedule (ideal.processor_state Job) EDF : EDF_at S t
scheduled_at S j t
rewrite -(identical_prefix_scheduled_at sched_edf _ t'.+1 ) //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job t : instant j : Job SCHED_j : scheduled_at sched_edf j t t' : instant j' : Job LE_t_t' : t <= t' SCHED_j' : scheduled_at sched_edf j' t' ARR_j' : job_arrival j' <= t S := edf_transform_prefix sched t'.+1 : schedule (ideal.processor_state Job) EDF : EDF_at S t
identical_prefix sched_edf S t'.+1
now apply edf_finite_prefix.
Qed .
(** Next, we observe that completed jobs still don't execute in the resulting
EDF schedule. This observation is needed to establish that the resulting
EDF schedule is valid. *)
Lemma edf_transform_completed_jobs_dont_execute :
completed_jobs_dont_execute sched_edf.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
completed_jobs_dont_execute sched_edf
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
completed_jobs_dont_execute sched_edf
move => j t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant
scheduled_at sched_edf j t ->
service sched_edf j t < job_cost j
set S := (edf_transform_prefix sched t.+1 ).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant S := edf_transform_prefix sched t.+1 : schedule (ideal.processor_state Job)
scheduled_at sched_edf j t ->
service sched_edf j t < job_cost j
rewrite (identical_prefix_scheduled_at _ S t.+1 ) //;
last by apply edf_finite_prefix.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant S := edf_transform_prefix sched t.+1 : schedule (ideal.processor_state Job)
scheduled_at S j t ->
service sched_edf j t < job_cost j
rewrite (identical_prefix_service _ S t) //;
last by apply (identical_prefix_inclusion _ _ t.+1 ) => //; apply edf_finite_prefix.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant S := edf_transform_prefix sched t.+1 : schedule (ideal.processor_state Job)
scheduled_at S j t -> service S j t < job_cost j
move : (edf_prefix_well_formedness sched H_jobs_must_arrive_to_execute
H_completed_jobs_dont_execute H_no_deadline_misses t.+1 ) => [COMP _].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant S := edf_transform_prefix sched t.+1 : schedule (ideal.processor_state Job) COMP : completed_jobs_dont_execute
(edf_transform_prefix sched t.+1 )
scheduled_at S j t -> service S j t < job_cost j
now apply COMP.
Qed .
(** Similarly, we observe that no job is scheduled prior to its arrival. *)
Lemma edf_transform_jobs_must_arrive :
jobs_must_arrive_to_execute sched_edf.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
jobs_must_arrive_to_execute sched_edf
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
jobs_must_arrive_to_execute sched_edf
move => j t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant
scheduled_at sched_edf j t -> has_arrived j t
rewrite /sched_edf /edf_transform.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant
scheduled_at
(fun t : instant =>
edf_transform_prefix sched t.+1 t) j t ->
has_arrived j t
move : (edf_prefix_well_formedness sched H_jobs_must_arrive_to_execute H_completed_jobs_dont_execute H_no_deadline_misses t.+1 ) => [_ [ARR _]].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant ARR : jobs_must_arrive_to_execute
(edf_transform_prefix sched t.+1 )
scheduled_at
(fun t : instant =>
edf_transform_prefix sched t.+1 t) j t ->
has_arrived j t
now apply ARR.
Qed .
(** We next establish the second key property: in the transformed EDF
schedule, no scheduled job misses a deadline. *)
Theorem edf_transform_deadlines_met :
all_deadlines_met sched_edf.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
all_deadlines_met sched_edf
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
all_deadlines_met sched_edf
move => j t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant
scheduled_at sched_edf j t ->
job_meets_deadline sched_edf j
rewrite /sched_edf /job_meets_deadline.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant
scheduled_at (edf_transform sched) j t ->
completed_by (edf_transform sched) j (job_deadline j)
set t_dl := (job_deadline j).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant t_dl := job_deadline j : instant
scheduled_at (edf_transform sched) j t ->
completed_by (edf_transform sched) j t_dl
rewrite (identical_prefix_completed_by _ (edf_transform_prefix sched t_dl.+1 ) t_dl) //;
last by apply (identical_prefix_inclusion _ _ t_dl.+1 ) => //; apply edf_finite_prefix.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant t_dl := job_deadline j : instant
scheduled_at (edf_transform sched) j t ->
completed_by (edf_transform_prefix sched t_dl.+1 ) j
t_dl
move => SCHED_AT; move : (SCHED_AT).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant t_dl := job_deadline j : instant SCHED_AT : scheduled_at (edf_transform sched) j t
scheduled_at (edf_transform sched) j t ->
completed_by (edf_transform_prefix sched t_dl.+1 ) j
t_dl
rewrite (identical_prefix_scheduled_at _ (edf_transform_prefix sched t_dl.+1 ) t_dl).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant t_dl := job_deadline j : instant SCHED_AT : scheduled_at (edf_transform sched) j t
scheduled_at (edf_transform_prefix sched t_dl.+1 ) j t ->
completed_by (edf_transform_prefix sched t_dl.+1 ) j
t_dl
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant t_dl := job_deadline j : instant SCHED_AT : scheduled_at (edf_transform sched) j t
scheduled_at (edf_transform_prefix sched t_dl.+1 ) j t ->
completed_by (edf_transform_prefix sched t_dl.+1 ) j
t_dl
move : (edf_prefix_well_formedness sched H_jobs_must_arrive_to_execute
H_completed_jobs_dont_execute H_no_deadline_misses t_dl.+1 ) => [_ [_ DL]].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant t_dl := job_deadline j : instant SCHED_AT : scheduled_at (edf_transform sched) j t DL : all_deadlines_met
(edf_transform_prefix sched t_dl.+1 )
scheduled_at (edf_transform_prefix sched t_dl.+1 ) j t ->
completed_by (edf_transform_prefix sched t_dl.+1 ) j
t_dl
now apply (DL j t).
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant t_dl := job_deadline j : instant SCHED_AT : scheduled_at (edf_transform sched) j t
identical_prefix (edf_transform sched)
(edf_transform_prefix sched t_dl.+1 ) t_dl
by apply (identical_prefix_inclusion _ _ t_dl.+1 ) => //; apply edf_finite_prefix.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant t_dl := job_deadline j : instant SCHED_AT : scheduled_at (edf_transform sched) j t
t < t_dl
by apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := t.+1 ).
Qed .
(** We observe that no new jobs are introduced: any job scheduled in the EDF
schedule were also present in the reference schedule. *)
Lemma edf_transform_job_scheduled :
forall j t , scheduled_at sched_edf j t -> exists t' , scheduled_at sched j t'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
forall (j : Job) (t : instant),
scheduled_at sched_edf j t ->
exists t' : instant, scheduled_at sched j t'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
forall (j : Job) (t : instant),
scheduled_at sched_edf j t ->
exists t' : instant, scheduled_at sched j t'
move => j t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant
scheduled_at sched_edf j t ->
exists t' : instant, scheduled_at sched j t'
rewrite /sched_edf /edf_transform {1 }scheduled_at_def -scheduled_at_def.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant
scheduled_at (edf_transform_prefix sched t.+1 ) j t ->
exists t' : instant, scheduled_at sched j t'
by apply edf_prefix_job_scheduled.
Qed .
(** Conversely, we observe that no jobs are lost: any job scheduled in the
reference schedule is also present in the EDF schedule. *)
Lemma edf_transform_job_scheduled' :
forall j t , scheduled_at sched j t -> exists t' , scheduled_at sched_edf j t'.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
forall (j : Job) (t : instant),
scheduled_at sched j t ->
exists t' : instant, scheduled_at sched_edf j t'
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job
forall (j : Job) (t : instant),
scheduled_at sched j t ->
exists t' : instant, scheduled_at sched_edf j t'
move => j t SCHED_j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant SCHED_j : scheduled_at sched j t
exists t' : instant, scheduled_at sched_edf j t'
have EX: exists t' , scheduled_at (edf_transform_prefix sched (job_deadline j)) j t'
by apply edf_prefix_job_scheduled' with (t := t).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant SCHED_j : scheduled_at sched j t EX : exists t' : instant,
scheduled_at
(edf_transform_prefix sched (job_deadline j))
j t'
exists t' : instant, scheduled_at sched_edf j t'
move : EX => [t' SCHED'].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant SCHED_j : scheduled_at sched j t t' : instant SCHED' : scheduled_at
(edf_transform_prefix sched
(job_deadline j)) j t'
exists t' : instant, scheduled_at sched_edf j t'
exists t' .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant SCHED_j : scheduled_at sched j t t' : instant SCHED' : scheduled_at
(edf_transform_prefix sched
(job_deadline j)) j t'
scheduled_at sched_edf j t'
rewrite /sched_edf /edf_transform scheduled_at_def.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant SCHED_j : scheduled_at sched j t t' : instant SCHED' : scheduled_at
(edf_transform_prefix sched
(job_deadline j)) j t'
edf_transform_prefix sched t'.+1 t' == Some j
rewrite (edf_prefix_inclusion _ _ _ _ t'.+1 (job_deadline j)) -?scheduled_at_def => //.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job j : Job t : instant SCHED_j : scheduled_at sched j t t' : instant SCHED' : scheduled_at
(edf_transform_prefix sched
(job_deadline j)) j t'
t' < job_deadline j
now apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := job_deadline j).
Qed .
(** Next, we note that [edf_transform] maintains the property that all jobs
stem from a given arrival sequence. *)
Section ArrivalSequence .
(** For any arrival sequence,... *)
Variable arr_seq : arrival_sequence Job.
(** ...if all jobs in the original schedule come from the arrival sequence,... *)
Hypothesis H_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq.
(** ...then all jobs in the transformed EDF schedule still come from the
same arrival sequence. *)
Lemma edf_transform_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched_edf arr_seq.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq
jobs_come_from_arrival_sequence sched_edf arr_seq
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq
jobs_come_from_arrival_sequence sched_edf arr_seq
rewrite /sched_edf /edf_transform.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq
jobs_come_from_arrival_sequence
(fun t : instant =>
edf_transform_prefix sched t.+1 t) arr_seq
move => j t.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq j : Job t : instant
scheduled_at
(fun t : instant =>
edf_transform_prefix sched t.+1 t) j t ->
arrives_in arr_seq j
rewrite scheduled_at_def - scheduled_at_def.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job sched : schedule (ideal.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_no_deadline_misses : all_deadlines_met sched sched_edf := edf_transform sched : instant -> ideal.processor_state Job arr_seq : arrival_sequence Job H_from_arr_seq : jobs_come_from_arrival_sequence sched
arr_seq j : Job t : instant
scheduled_at (edf_transform_prefix sched t.+1 ) j t ->
arrives_in arr_seq j
now apply (edf_prefix_jobs_come_from_arrival_sequence sched t.+1 arr_seq H_from_arr_seq).
Qed .
End ArrivalSequence .
End EDFTransformFacts .
(** Finally, we state the theorems that jointly make up the EDF optimality claim. *)
Section Optimality .
(** We assume the classic (i.e., Liu & Layland) model of readiness
without jitter or self-suspensions, wherein pending jobs are
always ready. *)
#[local] Existing Instance basic_ready_instance .
(** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(** ... consider an arbitrary valid job arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arr_seq_valid : valid_arrival_sequence arr_seq.
(** ... and an ideal uniprocessor schedule... *)
Variable sched : schedule (ideal.processor_state Job).
(** ... that corresponds to the given arrival sequence. *)
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
(** In the following, let [equivalent_edf_schedule] denote the schedule that
results from the EDF transformation. *)
Let equivalent_edf_schedule := edf_transform sched.
Section AllDeadlinesMet .
(** Suppose no job scheduled in the given reference schedule misses a deadline. *)
Hypothesis H_no_deadline_misses : all_deadlines_met sched.
(** Then the resulting EDF schedule is a valid schedule for the given
arrival sequence... *)
Theorem edf_schedule_is_valid :
valid_schedule equivalent_edf_schedule arr_seq.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses : all_deadlines_met sched
valid_schedule equivalent_edf_schedule arr_seq
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses : all_deadlines_met sched
valid_schedule equivalent_edf_schedule arr_seq
rewrite /valid_schedule; split ;
first by apply edf_transform_jobs_come_from_arrival_sequence.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses : all_deadlines_met sched
jobs_must_be_ready_to_execute equivalent_edf_schedule
apply basic_readiness_compliance.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses : all_deadlines_met sched
jobs_must_arrive_to_execute equivalent_edf_schedule
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses : all_deadlines_met sched
jobs_must_arrive_to_execute equivalent_edf_schedule
exact : edf_transform_jobs_must_arrive.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses : all_deadlines_met sched
completed_jobs_dont_execute equivalent_edf_schedule
exact : edf_transform_completed_jobs_dont_execute.
Qed .
(** ...and no scheduled job misses its deadline. *)
Theorem edf_schedule_meets_all_deadlines :
all_deadlines_met equivalent_edf_schedule.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses : all_deadlines_met sched
all_deadlines_met equivalent_edf_schedule
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses : all_deadlines_met sched
all_deadlines_met equivalent_edf_schedule
exact : edf_transform_deadlines_met. Qed .
End AllDeadlinesMet .
(** Next, we strengthen the above "no deadline misses" claim by relating it
not just to all scheduled jobs, but to all jobs in the given arrival
sequence. *)
Section AllDeadlinesOfArrivalsMet .
(** Suppose no job that's part of the arrival sequence misses a deadline in
the given reference schedule. *)
Hypothesis H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met arr_seq sched.
(** Then no job that's part of the arrival sequence misses a deadline in the
EDF schedule, either. *)
Theorem edf_schedule_meets_all_deadlines_wrt_arrivals :
all_deadlines_of_arrivals_met arr_seq equivalent_edf_schedule.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched
all_deadlines_of_arrivals_met arr_seq
equivalent_edf_schedule
Proof .Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched
all_deadlines_of_arrivals_met arr_seq
equivalent_edf_schedule
move => j ARR_j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j
job_meets_deadline equivalent_edf_schedule j
move : H_sched_valid => [COME READY].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched
job_meets_deadline equivalent_edf_schedule j
have ARR := jobs_must_arrive_to_be_ready sched READY.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched
job_meets_deadline equivalent_edf_schedule j
have COMP := completed_jobs_are_not_ready sched READY.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched
job_meets_deadline equivalent_edf_schedule j
destruct (job_cost j == 0 ) eqn :COST.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched COST : (job_cost j == 0 ) = true
job_meets_deadline equivalent_edf_schedule j
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched COST : (job_cost j == 0 ) = true
job_meets_deadline equivalent_edf_schedule j
move : COST => /eqP COST.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched COST : job_cost j = 0
job_meets_deadline equivalent_edf_schedule j
rewrite /job_meets_deadline /completed_by COST.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched COST : job_cost j = 0
0 <=
service equivalent_edf_schedule j (job_deadline j)
by apply leq0n.
- Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched COST : (job_cost j == 0 ) = false
job_meets_deadline equivalent_edf_schedule j
move : (neq0_lt0n COST) => NONZERO.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched COST : (job_cost j == 0 ) = false NONZERO : 0 < job_cost j
job_meets_deadline equivalent_edf_schedule j
move : (H_no_deadline_misses_of_arrivals j ARR_j).Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched COST : (job_cost j == 0 ) = false NONZERO : 0 < job_cost j
job_meets_deadline sched j ->
job_meets_deadline equivalent_edf_schedule j
rewrite {1 }/job_meets_deadline => COMP_j.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched COST : (job_cost j == 0 ) = false NONZERO : 0 < job_cost jCOMP_j : completed_by sched j (job_deadline j)
job_meets_deadline equivalent_edf_schedule j
move : (completed_implies_scheduled_before sched j NONZERO ARR (job_deadline j) COMP_j) => [t' [_ SCHED']].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched COST : (job_cost j == 0 ) = false NONZERO : 0 < job_cost jCOMP_j : completed_by sched j (job_deadline j) t' : nat SCHED' : scheduled_at sched j t'
job_meets_deadline equivalent_edf_schedule j
move : (all_deadlines_met_in_valid_schedule arr_seq sched COME H_no_deadline_misses_of_arrivals) => NO_MISSES.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched COST : (job_cost j == 0 ) = false NONZERO : 0 < job_cost jCOMP_j : completed_by sched j (job_deadline j) t' : nat SCHED' : scheduled_at sched j t' NO_MISSES : all_deadlines_met sched
job_meets_deadline equivalent_edf_schedule j
move : (edf_transform_job_scheduled' sched ARR COMP NO_MISSES j t' SCHED') => [t'' SCHED''].Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched COST : (job_cost j == 0 ) = false NONZERO : 0 < job_cost jCOMP_j : completed_by sched j (job_deadline j) t' : nat SCHED' : scheduled_at sched j t' NO_MISSES : all_deadlines_met sched t'' : instant SCHED'' : scheduled_at (edf_transform sched) j t''
job_meets_deadline equivalent_edf_schedule j
move : (edf_schedule_meets_all_deadlines NO_MISSES) => DL_MET.Job : JobType H : JobCost Job H0 : JobDeadline Job H1 : JobArrival Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq equivalent_edf_schedule := edf_transform sched : instant ->
ideal.processor_state Job H_no_deadline_misses_of_arrivals : all_deadlines_of_arrivals_met
arr_seq sched j : Job ARR_j : arrives_in arr_seq j COME : jobs_come_from_arrival_sequence sched arr_seq READY : jobs_must_be_ready_to_execute sched ARR : jobs_must_arrive_to_execute sched COMP : completed_jobs_dont_execute sched COST : (job_cost j == 0 ) = false NONZERO : 0 < job_cost jCOMP_j : completed_by sched j (job_deadline j) t' : nat SCHED' : scheduled_at sched j t' NO_MISSES : all_deadlines_met sched t'' : instant SCHED'' : scheduled_at (edf_transform sched) j t'' DL_MET : all_deadlines_met equivalent_edf_schedule
job_meets_deadline equivalent_edf_schedule j
by apply : (DL_MET j t'' SCHED'').
Qed .
End AllDeadlinesOfArrivalsMet .
End Optimality .