Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.facts.model.ideal.schedule.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.analysis.abstract .search_space.
Require Export prosa.analysis.abstract .abstract_rta.
Require Export prosa.analysis.abstract .iw_auxiliary.
(** * Abstract Response-Time Analysis For Processor State with Ideal Uni-Service Progress Model *)
(** In this module, we present an instantiation of the general
response-time analysis framework for models that satisfy the ideal
uni-service progress assumptions. *)
(** 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 [tsk]. Note that in this section we add
additional restrictions on the processor state. These assumptions
allow us to eliminate the second equation from [aRTA+]'s
recurrence since jobs experience no delays while executing
non-preemptively. *)
Section AbstractRTAIdeal .
(** 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}.
Context `{JobPreemptable Job}.
(** Consider any kind of uni-service ideal processor state model. *)
Context `{PState : ProcessorState Job}.
Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** Next, consider any schedule of this arrival sequence... *)
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival nor after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** Consider a task set [ts]... *)
Variable ts : list Task.
(** ... and a task [tsk] of [ts] that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Consider a valid preemption model... *)
Hypothesis H_valid_preemption_model :
valid_preemption_model arr_seq sched.
(** ...and a valid task run-to-completion threshold function. That
is, [task_rtc tsk] is (1) no bigger than [tsk]'s cost and (2)
for any job [j] of task [tsk] [job_rtct j] is bounded by
[task_rtct tsk]. *)
Hypothesis H_valid_run_to_completion_threshold :
valid_task_run_to_completion_threshold arr_seq tsk.
(** 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 any busy interval of task [tsk]. *)
Variable L : duration.
Hypothesis H_busy_interval_exists :
busy_intervals_are_bounded_by arr_seq sched tsk L.
(** Next, assume that [interference_bound_function] is a bound on
the interference incurred by jobs of task [tsk] parametrized by
the relative arrival time [A]. *)
Variable interference_bound_function : (* A *) duration -> (* Δ *) duration -> duration.
Hypothesis H_job_interference_is_bounded :
job_interference_is_bounded_by
arr_seq sched tsk interference_bound_function (relative_arrival_time_of_job_is_A sched).
(** To apply the generalized aRTA, we have to instantiate [IBF_P]
and [IBF_NP]. In this file, we assume we are given a generic function
[interference_bound_function] that bounds interference of jobs
of tasks in [ts] and which have to be instantiated in subsequent
files. We use this function to instantiate [IBF_P]. *)
(** However, we still have to instantiate function [IBF_NP], which
is a function that bounds interference in a non-preemptive stage
of execution. We prove that this function can be instantiated
with a constant function [λ F Δ ⟹ F - task_rtct tsk]. *)
Let IBF_NP (F : duration) (Δ : duration) := F - task_rtct tsk.
(** Let us re-iterate on the intuitive interpretation of this
function. Since [F] is a solution to the first equation
[task_rtct tsk + IBF_P tsk A F <= F], we know that by time
instant [t1 + F] a job receives [task_rtct tsk] units of service
and, hence, it becomes non-preemptive. Given this information,
how can we bound the job's interference in an interval <<[t1, t1
+ R)>>? Note that this interval starts with the beginning of the
busy interval. We know that the job receives [F - task_rtct tsk]
units of interference, and there will no more
interference. Hence, [IBF_NP tsk F Δ := F - task_rtct tsk]. *)
Lemma nonpreemptive_interference_is_bounded :
job_interference_is_bounded_by
arr_seq sched tsk IBF_NP (relative_time_to_reach_rtct sched tsk interference_bound_function).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat
job_interference_is_bounded_by arr_seq sched tsk
IBF_NP
(relative_time_to_reach_rtct sched tsk
interference_bound_function)
Proof .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat
job_interference_is_bounded_by arr_seq sched tsk
IBF_NP
(relative_time_to_reach_rtct sched tsk
interference_bound_function)
move => t1 t2 Δ j ARR TSK BUSY LT NCOM F RTC; specialize (RTC _ _ BUSY).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat RTC : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F)
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) <=
IBF_NP F Δ
have POS : 0 < job_cost j.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat RTC : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F)
0 < job_cost j
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat RTC : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F)
0 < job_cost j
move_neq_up ZE; move : ZE; rewrite leqn0; move => /eqP ZE. Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat RTC : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F) ZE : job_cost j = 0
False
move : NCOM => /negP NCOM; apply : NCOM.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 F : nat RTC : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F) ZE : job_cost j = 0
completed_by sched j (t1 + Δ)
by rewrite /completed_by ZE.
} Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat RTC : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F) POS : 0 < job_cost j
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) <=
IBF_NP F Δ
move : (BUSY) => [PREF _].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat RTC : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F /\
task_rtct tsk <= service sched j (t1 + F) POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) <=
IBF_NP F Δ
move : (TSK) (BUSY) RTC => /eqP TSKeq [[/andP [LE1 LE2] [QT1 AQT]] QT2] [LEQ RTC].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F)
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) <=
IBF_NP F Δ
rewrite leq_subRL_impl // addnC -/cumulative_interference.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F)
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
destruct (leqP t2 (t1 + F)) as [NEQ1|NEQ1]; last destruct (leqP F Δ) as [NEQ2|NEQ2].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t2 <= t1 + F
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t2 <= t1 + F
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
rewrite -leq_subLR in NEQ1.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t2 - t1 <= F
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
rewrite -(leqRW NEQ1) (leqRW RTC) (leqRW (service_at_most_cost _ _ _ _ _)) //
(leqRW (service_within_busy_interval_ge_job_cost _ _ _ _ _ _ _)) //.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t2 - t1 <= F
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) +
service_during sched j t1 t2 <= t2 - t1
rewrite (leqRW (cumulative_interference_sub _ _ t1 _ t1 t2 _ _)) //.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t2 - t1 <= F
cumul_cond_interference (fun => xpredT) j t1 t2 +
service_during sched j t1 t2 <= t2 - t1
have LLL : (t1 < t2) = true by apply leq_ltn_trans with (t1 + Δ); lia .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t2 - t1 <= F LLL : (t1 < t2) = true
cumul_cond_interference (fun => xpredT) j t1 t2 +
service_during sched j t1 t2 <= t2 - t1
interval_to_duration t1 t2 k. Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j k : nat LT : t1 + Δ < t1 + k BUSY : definitions.busy_interval sched j t1 (t1 + k) NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1
(t1 + k) TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t1 + k QT1 : definitions.quiet_time sched j t1 QT2 : definitions.quiet_time sched j (t1 + k) AQT : forall t : nat,
t1 < t < t1 + k ->
~ definitions.quiet_time sched j tLEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + k - t1 <= F
cumul_cond_interference (fun => xpredT) j t1 (t1 + k) +
service_during sched j t1 (t1 + k) <= t1 + k - t1
eapply leq_trans.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j k : nat LT : t1 + Δ < t1 + k BUSY : definitions.busy_interval sched j t1 (t1 + k) NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1
(t1 + k) TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t1 + k QT1 : definitions.quiet_time sched j t1 QT2 : definitions.quiet_time sched j (t1 + k) AQT : forall t : nat,
t1 < t < t1 + k ->
~ definitions.quiet_time sched j tLEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + k - t1 <= F
cumul_cond_interference (fun => xpredT) j t1 (t1 + k) +
service_during sched j t1 (t1 + k) <= ?n
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j k : nat LT : t1 + Δ < t1 + k BUSY : definitions.busy_interval sched j t1 (t1 + k) NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1
(t1 + k) TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t1 + k QT1 : definitions.quiet_time sched j t1 QT2 : definitions.quiet_time sched j (t1 + k) AQT : forall t : nat,
t1 < t < t1 + k ->
~ definitions.quiet_time sched j tLEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + k - t1 <= F
cumul_cond_interference (fun => xpredT) j t1 (t1 + k) +
service_during sched j t1 (t1 + k) <= ?n
by rewrite addnC; (eapply service_and_interference_bounded with (t := t1) (t3 := t1+k)
|| eapply service_and_interference_bounded with (t := t1) (t2 := t1+k)).
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j k : nat LT : t1 + Δ < t1 + k BUSY : definitions.busy_interval sched j t1 (t1 + k) NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1
(t1 + k) TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t1 + k QT1 : definitions.quiet_time sched j t1 QT2 : definitions.quiet_time sched j (t1 + k) AQT : forall t : nat,
t1 < t < t1 + k ->
~ definitions.quiet_time sched j tLEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + k - t1 <= F
k <= t1 + k - t1
lia .
} Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
have NoInterference: cumulative_interference j (t1 + F) (t1 + Δ) = 0 .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ
cumulative_interference j (t1 + F) (t1 + Δ) = 0
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ
cumulative_interference j (t1 + F) (t1 + Δ) = 0
rewrite /cumulative_interference /cumul_cond_interference big_nat.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ
\sum_(t1 + F <= i < t1 + Δ | t1 + F <= i < t1 + Δ)
cond_interference (fun => xpredT) j i = 0
apply big1; move => t /andP [GE__t LT__t].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ t : nat GE__t : t1 + F <= t LT__t : t < t1 + Δ
cond_interference (fun => xpredT) j t = 0
apply /eqP; rewrite eqb0; apply /negP; eapply H_work_conserving => //.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ t : nat GE__t : t1 + F <= t LT__t : t < t1 + Δ
t1 <= t < t2
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ t : nat GE__t : t1 + F <= t LT__t : t < t1 + Δ
t1 <= t < t2
by apply /andP; split ; lia . } Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ t : nat GE__t : t1 + F <= t LT__t : t < t1 + Δ
receives_service_at sched j t
apply : H_ideal_progress_proc_model.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ t : nat GE__t : t1 + F <= t LT__t : t < t1 + Δ
scheduled_in j (sched t)
apply : job_nonpreemptive_after_run_to_completion_threshold GE__t _ _ => //.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ t : nat LT__t : t < t1 + Δ
job_rtct 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 H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ t : nat LT__t : t < t1 + Δ
job_rtct j <= service sched j (t1 + F)
by rewrite -(leqRW RTC); apply H_valid_run_to_completion_threshold.
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ t : nat LT__t : t < t1 + Δ
~~ completed_by sched j t
by move : NCOM; apply contra; apply completion_monotonic; lia .
} Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ NoInterference : cumulative_interference j
(t1 + F)
(t1 + Δ) = 0
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
rewrite (leqRW RTC); erewrite cumulative_interference_cat with (t := t1 + F); last by lia .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ NoInterference : cumulative_interference j
(t1 + F)
(t1 + Δ) = 0
cumul_cond_interference (fun => xpredT) j t1 (t1 + F) +
cumul_cond_interference (fun => xpredT) j (t1 + F)
(t1 + Δ) + service sched j (t1 + F) <= F
rewrite /cumulative_interference in NoInterference.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ NoInterference : cumul_cond_interference
(fun => xpredT) j
(t1 + F)
(t1 + Δ) = 0
cumul_cond_interference (fun => xpredT) j t1 (t1 + F) +
cumul_cond_interference (fun => xpredT) j (t1 + F)
(t1 + Δ) + service sched j (t1 + F) <= F
rewrite NoInterference addn0; erewrite no_service_before_busy_interval => //.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : F <= Δ NoInterference : cumul_cond_interference
(fun => xpredT) j
(t1 + F)
(t1 + Δ) = 0
cumul_cond_interference (fun => xpredT) j t1 (t1 + F) +
service_during sched j t1 (t1 + F) <= F
by rewrite addnC; apply : service_and_interference_bounded.
} Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : Δ < F
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : Δ < F
cumul_cond_interference (fun => xpredT) j t1 (t1 + Δ) +
task_rtct tsk <= F
rewrite (leqRW RTC) (leqRW (cumulative_interference_sub _ _ t1 _ t1 (t1 + F) _ _ )); try lia .Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : Δ < F
cumul_cond_interference (fun => xpredT) j t1 (t1 + F) +
service sched j (t1 + F) <= F
erewrite no_service_before_busy_interval => //.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat t1, t2 : instant Δ : nat j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j BUSY : definitions.busy_interval sched j t1 t2 LT : t1 + Δ < t2 NCOM : ~~ completed_by sched j (t1 + Δ) F : nat POS : 0 < job_cost jPREF : definitions.busy_interval_prefix sched j t1 t2 TSKeq : job_task j = tsk LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : definitions.quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 ->
~ definitions.quiet_time sched j tQT2 : definitions.quiet_time sched j t2 LEQ : task_rtct tsk +
interference_bound_function
(job_arrival j - t1) F <= F RTC : task_rtct tsk <= service sched j (t1 + F) NEQ1 : t1 + F < t2 NEQ2 : Δ < F
cumul_cond_interference (fun => xpredT) j t1 (t1 + F) +
service_during sched j t1 (t1 + F) <= F
by rewrite addnC; eapply service_and_interference_bounded. }
Qed .
(** For simplicity, let's define a local name for the search space. *)
Let is_in_search_space A := is_in_search_space L interference_bound_function A.
(** 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 [F + (task_cost tsk - task_rtc tsk) <= R]. *)
Variable R : duration.
Hypothesis H_R_is_maximum_ideal :
forall A ,
is_in_search_space A ->
exists F ,
task_rtct tsk + interference_bound_function A (A + F) <= A + F /\
F + (task_cost tsk - task_rtct tsk) <= R.
(** Using the lemma about [IBF_NP], we instantiate the general RTA
theorem's result to the ideal uniprocessor's case to prove that
[R] is a response-time bound. *)
Theorem uniprocessor_response_time_bound_ideal :
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 H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= 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 H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= R
task_response_time_bound arr_seq sched tsk R
eapply uniprocessor_response_time_bound with (IBF_NP := fun F Δ => F - task_rtct tsk) => //.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= R
job_interference_is_bounded_by arr_seq sched tsk
(fun F : nat => fun => F - task_rtct tsk)
(relative_time_to_reach_rtct sched tsk
interference_bound_function)
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= R
job_interference_is_bounded_by arr_seq sched tsk
(fun F : nat => fun => F - task_rtct tsk)
(relative_time_to_reach_rtct sched tsk
interference_bound_function)
by apply nonpreemptive_interference_is_bounded. } Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= R
forall F : nat,
duration -> F <= task_cost tsk + (F - task_rtct tsk)
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= R
forall F : nat,
duration -> F <= task_cost tsk + (F - task_rtct tsk)
move => F _.Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= RF : nat
F <= task_cost tsk + (F - task_rtct tsk)
destruct (leqP F (task_rtct tsk)) as [NEQ|NEQ].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= RF : nat NEQ : F <= task_rtct tsk
F <= task_cost tsk + (F - task_rtct tsk)
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= RF : nat NEQ : F <= task_rtct tsk
F <= task_cost tsk + (F - task_rtct tsk)
eapply leq_trans; [apply NEQ | ].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= RF : nat NEQ : F <= task_rtct tsk
task_rtct tsk <= task_cost tsk + (F - task_rtct tsk)
by eapply leq_trans; [apply H_valid_run_to_completion_threshold | lia ].
- Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= RF : nat NEQ : task_rtct tsk < F
F <= task_cost tsk + (F - task_rtct tsk)
by rewrite addnBCA; [lia | apply H_valid_run_to_completion_threshold | lia ].
} Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= R
forall A : duration,
search_space.is_in_search_space L
interference_bound_function A ->
exists F : duration,
task_rtct tsk + interference_bound_function A F <= F /\
task_cost tsk + (F - task_rtct tsk) <= A + R
{ Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R : duration H_R_is_maximum_ideal : forall A : nat,
is_in_search_space A ->
exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= R
forall A : duration,
search_space.is_in_search_space L
interference_bound_function A ->
exists F : duration,
task_rtct tsk + interference_bound_function A F <= F /\
task_cost tsk + (F - task_rtct tsk) <= A + R
move => A SP; specialize (H_R_is_maximum_ideal A SP).Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R, A : duration H_R_is_maximum_ideal : exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= RSP : search_space.is_in_search_space L
interference_bound_function A
exists F : duration,
task_rtct tsk + interference_bound_function A F <= F /\
task_cost tsk + (F - task_rtct tsk) <= A + R
destruct H_R_is_maximum_ideal as [F [EQ1 EQ2]].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R, A : duration H_R_is_maximum_ideal : exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= RSP : search_space.is_in_search_space L
interference_bound_function A F : nat EQ1 : task_rtct tsk +
interference_bound_function A (A + F) <=
A + F EQ2 : F + (task_cost tsk - task_rtct tsk) <= R
exists F : duration,
task_rtct tsk + interference_bound_function A F <= F /\
task_cost tsk + (F - task_rtct tsk) <= A + R
exists (A + F); split => [//|].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R, A : duration H_R_is_maximum_ideal : exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= RSP : search_space.is_in_search_space L
interference_bound_function A F : nat EQ1 : task_rtct tsk +
interference_bound_function A (A + F) <=
A + F EQ2 : F + (task_cost tsk - task_rtct tsk) <= R
task_cost tsk + (A + F - task_rtct tsk) <= A + R
eapply leq_trans; [ | by erewrite leq_add2l; apply EQ2].Task : TaskType H : TaskCost Task H0 : TaskRunToCompletionThreshold Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job H3 : JobCost Job H4 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task tsk : Task H_tsk_in_ts : tsk \in ts H_valid_preemption_model : valid_preemption_model
arr_seq sched H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold
arr_seq tsk H5 : Interference Job H6 : InterferingWorkload Job H_work_conserving : work_conserving arr_seq sched L : duration H_busy_interval_exists : busy_intervals_are_bounded_by
arr_seq sched tsk L interference_bound_function : duration ->
duration -> duration H_job_interference_is_bounded : job_interference_is_bounded_by
arr_seq sched tsk
interference_bound_function
(relative_arrival_time_of_job_is_A
sched) IBF_NP := fun F : duration => fun => F - task_rtct tsk: duration -> duration -> nat is_in_search_space := [eta search_space.is_in_search_space
L
interference_bound_function] : nat -> Prop R, A : duration H_R_is_maximum_ideal : exists F : nat,
task_rtct tsk +
interference_bound_function A
(A + F) <=
A + F /\
F +
(task_cost tsk -
task_rtct tsk) <= RSP : search_space.is_in_search_space L
interference_bound_function A F : nat EQ1 : task_rtct tsk +
interference_bound_function A (A + F) <=
A + F EQ2 : F + (task_cost tsk - task_rtct tsk) <= R
task_cost tsk + (A + F - task_rtct tsk) <=
A + (F + (task_cost tsk - task_rtct tsk))
by rewrite addnBCA; [lia | apply H_valid_run_to_completion_threshold | lia ].
}
Qed .
End AbstractRTAIdeal .