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.rbf.[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.abstract .IBF.supply_task.
Require Export prosa.analysis.abstract .restricted_supply.abstract_rta.
(** * Abstract Response-Time Analysis for Restricted-Supply Processors with Sequential Tasks *)
(** In this section we propose a general framework for response-time
analysis (RTA) for real-time tasks with arbitrary arrival models
and _sequential_ _tasks_ under uni-processor scheduling subject to
supply restrictions, characterized by a given [SBF]. *)
(** In this section, we assume tasks to be sequential. This allows us
to establish a more precise response-time bound, since jobs of the
same task will be executed strictly in the order they arrive. *)
Section AbstractRTARestrictedSupplySequential .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskRunToCompletionThreshold Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context {jc : JobCost Job}.
Context `{JobPreemptable Job}.
(** Consider any kind of fully-supply-consuming, unit-supply
processor state model. *)
Context `{PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
(** Consider any valid arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
(** Consider any restricted supply uniprocessor schedule of this
arrival sequence ... *)
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival nor after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_valid_job_cost :
arrivals_have_valid_job_costs arr_seq.
(** Consider a task set [ts] ... *)
Variable ts : list Task.
(** ... and a task [tsk] of [ts] that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Consider a valid preemption model ... *)
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
(** ... with valid task run-to-completion thresholds. That is,
[task_rtc tsk] is (1) no bigger than [tsk]'s cost and (2) for
any job [j] of task [tsk] [job_rtct j] is bounded by [task_rtct
tsk]. *)
Hypothesis H_valid_run_to_completion_threshold :
valid_task_run_to_completion_threshold arr_seq tsk.
(** Let [max_arrivals] be a family of valid arrival curves, i.e.,
for any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
bound of [tsk], and (2) it is a monotonic function that equals
[0] for the empty interval [delta = 0]. *)
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
(** Assume we are provided with functions characterizing
interference and interfering workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** Let's define a local name for clarity. *)
Let task_rbf := task_request_bound_function tsk.
(** We assume that the scheduler is work-conserving. *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** Unlike the more general, underlying theorem
[uniprocessor_response_time_bound_restricted_supply], we assume
that tasks are sequential. *)
Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
Hypothesis H_interference_and_workload_consistent_with_sequential_tasks :
interference_and_workload_consistent_with_sequential_tasks arr_seq sched tsk.
(** Let [L] be a constant that bounds any busy interval of task [tsk]. *)
Variable L : duration.
Hypothesis H_busy_interval_exists :
busy_intervals_are_bounded_by arr_seq sched tsk L.
(** Consider a unit SBF valid in busy intervals (w.r.t. task
[tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
supply produced during a busy-interval prefix of length [Δ] is
at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
Context {SBF : SupplyBoundFunction}.
Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
(** Next, we assume that [task_intra_IBF] is a bound on intra-supply
interference incurred by task [tsk]. That is, [task_intra_IBF]
bounds interference ignoring interference due to lack of supply
_and_ due to self-interference. *)
Variable task_intra_IBF : duration -> duration -> duration.
Hypothesis H_interference_inside_reservation_is_bounded :
task_intra_interference_is_bounded_by arr_seq sched tsk task_intra_IBF.
(** We use the function [task_intra_IBF], which satisfies the
hypothesis [task_intra_interference_is_bounded_by], to construct
a new function [intra_IBF := (task_rbf (A + ε) - task_cost tsk)
+ task_intra_IBF A Δ] that satisfies the hypothesis
[intra_interference_is_bounded_by]. This is needed to later
apply the lemma
[uniprocessor_response_time_bound_restricted_supply] from file
[restricted_supply/abstract_rta] (recall that it requires
[intra_IBF], not [task_intra_IBF]). *)
(** The logic behind [intra_IBF] is quite simple. Consider a job [j]
of task [tsk] that arrives exactly [A] units after the beginning
of the busy interval. Then the bound on the total interference
incurred by [j] within an interval of length [Δ] is no greater
than [task_rbf (A + ε) - task_cost tsk + task_intra_IBF A
Δ]. Note that, for sequential tasks, the bound consists of two
parts: (1) the part that bounds the interference received from
other jobs of task [tsk] -- [task_rbf (A + ε) - task_cost tsk]
-- and (2) any other interference that is bounded by
[task_intra_IBF(tsk, A, Δ)]. *)
Let intra_IBF (A Δ : duration) :=
(task_rbf (A + ε) - task_cost tsk) + task_intra_IBF A Δ.
(** For clarity, let's define a local name for the search space. *)
Let is_in_search_space_rs := is_in_search_space L intra_IBF.
(** We use the following equation to bound the response-time of a
job of task [tsk]. Consider any value [R] that upper-bounds the
solution of each response-time recurrence, i.e., for any
relative arrival time [A] in the search space, there exists a
corresponding solution [F] such that
(1) [F <= A + R],
(2) [(task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + task_intra_IBF A F <= SBF F],
(3) and [SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R)]. *)
Variable R : duration.
Hypothesis H_R_is_maximum_seq_rs :
forall (A : duration),
is_in_search_space_rs A ->
exists (F : duration),
F <= A + R
/\ (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + task_intra_IBF A F <= SBF F
/\ SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R).
(** In the following section we prove that all the premises of
[aRSA] are satisfied. *)
Section aRSAPremises .
(** First, we show that [intra_IBF] correctly upper-bounds
interference in the preemptive stage of execution. *)
Lemma IBF_P_bounds_interference :
intra_interference_is_bounded_by arr_seq sched tsk intra_IBF.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)
intra_interference_is_bounded_by arr_seq sched tsk
intra_IBF
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)
intra_interference_is_bounded_by arr_seq sched tsk
intra_IBF
move => t1 t2 Δ j ARR TSK BUSY LT NCOM A PAR; move : (PAR _ _ BUSY) => EQ.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1
cumul_cond_interference (fun => [eta has_supply sched])
j t1 (t1 + Δ) <= intra_IBF A Δ
have [ZERO|POS] := posnP (@job_cost _ jc j).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 ZERO : job_cost j = 0
cumul_cond_interference (fun => [eta has_supply sched])
j t1 (t1 + Δ) <= intra_IBF A Δ
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 ZERO : job_cost j = 0
cumul_cond_interference (fun => [eta has_supply sched])
j t1 (t1 + Δ) <= intra_IBF A Δ
exfalso ; move : NCOM => /negP NCOM; apply : NCOM.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 ZERO : job_cost j = 0
completed_by sched j (t1 + Δ)
by rewrite /service.completed_by ZERO. } Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost j
cumul_cond_interference (fun => [eta has_supply sched])
j t1 (t1 + Δ) <= intra_IBF A Δ
rewrite (cumul_cond_interference_ID _ (nonself arr_seq sched)).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost j
cumul_cond_interference
(fun (j : Job) (t : instant) =>
has_supply sched t && nonself arr_seq sched j t) j
t1 (t1 + Δ) +
cumul_cond_interference
(fun (j : Job) (t : instant) =>
has_supply sched t && ~~ nonself arr_seq sched j t)
j t1 (t1 + Δ) <= intra_IBF A Δ
rewrite /intra_IBF addnC leq_add; first by done .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost j
cumul_cond_interference
(fun (j : Job) (t : instant) =>
has_supply sched t && ~~ nonself arr_seq sched j t)
j t1 (t1 + Δ) <= task_rbf (A + 1 ) - task_cost tsk
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost j
cumul_cond_interference
(fun (j : Job) (t : instant) =>
has_supply sched t && ~~ nonself arr_seq sched j t)
j t1 (t1 + Δ) <= task_rbf (A + 1 ) - task_cost tsk
rewrite -(leq_add2r (cumul_task_interference arr_seq sched j t1 (t1 + Δ))).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost j
cumul_cond_interference
(fun (j : Job) (t : instant) =>
has_supply sched t && ~~ nonself arr_seq sched j t)
j t1 (t1 + Δ) +
cumul_task_interference arr_seq sched j t1 (t1 + Δ) <=
task_rbf (A + 1 ) - task_cost tsk +
cumul_task_interference arr_seq sched j t1 (t1 + Δ)
eapply leq_trans; first last .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost j
?n <=
task_rbf (A + 1 ) - task_cost tsk +
cumul_task_interference arr_seq sched j t1 (t1 + Δ)
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost j
?n <=
task_rbf (A + 1 ) - task_cost tsk +
cumul_task_interference arr_seq sched j t1 (t1 + Δ)
by rewrite EQ; apply : task.cumulative_job_interference_bound => //. } Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost j
cumul_cond_interference
(fun (j : Job) (t : instant) =>
has_supply sched t && ~~ nonself arr_seq sched j t)
j t1 (t1 + Δ) +
cumul_task_interference arr_seq sched j t1 (t1 + Δ) <=
cumulative_interference j t1 (t1 + Δ)
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost j
cumul_cond_interference
(fun (j : Job) (t : instant) =>
has_supply sched t && ~~ nonself arr_seq sched j t)
j t1 (t1 + Δ) +
cumul_task_interference arr_seq sched j t1 (t1 + Δ) <=
cumulative_interference j t1 (t1 + Δ)
rewrite -big_split //= leq_sum // /cond_interference => t _.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost jt : nat
has_supply sched t && ~~ nonself arr_seq sched j t &&
interference j t +
nonself arr_seq sched j t && interference j t <=
true && interference j t
by case (interference j t), (has_supply sched t), (nonself arr_seq sched j t) => //. } } Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost j
cumul_cond_interference
(fun (j : Job) (t : instant) =>
has_supply sched t && nonself arr_seq sched j t) j
t1 (t1 + Δ) <= task_intra_IBF A Δ
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost j
cumul_cond_interference
(fun (j : Job) (t : instant) =>
has_supply sched t && nonself arr_seq sched j t) j
t1 (t1 + Δ) <= task_intra_IBF A Δ
rewrite (cumul_cond_interference_pred_eq _ (nonself_intra arr_seq sched)) => //.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) A : nat PAR : relative_arrival_time_of_job_is_A sched j A EQ : A = job_arrival j - t1 POS : 0 < job_cost j
forall (j : Job) (t : instant),
has_supply sched t && nonself arr_seq sched j t <->
nonself_intra arr_seq sched j t
by move => s t; split => //; rewrite andbC. }
Qed .
(** To rule out pathological cases with the
[H_R_is_maximum_seq_rs] equation (such as [task_cost tsk]
being greater than [task_rbf (A + ε)]), we assume that the
arrival curve is non-pathological. *)
Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
(** To later apply the theorem
[uniprocessor_response_time_bound_restricted_supply], we need
to provide the IBF, which bounds the total interference. *)
Let IBF A Δ := Δ - SBF Δ + intra_IBF A Δ.
(** Next we prove that [H_R_is_maximum_seq_rs] implies
[H_R_is_maximum_rs] from file ([.../restricted_supply/abstract_rta.v]).
In other words, a solution to the response-time recurrence for
restricted-supply processor models with sequential tasks can
be translated to a solution for the same processor model with
non-necessarily sequential tasks. *)
Lemma sol_seq_rs_equation_impl_sol_rs_equation :
forall (A : duration),
is_in_search_space L IBF A ->
exists F : duration,
F <= A + R
/\ task_rtct tsk + intra_IBF A F <= SBF F
/\ SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat
forall A : duration,
is_in_search_space L IBF A ->
exists F : duration,
F <= A + R /\
task_rtct tsk + intra_IBF A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat
forall A : duration,
is_in_search_space L IBF A ->
exists F : duration,
F <= A + R /\
task_rtct tsk + intra_IBF A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
rewrite /IBF; move => A SP.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A
exists F : duration,
F <= A + R /\
task_rtct tsk + intra_IBF A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
move : (H_R_is_maximum_seq_rs A) => T.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A T : is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
exists F : duration,
F <= A + R /\
task_rtct tsk + intra_IBF A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
feed T. Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A T : is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
is_in_search_space_rs A
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A T : is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
is_in_search_space_rs A
move : SP => [ZERO|[POS [x [LT NEQ]]]]; first by left .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration T : is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R) POS : 0 < A < Lx : nat LT : x < L NEQ : x - SBF x + intra_IBF (A - 1 ) x <>
x - SBF x + intra_IBF A x
is_in_search_space_rs A
by right ; split => //; exists x ; split => //. } Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A T : exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
exists F : duration,
F <= A + R /\
task_rtct tsk + intra_IBF A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
have [F [EQ0 [EQ1 EQ2]]] := T; clear T.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
exists F : duration,
F <= A + R /\
task_rtct tsk + intra_IBF A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
exists F ; split => //; split => //.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
task_rtct tsk + intra_IBF A F <= SBF F
rewrite /intra_IBF -(leqRW EQ1) addnA leq_add2r.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
task_rtct tsk + (task_rbf (A + 1 ) - task_cost tsk) <=
task_rbf (A + 1 ) - (task_cost tsk - task_rtct tsk)
rewrite addnBA; last first .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
task_cost tsk <= task_rbf (A + 1 )
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
task_cost tsk <= task_rbf (A + 1 )
apply leq_trans with (task_rbf 1 ).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
task_cost tsk <= task_rbf 1
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
task_cost tsk <= task_rbf 1
by apply : task_rbf_1_ge_task_cost => //.
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
task_rbf 1 <= task_rbf (A + 1 )
by eapply task_rbf_monotone => //; rewrite addn1. } Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
task_rtct tsk + task_rbf (A + 1 ) - task_cost tsk <=
task_rbf (A + 1 ) - (task_cost tsk - task_rtct tsk)
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
task_rtct tsk + task_rbf (A + 1 ) - task_cost tsk <=
task_rbf (A + 1 ) - (task_cost tsk - task_rtct tsk)
rewrite subnBA.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
task_rtct tsk + task_rbf (A + 1 ) - task_cost tsk <=
task_rbf (A + 1 ) + task_rtct tsk - task_cost tsk
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
task_rtct tsk + task_rbf (A + 1 ) - task_cost tsk <=
task_rbf (A + 1 ) + task_rtct tsk - task_cost tsk
by rewrite addnC.
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)H_arrival_curve_pos : 0 < max_arrivals tsk 1 IBF := fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ: duration -> nat -> nat A : duration SP : is_in_search_space L
(fun (A : duration) (Δ : nat) =>
Δ - SBF Δ + intra_IBF A Δ) A F : duration EQ0 : F <= A + R EQ1 : task_rbf (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF A F <=
SBF F EQ2 : SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
task_rtct tsk <= task_cost tsk
by apply H_valid_run_to_completion_threshold. }
Qed .
End aRSAPremises .
(** Finally, we apply the
[uniprocessor_response_time_bound_restricted_supply] theorem,
and using the lemmas above, prove that all its requirements are
satisfied. Hence, [R] is a response-time bound for task [tsk]. *)
Theorem uniprocessor_response_time_bound_restricted_supply_seq :
task_response_time_bound arr_seq sched tsk R.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)
task_response_time_bound arr_seq sched tsk R
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)
task_response_time_bound arr_seq sched tsk R
move => j ARR TSK.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j
job_response_time_bound sched j R
eapply uniprocessor_response_time_bound_restricted_supply => //.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j
intra_interference_is_bounded_by arr_seq sched tsk
?intra_IBF
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j
intra_interference_is_bounded_by arr_seq sched tsk
?intra_IBF
exact : IBF_P_bounds_interference. } Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j
forall A : duration,
is_in_search_space L
(fun A0 Δ : duration => Δ - SBF Δ + intra_IBF A0 Δ)
A ->
exists F : duration,
F <= A + R /\
task_rtct tsk + intra_IBF A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job jc : JobCost Job H3 : JobPreemptable Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState H_consumed_supply_proc_model : fully_consuming_proc_model PState arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H4 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H5 : Interference Job H6 : InterferingWorkload Job task_rbf := task_request_bound_function tsk : duration -> nat H_work_conserving : work_conserving arr_seq sched H_sequential_tasks : sequential_tasks arr_seq sched H_interference_and_workload_consistent_with_sequential_tasks : interference_and_workload_consistent_with_sequential_tasks
arr_seq sched
tsk L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L SBF : SupplyBoundFunction H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF H_unit_SBF : unit_supply_bound_function SBF task_intra_IBF : duration -> duration -> duration H_interference_inside_reservation_is_bounded : task_intra_interference_is_bounded_by
arr_seq sched
tsk
task_intra_IBF intra_IBF := fun A Δ : duration =>
task_rbf (A + 1 ) - task_cost tsk +
task_intra_IBF A Δ: duration -> duration -> nat is_in_search_space_rs := is_in_search_space L intra_IBF : nat -> Prop R : duration H_R_is_maximum_seq_rs : forall A : duration,
is_in_search_space_rs A ->
exists F : duration,
F <= A + R /\
task_rbf (A + 1 ) -
(task_cost tsk -
task_rtct tsk) +
task_intra_IBF A F <=
SBF F /\
SBF F +
(task_cost tsk -
task_rtct tsk) <=
SBF (A + R)j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j
forall A : duration,
is_in_search_space L
(fun A0 Δ : duration => Δ - SBF Δ + intra_IBF A0 Δ)
A ->
exists F : duration,
F <= A + R /\
task_rtct tsk + intra_IBF A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
exact : sol_seq_rs_equation_impl_sol_rs_equation. }
Qed .
End AbstractRTARestrictedSupplySequential .