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 Export prosa.model.schedule.work_conserving.[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 Import prosa.model.readiness.basic.
Require Export prosa.analysis.facts.model.ideal.schedule.
Require Export prosa.analysis.transform.wc_trans.
Require Export prosa.analysis.facts.transform.swaps.
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.util.list.
Require Export prosa.util.tactics.
(** * Correctness of the work-conservation transformation *)
(** This file contains the main argument of the work-conservation proof,
starting with an analysis of the individual functions that drive
the work-conservation transformation of a given reference schedule
and ending with the proofs of individual properties of the obtained
work-conserving schedule. *)
(** In order to discuss the correctness of the work-conservation transformation at a high level,
we first need a set of lemmas about the inner parts of the procedure. *)
Section AuxiliaryLemmasWorkConservingTransformation .
(** We assume ideal uni-processor schedules. *)
#[local] Existing Instance ideal .processor_state.
(** We assume the basic (i.e., Liu & Layland)
readiness model under which any pending job is ready. *)
#[local] Existing Instance basic_ready_instance .
(** Consider any type of jobs with arrival times, costs, and deadlines... *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
(** ...and an arbitrary arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arr_seq_valid : valid_arrival_sequence arr_seq.
(** We introduce the notion of work-conservation at a
given time [t]. The definition is based on the concept of readiness
of a job, and states that the presence of a ready job implies that
the processor is not idle. *)
Definition is_work_conserving_at sched t :=
(exists j , arrives_in arr_seq j /\ job_ready sched j t) ->
exists j , sched t = Some j.
(** First, we prove some useful properties about the most fundamental
operation of the work-conservation transformation: swapping two processor
states [t1] and [fsc], with [fsc] being a valid swap candidate of [t1]. *)
Section JobsMustBeReadyFindSwapCandidate .
(** Consider an ideal uniprocessor schedule... *)
Variable sched : schedule (ideal.processor_state Job).
(** ...in which jobs must be ready to execute. *)
Hypothesis H_jobs_must_be_ready : jobs_must_be_ready_to_execute sched.
(** Consider an arbitrary time instant [t1]. *)
Variable t1 : instant.
(** Let us define [fsc] as the result of the search for a swap candidate
starting from [t1]... *)
Let fsc := find_swap_candidate arr_seq sched t1.
(** ...and [sched'] as the schedule resulting from the swap. *)
Let sched' := swapped sched t1 fsc.
(** First, we show that, in any case, the result of the search will yield an
instant that is in the future (or, in case of failure, equal to [t1]). *)
Lemma swap_candidate_is_in_future :
t1 <= fsc.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job)
t1 <= fsc
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job)
t1 <= fsc
rewrite /fsc /find_swap_candidate.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job)
t1 <=
match
search_arg sched (relevant_pstate t1) (fun => xpred0)
t1
(max_deadline_for_jobs_arrived_before arr_seq t1)
with
| Some t_swap => t_swap
| None => t1
end
destruct search_arg as [n|] eqn :search_result => [|//].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) n : nat search_result : search_arg sched (relevant_pstate t1)
(fun => xpred0) t1
(max_deadline_for_jobs_arrived_before
arr_seq t1) = Some n
t1 <= n
apply search_arg_in_range in search_result.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) n : nat search_result : t1 <= n <
max_deadline_for_jobs_arrived_before
arr_seq t1
t1 <= n
by move :search_result => /andP [LEQ LMAX].
Qed .
(** Also, we show that the search will not yield jobs that arrive later than the
given reference time. *)
Lemma fsc_respects_has_arrived :
forall j t ,
sched (find_swap_candidate arr_seq sched t) == Some j ->
has_arrived j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job)
forall (j : Job) (t : instant),
sched (find_swap_candidate arr_seq sched t) == Some j ->
has_arrived j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job)
forall (j : Job) (t : instant),
sched (find_swap_candidate arr_seq sched t) == Some j ->
has_arrived j t
move => j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant
sched (find_swap_candidate arr_seq sched t) == Some j ->
has_arrived j t
rewrite /find_swap_candidate.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant
sched
match
search_arg sched (relevant_pstate t)
(fun => xpred0) t
(max_deadline_for_jobs_arrived_before arr_seq t)
with
| Some t_swap => t_swap
| None => t
end == Some j -> has_arrived j t
destruct search_arg eqn :RES; last first .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant RES : search_arg sched (relevant_pstate t)
(fun => xpred0) t
(max_deadline_for_jobs_arrived_before arr_seq
t) = None
sched t == Some j -> has_arrived j t
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant RES : search_arg sched (relevant_pstate t)
(fun => xpred0) t
(max_deadline_for_jobs_arrived_before arr_seq
t) = None
sched t == Some j -> has_arrived j t
rewrite -scheduled_in_def => sched_j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant RES : search_arg sched (relevant_pstate t)
(fun => xpred0) t
(max_deadline_for_jobs_arrived_before arr_seq
t) = None sched_j : scheduled_in j (sched t)
has_arrived j t
apply : (ready_implies_arrived sched).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant RES : search_arg sched (relevant_pstate t)
(fun => xpred0) t
(max_deadline_for_jobs_arrived_before arr_seq
t) = None sched_j : scheduled_in j (sched t)
job_ready sched j t
exact : job_scheduled_implies_ready. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant n : nat RES : search_arg sched (relevant_pstate t)
(fun => xpred0) t
(max_deadline_for_jobs_arrived_before arr_seq
t) = Some n
sched n == Some j -> has_arrived j t
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant n : nat RES : search_arg sched (relevant_pstate t)
(fun => xpred0) t
(max_deadline_for_jobs_arrived_before arr_seq
t) = Some n
sched n == Some j -> has_arrived j t
move => /eqP SCHED_J.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant n : nat RES : search_arg sched (relevant_pstate t)
(fun => xpred0) t
(max_deadline_for_jobs_arrived_before arr_seq
t) = Some n SCHED_J : sched n = Some j
has_arrived j t
move : RES => /search_arg_pred.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant n : nat SCHED_J : sched n = Some j
relevant_pstate t (sched n) -> has_arrived j t
rewrite SCHED_J //. }
Qed .
(** Next, we extend the previous lemma by stating that no job in the transformed
schedule is scheduled before its arrival. *)
Lemma swap_jobs_must_arrive_to_execute :
jobs_must_arrive_to_execute sched'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job)
jobs_must_arrive_to_execute sched'
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job)
jobs_must_arrive_to_execute sched'
move => j t SCHED_AT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t
has_arrived j t
move : (swap_job_scheduled_cases _ _ _ _ _ SCHED_AT)=> [OTHER |[AT_T1 | AT_T2]].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t OTHER : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t
has_arrived j t
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t OTHER : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t
has_arrived j t
apply : (ready_implies_arrived sched).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t OTHER : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t
job_ready sched j t
by apply : job_scheduled_implies_ready; rewrite // -OTHER. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t AT_T1 : t = t1 /\
scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j fsc
has_arrived j t
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t AT_T1 : t = t1 /\
scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j fsc
has_arrived j t
set t2 := find_swap_candidate arr_seq sched t1 in AT_T1.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat AT_T1 : t = t1 /\
scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j fsc
has_arrived j t
move : AT_T1 => [EQ_T1 SCHED_AT'].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T1 : t = t1 SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j fsc
has_arrived j t
apply fsc_respects_has_arrived.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T1 : t = t1 SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j fsc
sched (find_swap_candidate arr_seq sched t) == Some j
move : SCHED_AT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T1 : t = t1 SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j fsc
scheduled_at sched' j t ->
sched (find_swap_candidate arr_seq sched t) == Some j
rewrite EQ_T1 /SCHED_AT' /sched' -/t2.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T1 : t = t1 SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j fsc
scheduled_at (swapped sched t1 fsc) j t1 ->
sched t2 == Some j
rewrite EQ_T1 in SCHED_AT'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T1 : t = t1 SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t1 =
scheduled_at sched j fsc
scheduled_at (swapped sched t1 fsc) j t1 ->
sched t2 == Some j
rewrite SCHED_AT' /scheduled_at.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T1 : t = t1 SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t1 =
scheduled_at sched j fsc
scheduled_in j (sched fsc) -> sched t2 == Some j
by rewrite scheduled_in_def. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t AT_T2 : t = fsc /\
scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t1
has_arrived j t
set t2 := find_swap_candidate arr_seq sched t1 in AT_T2.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat AT_T2 : t = fsc /\
scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t1
has_arrived j t
move : AT_T2 => [EQ_T2 SCHED_AT'].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T2 : t = fsc SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t1
has_arrived j t
have ORDER: t1<=t2 by apply swap_candidate_is_in_future.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T2 : t = fsc SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t1 ORDER : t1 <= t2
has_arrived j t
have READY: job_ready sched j t1.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T2 : t = fsc SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t1 ORDER : t1 <= t2
job_ready sched j t1
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T2 : t = fsc SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t1 ORDER : t1 <= t2
job_ready sched j t1
by apply : job_scheduled_implies_ready; rewrite // -SCHED_AT'. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T2 : t = fsc SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t1 ORDER : t1 <= t2 READY : job_ready sched j t1
has_arrived j t
rewrite /job_ready /basic_ready_instance /pending /completed_by in READY.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T2 : t = fsc SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t1 ORDER : t1 <= t2 READY : has_arrived j t1 &&
~~ (job_cost j <= service sched j t1)
has_arrived j t
move : READY => /andP [ARR _].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T2 : t = fsc SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t1 ORDER : t1 <= t2 ARR : has_arrived j t1
has_arrived j t
rewrite EQ_T2.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat EQ_T2 : t = fsc SCHED_AT' : scheduled_at (swapped sched t1 fsc) j t =
scheduled_at sched j t1 ORDER : t1 <= t2 ARR : has_arrived j t1
has_arrived j fsc
exact : (leq_trans ARR).
Qed .
(** Finally we show that, in the transformed schedule, jobs are scheduled
only if they are ready. *)
Lemma fsc_jobs_must_be_ready_to_execute :
jobs_must_be_ready_to_execute sched'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job)
jobs_must_be_ready_to_execute sched'
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job)
jobs_must_be_ready_to_execute sched'
move => j t SCHED_AT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t
job_ready sched' j t
rewrite /sched'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t
job_ready (swapped sched t1 fsc) j t
set t2 := find_swap_candidate arr_seq sched t1.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat
job_ready (swapped sched t1 fsc) j t
rewrite /job_ready /basic_ready_instance /pending.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat
has_arrived j t &&
~~ completed_by (swapped sched t1 fsc) j t
apply /andP; split ; first by apply swap_jobs_must_arrive_to_execute.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat
~~ completed_by (swapped sched t1 fsc) j t
rewrite /completed_by; rewrite -ltnNge.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat
service (swapped sched t1 fsc) j t < job_cost j
apply swapped_completed_jobs_dont_execute => //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat
t1 <= fsc
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat
t1 <= fsc
exact : swap_candidate_is_in_future.
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_jobs_must_be_ready : jobs_must_be_ready_to_execute
sched t1 : instant fsc := find_swap_candidate arr_seq sched t1 : nat sched' := swapped sched t1 fsc : schedule (processor_state Job) j : Job t : instant SCHED_AT : scheduled_at sched' j t t2 := find_swap_candidate arr_seq sched t1 : nat
completed_jobs_dont_execute sched
exact : completed_jobs_are_not_ready.
Qed .
End JobsMustBeReadyFindSwapCandidate .
(** In the following section, we put our attention on the point-wise
transformation performed at each point in time prior to the horizon. *)
Section MakeWCAtFacts .
(** Consider an ideal uniprocessor schedule... *)
Variable sched : schedule (ideal.processor_state Job).
(** ...and take an arbitrary point in time... *)
Variable t : instant.
(** ...we define [sched'] as the resulting schedule after one point-wise transformation. *)
Let sched' := make_wc_at arr_seq sched t.
(** We start by proving that the point-wise transformation can only lead
to higher service for a job at a given time. This is true because we
swap only idle processor states with ones in which a job is scheduled. *)
Lemma mwa_service_bound :
forall j t , service sched j t <= service sched' j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
forall (j : Job) (t : instant),
service sched j t <= service sched' j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
forall (j : Job) (t : instant),
service sched j t <= service sched' j t
intros j t'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant
service sched j t' <= service sched' j t'
rewrite /sched' /make_wc_at.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant
service sched j t' <=
service
match sched t with
| Some _ => sched
| None =>
swapped sched t
(find_swap_candidate arr_seq sched t)
end j t'
destruct (sched t) eqn :PSTATE => //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant PSTATE : sched t = None
service sched j t' <=
service
(swapped sched t
(find_swap_candidate arr_seq sched t)) j t'
set t2:= (find_swap_candidate arr_seq sched t).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant PSTATE : sched t = None t2 := find_swap_candidate arr_seq sched t : nat
service sched j t' <=
service (swapped sched t t2) j t'
move : (swap_candidate_is_in_future sched t) => ORDER.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant PSTATE : sched t = None t2 := find_swap_candidate arr_seq sched t : nat ORDER : t <= find_swap_candidate arr_seq sched t
service sched j t' <=
service (swapped sched t t2) j t'
destruct (leqP t' t) as [BOUND1|BOUND1];
first by rewrite (service_before_swap_invariant _ t t2) => //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant PSTATE : sched t = None t2 := find_swap_candidate arr_seq sched t : nat ORDER : t <= find_swap_candidate arr_seq sched t BOUND1 : t < t'
service sched j t' <=
service (swapped sched t t2) j t'
destruct (ltnP t2 t') as [BOUND2 | BOUND2];
first by rewrite (service_after_swap_invariant _ t t2) => //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant PSTATE : sched t = None t2 := find_swap_candidate arr_seq sched t : nat ORDER : t <= find_swap_candidate arr_seq sched t BOUND1 : t < t' BOUND2 : t' <= t2
service sched j t' <=
service (swapped sched t t2) j t'
destruct (scheduled_at sched j t) eqn :SCHED_AT_T1;
first by move :SCHED_AT_T1; rewrite scheduled_at_def PSTATE => /eqP.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant PSTATE : sched t = None t2 := find_swap_candidate arr_seq sched t : nat ORDER : t <= find_swap_candidate arr_seq sched t BOUND1 : t < t' BOUND2 : t' <= t2 SCHED_AT_T1 : scheduled_at sched j t = false
service sched j t' <=
service (swapped sched t t2) j t'
move : SCHED_AT_T1 => /negbT NOT_AT_t1.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant PSTATE : sched t = None t2 := find_swap_candidate arr_seq sched t : nat ORDER : t <= find_swap_candidate arr_seq sched t BOUND1 : t < t' BOUND2 : t' <= t2 NOT_AT_t1 : ~~ scheduled_at sched j t
service sched j t' <=
service (swapped sched t t2) j t'
destruct (scheduled_at sched j t2) eqn :SCHED_AT_T2;
last by move : SCHED_AT_T2 => /negbT NOT_AT_t2; rewrite (service_of_others_invariant _ t t2).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant PSTATE : sched t = None t2 := find_swap_candidate arr_seq sched t : nat ORDER : t <= find_swap_candidate arr_seq sched t BOUND1 : t < t' BOUND2 : t' <= t2 NOT_AT_t1 : ~~ scheduled_at sched j t SCHED_AT_T2 : scheduled_at sched j t2 = true
service sched j t' <=
service (swapped sched t t2) j t'
rewrite /swapped /service -service_at_other_times_invariant; last by left .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant PSTATE : sched t = None t2 := find_swap_candidate arr_seq sched t : nat ORDER : t <= find_swap_candidate arr_seq sched t BOUND1 : t < t' BOUND2 : t' <= t2 NOT_AT_t1 : ~~ scheduled_at sched j t SCHED_AT_T2 : scheduled_at sched j t2 = true
service_during sched j 0 t' <=
service_during (replace_at sched t (sched t2)) j 0 t'
rewrite service_in_replaced; last by apply /andP; split => //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant PSTATE : sched t = None t2 := find_swap_candidate arr_seq sched t : nat ORDER : t <= find_swap_candidate arr_seq sched t BOUND1 : t < t' BOUND2 : t' <= t2 NOT_AT_t1 : ~~ scheduled_at sched j t SCHED_AT_T2 : scheduled_at sched j t2 = true
service_during sched j 0 t' <=
service_during sched j 0 t' +
service_at (replace_at sched t (sched t2)) j t -
service_at sched j t
rewrite (not_scheduled_implies_no_service _ _ _ NOT_AT_t1) subn0.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant PSTATE : sched t = None t2 := find_swap_candidate arr_seq sched t : nat ORDER : t <= find_swap_candidate arr_seq sched t BOUND1 : t < t' BOUND2 : t' <= t2 NOT_AT_t1 : ~~ scheduled_at sched j t SCHED_AT_T2 : scheduled_at sched j t2 = true
service_during sched j 0 t' <=
service_during sched j 0 t' +
service_at (replace_at sched t (sched t2)) j t
by apply leq_addr.
Qed .
(** Next, we show that any ready job in the transformed schedule must be ready also in
the original one, since the transformation can only lead to higher service. *)
Lemma mwa_ready_job_also_ready_in_original_schedule :
forall j t , job_ready sched' j t -> job_ready sched j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
forall (j : Job) (t : instant),
job_ready sched' j t -> job_ready sched j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
forall (j : Job) (t : instant),
job_ready sched' j t -> job_ready sched j t
intros j t'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant
job_ready sched' j t' -> job_ready sched j t'
rewrite /job_ready /basic_ready_instance /pending.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant
has_arrived j t' && ~~ completed_by sched' j t' ->
has_arrived j t' && ~~ completed_by sched j t'
move => /andP [ARR COMP_BY].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant ARR : has_arrived j t' COMP_BY : ~~ completed_by sched' j t'
has_arrived j t' && ~~ completed_by sched j t'
rewrite ARR Bool.andb_true_l //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant ARR : has_arrived j t' COMP_BY : ~~ completed_by sched' j t'
~~ completed_by sched j t'
move : COMP_BY; apply contra.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant ARR : has_arrived j t'
completed_by sched j t' -> completed_by sched' j t'
rewrite /completed_by.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant ARR : has_arrived j t'
job_cost j <= service sched j t' ->
job_cost j <= service sched' j t'
have LEQ: (service sched j t') <= (service sched' j t') by apply mwa_service_bound.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant ARR : has_arrived j t' LEQ : service sched j t' <= service sched' j t'
job_cost j <= service sched j t' ->
job_cost j <= service sched' j t'
move => LEQ'; move :LEQ; move : LEQ'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : instant ARR : has_arrived j t'
job_cost j <= service sched j t' ->
service sched j t' <= service sched' j t' ->
job_cost j <= service sched' j t'
by apply leq_trans.
Qed .
(** Since the search for a swap candidate is performed until the latest deadline
among all the jobs arrived before the reference time, we need to show that the computed
deadline is indeed the latest. *)
Lemma max_dl_is_greatest_dl :
forall j t ,
arrives_in arr_seq j ->
job_arrival j <= t ->
job_deadline j <= max_deadline_for_jobs_arrived_before arr_seq t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
forall (j : Job) (t : nat),
arrives_in arr_seq j ->
job_arrival j <= t ->
job_deadline j <=
max_deadline_for_jobs_arrived_before arr_seq t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
forall (j : Job) (t : nat),
arrives_in arr_seq j ->
job_arrival j <= t ->
job_deadline j <=
max_deadline_for_jobs_arrived_before arr_seq t
move => j t' ARR_IN ARR.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : nat ARR_IN : arrives_in arr_seq j ARR : job_arrival j <= t'
job_deadline j <=
max_deadline_for_jobs_arrived_before arr_seq t'
rewrite /max_deadline_for_jobs_arrived_before.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : nat ARR_IN : arrives_in arr_seq j ARR : job_arrival j <= t'
job_deadline j <=
max0
[seq job_deadline i
| i <- arrivals_up_to arr_seq t']
apply in_max0_le; apply map_f.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : nat ARR_IN : arrives_in arr_seq j ARR : job_arrival j <= t'
j \in arrivals_up_to arr_seq t'
rewrite /arrivals_up_to.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job t' : nat ARR_IN : arrives_in arr_seq j ARR : job_arrival j <= t'
j \in arrivals_between arr_seq 0 t'.+1
apply arrived_between_implies_in_arrivals;
by move :H_arr_seq_valid => [CONS UNIQ].
Qed .
(** Next, we want to show that, if a job arriving from the arrival
sequence is ready at some instant, then the point-wise transformation
is guaranteed to find a job to swap with. We will proceed by doing a case
analysis, and show that it is impossible that a swap candidate is not found. *)
Section MakeWCAtFindsReadyJobs .
(** We need to assume that, in the original schedule, all the deadlines of
the jobs coming from the arrival sequence are met, in order to be sure that
a ready job will be eventually scheduled. *)
Hypothesis H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met arr_seq sched.
(** We define [max_dl] as the maximum deadline for all jobs arrived before [t]. *)
Let max_dl := max_deadline_for_jobs_arrived_before arr_seq t.
(** Next, we define [search_result] as the result of the search for a swap candidate.
In order to take the first result, it is sufficient to define the ordering function
as a constant false. *)
Definition order (_ _ : nat) := false.
Definition search_result := search_arg sched (relevant_pstate t) order t max_dl.
(** First, we consider the case in which the procedure finds a job to swap with. *)
Section MakeWCAtFindsReadyJobs_CaseResultFound .
(** Assuming that the processor is idle at time t... *)
Hypothesis H_sched_t_idle : ideal_is_idle sched t.
(** ...let [t_swap] be a time instant found by the search procedure. *)
Variable t_swap : instant.
Hypothesis search_result_found : search_result = Some t_swap.
(** We show that, since the search only yields relevant processor states, a job is found. *)
Lemma make_wc_at_case_result_found :
exists j : Job,
swapped sched t t_swap t = Some j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_sched_t_idle : ideal_is_idle sched t t_swap : instant search_result_found : search_result = Some t_swap
exists j : Job, swapped sched t t_swap t = Some j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_sched_t_idle : ideal_is_idle sched t t_swap : instant search_result_found : search_result = Some t_swap
exists j : Job, swapped sched t t_swap t = Some j
apply search_arg_pred in search_result_found.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_sched_t_idle : ideal_is_idle sched t t_swap : instant search_result_found : relevant_pstate t (sched t_swap)
exists j : Job, swapped sched t t_swap t = Some j
move :search_result_found; rewrite /relevant_pstate.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_sched_t_idle : ideal_is_idle sched t t_swap : instant search_result_found : relevant_pstate t (sched t_swap)
match sched t_swap with
| Some j => job_arrival j <= t
| None => false
end ->
exists j : Job, swapped sched t t_swap t = Some j
destruct (sched t_swap) as [j_swap|] eqn :SCHED => [|//].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_sched_t_idle : ideal_is_idle sched t t_swap : instant j_swap : Job SCHED : sched t_swap = Some j_swap search_result_found : relevant_pstate t (Some j_swap)
job_arrival j_swap <= t ->
exists j : Job, swapped sched t t_swap t = Some j
move =>ARR.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_sched_t_idle : ideal_is_idle sched t t_swap : instant j_swap : Job SCHED : sched t_swap = Some j_swap search_result_found : relevant_pstate t (Some j_swap) ARR : job_arrival j_swap <= t
exists j : Job, swapped sched t t_swap t = Some j
rewrite /swapped /replace_at.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_sched_t_idle : ideal_is_idle sched t t_swap : instant j_swap : Job SCHED : sched t_swap = Some j_swap search_result_found : relevant_pstate t (Some j_swap) ARR : job_arrival j_swap <= t
exists j : Job,
(if t_swap == t
then sched t
else if t == t then sched t_swap else sched t) =
Some j
destruct (t_swap == t) eqn :SAME_SWAP.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_sched_t_idle : ideal_is_idle sched t t_swap : instant j_swap : Job SCHED : sched t_swap = Some j_swap search_result_found : relevant_pstate t (Some j_swap) ARR : job_arrival j_swap <= t SAME_SWAP : (t_swap == t) = true
exists j : Job, sched t = Some j
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_sched_t_idle : ideal_is_idle sched t t_swap : instant j_swap : Job SCHED : sched t_swap = Some j_swap search_result_found : relevant_pstate t (Some j_swap) ARR : job_arrival j_swap <= t SAME_SWAP : (t_swap == t) = true
exists j : Job, sched t = Some j
move :SAME_SWAP => /eqP SAME_SWAP; subst t_swap.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_sched_t_idle : ideal_is_idle sched t j_swap : Job SCHED : sched t = Some j_swap search_result_found : relevant_pstate t (Some j_swap) ARR : job_arrival j_swap <= t
exists j : Job, sched t = Some j
move :H_sched_t_idle => /eqP SCHED_NONE.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_sched_t_idle : ideal_is_idle sched t j_swap : Job SCHED : sched t = Some j_swap search_result_found : relevant_pstate t (Some j_swap) ARR : job_arrival j_swap <= t SCHED_NONE : sched t = None
exists j : Job, sched t = Some j
by rewrite SCHED_NONE in SCHED; discriminate .
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_sched_t_idle : ideal_is_idle sched t t_swap : instant j_swap : Job SCHED : sched t_swap = Some j_swap search_result_found : relevant_pstate t (Some j_swap) ARR : job_arrival j_swap <= t SAME_SWAP : (t_swap == t) = false
exists j : Job,
(if t == t then sched t_swap else sched t) = Some j
by exists j_swap ; rewrite eq_refl; apply SCHED.
Qed .
End MakeWCAtFindsReadyJobs_CaseResultFound .
(** Conversely, we prove that assuming that the search yields no
result brings to a contradiction. *)
Section MakeWCAtFindsReadyJobs_CaseResultNone .
(** Consider a job that arrives in the arrival sequence, and assume that
it is ready at time [t] in the transformed schedule. *)
Variable j : Job.
Hypothesis H_arrives_in : arrives_in arr_seq j.
Hypothesis H_job_ready_sched' : job_ready sched' j t.
(** Moreover, assume the search for a swap candidate yields nothing. *)
Hypothesis H_search_result_none : search_result = None.
(** First, note that, since nothing was found, it means there is no relevant
processor state between [t] and [max_dl]. *)
Lemma no_relevant_state_in_range :
forall t' ,
t <= t' < max_dl ->
~~ (relevant_pstate t) (sched t').Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
forall t' : nat,
t <= t' < max_dl -> ~~ relevant_pstate t (sched t')
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
forall t' : nat,
t <= t' < max_dl -> ~~ relevant_pstate t (sched t')
by apply (search_arg_none _ _ (fun _ _ => false)).
Qed .
(** Since [j] is ready at time [t], then it must be incomplete. *)
Lemma service_of_j_is_less_than_cost : service sched j t < job_cost j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
service sched j t < job_cost j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
service sched j t < job_cost j
have READY_ORIG: job_ready sched j t
by apply (mwa_ready_job_also_ready_in_original_schedule _ _); apply H_job_ready_sched'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None READY_ORIG : job_ready sched j t
service sched j t < job_cost j
rewrite /job_ready /basic_ready_instance /pending.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None READY_ORIG : job_ready sched j t
service sched j t < job_cost j
move :READY_ORIG => /andP [ARR_ NOT_COMPL_ORIG].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR_ : has_arrived j t NOT_COMPL_ORIG : ~~ completed_by sched j t
service sched j t < job_cost j
rewrite /completed_by in NOT_COMPL_ORIG.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR_ : has_arrived j t NOT_COMPL_ORIG : ~~ (job_cost j <= service sched j t)
service sched j t < job_cost j
by rewrite leqNgt; apply NOT_COMPL_ORIG.
Qed .
(** And since [j] is incomplete and meets its deadline, the deadline of [j]
is in the future. *)
Lemma t_is_less_than_deadline_of_j : t <= job_deadline j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
t <= job_deadline j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
t <= job_deadline j
move : (H_all_deadlines_of_arrivals_met j H_arrives_in)=> MEETS_DL_j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None MEETS_DL_j : job_meets_deadline sched j
t <= job_deadline j
move_neq_up LEQ_t1. Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None MEETS_DL_j : job_meets_deadline sched j LEQ_t1 : job_deadline j < t
False
unfold job_meets_deadline, completed_by in MEETS_DL_j; move_neq_down MEETS_DL_j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None LEQ_t1 : job_deadline j < t
service sched j (job_deadline j) < job_cost j
eapply leq_ltn_trans; last apply service_of_j_is_less_than_cost.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None LEQ_t1 : job_deadline j < t
service sched j (job_deadline j) <= service sched j t
by apply service_monotonic, ltnW.
Qed .
(** On the other hand, since we know that there is no relevant state between [t] and [max_dl],
then it must be the case that [j] is never scheduled in this period, and hence gets no
service. *)
Lemma equal_service_t_max_dl : service sched j t = service sched j max_dl.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
service sched j t = service sched j max_dl
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
service sched j t = service sched j max_dl
move :(H_job_ready_sched') => /andP [ARR NOT_COMPL_sched'].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t
service sched j t = service sched j max_dl
rewrite -(service_cat sched j t max_dl);
last by apply (leq_trans t_is_less_than_deadline_of_j), max_dl_is_greatest_dl.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t
service sched j t =
service sched j t + service_during sched j t max_dl
have ZERO_SERVICE: service_during sched j t max_dl = 0 .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t
service_during sched j t max_dl = 0
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t
service_during sched j t max_dl = 0
apply not_scheduled_during_implies_zero_service.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t
forall t0 : nat,
t <= t0 < max_dl -> ~~ scheduled_at sched j t0
move => t_at RANGE.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t t_at : nat RANGE : t <= t_at < max_dl
~~ scheduled_at sched j t_at
move :(no_relevant_state_in_range t_at RANGE) => NOT_REL.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t t_at : nat RANGE : t <= t_at < max_dl NOT_REL : ~~ relevant_pstate t (sched t_at)
~~ scheduled_at sched j t_at
rewrite scheduled_at_def.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t t_at : nat RANGE : t <= t_at < max_dl NOT_REL : ~~ relevant_pstate t (sched t_at)
sched t_at != Some j
apply /negP; move => /eqP EQ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t t_at : nat RANGE : t <= t_at < max_dl NOT_REL : ~~ relevant_pstate t (sched t_at) EQ : sched t_at = Some j
False
by move : NOT_REL => /negP T; apply : T; rewrite EQ.
} Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t ZERO_SERVICE : service_during sched j t max_dl = 0
service sched j t =
service sched j t + service_during sched j t max_dl
by rewrite ZERO_SERVICE; rewrite addn0.
Qed .
(** Combining the previous lemmas, we can deduce that [j] misses its deadline. *)
Lemma j_misses_deadline : service sched j (job_deadline j) < job_cost j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
service sched j (job_deadline j) < job_cost j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
service sched j (job_deadline j) < job_cost j
move :(H_job_ready_sched') => /andP [ARR NOT_COMPL_sched'].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t
service sched j (job_deadline j) < job_cost j
have J_LESS := service_of_j_is_less_than_cost.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t J_LESS : service sched j t < job_cost j
service sched j (job_deadline j) < job_cost j
rewrite equal_service_t_max_dl in J_LESS.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t J_LESS : service sched j max_dl < job_cost j
service sched j (job_deadline j) < job_cost j
specialize (H_all_deadlines_of_arrivals_met j H_arrives_in).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job H_all_deadlines_of_arrivals_met : job_meets_deadline
sched j max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t J_LESS : service sched j max_dl < job_cost j
service sched j (job_deadline j) < job_cost j
unfold job_meets_deadline, completed_by in H_all_deadlines_of_arrivals_met.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job H_all_deadlines_of_arrivals_met : job_cost j <=
service sched j
(job_deadline j) max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t J_LESS : service sched j max_dl < job_cost j
service sched j (job_deadline j) < job_cost j
eapply leq_ltn_trans.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job H_all_deadlines_of_arrivals_met : job_cost j <=
service sched j
(job_deadline j) max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t J_LESS : service sched j max_dl < job_cost j
service sched j (job_deadline j) <= ?n
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job H_all_deadlines_of_arrivals_met : job_cost j <=
service sched j
(job_deadline j) max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t J_LESS : service sched j max_dl < job_cost j
service sched j (job_deadline j) <= ?n
by apply service_monotonic, (max_dl_is_greatest_dl _ _ H_arrives_in ARR).
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job H_all_deadlines_of_arrivals_met : job_cost j <=
service sched j
(job_deadline j) max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None ARR : has_arrived j t NOT_COMPL_sched' : ~~ completed_by sched' j t J_LESS : service sched j max_dl < job_cost j
service sched j
(max_deadline_for_jobs_arrived_before arr_seq t) <
job_cost j
by apply J_LESS.
Qed .
(** The fact that [j] misses its deadline contradicts the fact that all deadlines
of jobs coming from the arrival sequence are met. We have a contradiction. *)
Lemma make_wc_at_case_result_none : False .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
False
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
False
move : (H_all_deadlines_of_arrivals_met j H_arrives_in) => NEQ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None NEQ : job_meets_deadline sched j
False
unfold job_meets_deadline, completed_by in NEQ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None NEQ : job_cost j <= service sched j (job_deadline j)
False
move_neq_down NEQ. Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat j : Job H_arrives_in : arrives_in arr_seq j H_job_ready_sched' : job_ready sched' j t H_search_result_none : search_result = None
service sched j (job_deadline j) < job_cost j
by apply j_misses_deadline.
Qed .
End MakeWCAtFindsReadyJobs_CaseResultNone .
(** Next, we show that [make_wc_at] always manages to establish the work-conservation property
at the given time. Using the above case analysis, we can conclude that the presence of a
ready job always leads to a valid swap. *)
Lemma mwa_finds_ready_jobs :
all_deadlines_of_arrivals_met arr_seq sched ->
is_work_conserving_at sched' t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat
all_deadlines_of_arrivals_met arr_seq sched ->
is_work_conserving_at sched' t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat
all_deadlines_of_arrivals_met arr_seq sched ->
is_work_conserving_at sched' t
move => ALL_DL_MET P_PREFIX.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat ALL_DL_MET : all_deadlines_of_arrivals_met arr_seq
sched P_PREFIX : exists j : Job,
arrives_in arr_seq j /\
job_ready sched' j t
exists j : Job, sched' t = Some j
destruct (sched t) as [j'|] eqn :SCHED_WC_t;
first by rewrite /sched' /make_wc_at SCHED_WC_t; exists j' .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat ALL_DL_MET : all_deadlines_of_arrivals_met arr_seq
sched P_PREFIX : exists j : Job,
arrives_in arr_seq j /\
job_ready sched' j tSCHED_WC_t : sched t = None
exists j : Job, sched' t = Some j
move : P_PREFIX => [j [ARR_IN READY]].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat ALL_DL_MET : all_deadlines_of_arrivals_met arr_seq
sched SCHED_WC_t : sched t = None j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t
exists j : Job, sched' t = Some j
rewrite /sched' /make_wc_at.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat ALL_DL_MET : all_deadlines_of_arrivals_met arr_seq
sched SCHED_WC_t : sched t = None j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t
exists j : Job,
match sched t with
| Some _ => sched
| None =>
swapped sched t
(find_swap_candidate arr_seq sched t)
end t = Some j
rewrite SCHED_WC_t /find_swap_candidate.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat ALL_DL_MET : all_deadlines_of_arrivals_met arr_seq
sched SCHED_WC_t : sched t = None j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t
exists j : Job,
swapped sched t
match
search_arg sched (relevant_pstate t)
(fun => xpred0) t
(max_deadline_for_jobs_arrived_before arr_seq
t)
with
| Some t_swap => t_swap
| None => t
end t = Some j
destruct search_arg as [t_swap| ] eqn :SEARCH_RES.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat ALL_DL_MET : all_deadlines_of_arrivals_met arr_seq
sched SCHED_WC_t : sched t = None j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t t_swap : nat SEARCH_RES : search_arg sched
(relevant_pstate t)
(fun => xpred0) t
(max_deadline_for_jobs_arrived_before
arr_seq t) =
Some t_swap
exists j : Job, swapped sched t t_swap t = Some j
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat ALL_DL_MET : all_deadlines_of_arrivals_met arr_seq
sched SCHED_WC_t : sched t = None j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t t_swap : nat SEARCH_RES : search_arg sched
(relevant_pstate t)
(fun => xpred0) t
(max_deadline_for_jobs_arrived_before
arr_seq t) =
Some t_swap
exists j : Job, swapped sched t t_swap t = Some j
by apply make_wc_at_case_result_found; move :SCHED_WC_t => /eqP.
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched max_dl := max_deadline_for_jobs_arrived_before arr_seq t : nat ALL_DL_MET : all_deadlines_of_arrivals_met arr_seq
sched SCHED_WC_t : sched t = None j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t SEARCH_RES : search_arg sched
(relevant_pstate t)
(fun => xpred0) t
(max_deadline_for_jobs_arrived_before
arr_seq t) = None
exists j : Job, swapped sched t t t = Some j
by exfalso ; apply (make_wc_at_case_result_none j); eauto .
Qed .
End MakeWCAtFindsReadyJobs .
(** Next we prove that, given a schedule that respects the work-conservation property until [t-1],
applying the point-wise transformation at time [t] will extend the property until [t]. *)
Lemma mwa_establishes_wc :
all_deadlines_of_arrivals_met arr_seq sched ->
(forall t_l , t_l < t -> is_work_conserving_at sched t_l) ->
forall t_l , t_l <= t -> is_work_conserving_at sched' t_l.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
all_deadlines_of_arrivals_met arr_seq sched ->
(forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_l) ->
forall t_l : nat,
t_l <= t -> is_work_conserving_at sched' t_l
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
all_deadlines_of_arrivals_met arr_seq sched ->
(forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_l) ->
forall t_l : nat,
t_l <= t -> is_work_conserving_at sched' t_l
move => PROP P_PREFIX t' T_MIN [j [ARR_IN READY]].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t'
exists j : Job, sched' t' = Some j
set fsc := find_swap_candidate arr_seq sched t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat
exists j : Job, sched' t' = Some j
have LEQ_fsc: t <= fsc by apply swap_candidate_is_in_future.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc
exists j : Job, sched' t' = Some j
destruct (ltnP t' t) as [tLT | tGE].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tLT : t' < t
exists j : Job, sched' t' = Some j
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tLT : t' < t
exists j : Job, sched' t' = Some j
have SAME: sched' t' = sched t'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tLT : t' < t
sched' t' = sched t'
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tLT : t' < t
sched' t' = sched t'
rewrite /sched' /make_wc_at.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tLT : t' < t
match sched t with
| Some _ => sched
| None =>
swapped sched t
(find_swap_candidate arr_seq sched t)
end t' = sched t'
destruct (sched t) => [//|].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tLT : t' < t
swapped sched t (find_swap_candidate arr_seq sched t)
t' = sched t'
by rewrite (swap_before_invariant sched t fsc). } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tLT : t' < t SAME : sched' t' = sched t'
exists j : Job, sched' t' = Some j
rewrite SAME.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tLT : t' < t SAME : sched' t' = sched t'
exists j : Job, sched t' = Some j
apply P_PREFIX; eauto .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tLT : t' < t SAME : sched' t' = sched t'
exists j : Job,
arrives_in arr_seq j /\ job_ready sched j t'
exists j ; split ; auto .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tLT : t' < t SAME : sched' t' = sched t'
job_ready sched j t'
by eapply mwa_ready_job_also_ready_in_original_schedule, READY.
} Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tGE : t <= t'
exists j : Job, sched' t' = Some j
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tGE : t <= t'
exists j : Job, sched' t' = Some j
have EQ: t' = t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tGE : t <= t'
t' = t
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tGE : t <= t'
t' = t
by apply /eqP; rewrite eqn_leq; apply /andP; split . } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lt' : nat T_MIN : t' <= t j : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t' fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc tGE : t <= t' EQ : t' = t
exists j : Job, sched' t' = Some j
subst t'; clear T_MIN tGE.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) PROP : all_deadlines_of_arrivals_met arr_seq sched P_PREFIX : forall t_l : nat,
t_l < t -> is_work_conserving_at sched t_lj : Job ARR_IN : arrives_in arr_seq j READY : job_ready sched' j t fsc := find_swap_candidate arr_seq sched t : nat LEQ_fsc : t <= fsc
exists j : Job, sched' t = Some j
exact : mwa_finds_ready_jobs. }
Qed .
(** We now show that the point-wise transformation does not introduce any new job
that does not come from the arrival sequence. *)
Lemma mwa_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence sched' arr_seq.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence sched' arr_seq
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence sched' arr_seq
rewrite /sched' /make_wc_at.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence
match sched t with
| Some _ => sched
| None =>
swapped sched t
(find_swap_candidate arr_seq sched t)
end arr_seq
destruct (sched t) as [j_orig|] eqn :SCHED_orig => [//|].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) SCHED_orig : sched t = None
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence
(swapped sched t
(find_swap_candidate arr_seq sched t)) arr_seq
exact : swapped_jobs_come_from_arrival_sequence.
Qed .
(** We also show that the point-wise transformation does not schedule jobs in instants
in which they are not ready. *)
Lemma mwa_jobs_must_be_ready_to_execute :
jobs_must_be_ready_to_execute sched ->
jobs_must_be_ready_to_execute sched'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
jobs_must_be_ready_to_execute sched ->
jobs_must_be_ready_to_execute sched'
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
jobs_must_be_ready_to_execute sched ->
jobs_must_be_ready_to_execute sched'
move => READY.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) READY : jobs_must_be_ready_to_execute sched
jobs_must_be_ready_to_execute sched'
rewrite /sched' /make_wc_at.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) READY : jobs_must_be_ready_to_execute sched
jobs_must_be_ready_to_execute
match sched t with
| Some _ => sched
| None =>
swapped sched t
(find_swap_candidate arr_seq sched t)
end
destruct (sched t) as [j_orig|] eqn :SCHED_orig => [//|].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) READY : jobs_must_be_ready_to_execute sched SCHED_orig : sched t = None
jobs_must_be_ready_to_execute
(swapped sched t
(find_swap_candidate arr_seq sched t))
exact : fsc_jobs_must_be_ready_to_execute.
Qed .
(** Finally, we show that the point-wise transformation does not introduce deadline misses. *)
Lemma mwa_all_deadlines_of_arrivals_met :
all_deadlines_of_arrivals_met arr_seq sched ->
all_deadlines_of_arrivals_met arr_seq sched'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
all_deadlines_of_arrivals_met arr_seq sched ->
all_deadlines_of_arrivals_met arr_seq sched'
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job)
all_deadlines_of_arrivals_met arr_seq sched ->
all_deadlines_of_arrivals_met arr_seq sched'
move => ALL j ARR.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) ALL : all_deadlines_of_arrivals_met arr_seq sched j : Job ARR : arrives_in arr_seq j
job_meets_deadline sched' j
specialize (ALL j ARR).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job ALL : job_meets_deadline sched j ARR : arrives_in arr_seq j
job_meets_deadline sched' j
unfold job_meets_deadline, completed_by in *.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) t : instant sched' := make_wc_at arr_seq sched t : schedule (processor_state Job) j : Job ALL : job_cost j <= service sched j (job_deadline j) ARR : arrives_in arr_seq j
job_cost j <= service sched' j (job_deadline j)
by apply (leq_trans ALL (mwa_service_bound _ _)).
Qed .
End MakeWCAtFacts .
(** In the following section, we proceed by proving some useful properties respected by
the partial schedule obtained by applying the work-conservation transformation up to
an arbitrary horizon. *)
Section PrefixFacts .
(** Consider an ideal uniprocessor schedule. *)
Variable sched : schedule (ideal.processor_state Job).
(** We start by proving that the transformation performed with two different horizons
will yield two schedules that are identical until the earlier horizon. *)
Section PrefixInclusion .
(** Consider two horizons... *)
Variable h1 h2 : instant.
(** ...and assume w.l.o.g. that they are ordered... *)
Hypothesis H_horizon_order : h1 <= h2.
(** ...we define two schedules, resulting from the transformation
performed, respectively, until the first and the second horizon. *)
Let sched1 := wc_transform_prefix arr_seq sched h1.
Let sched2 := wc_transform_prefix arr_seq sched h2.
(** Then, we show that the two schedules are guaranteed to be equal until the
earlier horizon. *)
Lemma wc_transform_prefix_inclusion :
forall t , t < h1 -> sched1 t = sched2 t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job)
forall t : nat, t < h1 -> sched1 t = sched2 t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job)
forall t : nat, t < h1 -> sched1 t = sched2 t
move => t before_horizon.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1
sched1 t = sched2 t
rewrite /sched1 /sched2.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched h2 t
elim : h2 H_horizon_order => [|i IHi] horizon_order;
first by move : (leq_trans before_horizon horizon_order).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1 i : nat IHi : h1 <= i ->
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i t horizon_order : h1 <= i.+1
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i.+1 t
move : horizon_order; rewrite leq_eqVlt => /orP [/eqP-> // | LT].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1 i : nat IHi : h1 <= i ->
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i t LT : h1 < i.+1
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i.+1 t
move : LT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1 i : nat IHi : h1 <= i ->
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i t
h1 < i.+1 ->
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i.+1 t
rewrite ltnS => H_horizon_order_lt.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1 i : nat IHi : h1 <= i ->
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i t H_horizon_order_lt : h1 <= i
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i.+1 t
rewrite [RHS]/wc_transform_prefix /prefix_map -/prefix_map IHi //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1 i : nat IHi : h1 <= i ->
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i t H_horizon_order_lt : h1 <= i
wc_transform_prefix arr_seq sched i t =
make_wc_at arr_seq
(prefix_map sched (make_wc_at arr_seq) i) i t
rewrite {1 }/make_wc_at.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1 i : nat IHi : h1 <= i ->
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i t H_horizon_order_lt : h1 <= i
wc_transform_prefix arr_seq sched i t =
match prefix_map sched (make_wc_at arr_seq) i i with
| Some _ => prefix_map sched (make_wc_at arr_seq) i
| None =>
swapped (prefix_map sched (make_wc_at arr_seq) i)
i
(find_swap_candidate arr_seq
(prefix_map sched (make_wc_at arr_seq) i) i)
end t
destruct (prefix_map sched (make_wc_at arr_seq) i i) as [j|] eqn :SCHED => [//|].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1 i : nat IHi : h1 <= i ->
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i t H_horizon_order_lt : h1 <= i SCHED : prefix_map sched (make_wc_at arr_seq) i i =
None
wc_transform_prefix arr_seq sched i t =
swapped (prefix_map sched (make_wc_at arr_seq) i) i
(find_swap_candidate arr_seq
(prefix_map sched (make_wc_at arr_seq) i) i) t
rewrite -(swap_before_invariant _ i (find_swap_candidate arr_seq (wc_transform_prefix arr_seq sched i) i)).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1 i : nat IHi : h1 <= i ->
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i t H_horizon_order_lt : h1 <= i SCHED : prefix_map sched (make_wc_at arr_seq) i i =
None
wc_transform_prefix arr_seq sched i t =
prefix_map sched (make_wc_at arr_seq) i t
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1 i : nat IHi : h1 <= i ->
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i t H_horizon_order_lt : h1 <= i SCHED : prefix_map sched (make_wc_at arr_seq) i i =
None
wc_transform_prefix arr_seq sched i t =
prefix_map sched (make_wc_at arr_seq) i t
by [].
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1 i : nat IHi : h1 <= i ->
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i t H_horizon_order_lt : h1 <= i SCHED : prefix_map sched (make_wc_at arr_seq) i i =
None
i <=
find_swap_candidate arr_seq
(wc_transform_prefix arr_seq sched i) i
exact : swap_candidate_is_in_future.
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h1, h2 : instant H_horizon_order : h1 <= h2 sched1 := wc_transform_prefix arr_seq sched h1 : schedule (processor_state Job) sched2 := wc_transform_prefix arr_seq sched h2 : schedule (processor_state Job) t : nat before_horizon : t < h1 i : nat IHi : h1 <= i ->
wc_transform_prefix arr_seq sched h1 t =
wc_transform_prefix arr_seq sched i t H_horizon_order_lt : h1 <= i SCHED : prefix_map sched (make_wc_at arr_seq) i i =
None
t < i
by apply leq_trans with (n := h1).
Qed .
End PrefixInclusion .
(** Next, we show that repeating the point-wise transformation up to a given horizon
does not introduce any deadline miss. *)
Section JobsMeetDeadlinePrefix .
(** Assuming that all deadlines of jobs coming from the arrival sequence are met... *)
Hypothesis H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met arr_seq sched.
(** ...let us define [sched'] as the schedule resulting from the
full work-conservation transformation. Note that, if the schedule is sampled at time
[t], the transformation is performed until [t+1]. *)
Let sched' := wc_transform arr_seq sched.
(** Consider a job from the arrival sequence. *)
Variable j : Job.
Hypothesis H_arrives_in : arrives_in arr_seq j.
(** We show that, in the transformed schedule, the service of the job
is always greater or equal than in the original one, at any given time. *)
Lemma wc_prefix_service_bound :
forall t , service sched j t <= service sched' j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j
forall t : instant,
service sched j t <= service sched' j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j
forall t : instant,
service sched j t <= service sched' j t
move => t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant
service sched j t <= service sched' j t
rewrite /sched' /wc_transform.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant
service sched j t <=
service
(fun t : nat =>
wc_transform_prefix arr_seq sched t.+1 t) j t
set serv := service (fun t0 : instant => wc_transform_prefix arr_seq sched t0.+1 t0) j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant serv := service
(fun t0 : instant =>
wc_transform_prefix arr_seq sched t0.+1 t0) j
t : nat
service sched j t <= serv
set servp := service (wc_transform_prefix arr_seq sched t.+1 ) j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant serv := service
(fun t0 : instant =>
wc_transform_prefix arr_seq sched t0.+1 t0) j
t : nat servp := service
(wc_transform_prefix arr_seq sched t.+1 ) j t : nat
service sched j t <= serv
have ->: serv = servp.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant serv := service
(fun t0 : instant =>
wc_transform_prefix arr_seq sched t0.+1 t0) j
t : nat servp := service
(wc_transform_prefix arr_seq sched t.+1 ) j t : nat
serv = servp
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant serv := service
(fun t0 : instant =>
wc_transform_prefix arr_seq sched t0.+1 t0) j
t : nat servp := service
(wc_transform_prefix arr_seq sched t.+1 ) j t : nat
serv = servp
rewrite /serv /servp /service /service_during.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant serv := service
(fun t0 : instant =>
wc_transform_prefix arr_seq sched t0.+1 t0) j
t : nat servp := service
(wc_transform_prefix arr_seq sched t.+1 ) j t : nat
\sum_(0 <= t < t)
service_at
(fun t0 : instant =>
wc_transform_prefix arr_seq sched t0.+1 t0) j t =
\sum_(0 <= t0 < t)
service_at (wc_transform_prefix arr_seq sched t.+1 )
j t0
apply eq_big_nat => t' /andP [_ LT_t].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant serv := service
(fun t0 : instant =>
wc_transform_prefix arr_seq sched t0.+1 t0) j
t : nat servp := service
(wc_transform_prefix arr_seq sched t.+1 ) j t : nat t' : nat LT_t : t' < t
service_at
(fun t0 : instant =>
wc_transform_prefix arr_seq sched t0.+1 t0) j t' =
service_at (wc_transform_prefix arr_seq sched t.+1 ) j
t'
rewrite /service_at.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant serv := service
(fun t0 : instant =>
wc_transform_prefix arr_seq sched t0.+1 t0) j
t : nat servp := service
(wc_transform_prefix arr_seq sched t.+1 ) j t : nat t' : nat LT_t : t' < t
service_in j
(wc_transform_prefix arr_seq sched t'.+1 t') =
service_in j
(wc_transform_prefix arr_seq sched t.+1 t')
by rewrite (wc_transform_prefix_inclusion t'.+1 t.+1 ). } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant serv := service
(fun t0 : instant =>
wc_transform_prefix arr_seq sched t0.+1 t0) j
t : nat servp := service
(wc_transform_prefix arr_seq sched t.+1 ) j t : nat
service sched j t <= servp
rewrite /servp /wc_transform_prefix.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant serv := service
(fun t0 : instant =>
wc_transform_prefix arr_seq sched t0.+1 t0) j
t : nat servp := service
(wc_transform_prefix arr_seq sched t.+1 ) j t : nat
service sched j t <=
service (prefix_map sched (make_wc_at arr_seq) t.+1 ) j
t
clear serv servp.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant
service sched j t <=
service (prefix_map sched (make_wc_at arr_seq) t.+1 ) j
t
apply prefix_map_property_invariance => [|//].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant
forall (sched0 : schedule (processor_state Job))
(t0 : instant),
service sched j t <= service sched0 j t ->
service sched j t <=
service (make_wc_at arr_seq sched0 t0) j t
move => sched0 ? ?; apply leq_trans with (service sched0 j t)=> //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j t : instant sched0 : schedule (processor_state Job) _t_ : instant _Hyp_ : service sched j t <= service sched0 j t
service sched0 j t <=
service (make_wc_at arr_seq sched0 _t_) j t
by intros ; apply mwa_service_bound.
Qed .
(** Finally, it follows directly that the transformed schedule cannot introduce
a deadline miss for any job from the arrival sequence. *)
Lemma wc_prefix_job_meets_deadline :
job_meets_deadline sched' j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j
job_meets_deadline sched' j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j
job_meets_deadline sched' j
rewrite /job_meets_deadline /completed_by /sched'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j
job_cost j <=
service (wc_transform arr_seq sched) j
(job_deadline j)
apply leq_trans with (service sched j (job_deadline j));
last by apply wc_prefix_service_bound.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched' := wc_transform arr_seq sched : nat -> processor_state Job j : Job H_arrives_in : arrives_in arr_seq j
job_cost j <= service sched j (job_deadline j)
by apply H_all_deadlines_of_arrivals_met.
Qed .
End JobsMeetDeadlinePrefix .
(** Next, consider a given time, used as horizon for the transformation... *)
Variable h : instant.
(** ...and let us call [sched'] the schedule resulting from the transformation
performed until [h]. *)
Let sched' := wc_transform_prefix arr_seq sched h.
(** We prove that [sched'] will never introduce jobs not coming from the
arrival sequence. *)
Lemma wc_prefix_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence sched' arr_seq.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h : instant sched' := wc_transform_prefix arr_seq sched h : schedule (processor_state Job)
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence sched' arr_seq
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h : instant sched' := wc_transform_prefix arr_seq sched h : schedule (processor_state Job)
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence sched' arr_seq
move => FROM_ARR.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h : instant sched' := wc_transform_prefix arr_seq sched h : schedule (processor_state Job) FROM_ARR : jobs_come_from_arrival_sequence sched
arr_seq
jobs_come_from_arrival_sequence sched' arr_seq
rewrite /sched' /wc_transform_prefix.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h : instant sched' := wc_transform_prefix arr_seq sched h : schedule (processor_state Job) FROM_ARR : jobs_come_from_arrival_sequence sched
arr_seq
jobs_come_from_arrival_sequence
(prefix_map sched (make_wc_at arr_seq) h) arr_seq
apply prefix_map_property_invariance => [|//].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h : instant sched' := wc_transform_prefix arr_seq sched h : schedule (processor_state Job) FROM_ARR : jobs_come_from_arrival_sequence sched
arr_seq
forall (sched : schedule (processor_state Job))
(t : instant),
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence
(make_wc_at arr_seq sched t) arr_seq
move => schedX t ARR.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h : instant sched' := wc_transform_prefix arr_seq sched h : schedule (processor_state Job) FROM_ARR : jobs_come_from_arrival_sequence sched
arr_seq schedX : schedule (processor_state Job) t : instant ARR : jobs_come_from_arrival_sequence schedX arr_seq
jobs_come_from_arrival_sequence
(make_wc_at arr_seq schedX t) arr_seq
by apply mwa_jobs_come_from_arrival_sequence.
Qed .
(** Similarly, we can show that [sched'] will only schedule jobs if they are
ready. *)
Lemma wc_prefix_jobs_must_be_ready_to_execute :
jobs_must_be_ready_to_execute sched ->
jobs_must_be_ready_to_execute sched'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h : instant sched' := wc_transform_prefix arr_seq sched h : schedule (processor_state Job)
jobs_must_be_ready_to_execute sched ->
jobs_must_be_ready_to_execute sched'
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h : instant sched' := wc_transform_prefix arr_seq sched h : schedule (processor_state Job)
jobs_must_be_ready_to_execute sched ->
jobs_must_be_ready_to_execute sched'
move => READY.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h : instant sched' := wc_transform_prefix arr_seq sched h : schedule (processor_state Job) READY : jobs_must_be_ready_to_execute sched
jobs_must_be_ready_to_execute sched'
rewrite /sched' /wc_transform_prefix.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h : instant sched' := wc_transform_prefix arr_seq sched h : schedule (processor_state Job) READY : jobs_must_be_ready_to_execute sched
jobs_must_be_ready_to_execute
(prefix_map sched (make_wc_at arr_seq) h)
apply prefix_map_property_invariance => [|//].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h : instant sched' := wc_transform_prefix arr_seq sched h : schedule (processor_state Job) READY : jobs_must_be_ready_to_execute sched
forall (sched : schedule (processor_state Job))
(t : instant),
jobs_must_be_ready_to_execute sched ->
jobs_must_be_ready_to_execute
(make_wc_at arr_seq sched t)
move => schedX t ARR.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) h : instant sched' := wc_transform_prefix arr_seq sched h : schedule (processor_state Job) READY : jobs_must_be_ready_to_execute sched schedX : schedule (processor_state Job) t : instant ARR : jobs_must_be_ready_to_execute schedX
jobs_must_be_ready_to_execute
(make_wc_at arr_seq schedX t)
by apply mwa_jobs_must_be_ready_to_execute.
Qed .
End PrefixFacts .
End AuxiliaryLemmasWorkConservingTransformation .
(** Finally, we can leverage all the previous results to prove statements about the full
work-conservation transformation. *)
Section WorkConservingTransformation .
(** We assume the basic (i.e., Liu & Layland)
readiness model under which any pending job is ready. *)
#[local] Existing Instance basic_ready_instance .
(** Consider any type of jobs with arrival times, costs, and deadlines... *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
(** ...an arbitrary valid 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).
(** ...in which jobs come from the arrival sequence, and must be ready to execute... *)
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
(** ...and in which no job misses a deadline. *)
Hypothesis H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met arr_seq sched.
(** Let us call [sched_wc] the schedule obtained after applying the work-conservation transformation. *)
Let sched_wc := wc_transform arr_seq sched.
(** First, we show that any scheduled job still comes from the arrival sequence. *)
Lemma wc_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched_wc arr_seq.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
jobs_come_from_arrival_sequence sched_wc arr_seq
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
jobs_come_from_arrival_sequence sched_wc arr_seq
move => j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant
scheduled_at sched_wc j t -> arrives_in arr_seq j
rewrite /scheduled_at -/(scheduled_at _ j t).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant
scheduled_at sched_wc j t -> arrives_in arr_seq j
exact : (wc_prefix_jobs_come_from_arrival_sequence arr_seq sched t.+1 ).
Qed .
(** Similarly, jobs are only scheduled if they are ready. *)
Lemma wc_jobs_must_be_ready_to_execute :
jobs_must_be_ready_to_execute sched_wc.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
jobs_must_be_ready_to_execute sched_wc
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
jobs_must_be_ready_to_execute sched_wc
move => j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant
scheduled_at sched_wc j t -> job_ready sched_wc j t
rewrite /scheduled_at /sched_wc /wc_transform -/(scheduled_at _ j t) => SCHED_AT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant SCHED_AT : scheduled_at
(wc_transform_prefix arr_seq sched t.+1 )
j t
job_ready
(fun t : nat =>
wc_transform_prefix arr_seq sched t.+1 t) j t
have READY': job_ready (wc_transform_prefix arr_seq sched t.+1 ) j t by
exact : wc_prefix_jobs_must_be_ready_to_execute.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant SCHED_AT : scheduled_at
(wc_transform_prefix arr_seq sched t.+1 )
j t READY' : job_ready
(wc_transform_prefix arr_seq sched t.+1 ) j
t
job_ready
(fun t : nat =>
wc_transform_prefix arr_seq sched t.+1 t) j t
move : READY'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant SCHED_AT : scheduled_at
(wc_transform_prefix arr_seq sched t.+1 )
j t
job_ready (wc_transform_prefix arr_seq sched t.+1 ) j t ->
job_ready
(fun t : nat =>
wc_transform_prefix arr_seq sched t.+1 t) j t
rewrite /job_ready /basic.basic_ready_instance
/pending /completed_by /service.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant SCHED_AT : scheduled_at
(wc_transform_prefix arr_seq sched t.+1 )
j t
has_arrived j t &&
~~
(job_cost j <=
service_during
(wc_transform_prefix arr_seq sched t.+1 ) j 0 t) ->
has_arrived j t &&
~~
(job_cost j <=
service_during
(fun t : nat =>
wc_transform_prefix arr_seq sched t.+1 t) j 0 t)
rewrite (equal_prefix_implies_same_service_during sched_wc (wc_transform_prefix arr_seq sched t.+1 )) //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant SCHED_AT : scheduled_at
(wc_transform_prefix arr_seq sched t.+1 )
j t
forall t0 : nat,
0 <= t0 < t ->
sched_wc t0 =
wc_transform_prefix arr_seq sched t.+1 t0
move => t' /andP [_ BOUND_t'].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant SCHED_AT : scheduled_at
(wc_transform_prefix arr_seq sched t.+1 )
j t t' : nat BOUND_t' : t' < t
sched_wc t' =
wc_transform_prefix arr_seq sched t.+1 t'
rewrite /sched_wc /wc_transform.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant SCHED_AT : scheduled_at
(wc_transform_prefix arr_seq sched t.+1 )
j t t' : nat BOUND_t' : t' < t
wc_transform_prefix arr_seq sched t'.+1 t' =
wc_transform_prefix arr_seq sched t.+1 t'
by apply wc_transform_prefix_inclusion => //; rewrite ltnS; apply ltnW.
Qed .
(** Also, no deadline misses are introduced. *)
Lemma wc_all_deadlines_of_arrivals_met :
all_deadlines_of_arrivals_met arr_seq sched_wc.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
all_deadlines_of_arrivals_met arr_seq sched_wc
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
all_deadlines_of_arrivals_met arr_seq sched_wc
move => j ARR_IN.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job ARR_IN : arrives_in arr_seq j
job_meets_deadline sched_wc j
rewrite /sched_wc /wc_transform_prefix.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job ARR_IN : arrives_in arr_seq j
job_meets_deadline (wc_transform arr_seq sched) j
by apply wc_prefix_job_meets_deadline.
Qed .
(** Finally, we can show that the transformation leads to a schedule in which
the processor is not idle if a job is ready. *)
Lemma wc_is_work_conserving_at :
forall j t ,
job_ready sched_wc j t ->
arrives_in arr_seq j ->
exists j' , sched_wc t = Some j'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
forall (j : Job) (t : instant),
job_ready sched_wc j t ->
arrives_in arr_seq j ->
exists j' : Job, sched_wc t = Some j'
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
forall (j : Job) (t : instant),
job_ready sched_wc j t ->
arrives_in arr_seq j ->
exists j' : Job, sched_wc t = Some j'
move => j t READY ARR_IN.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
exists j' : Job, sched_wc t = Some j'
rewrite /sched_wc /wc_transform /wc_transform_prefix.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
exists j' : Job,
prefix_map sched (make_wc_at arr_seq) t.+1 t =
Some j'
apply (prefix_map_pointwise_property (all_deadlines_of_arrivals_met arr_seq)
(is_work_conserving_at arr_seq)
(make_wc_at arr_seq)); rewrite //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
forall (sched : schedule (processor_state Job))
(t_ref : instant),
all_deadlines_of_arrivals_met arr_seq sched ->
all_deadlines_of_arrivals_met arr_seq
(make_wc_at arr_seq sched t_ref)
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
forall (sched : schedule (processor_state Job))
(t_ref : instant),
all_deadlines_of_arrivals_met arr_seq sched ->
all_deadlines_of_arrivals_met arr_seq
(make_wc_at arr_seq sched t_ref)
by apply mwa_all_deadlines_of_arrivals_met. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
forall (sched : schedule (processor_state Job))
(t_ref : nat),
all_deadlines_of_arrivals_met arr_seq sched ->
(forall t' : nat,
t' < t_ref -> is_work_conserving_at arr_seq sched t') ->
forall t' : nat,
t' <= t_ref ->
is_work_conserving_at arr_seq
(make_wc_at arr_seq sched t_ref) t'
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
forall (sched : schedule (processor_state Job))
(t_ref : nat),
all_deadlines_of_arrivals_met arr_seq sched ->
(forall t' : nat,
t' < t_ref -> is_work_conserving_at arr_seq sched t') ->
forall t' : nat,
t' <= t_ref ->
is_work_conserving_at arr_seq
(make_wc_at arr_seq sched t_ref) t'
by intros ; apply mwa_establishes_wc. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
exists j : Job,
arrives_in arr_seq j /\
job_ready
(prefix_map sched (make_wc_at arr_seq) t.+1 ) j t
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
exists j : Job,
arrives_in arr_seq j /\
job_ready
(prefix_map sched (make_wc_at arr_seq) t.+1 ) j t
exists j .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
arrives_in arr_seq j /\
job_ready (prefix_map sched (make_wc_at arr_seq) t.+1 )
j t
split ; first by apply ARR_IN.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
job_ready (prefix_map sched (make_wc_at arr_seq) t.+1 )
j t
have EQ: job_ready sched_wc j t = job_ready (prefix_map sched (make_wc_at arr_seq) (succn t)) j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
job_ready sched_wc j t =
job_ready (prefix_map sched (make_wc_at arr_seq) t.+1 )
j t
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
job_ready sched_wc j t =
job_ready (prefix_map sched (make_wc_at arr_seq) t.+1 )
j t
rewrite /sched_wc /wc_transform /job_ready
/basic_ready_instance /pending /completed_by
/service /service_during /service_at /wc_transform_prefix.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
has_arrived j t &&
~~
(job_cost j <=
\sum_(0 <= t < t)
service_in j
(prefix_map sched (make_wc_at arr_seq) t.+1 t)) =
has_arrived j t &&
~~
(job_cost j <=
\sum_(0 <= t0 < t)
service_in j
(prefix_map sched (make_wc_at arr_seq) t.+1 t0))
destruct has_arrived; last by rewrite Bool.andb_false_l.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
true &&
~~
(job_cost j <=
\sum_(0 <= t < t)
service_in j
(prefix_map sched (make_wc_at arr_seq) t.+1 t)) =
true &&
~~
(job_cost j <=
\sum_(0 <= t0 < t)
service_in j
(prefix_map sched (make_wc_at arr_seq) t.+1 t0))
have EQ_SUM: \sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) (succn t0) t0)
= \sum_(0 <= t0 < t) service_in j (prefix_map sched (make_wc_at arr_seq) (succn t) t0).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
\sum_(0 <= t0 < t)
service_in j
(prefix_map sched (make_wc_at arr_seq) t0.+1 t0) =
\sum_(0 <= t0 < t)
service_in j
(prefix_map sched (make_wc_at arr_seq) t.+1 t0)
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j
\sum_(0 <= t0 < t)
service_in j
(prefix_map sched (make_wc_at arr_seq) t0.+1 t0) =
\sum_(0 <= t0 < t)
service_in j
(prefix_map sched (make_wc_at arr_seq) t.+1 t0)
apply eq_big_nat => t' /andP [_ LT_t].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j t' : nat LT_t : t' < t
service_in j
(prefix_map sched (make_wc_at arr_seq) t'.+1 t') =
service_in j
(prefix_map sched (make_wc_at arr_seq) t.+1 t')
rewrite -/(wc_transform_prefix arr_seq sched _ _).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j t' : nat LT_t : t' < t
service_in j
(wc_transform_prefix arr_seq sched t'.+1 t') =
service_in j
(prefix_map sched (make_wc_at arr_seq) t.+1 t')
rewrite -/(wc_transform_prefix arr_seq sched _ _).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j t' : nat LT_t : t' < t
service_in j
(wc_transform_prefix arr_seq sched t'.+1 t') =
service_in j
(wc_transform_prefix arr_seq sched t.+1 t')
by rewrite (wc_transform_prefix_inclusion arr_seq sched t'.+1 t.+1 ). } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j EQ_SUM : \sum_(0 <= t0 < t)
service_in j
(prefix_map sched
(make_wc_at arr_seq) t0.+1 t0) =
\sum_(0 <= t0 < t)
service_in j
(prefix_map sched
(make_wc_at arr_seq) t.+1 t0)
true &&
~~
(job_cost j <=
\sum_(0 <= t < t)
service_in j
(prefix_map sched (make_wc_at arr_seq) t.+1 t)) =
true &&
~~
(job_cost j <=
\sum_(0 <= t0 < t)
service_in j
(prefix_map sched (make_wc_at arr_seq) t.+1 t0))
by rewrite EQ_SUM. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant READY : job_ready sched_wc j t ARR_IN : arrives_in arr_seq j EQ : job_ready sched_wc j t =
job_ready
(prefix_map sched (make_wc_at arr_seq) t.+1 ) j
t
job_ready (prefix_map sched (make_wc_at arr_seq) t.+1 )
j t
move : READY.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant ARR_IN : arrives_in arr_seq j EQ : job_ready sched_wc j t =
job_ready
(prefix_map sched (make_wc_at arr_seq) t.+1 ) j
t
job_ready sched_wc j t ->
job_ready (prefix_map sched (make_wc_at arr_seq) t.+1 )
j t
by rewrite EQ. }
Qed .
(** We can easily extend the previous lemma to obtain the definition
of a work-conserving schedule. *)
Lemma wc_is_work_conserving :
work_conserving arr_seq sched_wc.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
work_conserving arr_seq sched_wc
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
work_conserving arr_seq sched_wc
move => j t ARR_IN.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant ARR_IN : arrives_in arr_seq j
backlogged sched_wc j t ->
exists j_other : Job, scheduled_at sched_wc j_other t
rewrite /backlogged => /andP [READY _].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant ARR_IN : arrives_in arr_seq j READY : job_ready sched_wc j t
exists j_other : Job, scheduled_at sched_wc j_other t
move : (wc_is_work_conserving_at j t READY ARR_IN) => [j' SCHED_wc].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job j : Job t : instant ARR_IN : arrives_in arr_seq j READY : job_ready sched_wc j t j' : Job SCHED_wc : sched_wc t = Some j'
exists j_other : Job, scheduled_at sched_wc j_other t
by exists j' ; rewrite scheduled_at_def; apply /eqP.
Qed .
(** Ultimately, we can show that the work-conservation transformation maintains
all the properties of validity, does not introduce new deadline misses, and
establishes the work-conservation property. *)
Theorem wc_transform_correctness :
valid_schedule sched_wc arr_seq /\
all_deadlines_of_arrivals_met arr_seq sched_wc /\
work_conserving arr_seq sched_wc.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
valid_schedule sched_wc arr_seq /\
all_deadlines_of_arrivals_met arr_seq sched_wc /\
work_conserving arr_seq sched_wc
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
valid_schedule sched_wc arr_seq /\
all_deadlines_of_arrivals_met arr_seq sched_wc /\
work_conserving arr_seq sched_wc
repeat split .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
jobs_come_from_arrival_sequence sched_wc arr_seq
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
jobs_come_from_arrival_sequence sched_wc arr_seq
apply wc_jobs_come_from_arrival_sequence.
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
jobs_must_be_ready_to_execute sched_wc
apply wc_jobs_must_be_ready_to_execute.
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
all_deadlines_of_arrivals_met arr_seq sched_wc
apply wc_all_deadlines_of_arrivals_met.
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobDeadline Job arr_seq : arrival_sequence Job H_arr_seq_valid : valid_arrival_sequence arr_seq sched : schedule (processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_all_deadlines_of_arrivals_met : all_deadlines_of_arrivals_met
arr_seq sched sched_wc := wc_transform arr_seq sched : nat -> processor_state Job
work_conserving arr_seq sched_wc
apply wc_is_work_conserving.
Qed .
End WorkConservingTransformation .