Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.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.definitions.schedulability.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.analysis.abstract .search_space.
Require Export prosa.analysis.abstract .lower_bound_on_service.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** * Abstract Response-Time Analysis *)
(** In this module, we propose the general framework for response-time
analysis (RTA) of uni-processor scheduling of real-time tasks with
arbitrary arrival models. *)
(** We prove that the maximum (with respect to the set of offsets)
among the solutions of the response-time bound recurrence is a
response-time bound for the task under analysis. *)
Section Abstract_RTA .
(** 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 `{JobCost Job}.
(** Consider _any_ kind of processor state model. *)
Context {PState : ProcessorState Job}.
(** Consider any arrival and any schedule of this arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Variable sched : schedule PState.
(** 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.
(** Assume we are provided with abstract functions for interference
and interfering workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** We assume that the scheduler is work-conserving. *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** Let [L] be a constant that bounds the length of any busy interval of task [tsk]. *)
Variable L : duration.
Hypothesis H_bounded_busy_interval_exists :
busy_intervals_are_bounded_by arr_seq sched tsk L.
(** Note that response-time analyses are static analyses and by
definition have no access to dynamic information of an
individual execution of a system. However, oftentimes some
dynamic information can improve the tightness of a response-time
bound. For example, in case of a model with sequential tasks,
information about relative arrival time of a job can be used to
bound the maximum self-interference. *)
(** To gain access to some dynamic information for a response-time
recurrence, one can _assume_ that an execution of a system
satisfies a statically defined predicate. Then a response-time
bound can be calculated by considering a family of inputs to the
predicate that covers all the relevant dynamic scenarios.
To give a concrete example, one can (1) assume that any job [j]
of a task [tsk] arrives exactly [A] time units after the
beginning of [j]'s busy interval, (2) calculate the
response-time bound of [tsk] as if the assumption of step (1)
was satisfied, and (3) try all the possible [A]s. That results
in a "relative-arrival"-aware analysis. *)
(** The idea we will employ in this file is that one can use more
sophisticated dynamic information in a response-time recurrence.
In the following, we consider a case when information about (1)
relative arrival time of a job and (2) relative time when any
job of task [tsk] receives at least [task_rtc tsk] units of
service is used in the response-time recurrence. *)
(** Next, the response-time analysis will proceed in a sequence of
stages. A stage defines the set of sources of interference that
can postpone the execution of a job. Note that this separation
is mostly a design question. And for different models there might be
a varying number of stages with different meanings. *)
(** For our purposes, we consider two stages. *)
(** First stage: A job [j] can be (1) preempted because of the
presence of higher-or-equal priority workload and (2) make no
progress due to some other reason (spinning, lack of supply, and
so on). To bound all this interference we introduce an
interference bound function [IBF_P]. Note that [IBF_P] (1)
counts any job with higher-or-equal priority as interference and
(2) depends on the relative arrival time of a job. To bound time
that [j] spends in the first stage, we need to find a fixpoint
of equation [F : task_rtc tsk + IBF_P tsk A F ≤ F]. *)
(** To formalize the dependency of [IBF_P] on the relative arrival
time in Coq, we introduce a predicate that tests whether a job
[j] arrives exactly [A] time units after the beginning of its
busy interval, which is unique (if it exists). *)
Definition relative_arrival_time_of_job_is_A (j : Job) (A : duration) :=
forall (t1 t2 : instant),
busy_interval sched j t1 t2 ->
job_arrival j = t1 + A.
(** Next, consider a valid interference bound function [IBF_P] that
can use information about relative time arrival of a job of task
[tsk]. Recall that an interference bound function gives a bound on
the cumulative interference incurred by jobs of task [tsk]. *)
Variable IBF_P : Task -> (* A *) duration -> (* Δ *) duration -> duration.
Hypothesis H_job_interference_is_bounded_IBFP :
job_interference_is_bounded_by
arr_seq sched tsk IBF_P relative_arrival_time_of_job_is_A.
(** Second stage: Job [j] reaches its run-to-completion
threshold. After this point the job cannot be preempted by a
high-or-equal priority job (so we can forget about any
task-generated workload). At this stage, the only reason why the
job cannot make progress is due to lack of supply or similar. To
bound time that [j] spends in the second stage we use
[IBF_NP]. Note that the amount of interference may depend on the
relative time when job [j] receives [task_rtc tsk] units of
service; hence, [IBF_NP] depends on this parameter. Also, notice
that [IBF_NP] still bounds interference starting from the
beginning of the busy window, even though it can use the
solution of the first fixpoint equation. *)
(** To formalize the dependency of [IBF_NP] on the relative time
when job [j] receives [task_rtc tsk] units of service in Coq, we
introduce a predicate that tests whether a job [j] has more than
[task_rtc tsk] units of service at a time instant [t1 + F],
where [t1] is the beginning of [j]'s busy interval. The first
conjunct of the proposition is needed to derive a fact that by
time [t1 + F] job [j] does not receive any interference from
higher-or-equal priority jobs. *)
Definition relative_time_to_reach_rtct (j : Job) (F : duration) :=
forall (t1 t2 : instant),
busy_interval sched j t1 t2 ->
task_rtct tsk + IBF_P tsk (job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F).
(** Next, consider a valid interference bound function [IBF_NP] that
can use information about the relative time when any given job of task
[tsk] receives at least [task_rtc tsk] units of service. *)
Variable IBF_NP : Task -> (* F *) duration -> (* Δ *) duration -> duration.
Hypothesis H_job_interference_is_bounded_IBFNP :
job_interference_is_bounded_by
arr_seq sched tsk IBF_NP relative_time_to_reach_rtct.
(** In addition, we assume that [IBF_NP] indeed takes into account
information received in the first stage. Specifically, we assume
that the sum of [tsk]'s cost and [IBF_NP tsk F Δ] is never smaller
than [F]. This intuitively means that the second stage cannot
have a solution that is smaller than the solution to the first
stage. *)
Hypothesis H_IBF_NP_ge_param : forall F Δ , F <= task_cost tsk + IBF_NP tsk F Δ.
(** Given [IBF_P] and [IBF_NP] we construct a response-time recurrence. *)
(** For clarity, let's define a local name for the search space. *)
Let is_in_search_space A := is_in_search_space tsk L IBF_P A.
(** 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 [task_rtc tsk + IBF_P tsk A
F ≤ F] and [task_cost tsk + IBF_NP tsk F (A + R) ≤ A + R]. *)
Variable R : duration.
Hypothesis H_R_is_maximum :
forall (A : duration),
is_in_search_space A ->
exists (F : duration),
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk + IBF_NP tsk F (A + R) <= A + R.
(** * Proof of the Theorem *)
(** In the next section we show a detailed proof of the main theorem
that establishes that [R] is indeed a response-time bound of
task [tsk]. *)
Section ProofOfTheorem .
(** Consider any job [j] of [tsk] with a positive cost. Note that
the assumption about positive job cost is needed to apply
hypothesis [H_bounded_busy_interval_exists]. Later, we
consider the case when [job_cost j = 0] as well. This way, we
ensure that this assumption does not propagate further. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** Assume we have a busy interval <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval sched j t1 t2.
(** Let's define [A] as a relative arrival time of job
[j] (with respect to time [t1]). *)
Let A := job_arrival j - t1.
(** First, note that [job_arrival j] is equal to [t1 + A]. *)
Fact job_arrival_eq_t1_plus_A : job_arrival j = t1 + A.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat
job_arrival j = t1 + A
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat
job_arrival j = t1 + A
by move : H_busy_interval => [[/andP [GT LT] _] _]; rewrite /A subnKC. Qed .
(** Since the length of the busy interval is bounded by [L], the
relative arrival time [A] of job [j] is less than [L]. *)
Fact relative_arrival_is_bounded : A < L.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat
A < L
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat
A < L
move : (H_job_of_tsk) => /eqP TSK.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat TSK : job_task j = tsk
A < L
edestruct H_bounded_busy_interval_exists as [t1' [t2' [_ [BOUND BUSY]]]]; rt_eauto.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat TSK : job_task j = tsk t1', t2' : nat BOUND : t2' <= t1' + L BUSY : busy_interval sched j t1' t2'
A < L
edestruct busy_interval_is_unique; [exact H_busy_interval | exact BUSY| ].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat TSK : job_task j = tsk t1', t2' : nat BOUND : t2' <= t1' + L BUSY : busy_interval sched j t1' t2' H6 : t1 = t1' H7 : t2 = t2'
A < L
subst t1' t2'; clear BUSY.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat TSK : job_task j = tsk BOUND : t2 <= t1 + L
A < L
apply leq_trans with (t2 - t1); last by rewrite leq_subLR.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat TSK : job_task j = tsk BOUND : t2 <= t1 + L
A < t2 - t1
move : (H_busy_interval)=> [[/andP [T1 T3] [_ _]] _].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat TSK : job_task j = tsk BOUND : t2 <= t1 + L T1 : t1 <= job_arrival j T3 : job_arrival j < t2
A < t2 - t1
by apply ltn_sub2r; first apply leq_ltn_trans with (job_arrival j).
Qed .
(** In order to prove that [R] is a response-time bound of job
[j], we use hypothesis [H_R_is_maximum]. Note that the
relative arrival time [A] does not necessarily belong to the
search space. However, earlier (see file
[abstract.search_space]) we have proven that for any [A] there
exists another [A_sp] from the search space that shares the
same [IBF_P] value.
Moreover, since the function [IBF_P(A, ⋅)] is equivalent to
the function [IBF_P(A_sp, ⋅)], a solution [F] for [task_rtc
tsk + IBF_P tsk A_sp F ≤ F] also is a solution for [task_rtc
tsk + IBF_P tsk A F ≤ F]. Thus, despite the fact that the
relative arrival time may not lie in the search space, we can
still use the assumption [H_R_is_maximum]. *)
(** More formally, consider any [A_sp] such that: *)
Variable A_sp : duration.
(** (a) [A_sp] is less than or equal to [A]. *)
Hypothesis H_Asp_le_A : A_sp <= A.
(** (b) [IBF_P A x] is equal to [IBF_P A_sp x] for all [x] less than [L]. *)
Hypothesis H_equivalent :
are_equivalent_at_values_less_than (IBF_P tsk A) (IBF_P tsk A_sp) L.
(** (c) [A_sp] is in the search space. *)
Hypothesis H_Asp_is_in_search_space : is_in_search_space A_sp.
(** (d) [F] such that ... *)
Variable F : duration.
(** ... [F] is a solution of the response-time recurrence. *)
Hypothesis H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F.
(** And finally, (e) [task_cost tsk + IBF_NP tsk F (A_sp + R)] is
no greater than [A_sp + R]. *)
Hypothesis H_Asp_R_fixpoint :
task_cost tsk + IBF_NP tsk F (A_sp + R) <= A_sp + R.
(** ** Case 1 *)
(** First, we consider the case where the solution [F] is so large
that the value of [t1 + F] goes beyond the busy
interval. Depending on the pessimism of [IBF_P] and [IBP_NP]
this might be either possible or impossible. Regardless, the
response-time bound can be easily proven, since any job that
completes by the end of the busy interval remains
completed. *)
Section FixpointOutsideBusyInterval1 .
(** By assumption, suppose that [t2] is less than or equal to [t1 + F]. *)
Hypothesis H_big_fixpoint_solution : t2 <= t1 + F.
(** Then we prove that [job_arrival j + R] is no less than [t2]. *)
Lemma t2_le_arrival_plus_R_1 :
t2 <= job_arrival j + R.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F
t2 <= job_arrival j + R
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F
t2 <= job_arrival j + R
move : H_busy_interval => [[/andP [GT LT] [QT1 NTQ]] QT2].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
t2 <= job_arrival j + R
apply leq_trans with (t1 + F); first by done .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
t1 + F <= job_arrival j + R
rewrite job_arrival_eq_t1_plus_A -addnA leq_add2l.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
F <= A + R
rewrite -(leqRW H_Asp_le_A) -(leqRW H_Asp_R_fixpoint).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
F <= task_cost tsk + IBF_NP tsk F (A_sp + R)
by apply H_IBF_NP_ge_param.
Qed .
(** But since we know that the job is completed by the end of
its busy interval, we can show that job [j] is completed by
[job arrival j + R]. *)
Lemma job_completed_by_arrival_plus_R_1 :
completed_by sched j (job_arrival j + R).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F
completed_by sched j (job_arrival j + R)
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F
completed_by sched j (job_arrival j + R)
move : H_busy_interval => [[/andP [GT LT] [QT1 NTQ]] QT2].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
completed_by sched j (job_arrival j + R)
apply completion_monotonic with t2; rt_eauto.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
t2 <= job_arrival j + R
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
t2 <= job_arrival j + R
by apply t2_le_arrival_plus_R_1.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
completed_by sched j t2
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_big_fixpoint_solution : t2 <= t1 + F GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
completed_by sched j t2
by eapply job_completes_within_busy_interval; rt_eauto.
Qed .
End FixpointOutsideBusyInterval1 .
(** ** Case 2 *)
(** Next, we consider the case where the solution of the first
recurrence is small ([t1 + F < t2]), but the solution of the
second fixpoint goes beyond the busy interval. Although this
case may be (also) impossible, the response-time bound can be
easily proven, since any job that completes by the end of the
busy interval remains completed. *)
Section FixpointOutsideBusyInterval2 .
(** Assume that [t1 + F] is less than [t2], ... *)
Hypothesis H_small_fixpoint_solution : t1 + F < t2.
(** ... but [t1 + (A_sp + R)] is at least [t2]. *)
Hypothesis H_big_fixpoint_solution : t2 <= t1 + (A_sp + R).
(** Then we prove that [job_arrival j + R] is no less than [t2]. *)
Lemma t2_le_arrival_plus_R_2 :
t2 <= job_arrival j + R.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution : t1 + F < t2 H_big_fixpoint_solution : t2 <= t1 + (A_sp + R)
t2 <= job_arrival j + R
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution : t1 + F < t2 H_big_fixpoint_solution : t2 <= t1 + (A_sp + R)
t2 <= job_arrival j + R
move : H_busy_interval => [[/andP [GT LT] [QT1 NTQ]] QT2].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution : t1 + F < t2 H_big_fixpoint_solution : t2 <= t1 + (A_sp + R) GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
t2 <= job_arrival j + R
apply leq_trans with (t1 + (A_sp + R)); first by done .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution : t1 + F < t2 H_big_fixpoint_solution : t2 <= t1 + (A_sp + R) GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
t1 + (A_sp + R) <= job_arrival j + R
by rewrite job_arrival_eq_t1_plus_A -addnA leq_add2l leq_add2r.
Qed .
(** But since we know that the job is completed by the end of
its busy interval, we can show that job [j] is completed by
[job arrival j + R]. *)
Lemma job_completed_by_arrival_plus_R_2 :
completed_by sched j (job_arrival j + R).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution : t1 + F < t2 H_big_fixpoint_solution : t2 <= t1 + (A_sp + R)
completed_by sched j (job_arrival j + R)
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution : t1 + F < t2 H_big_fixpoint_solution : t2 <= t1 + (A_sp + R)
completed_by sched j (job_arrival j + R)
move : H_busy_interval => [[/andP [GT LT] [QT1 NTQ]] QT2].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution : t1 + F < t2 H_big_fixpoint_solution : t2 <= t1 + (A_sp + R) GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
completed_by sched j (job_arrival j + R)
apply completion_monotonic with t2; try done .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution : t1 + F < t2 H_big_fixpoint_solution : t2 <= t1 + (A_sp + R) GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
t2 <= job_arrival j + R
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution : t1 + F < t2 H_big_fixpoint_solution : t2 <= t1 + (A_sp + R) GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
t2 <= job_arrival j + R
by apply t2_le_arrival_plus_R_2.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution : t1 + F < t2 H_big_fixpoint_solution : t2 <= t1 + (A_sp + R) GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
completed_by sched j t2
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution : t1 + F < t2 H_big_fixpoint_solution : t2 <= t1 + (A_sp + R) GT : t1 <= job_arrival j LT : job_arrival j < t2 QT1 : quiet_time sched j t1 NTQ : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
completed_by sched j t2
by eapply job_completes_within_busy_interval; rt_eauto.
Qed .
End FixpointOutsideBusyInterval2 .
(** ** Case 3 *)
(** Next, we consider the case when both solutions are smaller
than the length of the busy interval. *)
Section FixpointsInsideBusyInterval .
(** So, assume that [t1 + F] and [t1 + (A_sp + R)] are both
smaller than [t2]. *)
Hypothesis H_small_fixpoint_solution1 : t1 + F < t2.
Hypothesis H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2.
(** First note that [F] is indeed less than [L]. *)
Lemma relative_rtc_time_is_bounded : F < L.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2
F < L
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2
F < L
edestruct H_bounded_busy_interval_exists as [t1' [t2' [_ [BOUND BUSY]]]]; eauto 2 .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 t1', t2' : nat BOUND : t2' <= t1' + L BUSY : busy_interval sched j t1' t2'
F < L
edestruct busy_interval_is_unique; [exact H_busy_interval | exact BUSY| ].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 t1', t2' : nat BOUND : t2' <= t1' + L BUSY : busy_interval sched j t1' t2' H6 : t1 = t1' H7 : t2 = t2'
F < L
subst t1' t2'; clear BUSY.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 BOUND : t2 <= t1 + L
F < L
apply leq_trans with (t2 - t1); last by rewrite leq_subLR.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 BOUND : t2 <= t1 + L
F < t2 - t1
by rewrite ltn_subRL.
Qed .
(** Next we consider two sub-cases. *)
(** *** Case 3.1 *)
(** The cost of job [j] is smaller than or equal to the
run-to-completion threshold of task [tsk]. *)
Section JobCostIsSmall .
(** We assume that [job_cost j <= task_rtc tsk]. *)
Hypothesis H_job_cost_is_small : job_cost j <= task_rtct tsk.
(** Then we apply lemma [j_receives_enough_service] with
parameters [progress_of_job := job_cost j] and [delta :=
F] to obtain the fact that the service of [j] by time [t1
+ F] is no less than [job_cost j] (that is, the job is
completed). *)
Lemma job_receives_enough_service_1 :
job_cost j <= service sched j (t1 + F).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk
job_cost j <= service sched j (t1 + F)
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk
job_cost j <= service sched j (t1 + F)
move_neq_up T; move : (T) => NC; move_neq_down T. Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk NC : service sched j (t1 + F) < job_cost j
job_cost j <= service sched j (t1 + F)
eapply j_receives_enough_service; eauto 2 ;
rewrite /definitions.cumulative_interference.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk NC : service sched j (t1 + F) < job_cost j
job_cost j + \sum_(t1 <= t < t1 + F) interference j t <=
F
rewrite -{2 }(leqRW H_F_fixpoint).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk NC : service sched j (t1 + F) < job_cost j
job_cost j + \sum_(t1 <= t < t1 + F) interference j t <=
task_rtct tsk + IBF_P tsk A_sp F
rewrite leq_add //.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk NC : service sched j (t1 + F) < job_cost j
\sum_(t1 <= t < t1 + F) interference j t <=
IBF_P tsk A_sp F
rewrite -H_equivalent; [ | apply relative_rtc_time_is_bounded].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk NC : service sched j (t1 + F) < job_cost j
\sum_(t1 <= t < t1 + F) interference j t <=
IBF_P tsk A F
eapply H_job_interference_is_bounded_IBFP with t2; try done .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk NC : service sched j (t1 + F) < job_cost j
~~ completed_by sched j (t1 + F)
+ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk NC : service sched j (t1 + F) < job_cost j
~~ completed_by sched j (t1 + F)
by rewrite -ltnNge.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk NC : service sched j (t1 + F) < job_cost j
relative_arrival_time_of_job_is_A j A
+ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk NC : service sched j (t1 + F) < job_cost j
relative_arrival_time_of_job_is_A j A
move => t1' t2' BUSY.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk NC : service sched j (t1 + F) < job_cost j t1', t2' : instant BUSY : busy_interval sched j t1' t2'
job_arrival j = t1' + A
edestruct busy_interval_is_unique; [exact H_busy_interval | exact BUSY| ].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_small : job_cost j <= task_rtct tsk NC : service sched j (t1 + F) < job_cost j t1', t2' : instant BUSY : busy_interval sched j t1' t2' H6 : t1 = t1' H7 : t2 = t2'
job_arrival j = t1' + A
by subst t1' t2'; rewrite -job_arrival_eq_t1_plus_A.
Qed .
End JobCostIsSmall .
(** *** Case 3.2 *)
(** The cost of job [j] is greater than or equal to
the run-to-completion threshold of task [tsk ]. *)
Section JobCostIsBig .
(** We assume that [task_rtc tsk <= job_cost j]. *)
Hypothesis H_job_cost_is_big : task_rtct tsk <= job_cost j.
(** We apply lemma [j_receives_enough_service] with parameters
[progress_of_job := task_rtc tsk] and [delta := F] to
obtain the fact that the service of [j] by time [t1 + F]
is no less than [task_rtc tsk]. *)
Lemma job_receives_enough_service_2 :
task_rtct tsk <= service sched j (t1 + F).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j
task_rtct tsk <= service sched j (t1 + F)
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j
task_rtct tsk <= service sched j (t1 + F)
move_neq_up T; move : (T) (H_job_of_tsk) => NC /eqP TSK; move_neq_down T. Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j NC : service sched j (t1 + F) < task_rtct tsk TSK : job_task j = tsk
task_rtct tsk <= service sched j (t1 + F)
eapply j_receives_enough_service; rt_eauto;
rewrite /definitions.cumulative_interference.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j NC : service sched j (t1 + F) < task_rtct tsk TSK : job_task j = tsk
task_rtct tsk +
\sum_(t1 <= t < t1 + F) interference j t <= F
erewrite leq_trans; last apply H_F_fixpoint; auto .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j NC : service sched j (t1 + F) < task_rtct tsk TSK : job_task j = tsk
task_rtct tsk +
\sum_(t1 <= t < t1 + F) interference j t <=
task_rtct tsk + IBF_P tsk A_sp F
rewrite leq_add //.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j NC : service sched j (t1 + F) < task_rtct tsk TSK : job_task j = tsk
\sum_(t1 <= t < t1 + F) interference j t <=
IBF_P tsk A_sp F
rewrite -H_equivalent; [ | apply relative_rtc_time_is_bounded].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j NC : service sched j (t1 + F) < task_rtct tsk TSK : job_task j = tsk
\sum_(t1 <= t < t1 + F) interference j t <=
IBF_P tsk A F
eapply H_job_interference_is_bounded_IBFP with t2; try done .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j NC : service sched j (t1 + F) < task_rtct tsk TSK : job_task j = tsk
~~ completed_by sched j (t1 + F)
+ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j NC : service sched j (t1 + F) < task_rtct tsk TSK : job_task j = tsk
~~ completed_by sched j (t1 + F)
by rewrite -ltnNge (leqRW NC).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j NC : service sched j (t1 + F) < task_rtct tsk TSK : job_task j = tsk
relative_arrival_time_of_job_is_A j A
+ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j NC : service sched j (t1 + F) < task_rtct tsk TSK : job_task j = tsk
relative_arrival_time_of_job_is_A j A
intros ? ? BUSY.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j NC : service sched j (t1 + F) < task_rtct tsk TSK : job_task j = tsk t0, t3 : instant BUSY : busy_interval sched j t0 t3
job_arrival j = t0 + A
edestruct busy_interval_is_unique; [exact H_busy_interval | exact BUSY| ].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j NC : service sched j (t1 + F) < task_rtct tsk TSK : job_task j = tsk t0, t3 : instant BUSY : busy_interval sched j t0 t3 H6 : t1 = t0 H7 : t2 = t3
job_arrival j = t0 + A
subst t0 t3; clear BUSY.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j NC : service sched j (t1 + F) < task_rtct tsk TSK : job_task j = tsk
job_arrival j = t1 + A
by rewrite -job_arrival_eq_t1_plus_A.
Qed .
(** Next, we again apply lemma [j_receives_enough_service]
with parameters [progress_of_job := job_cost j] and [delta
:= A_sp + R] to obtain the fact that the service of [j] by
time [t1 + (A_sp + R)] is no less than [job_cost j]. *)
Lemma job_receives_enough_service_3 :
job_cost j <= service sched j (t1 + (A_sp + R)).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j
job_cost j <= service sched j (t1 + (A_sp + R))
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j
job_cost j <= service sched j (t1 + (A_sp + R))
move : (H_job_of_tsk) => /eqP TSK.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j TSK : job_task j = tsk
job_cost j <= service sched j (t1 + (A_sp + R))
apply /negPn/negP; intros NC; move : NC => /negP NC; apply NC; move : NC => /negP NC.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j TSK : job_task j = tsk NC : ~~
(job_cost j <= service sched j (t1 + (A_sp + R)))
job_cost j <= service sched j (t1 + (A_sp + R))
eapply j_receives_enough_service; rt_eauto.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j TSK : job_task j = tsk NC : ~~
(job_cost j <= service sched j (t1 + (A_sp + R)))
job_cost j +
cumulative_interference j t1 (t1 + (A_sp + R)) <=
A_sp + R
erewrite leq_trans; [ | | apply H_Asp_R_fixpoint]; auto .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j TSK : job_task j = tsk NC : ~~
(job_cost j <= service sched j (t1 + (A_sp + R)))
job_cost j +
cumulative_interference j t1 (t1 + (A_sp + R)) <=
task_cost tsk + IBF_NP tsk F (A_sp + R)
apply leq_add; [by rewrite -TSK; apply H_valid_job_cost | ].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j TSK : job_task j = tsk NC : ~~
(job_cost j <= service sched j (t1 + (A_sp + R)))
cumulative_interference j t1 (t1 + (A_sp + R)) <=
IBF_NP tsk F (A_sp + R)
eapply H_job_interference_is_bounded_IBFNP with (t2 := t2); eauto 2 .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j TSK : job_task j = tsk NC : ~~
(job_cost j <= service sched j (t1 + (A_sp + R)))
relative_time_to_reach_rtct j F
intros ? ? BUSY.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j TSK : job_task j = tsk NC : ~~
(job_cost j <= service sched j (t1 + (A_sp + R))) t0, t3 : instant BUSY : busy_interval sched j t0 t3
task_rtct tsk + IBF_P tsk (job_arrival j - t0) F <= F /\
task_rtct tsk <= service sched j (t0 + F)
edestruct busy_interval_is_unique; [exact H_busy_interval | exact BUSY| ].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j TSK : job_task j = tsk NC : ~~
(job_cost j <= service sched j (t1 + (A_sp + R))) t0, t3 : instant BUSY : busy_interval sched j t0 t3 H6 : t1 = t0 H7 : t2 = t3
task_rtct tsk + IBF_P tsk (job_arrival j - t0) F <= F /\
task_rtct tsk <= service sched j (t0 + F)
subst t0 t3; clear BUSY; split .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j TSK : job_task j = tsk NC : ~~
(job_cost j <= service sched j (t1 + (A_sp + R)))
task_rtct tsk + IBF_P tsk (job_arrival j - t1) F <= F
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j TSK : job_task j = tsk NC : ~~
(job_cost j <= service sched j (t1 + (A_sp + R)))
task_rtct tsk + IBF_P tsk (job_arrival j - t1) F <= F
by rewrite H_equivalent //; apply relative_rtc_time_is_bounded.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j TSK : job_task j = tsk NC : ~~
(job_cost j <= service sched j (t1 + (A_sp + R)))
task_rtct tsk <= service sched j (t1 + F)
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 H_job_cost_is_big : task_rtct tsk <= job_cost j TSK : job_task j = tsk NC : ~~
(job_cost j <= service sched j (t1 + (A_sp + R)))
task_rtct tsk <= service sched j (t1 + F)
by rewrite -(leqRW job_receives_enough_service_2).
Qed .
End JobCostIsBig .
(** Either way, job [j] is completed by time [job_arrival j + R]. *)
Lemma job_is_completed_by_arrival_plus_R :
completed_by sched j (job_arrival j + R).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2
completed_by sched j (job_arrival j + R)
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2
completed_by sched j (job_arrival j + R)
edestruct (leqP (job_cost j) (task_rtct tsk)) as [LE|LE].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 LE : job_cost j <= task_rtct tsk
completed_by sched j (job_arrival j + R)
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 LE : job_cost j <= task_rtct tsk
completed_by sched j (job_arrival j + R)
eapply completion_monotonic; [ | eapply job_receives_enough_service_1; auto ].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 LE : job_cost j <= task_rtct tsk
t1 + F <= job_arrival j + R
apply leq_trans with (t1 + (A_sp + R));
[ rewrite leq_add2l; eapply leq_trans; [ | apply H_Asp_R_fixpoint]; eauto
| by rewrite job_arrival_eq_t1_plus_A -addnA leq_add2l leq_add2r].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 LE : task_rtct tsk < job_cost j
completed_by sched j (job_arrival j + R)
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 LE : task_rtct tsk < job_cost j
completed_by sched j (job_arrival j + R)
eapply completion_monotonic; [ | eapply job_receives_enough_service_3; auto ].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat A_sp : duration H_Asp_le_A : A_sp <= A H_equivalent : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A_sp) L H_Asp_is_in_search_space : is_in_search_space A_sp F : duration H_F_fixpoint : task_rtct tsk + IBF_P tsk A_sp F <= F H_Asp_R_fixpoint : task_cost tsk +
IBF_NP tsk F (A_sp + R) <=
A_sp + R H_small_fixpoint_solution1 : t1 + F < t2 H_small_fixpoint_solution2 : t1 + (A_sp + R) < t2 LE : task_rtct tsk < job_cost j
t1 + (A_sp + R) <= job_arrival j + R
by rewrite addnA leq_add2r job_arrival_eq_t1_plus_A leq_add2l.
Qed .
End FixpointsInsideBusyInterval .
End ProofOfTheorem .
(** * Response-Time Bound *)
(** Using the lemmas above, we prove that [R] is a response-time bound. *)
Theorem uniprocessor_response_time_bound :
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 H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
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 H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + R
task_response_time_bound arr_seq sched tsk R
move => j ARR JOBtsk; unfold job_response_time_bound.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j
completed_by sched j (job_arrival j + R)
move : (posnP (@job_cost _ H3 j)) => [ZERO|POS].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j ZERO : job_cost j = 0
completed_by sched j (job_arrival j + R)
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j ZERO : job_cost j = 0
completed_by sched j (job_arrival j + R)
by rewrite /completed_by ZERO. } Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j POS : 0 < job_cost j
completed_by sched j (job_arrival j + R)
move : (H_bounded_busy_interval_exists _ ARR JOBtsk POS) => [t1 [t2 [NEQ [T2 BUSY]]]].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j POS : 0 < job_cost jt1, t2 : nat NEQ : t1 <= job_arrival j < t2 T2 : t2 <= t1 + L BUSY : busy_interval sched j t1 t2
completed_by sched j (job_arrival j + R)
move : (relative_arrival_is_bounded _ ARR JOBtsk POS _ _ BUSY) => AltL.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j POS : 0 < job_cost jt1, t2 : nat NEQ : t1 <= job_arrival j < t2 T2 : t2 <= t1 + L BUSY : busy_interval sched j t1 t2 AltL : job_arrival j - t1 < L
completed_by sched j (job_arrival j + R)
move : (representative_exists tsk _ IBF_P _ AltL) => [A__sp [ALEA2 [EQΦ INSP]]].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j POS : 0 < job_cost jt1, t2 : nat NEQ : t1 <= job_arrival j < t2 T2 : t2 <= t1 + L BUSY : busy_interval sched j t1 t2 AltL : job_arrival j - t1 < L A__sp : nat ALEA2 : A__sp <= job_arrival j - t1 EQΦ : are_equivalent_at_values_less_than
(IBF_P tsk (job_arrival j - t1))
(IBF_P tsk A__sp) L INSP : search_space.is_in_search_space tsk L IBF_P
A__sp
completed_by sched j (job_arrival j + R)
set (A := job_arrival j - t1) in *.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j POS : 0 < job_cost jt1, t2 : nat NEQ : t1 <= job_arrival j < t2 T2 : t2 <= t1 + L BUSY : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat AltL : A < L A__sp : nat ALEA2 : A__sp <= A EQΦ : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A__sp) L INSP : search_space.is_in_search_space tsk L IBF_P
A__sp
completed_by sched j (job_arrival j + R)
move : (H_R_is_maximum _ INSP) => [F [FIX1 FIX2]].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j POS : 0 < job_cost jt1, t2 : nat NEQ : t1 <= job_arrival j < t2 T2 : t2 <= t1 + L BUSY : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat AltL : A < L A__sp : nat ALEA2 : A__sp <= A EQΦ : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A__sp) L INSP : search_space.is_in_search_space tsk L IBF_P
A__sp F : duration FIX1 : task_rtct tsk + IBF_P tsk A__sp F <= F FIX2 : task_cost tsk + IBF_NP tsk F (A__sp + R) <=
A__sp + R
completed_by sched j (job_arrival j + R)
edestruct (leqP t2 (t1 + F)) as [LE1|LE1];
[ | edestruct (leqP t2 (t1 + (A__sp + R))) as [LE2|LE2]].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j POS : 0 < job_cost jt1, t2 : nat NEQ : t1 <= job_arrival j < t2 T2 : t2 <= t1 + L BUSY : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat AltL : A < L A__sp : nat ALEA2 : A__sp <= A EQΦ : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A__sp) L INSP : search_space.is_in_search_space tsk L IBF_P
A__sp F : duration FIX1 : task_rtct tsk + IBF_P tsk A__sp F <= F FIX2 : task_cost tsk + IBF_NP tsk F (A__sp + R) <=
A__sp + R LE1 : t2 <= t1 + F
completed_by sched j (job_arrival j + R)
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j POS : 0 < job_cost jt1, t2 : nat NEQ : t1 <= job_arrival j < t2 T2 : t2 <= t1 + L BUSY : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat AltL : A < L A__sp : nat ALEA2 : A__sp <= A EQΦ : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A__sp) L INSP : search_space.is_in_search_space tsk L IBF_P
A__sp F : duration FIX1 : task_rtct tsk + IBF_P tsk A__sp F <= F FIX2 : task_cost tsk + IBF_NP tsk F (A__sp + R) <=
A__sp + R LE1 : t2 <= t1 + F
completed_by sched j (job_arrival j + R)
by eapply job_completed_by_arrival_plus_R_1; eauto .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j POS : 0 < job_cost jt1, t2 : nat NEQ : t1 <= job_arrival j < t2 T2 : t2 <= t1 + L BUSY : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat AltL : A < L A__sp : nat ALEA2 : A__sp <= A EQΦ : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A__sp) L INSP : search_space.is_in_search_space tsk L IBF_P
A__sp F : duration FIX1 : task_rtct tsk + IBF_P tsk A__sp F <= F FIX2 : task_cost tsk + IBF_NP tsk F (A__sp + R) <=
A__sp + R LE1 : t1 + F < t2 LE2 : t2 <= t1 + (A__sp + R)
completed_by sched j (job_arrival j + R)
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j POS : 0 < job_cost jt1, t2 : nat NEQ : t1 <= job_arrival j < t2 T2 : t2 <= t1 + L BUSY : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat AltL : A < L A__sp : nat ALEA2 : A__sp <= A EQΦ : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A__sp) L INSP : search_space.is_in_search_space tsk L IBF_P
A__sp F : duration FIX1 : task_rtct tsk + IBF_P tsk A__sp F <= F FIX2 : task_cost tsk + IBF_NP tsk F (A__sp + R) <=
A__sp + R LE1 : t1 + F < t2 LE2 : t2 <= t1 + (A__sp + R)
completed_by sched j (job_arrival j + R)
by eapply job_completed_by_arrival_plus_R_2; eauto .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j POS : 0 < job_cost jt1, t2 : nat NEQ : t1 <= job_arrival j < t2 T2 : t2 <= t1 + L BUSY : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat AltL : A < L A__sp : nat ALEA2 : A__sp <= A EQΦ : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A__sp) L INSP : search_space.is_in_search_space tsk L IBF_P
A__sp F : duration FIX1 : task_rtct tsk + IBF_P tsk A__sp F <= F FIX2 : task_cost tsk + IBF_NP tsk F (A__sp + R) <=
A__sp + R LE1 : t1 + F < t2 LE2 : t1 + (A__sp + R) < t2
completed_by sched j (job_arrival j + R)
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H4 : Interference Job H5 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_bounded_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L IBF_P : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_P
relative_arrival_time_of_job_is_A IBF_NP : Task -> duration -> duration -> duration H_job_interference_is_bounded_IBFNP : job_interference_is_bounded_by
arr_seq sched
tsk IBF_NP
relative_time_to_reach_rtct H_IBF_NP_ge_param : forall (F : nat) (Δ : duration),
F <=
task_cost tsk + IBF_NP tsk F Δis_in_search_space := [eta search_space.is_in_search_space
tsk L IBF_P] : nat -> Prop R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
task_rtct tsk + IBF_P tsk A F <= F /\
task_cost tsk +
IBF_NP tsk F (A + R) <=
A + Rj : Job ARR : arrives_in arr_seq j JOBtsk : job_of_task tsk j POS : 0 < job_cost jt1, t2 : nat NEQ : t1 <= job_arrival j < t2 T2 : t2 <= t1 + L BUSY : busy_interval sched j t1 t2 A := job_arrival j - t1 : nat AltL : A < L A__sp : nat ALEA2 : A__sp <= A EQΦ : are_equivalent_at_values_less_than
(IBF_P tsk A)
(IBF_P tsk A__sp) L INSP : search_space.is_in_search_space tsk L IBF_P
A__sp F : duration FIX1 : task_rtct tsk + IBF_P tsk A__sp F <= F FIX2 : task_cost tsk + IBF_NP tsk F (A__sp + R) <=
A__sp + R LE1 : t1 + F < t2 LE2 : t1 + (A__sp + R) < t2
completed_by sched j (job_arrival j + R)
by eapply job_is_completed_by_arrival_plus_R with (A_sp := A__sp); eauto 2 .
Qed .
End Abstract_RTA .