Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.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.analysis.facts.delay_propagation.[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 ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.model.readiness.basic.
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.definitions.schedulability.
(** * Propagation of Release Jitter in Arrival Curves *)
(** In this module, we prove correct an approach to "hiding" release jitter by
"folding" it into arrival curves. *)
Section JitterPropagationFacts .
(** Consider any type of tasks described by arrival curves and the
corresponding jobs. *)
Context {Task : TaskType} {arrival_curve : MaxArrivals Task}
{Job : JobType} `{JobTask Job Task}.
(** Let [original_arrival] denote each job's _actual_ arrival time ... *)
Context {original_arrival : JobArrival Job}.
(** ... and suppose the jobs are affected by bounded release jitter. *)
Context `{TaskJitter Task} `{JobJitter Job}.
(** In the following, consider an arbitrary valid arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** Recall the induced "release curve" and associated definitions. *)
#[local] Existing Instance release_as_arrival .
#[local] Existing Instance release_curve .
(** In the following, we let [rel_seq] denote the induced "release curve". *)
Let rel_seq := release_sequence arr_seq.
(** Suppose we are given a set of tasks ... *)
Variable ts : seq Task.
(** ... with valid bounds on release jitter. *)
Hypothesis H_valid_jitter : valid_jitter_bounds ts.
(** ** Restated General Properties *)
(** We begin by restating general properties of delay propagation, specialized
to the case of jitter propagation. *)
(** The arrival and release sequences contain an identical set of jobs. *)
Corollary jitter_arrives_in_iff :
forall j ,
arrives_in arr_seq j <-> arrives_in rel_seq j.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts
forall j : Job,
arrives_in arr_seq j <-> arrives_in rel_seq j
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts
forall j : Job,
arrives_in arr_seq j <-> arrives_in rel_seq j
move => j; split ;
[ apply : (arrives_in_propagated_if original_arrival release_as_arrival) => //
| apply : (arrives_in_propagated_only_if original_arrival release_as_arrival) => //
]; exact : jitter_arr_seq_mapping_valid.
Qed .
(** The induced "release sequence" is valid. *)
Corollary valid_release_sequence :
@valid_arrival_sequence _ release_as_arrival rel_seq.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts
valid_arrival_sequence rel_seq
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts
valid_arrival_sequence rel_seq
apply : (valid_propagated_arrival_sequence original_arrival release_as_arrival) => //.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts
valid_arr_seq_propagation_mapping original_arrival
release_as_arrival id ?Goal arr_seq (cons^~ [::])
job_jitter ?Goal0
by apply : jitter_arr_seq_mapping_valid.
Qed .
(** If the arrival curve is structurally valid, then so is the induced release
curve. *)
Corollary valid_release_curve :
valid_taskset_arrival_curve ts max_arrivals ->
valid_taskset_arrival_curve ts release_curve.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts
valid_taskset_arrival_curve ts max_arrivals ->
valid_taskset_arrival_curve ts release_curve
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts
valid_taskset_arrival_curve ts max_arrivals ->
valid_taskset_arrival_curve ts release_curve
move => VALID.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts VALID : valid_taskset_arrival_curve ts max_arrivals
valid_taskset_arrival_curve ts release_curve
apply : propagated_arrival_curve_valid => tsk IN.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts VALID : valid_taskset_arrival_curve ts max_arrivals tsk : Task IN : tsk \in ts
monotone leq (max_arrivals tsk)
by move : (VALID tsk IN) => [_ {}].
Qed .
(** Furthermore, if the arrival curve correctly bounds arrivals according to
[arr_seq], then the "release curve" also correctly bounds releases
according to [rel_seq]. *)
Corollary release_curve_respected :
valid_taskset_arrival_curve ts max_arrivals ->
@taskset_respects_max_arrivals _ _ _ arr_seq arrival_curve ts ->
@taskset_respects_max_arrivals _ _ _ rel_seq release_curve ts.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts
valid_taskset_arrival_curve ts max_arrivals ->
taskset_respects_max_arrivals arr_seq ts ->
taskset_respects_max_arrivals rel_seq ts
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts
valid_taskset_arrival_curve ts max_arrivals ->
taskset_respects_max_arrivals arr_seq ts ->
taskset_respects_max_arrivals rel_seq ts
move => AC VALID.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts AC : valid_taskset_arrival_curve ts max_arrivals VALID : taskset_respects_max_arrivals arr_seq ts
taskset_respects_max_arrivals rel_seq ts
apply : (propagated_arrival_curve_respected original_arrival release_as_arrival) => //; try by rewrite map_id.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts AC : valid_taskset_arrival_curve ts max_arrivals VALID : taskset_respects_max_arrivals arr_seq ts
valid_delay_propagation_mapping original_arrival
release_as_arrival id id task_jitter ts
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts AC : valid_taskset_arrival_curve ts max_arrivals VALID : taskset_respects_max_arrivals arr_seq ts
valid_delay_propagation_mapping original_arrival
release_as_arrival id id task_jitter ts
by apply : jitter_delay_mapping_valid.
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts AC : valid_taskset_arrival_curve ts max_arrivals VALID : taskset_respects_max_arrivals arr_seq ts
valid_arr_seq_propagation_mapping original_arrival
release_as_arrival id task_jitter arr_seq
(cons^~ [::]) job_jitter ts
by apply : jitter_arr_seq_mapping_valid.
Qed .
(** ** Jitter Propagation Properties *)
(** Next, we establish validity properties specific to jitter
propagation. These are needed to apply response-time analysis results. *)
(** Since the arrival and release sequence describe identical sets of jobs,
trivially all jobs continue to belong to the tasks in the task set. *)
Lemma jitter_prop_same_jobs :
all_jobs_from_taskset arr_seq ts ->
all_jobs_from_taskset rel_seq ts.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts
all_jobs_from_taskset arr_seq ts ->
all_jobs_from_taskset rel_seq ts
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts
all_jobs_from_taskset arr_seq ts ->
all_jobs_from_taskset rel_seq ts
by move => ALL j IN; apply : ALL; rewrite jitter_arrives_in_iff. Qed .
(** Next, consider an arbitrary schedule of the workload. *)
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
(** Again, trivially, all jobs in the schedule continue to belong to the
release sequence. *)
Lemma jitter_prop_same_jobs' :
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence sched rel_seq.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence sched rel_seq
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState
jobs_come_from_arrival_sequence sched arr_seq ->
jobs_come_from_arrival_sequence sched rel_seq
move => FROM j t SCHED; rewrite -jitter_arrives_in_iff; exact : FROM. Qed .
(** Let us now consider the execution costs. *)
Context `{JobCost Job} `{TaskCost Task}.
(** Since the set of jobs didn't change, and since release jitter propagation
does not change execution costs, job costs remain trivially valid. *)
Lemma jitter_prop_valid_costs :
arrivals_have_valid_job_costs arr_seq ->
arrivals_have_valid_job_costs rel_seq.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task
arrivals_have_valid_job_costs arr_seq ->
arrivals_have_valid_job_costs rel_seq
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task
arrivals_have_valid_job_costs arr_seq ->
arrivals_have_valid_job_costs rel_seq
move => VALID j IN.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task VALID : arrivals_have_valid_job_costs arr_seq j : Job IN : arrives_in rel_seq j
valid_job_cost j
apply : VALID.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task j : Job IN : arrives_in rel_seq j
arrives_in arr_seq j
by rewrite jitter_arrives_in_iff.
Qed .
(** If the given schedule respects release jitter, then it continues to do so
after we've reinterpreted the release times to be the arrival times. *)
Lemma jitter_ready_to_execute :
@jobs_must_be_ready_to_execute _ _ sched _ original_arrival jitter_ready_instance ->
@jobs_must_be_ready_to_execute _ _ sched _ release_as_arrival basic_ready_instance.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task
jobs_must_be_ready_to_execute sched ->
jobs_must_be_ready_to_execute sched
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task
jobs_must_be_ready_to_execute sched ->
jobs_must_be_ready_to_execute sched
move => RDY j t SCHED; by move : (RDY j t SCHED). Qed .
(** If the schedule is work-conserving, then it continues to be so after we've
"hidden" release jitter by reinterpreting release times as arrival
times. *)
Theorem jitter_work_conservation :
@work_conserving _ original_arrival _ _ jitter_ready_instance arr_seq sched ->
@work_conserving _ release_as_arrival _ _ basic_ready_instance rel_seq sched.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task
work_conserving arr_seq sched ->
work_conserving rel_seq sched
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task
work_conserving arr_seq sched ->
work_conserving rel_seq sched
move => WC_jit j t ARR_rel /andP [R_rel NSCHED].Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task WC_jit : work_conserving arr_seq sched j : Job t : instant ARR_rel : arrives_in rel_seq j R_rel : job_ready sched j t NSCHED : ~~ scheduled_at sched j t
exists j_other : Job, scheduled_at sched j_other t
have ARR_arr: arrives_in arr_seq j by rewrite jitter_arrives_in_iff.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task WC_jit : work_conserving arr_seq sched j : Job t : instant ARR_rel : arrives_in rel_seq j R_rel : job_ready sched j t NSCHED : ~~ scheduled_at sched j t ARR_arr : arrives_in arr_seq j
exists j_other : Job, scheduled_at sched j_other t
apply : WC_jit; first exact : ARR_arr.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task j : Job t : instant ARR_rel : arrives_in rel_seq j R_rel : job_ready sched j t NSCHED : ~~ scheduled_at sched j t ARR_arr : arrives_in arr_seq j
backlogged sched j t
by apply /andP; split .
Qed .
(** If the given schedule is valid w.r.t. to original arrivals, then it
continues to be valid after reinterpreting release times as arrival
times. *)
Lemma jitter_valid_schedule :
@valid_schedule _ _ sched _ original_arrival jitter_ready_instance arr_seq ->
@valid_schedule _ _ sched _ release_as_arrival basic_ready_instance rel_seq.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task
valid_schedule sched arr_seq ->
valid_schedule sched rel_seq
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task
valid_schedule sched arr_seq ->
valid_schedule sched rel_seq
move => [SRC RDY].Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task SRC : jobs_come_from_arrival_sequence sched arr_seq RDY : jobs_must_be_ready_to_execute sched
valid_schedule sched rel_seq
split .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task SRC : jobs_come_from_arrival_sequence sched arr_seq RDY : jobs_must_be_ready_to_execute sched
jobs_come_from_arrival_sequence sched rel_seq
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task SRC : jobs_come_from_arrival_sequence sched arr_seq RDY : jobs_must_be_ready_to_execute sched
jobs_come_from_arrival_sequence sched rel_seq
exact : jitter_prop_same_jobs'.
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task SRC : jobs_come_from_arrival_sequence sched arr_seq RDY : jobs_must_be_ready_to_execute sched
jobs_must_be_ready_to_execute sched
exact : jitter_ready_to_execute.
Qed .
(** In the following, suppose the given schedule is valid w.r.t. the original
arrival times and jitter-affected readiness. *)
Hypothesis H_valid_schedule :
@valid_schedule _ _ sched _ original_arrival jitter_ready_instance arr_seq.
(** As one would think, the set of scheduled jobs remains unchanged. For
technical reasons (dependence of the definition of [scheduled_jobs_at] on
the arrival sequence), this is a lot less obvious at the Coq level than
one intuitively might expect. *)
Lemma jitter_scheduled_jobs_at_equiv :
forall t j ,
(j \in scheduled_jobs_at rel_seq sched t) =
(j \in scheduled_jobs_at arr_seq sched t).Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq
forall (t : instant) (j : Job),
(j \in scheduled_jobs_at rel_seq sched t) =
(j \in scheduled_jobs_at arr_seq sched t)
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq
forall (t : instant) (j : Job),
(j \in scheduled_jobs_at rel_seq sched t) =
(j \in scheduled_jobs_at arr_seq sched t)
move => j t.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq j : instant t : Job
(t \in scheduled_jobs_at rel_seq sched j) =
(t \in scheduled_jobs_at arr_seq sched j)
have SRC := @valid_schedule_jobs_come_from_arrival_sequence _ _ sched _
original_arrival jitter_ready_instance arr_seq H_valid_schedule.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq j : instant t : Job SRC : jobs_come_from_arrival_sequence sched arr_seq
(t \in scheduled_jobs_at rel_seq sched j) =
(t \in scheduled_jobs_at arr_seq sched j)
rewrite [RHS]scheduled_jobs_at_iff; [| |exact : SRC|] => //.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq j : instant t : Job SRC : jobs_come_from_arrival_sequence sched arr_seq
(t \in scheduled_jobs_at rel_seq sched j) =
scheduled_at sched t j
rewrite (@scheduled_jobs_at_iff _ release_as_arrival); first by done .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq j : instant t : Job SRC : jobs_come_from_arrival_sequence sched arr_seq
valid_arrival_sequence rel_seq
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq j : instant t : Job SRC : jobs_come_from_arrival_sequence sched arr_seq
valid_arrival_sequence rel_seq
exact : valid_release_sequence.
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq j : instant t : Job SRC : jobs_come_from_arrival_sequence sched arr_seq
jobs_come_from_arrival_sequence sched rel_seq
exact : jitter_prop_same_jobs'.
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq j : instant t : Job SRC : jobs_come_from_arrival_sequence sched arr_seq
jobs_must_arrive_to_execute sched
exact
/(@jobs_must_arrive_to_be_ready _ _ sched _ release_as_arrival basic_ready_instance)
/jitter_ready_to_execute.
Qed .
(** Unsurprisingly, on a uniprocessor, the scheduled job remains unchanged,
too. Again, this is less straightforward than one might think due to
technical reasons (type-class resolution). *)
Lemma jitter_scheduled_job_at_eq :
forall t ,
uniprocessor_model PState ->
scheduled_job_at arr_seq sched t = scheduled_job_at rel_seq sched t.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq
forall t : instant,
uniprocessor_model PState ->
scheduled_job_at arr_seq sched t =
scheduled_job_at rel_seq sched t
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq
forall t : instant,
uniprocessor_model PState ->
scheduled_job_at arr_seq sched t =
scheduled_job_at rel_seq sched t
move => t UNI.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState
scheduled_job_at arr_seq sched t =
scheduled_job_at rel_seq sched t
have SRC := @valid_schedule_jobs_come_from_arrival_sequence _ _ sched _
original_arrival jitter_ready_instance arr_seq H_valid_schedule.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq
scheduled_job_at arr_seq sched t =
scheduled_job_at rel_seq sched t
(* Note: there is a lot of repetition here because the automation chokes on
the multiple available type-class instances and/or promptly picks the
wrong ones. Not pretty, but it works. *)
case SCHED: scheduled_job_at => [j|];
case SCHED': scheduled_job_at => [j'|]; last by done .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j : Job SCHED : scheduled_job_at arr_seq sched t = Some j j' : Job SCHED' : scheduled_job_at rel_seq sched t = Some j'
Some j = Some j'
{ Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j : Job SCHED : scheduled_job_at arr_seq sched t = Some j j' : Job SCHED' : scheduled_job_at rel_seq sched t = Some j'
Some j = Some j'
move : SCHED => /eqP; rewrite scheduled_job_at_scheduled_at; [| |exact : SRC| |] => // SCHED.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j, j' : Job SCHED' : scheduled_job_at rel_seq sched t = Some j' SCHED : scheduled_at sched j t
Some j = Some j'
move : SCHED' => /eqP; rewrite (@scheduled_job_at_scheduled_at _ release_as_arrival).Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j, j' : Job SCHED : scheduled_at sched j t
scheduled_at sched j' t -> Some j = Some j'
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j, j' : Job SCHED : scheduled_at sched j t
scheduled_at sched j' t -> Some j = Some j'
move => SCHED'.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j, j' : Job SCHED : scheduled_at sched j t SCHED' : scheduled_at sched j' t
Some j = Some j'
by rewrite (UNI j j' sched t).
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j, j' : Job SCHED : scheduled_at sched j t
valid_arrival_sequence rel_seq
exact : valid_release_sequence.
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j, j' : Job SCHED : scheduled_at sched j t
jobs_come_from_arrival_sequence sched rel_seq
exact : jitter_prop_same_jobs'.
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j, j' : Job SCHED : scheduled_at sched j t
jobs_must_arrive_to_execute sched
exact
/(@jobs_must_arrive_to_be_ready _ _ sched _ release_as_arrival basic_ready_instance)
/jitter_ready_to_execute.
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j, j' : Job SCHED : scheduled_at sched j t
uniprocessor_model PState
by [].
} Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j : Job SCHED : scheduled_job_at arr_seq sched t = Some j SCHED' : scheduled_job_at rel_seq sched t = None
Some j = None
{ Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j : Job SCHED : scheduled_job_at arr_seq sched t = Some j SCHED' : scheduled_job_at rel_seq sched t = None
Some j = None
exfalso .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j : Job SCHED : scheduled_job_at arr_seq sched t = Some j SCHED' : scheduled_job_at rel_seq sched t = None
False
move : SCHED => /eqP; rewrite scheduled_job_at_scheduled_at; [| |exact : SRC| |] => //.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j : Job SCHED' : scheduled_job_at rel_seq sched t = None
scheduled_at sched j t -> False
move : SCHED'; rewrite (@scheduled_job_at_none _ release_as_arrival);
first by move => NSCHED; apply /negP.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j : Job
valid_arrival_sequence rel_seq
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j : Job
valid_arrival_sequence rel_seq
exact : valid_release_sequence.
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j : Job
jobs_come_from_arrival_sequence sched rel_seq
exact : jitter_prop_same_jobs'.
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j : Job
jobs_must_arrive_to_execute sched
exact
/(@jobs_must_arrive_to_be_ready _ _ sched _ release_as_arrival basic_ready_instance)
/jitter_ready_to_execute. } Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq SCHED : scheduled_job_at arr_seq sched t = None j' : Job SCHED' : scheduled_job_at rel_seq sched t = Some j'
None = Some j'
{ Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq SCHED : scheduled_job_at arr_seq sched t = None j' : Job SCHED' : scheduled_job_at rel_seq sched t = Some j'
None = Some j'
exfalso .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq SCHED : scheduled_job_at arr_seq sched t = None j' : Job SCHED' : scheduled_job_at rel_seq sched t = Some j'
False
move : SCHED; rewrite scheduled_job_at_none; [| |exact : SRC|] => // NSCHED.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j' : Job SCHED' : scheduled_job_at rel_seq sched t = Some j' NSCHED : forall j : Job, ~~ scheduled_at sched j t
False
move : SCHED' => /eqP; rewrite (@scheduled_job_at_scheduled_at _ release_as_arrival);
first by apply /negP.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j' : Job NSCHED : forall j : Job, ~~ scheduled_at sched j t
valid_arrival_sequence rel_seq
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j' : Job NSCHED : forall j : Job, ~~ scheduled_at sched j t
valid_arrival_sequence rel_seq
exact : valid_release_sequence.
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j' : Job NSCHED : forall j : Job, ~~ scheduled_at sched j t
jobs_come_from_arrival_sequence sched rel_seq
exact : jitter_prop_same_jobs'.
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j' : Job NSCHED : forall j : Job, ~~ scheduled_at sched j t
jobs_must_arrive_to_execute sched
exact
/(@jobs_must_arrive_to_be_ready _ _ sched _ release_as_arrival basic_ready_instance)
/jitter_ready_to_execute.
- Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq t : instant UNI : uniprocessor_model PState SRC : jobs_come_from_arrival_sequence sched arr_seq j' : Job NSCHED : forall j : Job, ~~ scheduled_at sched j t
uniprocessor_model PState
by []. }
Qed .
(** Importantly, the schedule remains FP-policy compliant if it was so to
begin with, despite the postponed arrival times. *)
Theorem jitter_FP_compliance `{FP : FP_policy Task} `{JobPreemptable Job}:
uniprocessor_model PState ->
@respects_FP_policy_at_preemption_point
_ _ _ original_arrival _ _ _ jitter_ready_instance arr_seq sched FP ->
@respects_FP_policy_at_preemption_point
_ _ _ release_as_arrival _ _ _ basic_ready_instance rel_seq sched FP.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq FP : FP_policy Task H4 : JobPreemptable Job
uniprocessor_model PState ->
respects_FP_policy_at_preemption_point arr_seq sched
FP ->
respects_FP_policy_at_preemption_point rel_seq sched
FP
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq FP : FP_policy Task H4 : JobPreemptable Job
uniprocessor_model PState ->
respects_FP_policy_at_preemption_point arr_seq sched
FP ->
respects_FP_policy_at_preemption_point rel_seq sched
FP
move => UNI COMP j j_hp t ARR_rel PT_rel BL SCHED_hp.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq FP : FP_policy Task H4 : JobPreemptable Job UNI : uniprocessor_model PState COMP : respects_FP_policy_at_preemption_point arr_seq
sched FP j, j_hp : Job t : instant ARR_rel : arrives_in rel_seq j PT_rel : preemption_time rel_seq sched t BL : backlogged sched j t SCHED_hp : scheduled_at sched j_hp t
hep_job_at t j_hp j
have ARR_arr: arrives_in arr_seq j by rewrite jitter_arrives_in_iff.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq FP : FP_policy Task H4 : JobPreemptable Job UNI : uniprocessor_model PState COMP : respects_FP_policy_at_preemption_point arr_seq
sched FP j, j_hp : Job t : instant ARR_rel : arrives_in rel_seq j PT_rel : preemption_time rel_seq sched t BL : backlogged sched j t SCHED_hp : scheduled_at sched j_hp t ARR_arr : arrives_in arr_seq j
hep_job_at t j_hp j
apply : COMP => //.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq FP : FP_policy Task H4 : JobPreemptable Job UNI : uniprocessor_model PState j, j_hp : Job t : instant ARR_rel : arrives_in rel_seq j PT_rel : preemption_time rel_seq sched t BL : backlogged sched j t SCHED_hp : scheduled_at sched j_hp t ARR_arr : arrives_in arr_seq j
preemption_time arr_seq sched t
by rewrite /preemption_time jitter_scheduled_job_at_eq.
Qed .
(** ** Transferred Response-Time Bound *)
(** Finally, we state the main result, which is the whole point of jitter
propagation in the first place: if it is possible to bound response times
after release jitter has been folded into the arrival curves, then this
implies a response-time bound for the original problem with jitter.
This theorem conceptually corresponds to equations (5) and (6) in Audsley
et al. (1993), but has been generalized to arbitrary arrival curves.
- Audsley, N., Burns, A., Richardson, M., Tindell, K., and Wellings,
A. (1993). Applying new scheduling theory to static priority preemptive
scheduling. Software Engineering Journal, 8(5):284–292. *)
Theorem jitter_response_time_bound :
forall tsk R ,
tsk \in ts ->
@task_response_time_bound _ _ release_as_arrival _ _ _ rel_seq sched tsk R ->
@task_response_time_bound _ _ original_arrival _ _ _ arr_seq sched tsk (task_jitter tsk + R).Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq
forall (tsk : Task) (R : duration),
tsk \in ts ->
task_response_time_bound rel_seq sched tsk R ->
task_response_time_bound arr_seq sched tsk
(task_jitter tsk + R)
Proof .Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq
forall (tsk : Task) (R : duration),
tsk \in ts ->
task_response_time_bound rel_seq sched tsk R ->
task_response_time_bound arr_seq sched tsk
(task_jitter tsk + R)
move => tsk R IN RTB j IN_arr TSK.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq tsk : Task R : duration IN : tsk \in ts RTB : task_response_time_bound rel_seq sched tsk R j : Job IN_arr : arrives_in arr_seq j TSK : job_of_task tsk j
job_response_time_bound sched j (task_jitter tsk + R)
have IN_rel: arrives_in rel_seq j by rewrite -jitter_arrives_in_iff.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq tsk : Task R : duration IN : tsk \in ts RTB : task_response_time_bound rel_seq sched tsk R j : Job IN_arr : arrives_in arr_seq j TSK : job_of_task tsk j IN_rel : arrives_in rel_seq j
job_response_time_bound sched j (task_jitter tsk + R)
move : (RTB j IN_rel TSK).Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq tsk : Task R : duration IN : tsk \in ts RTB : task_response_time_bound rel_seq sched tsk R j : Job IN_arr : arrives_in arr_seq j TSK : job_of_task tsk j IN_rel : arrives_in rel_seq j
job_response_time_bound sched j R ->
job_response_time_bound sched j (task_jitter tsk + R)
rewrite /job_response_time_bound/job_arrival/release_as_arrival/job_arrival.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq tsk : Task R : duration IN : tsk \in ts RTB : task_response_time_bound rel_seq sched tsk R j : Job IN_arr : arrives_in arr_seq j TSK : job_of_task tsk j IN_rel : arrives_in rel_seq j
completed_by sched j
(original_arrival j + job_jitter j + R) ->
completed_by sched j
(original_arrival j + (task_jitter tsk + R))
apply : completion_monotonic.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq tsk : Task R : duration IN : tsk \in ts RTB : task_response_time_bound rel_seq sched tsk R j : Job IN_arr : arrives_in arr_seq j TSK : job_of_task tsk j IN_rel : arrives_in rel_seq j
original_arrival j + job_jitter j + R <=
original_arrival j + (task_jitter tsk + R)
move : TSK; rewrite /job_of_task => /eqP TSK.Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq tsk : Task R : duration IN : tsk \in ts RTB : task_response_time_bound rel_seq sched tsk R j : Job IN_arr : arrives_in arr_seq j IN_rel : arrives_in rel_seq j TSK : job_task j = tsk
original_arrival j + job_jitter j + R <=
original_arrival j + (task_jitter tsk + R)
move : (H_valid_jitter tsk IN j TSK).Task : TaskType arrival_curve : MaxArrivals Task Job : JobType H : JobTask Job Task original_arrival : JobArrival Job H0 : TaskJitter Task H1 : JobJitter Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq rel_seq := release_sequence arr_seq : instant -> seq Job ts : seq Task H_valid_jitter : valid_jitter_bounds ts PState : ProcessorState Job sched : schedule PState H2 : JobCost Job H3 : TaskCost Task H_valid_schedule : valid_schedule sched arr_seq tsk : Task R : duration IN : tsk \in ts RTB : task_response_time_bound rel_seq sched tsk R j : Job IN_arr : arrives_in arr_seq j IN_rel : arrives_in rel_seq j TSK : job_task j = tsk
job_jitter j <= task_jitter tsk ->
original_arrival j + job_jitter j + R <=
original_arrival j + (task_jitter tsk + R)
by lia .
Qed .
End JitterPropagationFacts .