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.model.service_of_jobs.[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.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export prosa.analysis.abstract .definitions.
Require Export prosa.analysis.abstract .busy_interval.
(** * Lower Bound On Job Service *)
(** In this section we prove that if the cumulative interference
inside a busy interval is bounded by a certain constant then a job
executes long enough to reach a specified amount of service. *)
Section LowerBoundOnService .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** In addition, we assume existence of a function mapping jobs to
their preemption points. *)
Context `{JobPreemptable Job}.
(** Consider _any_ kind of processor state model. *)
Context {PState : ProcessorState Job}.
(** Consider any arrival sequence with consistent arrivals ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** ... and any schedule of this arrival sequence. *)
Variable sched : schedule PState.
(** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq.
(** Let [tsk] be any task that is to be analyzed. *)
Variable tsk : Task.
(** Assume we are provided with abstract functions for interference
and interfering workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** We assume that the schedule is work-conserving. *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** Let [j] be any job of task [tsk] with positive cost. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** In this section, we show that the cumulative interference is a
complement to the total time where job [j] is scheduled inside a
busy interval prefix. *)
Section InterferenceIsComplement .
(** Consider any busy interval prefix <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval_prefix sched j t1 t2.
(** Consider any sub-interval <<[t, t + δ)>> inside the busy interval <<[t1, t2)>>. *)
Variables (t : instant) (δ : duration).
Hypothesis H_t1_le_t : t1 <= t.
Hypothesis H_tδ_le_t2 : t + δ <= t2.
(** We prove that sum of cumulative service and cumulative
interference in the interval <<[t, t + δ)>> is equal to
[δ]. *)
Lemma interference_is_complement_to_schedule :
service_during sched j t (t + δ) + cumulative_interference j t (t + δ) >= δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2
δ <=
service_during sched j t (t + δ) +
cumulative_interference j t (t + δ)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2
δ <=
service_during sched j t (t + δ) +
cumulative_interference j t (t + δ)
rewrite /service_during /cumulative_interference /cumul_cond_interference /service_at.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2
δ <=
\sum_(t <= t < t + δ) service_in j (sched t) +
\sum_(t <= t < t + δ)
cond_interference (fun => xpredT) j t
rewrite -big_split //= -{1 }(sum_of_ones t δ) big_nat [in X in _ <= X]big_nat leq_sum // => x /andP[Lo Hi].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 x : nat Lo : t <= x Hi : x < t + δ
0 <
service_in j (sched x) +
cond_interference (fun => xpredT) j x
move : (H_work_conserving j t1 t2 x) => Workj.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 x : nat Lo : t <= x Hi : x < t + δ Workj : arrives_in arr_seq j ->
0 < job_cost j ->
busy_interval_prefix sched j t1 t2 ->
t1 <= x < t2 ->
~ interference j x <->
receives_service_at sched j x
0 <
service_in j (sched x) +
cond_interference (fun => xpredT) j x
feed_n 4 Workj => //; first by lia . Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 x : nat Lo : t <= x Hi : x < t + δ Workj : ~ interference j x <->
receives_service_at sched j x
0 <
service_in j (sched x) +
cond_interference (fun => xpredT) j x
rewrite /cond_interference //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 x : nat Lo : t <= x Hi : x < t + δ Workj : ~ interference j x <->
receives_service_at sched j x
0 < service_in j (sched x) + interference j x
case INT: interference; first by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 x : nat Lo : t <= x Hi : x < t + δ Workj : ~ interference j x <->
receives_service_at sched j x INT : interference j x = false
0 < service_in j (sched x) + false
by rewrite // addn0; apply Workj; rewrite INT.
Qed .
(** Also, note that under the unit-service processor model
assumption, the sum of service within the interval <<[t, t + δ)>>
and the cumulative interference within the same interval
is bounded by the length of the interval (i.e., [δ]). *)
Remark service_and_interference_bounded :
unit_service_proc_model PState ->
service_during sched j t (t + δ) + cumulative_interference j t (t + δ) <= δ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2
unit_service_proc_model PState ->
service_during sched j t (t + δ) +
cumulative_interference j t (t + δ) <= δ
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2
unit_service_proc_model PState ->
service_during sched j t (t + δ) +
cumulative_interference j t (t + δ) <= δ
move => UNIT.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState
service_during sched j t (t + δ) +
cumulative_interference j t (t + δ) <= δ
rewrite /service_during /cumulative_interference/service_at -big_split //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState
\sum_(t <= i < t + δ)
(service_in j (sched i) +
cond_interference (fun => xpredT) j i) <= δ
rewrite -{2 }(sum_of_ones t δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState
\sum_(t <= i < t + δ)
(service_in j (sched i) +
cond_interference (fun => xpredT) j i) <=
\sum_(t <= x < t + δ) 1
rewrite big_nat [in X in _ <= X]big_nat; apply leq_sum => x /andP[Lo Hi].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState x : nat Lo : t <= x Hi : x < t + δ
service_in j (sched x) +
cond_interference (fun => xpredT) j x <= 1
move : (H_work_conserving j t1 t2 x) => Workj.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState x : nat Lo : t <= x Hi : x < t + δ Workj : arrives_in arr_seq j ->
0 < job_cost j ->
busy_interval_prefix sched j t1 t2 ->
t1 <= x < t2 ->
~ interference j x <->
receives_service_at sched j x
service_in j (sched x) +
cond_interference (fun => xpredT) j x <= 1
feed_n 4 Workj => //. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState x : nat Lo : t <= x Hi : x < t + δ Workj : t1 <= x < t2 ->
~ interference j x <->
receives_service_at sched j x
t1 <= x < t2
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState x : nat Lo : t <= x Hi : x < t + δ Workj : t1 <= x < t2 ->
~ interference j x <->
receives_service_at sched j x
t1 <= x < t2
by apply /andP; split ; lia . } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState x : nat Lo : t <= x Hi : x < t + δ Workj : ~ interference j x <->
receives_service_at sched j x
service_in j (sched x) +
cond_interference (fun => xpredT) j x <= 1
rewrite /cond_interference //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState x : nat Lo : t <= x Hi : x < t + δ Workj : ~ interference j x <->
receives_service_at sched j x
service_in j (sched x) + interference j x <= 1
destruct interference.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState x : nat Lo : t <= x Hi : x < t + δ Workj : ~ true <-> receives_service_at sched j x
service_in j (sched x) + true <= 1
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState x : nat Lo : t <= x Hi : x < t + δ Workj : ~ true <-> receives_service_at sched j x
service_in j (sched x) + true <= 1
rewrite addn1 ltnS.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState x : nat Lo : t <= x Hi : x < t + δ Workj : ~ true <-> receives_service_at sched j x
service_in j (sched x) <= 0
by move_neq_up NE; apply Workj.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval_prefix sched j t1 t2 t : instant δ : duration H_t1_le_t : t1 <= t H_tδ_le_t2 : t + δ <= t2 UNIT : unit_service_proc_model PState x : nat Lo : t <= x Hi : x < t + δ Workj : ~ false <-> receives_service_at sched j x
service_in j (sched x) + false <= 1
by rewrite addn0; apply UNIT.
Qed .
End InterferenceIsComplement .
(** In this section, we prove a sufficient condition under which job
[j] receives enough service. *)
Section InterferenceBoundedImpliesEnoughService .
(** Consider any busy interval <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval sched j t1 t2.
(** Let [progress_of_job] be the desired service of job [j]. *)
Variable progress_of_job : duration.
Hypothesis H_progress_le_job_cost : progress_of_job <= job_cost j.
(** Assume that for some [δ] the sum of desired progress and
cumulative interference is bounded by [δ]. *)
Variable δ : duration.
Hypothesis H_total_workload_is_bounded :
progress_of_job + cumulative_interference j t1 (t1 + δ) <= δ.
(** Then, it must be the case that the job has received no less
service than [progress_of_job]. *)
Theorem j_receives_enough_service :
service sched j (t1 + δ) >= progress_of_job.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ
progress_of_job <= service sched j (t1 + δ)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ
progress_of_job <= service sched j (t1 + δ)
destruct (leqP (t1 + δ) t2) as [NEQ|NEQ]; last first .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t2 < t1 + δ
progress_of_job <= service sched j (t1 + δ)
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t2 < t1 + δ
progress_of_job <= service sched j (t1 + δ)
move : (job_completes_within_busy_interval _ _ _ _ H_busy_interval) => COMPL.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t2 < t1 + δ COMPL : completed_by sched j t2
progress_of_job <= service sched j (t1 + δ)
apply leq_trans with (job_cost j) => [//|].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t2 < t1 + δ COMPL : completed_by sched j t2
job_cost j <= service sched j (t1 + δ)
rewrite /service -(service_during_cat _ _ _ t2); last by apply /andP; split ; last apply ltnW.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t2 < t1 + δ COMPL : completed_by sched j t2
job_cost j <=
service_during sched j 0 t2 +
service_during sched j t2 (t1 + δ)
by apply leq_trans with (service_during sched j 0 t2); [| rewrite leq_addr].
} Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t1 + δ <= t2
progress_of_job <= service sched j (t1 + δ)
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t1 + δ <= t2
progress_of_job <= service sched j (t1 + δ)
move : H_total_workload_is_bounded => BOUND.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t1 + δ <= t2 BOUND : progress_of_job +
cumulative_interference j t1 (t1 + δ) <= δ
progress_of_job <= service sched j (t1 + δ)
rewrite addnC in BOUND; apply leq_subRL_impl in BOUND.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t1 + δ <= t2 BOUND : progress_of_job <=
δ - cumulative_interference j t1 (t1 + δ)
progress_of_job <= service sched j (t1 + δ)
apply leq_trans with (δ - cumulative_interference j t1 (t1 + δ)) => [//|].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t1 + δ <= t2 BOUND : progress_of_job <=
δ - cumulative_interference j t1 (t1 + δ)
δ - cumulative_interference j t1 (t1 + δ) <=
service sched j (t1 + δ)
apply leq_trans with (service_during sched j t1 (t1 + δ)).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t1 + δ <= t2 BOUND : progress_of_job <=
δ - cumulative_interference j t1 (t1 + δ)
δ - cumulative_interference j t1 (t1 + δ) <=
service_during sched j t1 (t1 + δ)
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t1 + δ <= t2 BOUND : progress_of_job <=
δ - cumulative_interference j t1 (t1 + δ)
δ - cumulative_interference j t1 (t1 + δ) <=
service_during sched j t1 (t1 + δ)
eapply leq_trans.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t1 + δ <= t2 BOUND : progress_of_job <=
δ - cumulative_interference j t1 (t1 + δ)
δ - cumulative_interference j t1 (t1 + δ) <= ?n
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t1 + δ <= t2 BOUND : progress_of_job <=
δ - cumulative_interference j t1 (t1 + δ)
δ - cumulative_interference j t1 (t1 + δ) <= ?n
by apply leq_sub2r, (interference_is_complement_to_schedule t1 t2);
[apply H_busy_interval | apply leqnn | apply NEQ].
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t1 + δ <= t2 BOUND : progress_of_job <=
δ - cumulative_interference j t1 (t1 + δ)
service_during sched j t1 (t1 + δ) +
cumulative_interference j t1 (t1 + δ) -
cumulative_interference j t1 (t1 + δ) <=
service_during sched j t1 (t1 + δ)
by rewrite -addnBA // subnn addn0 //.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t1 + δ <= t2 BOUND : progress_of_job <=
δ - cumulative_interference j t1 (t1 + δ)
service_during sched j t1 (t1 + δ) <=
service sched j (t1 + δ)
rewrite /service -[X in _ <= X](service_during_cat _ _ _ t1); first by rewrite leq_addl //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs
arr_seq tsk : Task H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j δ : duration H_total_workload_is_bounded : progress_of_job +
cumulative_interference
j t1 (t1 + δ) <= δ NEQ : t1 + δ <= t2 BOUND : progress_of_job <=
δ - cumulative_interference j t1 (t1 + δ)
0 <= t1 <= t1 + δ
by apply /andP; split ; last rewrite leq_addr.
}
Qed .
End InterferenceBoundedImpliesEnoughService .
End LowerBoundOnService .