Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.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.task_cost.[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 ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_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 ]
Require Export prosa.analysis.facts.readiness.sequential.Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.model.restricted_supply.schedule.
Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
Require Export prosa.analysis.abstract .restricted_supply.task_intra_interference_bound.
Require Export prosa.analysis.abstract .restricted_supply.bounded_bi.fp.
Require Export prosa.analysis.abstract .restricted_supply.search_space.fp.
(** * RTA for FP Scheduling with Floating Non-Preemptive Regions on Restricted-Supply Uniprocessors *)
(** In the following, we derive a response-time analysis for FP
schedulers, assuming a workload of sporadic real-time tasks
characterized by arbitrary arrival curves executing upon a
uniprocessor with arbitrary supply restrictions. To this end, we
instantiate the sequential variant of _abstract Restricted-Supply
Response-Time Analysis_ (aRSA) as provided in the
[prosa.analysis.abstract.restricted_supply] module. *)
Section RTAforFloatingFPModelwithArrivalCurves .
(** ** Defining the System Model *)
(** Before any formal claims can be stated, an initial setup is
needed to define the system model under consideration. To this
end, we next introduce and define the following notions using
Prosa's standard definitions and behavioral semantics:
- processor model,
- tasks, jobs, and their parameters,
- the sequence of job arrivals,
- worst-case execution time (WCET) and the absence of self-suspensions,
- the task under analysis,
- an arbitrary schedule of the task set, and finally,
- a supply-bound function. *)
(** *** Processor Model *)
(** Consider a restricted-supply uniprocessor model. *)
#[local] Existing Instance rs_processor_state .
(** *** Tasks and Jobs *)
(** Consider any type of tasks, each characterized by a WCET
[task_cost], an arrival curve [max_arrivals], and a bound on the
the task's longest non-preemptive segment
[task_max_nonpreemptive_segment], ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{MaxArrivals Task}.
Context `{TaskMaxNonpreemptiveSegment Task}.
(** ... and any type of jobs associated with these tasks, where each
job has a task [job_task], a cost [job_cost], an arrival time
[job_arrival], and a predicate indicating job's preemption
points [job_preemptive_points]. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobCost Job}.
Context `{JobArrival Job}.
Context `{JobPreemptionPoints Job}.
(** We assume that jobs are limited-preemptive. *)
#[local] Existing Instance limited_preemptive_job_model .
(** *** The Job Arrival Sequence *)
(** Consider any arrival sequence [arr_seq] with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** *** Absence of Self-Suspensions and WCET Compliance *)
(** We assume the sequential model of readiness without jitter or
self-suspensions, wherein a pending job [j] is ready as soon as
all prior jobs from the same task completed. *)
#[local] Instance sequential_readiness : JobReady _ _ :=
sequential_ready_instance arr_seq.
(** We further require that a job's cost cannot exceed its task's stated WCET. *)
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** *** The Task Set *)
(** We consider an arbitrary task set [ts] ... *)
Variable ts : seq Task.
(** ... and assume that all jobs stem from tasks in this task set. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** Assume a model with floating non-preemptive regions. I.e., for
each task only the length of the maximal non-preemptive segment
is known and each job level is divided into a number of
non-preemptive segments by inserting preemption points. *)
Hypothesis H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq.
(** We assume that [max_arrivals] is a family of valid arrival
curves that constrains the arrival sequence [arr_seq], i.e., for
any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
bound of [tsk], and ... *)
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
(** ... (2) a monotonic function that equals 0 for the empty interval [delta = 0]. *)
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
(** *** The Task Under Analysis *)
(** Let [tsk] be any task in [ts] that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** *** The Schedule *)
(** Consider any arbitrary, work-conserving, valid restricted-supply
uni-processor schedule with limited preemptions of the given
arrival sequence [arr_seq] (and hence the given task set [ts]). *)
Variable sched : schedule (rs_processor_state Job).
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
Hypothesis H_schedule_with_limited_preemptions :
schedule_respects_preemption_model arr_seq sched.
(** Consider an FP policy that indicates a higher-or-equal priority
relation, and assume that the relation is reflexive and
transitive. *)
Context {FP : FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
Hypothesis H_priority_is_transitive : transitive_task_priorities FP.
(** We assume that the schedule respects the [FP] scheduling policy. *)
Hypothesis H_respects_policy_at_preemption_point :
respects_FP_policy_at_preemption_point arr_seq sched FP.
(** *** Supply-Bound Function *)
(** Assume the minimum amount of supply that any job of task [tsk]
receives is defined by a monotone unit-supply-bound function [SBF]. *)
Context {SBF : SupplyBoundFunction}.
Hypothesis H_SBF_monotone : sbf_is_monotone SBF.
Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
(** We assume that [SBF] properly characterizes all busy intervals
(w.r.t. task [tsk]) in [sched]. That is, (1) [SBF 0 = 0] and (2)
for any duration [Δ], at least [SBF Δ] supply is available in
any busy-interval prefix of length [Δ]. *)
Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
(** ** Workload Abbreviation *)
(** We introduce the abbreviation [rbf] for the task request-bound
function, which is defined as [task_cost(T) × max_arrivals(T,Δ)]
for a task [T]. *)
Let rbf := task_request_bound_function.
(** Next, we introduce [total_hep_rbf] as an abbreviation for the
request-bound function of all tasks with higher-or-equal
priority ... *)
Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
(** ... and [total_ohep_rbf] as an abbreviation for the
request-bound function of all tasks with higher-or-equal
priority other than task [tsk]. *)
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
(** ** Length of Busy Interval *)
(** The next step is to establish a bound on the maximum busy-window
length, which aRSA requires to be given. *)
(** To this end, let [L] be any positive fixed point of the
busy-interval recurrence. As the lemma
[busy_intervals_are_bounded_rs_fp] shows, under [FP] scheduling,
this is sufficient to guarantee that all busy intervals are
bounded by [L]. *)
Variable L : duration.
Hypothesis H_L_positive : 0 < L.
Hypothesis H_fixed_point : blocking_bound ts tsk + total_hep_rbf L <= SBF L.
(** ** Response-Time Bound *)
(** Having established all necessary preliminaries, it is finally
time to state the claimed response-time bound [R]. *)
(** A value [R] is a response-time bound if, for any given offset
[A] in the search space, the response-time bound recurrence has
a solution [F] not exceeding [R]. *)
Definition rta_recurrence_solution R :=
forall (A : duration),
is_in_search_space tsk L A ->
exists (F : duration),
A <= F <= A + R
/\ blocking_bound ts tsk + rbf tsk (A + ε) + total_ohep_rbf F <= SBF F.
(** Finally, using the sequential variant of abstract
restricted-supply analysis, we establish that any such [R] is a
sound response-time bound for the concrete model of
fixed-priority scheduling with floating non-preemptive regions
and with arbitrary supply restrictions. *)
Theorem uniprocessor_response_time_bound_floating_fp :
forall (R : duration),
rta_recurrence_solution R ->
task_response_time_bound arr_seq sched tsk R.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L
forall R : duration,
rta_recurrence_solution R ->
task_response_time_bound arr_seq sched tsk R
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L
forall R : duration,
rta_recurrence_solution R ->
task_response_time_bound arr_seq sched tsk R
move => R SOL js ARRs TSKs.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js
job_response_time_bound sched js R
have VAL1 : valid_preemption_model arr_seq sched.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js
valid_preemption_model arr_seq sched
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js
valid_preemption_model arr_seq sched
apply valid_fixed_preemption_points_model_lemma => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js
valid_limited_preemptions_job_model arr_seq
by apply H_valid_task_model_with_floating_nonpreemptive_regions. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched
job_response_time_bound sched js R
have [ZERO|POS] := posnP (job_cost js);
first by rewrite /job_response_time_bound /completed_by ZERO.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost js
job_response_time_bound sched js R
have READ : work_bearing_readiness arr_seq sched
by exact : sequential_readiness_implies_work_bearing_readiness.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
job_response_time_bound sched js R
eapply uniprocessor_response_time_bound_restricted_supply_seq with (L := L) => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
definitions.work_conserving arr_seq sched
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
definitions.work_conserving arr_seq sched
exact : instantiated_i_and_w_are_coherent_with_schedule.
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
sequential_tasks arr_seq sched
exact : sequential_readiness_implies_sequential_tasks.
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
interference_and_workload_consistent_with_sequential_tasks
arr_seq sched tsk
exact : instantiated_interference_and_workload_consistent_with_sequential_tasks.
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
busy_intervals_are_bounded_by arr_seq sched tsk L
apply : busy_intervals_are_bounded_rs_fp => //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
definitions.work_conserving arr_seq sched
by apply : instantiated_i_and_w_are_coherent_with_schedule.
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
busy_sbf.valid_busy_sbf arr_seq sched tsk SBF
apply : valid_pred_sbf_switch_predicate; last by exact : H_valid_SBF.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
forall (j : Job) (t1 t2 : instant),
arrives_in arr_seq j ->
job_of_task tsk j /\
definitions.busy_interval_prefix sched j t1 t2 ->
(fun (j0 : Job) (t3 t4 : instant) =>
job_of_task tsk j0 /\
busy_interval_prefix arr_seq sched j0 t3 t4) j t1 t2
move => ? ? ? ? [? ?]; split => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched _j_ : Job _t1_, _t2_ : instant _Hyp_ : arrives_in arr_seq _j_ _a_ : job_of_task tsk _j_ _b_ : definitions.busy_interval_prefix sched _j_ _t1_
_t2_
busy_interval_prefix arr_seq sched _j_ _t1_ _t2_
by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
task_intra_interference_is_bounded_by arr_seq sched
tsk ?task_intra_IBF
apply : instantiated_task_intra_interference_is_bounded; eauto 1 => //; first last .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
athep_workload_is_bounded arr_seq sched tsk ?Goal2
+ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
athep_workload_is_bounded arr_seq sched tsk ?Goal2
by apply athep_workload_le_total_ohep_rbf.
+ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
service_inversion_is_bounded_by arr_seq sched tsk
?Goal0
apply : service_inversion_is_bounded => // => jo t1 t2 ARRo TSKo BUSYo.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched jo : Job t1, t2 : instant ARRo : arrives_in arr_seq jo TSKo : job_of_task tsk jo BUSYo : busy_interval_prefix arr_seq sched jo t1 t2
max_lp_nonpreemptive_segment arr_seq jo t1 <=
?Goal0 (job_arrival jo - t1)
unshelve rewrite (leqRW (nonpreemptive_segments_bounded_by_blocking _ _ _ _ _ _ _ _ _)) => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched jo : Job t1, t2 : instant ARRo : arrives_in arr_seq jo TSKo : job_of_task tsk jo BUSYo : busy_interval_prefix arr_seq sched jo t1 t2
blocking_bound ts tsk <= ?Goal0 (job_arrival jo - t1)
by instantiate (1 := fun _ => blocking_bound ts tsk).
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched
forall A : duration,
search_space.is_in_search_space L
(fun A0 Δ : duration =>
task_request_bound_function tsk (A0 + 1 ) -
task_cost tsk +
task_intra_IBF (fun => blocking_bound ts tsk)
(fun => [eta total_ohep_request_bound_function_FP
ts tsk]) A0 Δ) A ->
exists F : duration,
F <= A + R /\
task_request_bound_function tsk (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF (fun => blocking_bound ts tsk)
(fun => [eta total_ohep_request_bound_function_FP
ts tsk]) A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
move => A SP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched A : duration SP : search_space.is_in_search_space L
(fun A Δ : duration =>
task_request_bound_function tsk (A + 1 ) -
task_cost tsk +
task_intra_IBF
(fun => blocking_bound ts tsk)
(fun => [eta
total_ohep_request_bound_function_FP ts tsk])
A Δ) A
exists F : duration,
F <= A + R /\
task_request_bound_function tsk (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF (fun => blocking_bound ts tsk)
(fun => [eta total_ohep_request_bound_function_FP
ts tsk]) A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
move : (SOL A) => [].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched A : duration SP : search_space.is_in_search_space L
(fun A Δ : duration =>
task_request_bound_function tsk (A + 1 ) -
task_cost tsk +
task_intra_IBF
(fun => blocking_bound ts tsk)
(fun => [eta
total_ohep_request_bound_function_FP ts tsk])
A Δ) A
is_in_search_space tsk L A
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched A : duration SP : search_space.is_in_search_space L
(fun A Δ : duration =>
task_request_bound_function tsk (A + 1 ) -
task_cost tsk +
task_intra_IBF
(fun => blocking_bound ts tsk)
(fun => [eta
total_ohep_request_bound_function_FP ts tsk])
A Δ) A
is_in_search_space tsk L A
by apply : search_space_sub => //; apply : search_space_switch_IBF. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched A : duration SP : search_space.is_in_search_space L
(fun A Δ : duration =>
task_request_bound_function tsk (A + 1 ) -
task_cost tsk +
task_intra_IBF
(fun => blocking_bound ts tsk)
(fun => [eta
total_ohep_request_bound_function_FP ts tsk])
A Δ) A
forall x : duration,
A <= x <= A + R /\
blocking_bound ts tsk + rbf tsk (A + 1 ) +
total_ohep_rbf x <= SBF x ->
exists F : duration,
F <= A + R /\
task_request_bound_function tsk (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF (fun => blocking_bound ts tsk)
(fun => [eta total_ohep_request_bound_function_FP
ts tsk]) A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
move => FF [EQ1 EQ2].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched A : duration SP : search_space.is_in_search_space L
(fun A Δ : duration =>
task_request_bound_function tsk (A + 1 ) -
task_cost tsk +
task_intra_IBF
(fun => blocking_bound ts tsk)
(fun => [eta
total_ohep_request_bound_function_FP ts tsk])
A Δ) A FF : duration EQ1 : A <= FF <= A + R EQ2 : blocking_bound ts tsk + rbf tsk (A + 1 ) +
total_ohep_rbf FF <=
SBF FF
exists F : duration,
F <= A + R /\
task_request_bound_function tsk (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF (fun => blocking_bound ts tsk)
(fun => [eta total_ohep_request_bound_function_FP
ts tsk]) A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
exists FF ; split ; last split .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched A : duration SP : search_space.is_in_search_space L
(fun A Δ : duration =>
task_request_bound_function tsk (A + 1 ) -
task_cost tsk +
task_intra_IBF
(fun => blocking_bound ts tsk)
(fun => [eta
total_ohep_request_bound_function_FP ts tsk])
A Δ) A FF : duration EQ1 : A <= FF <= A + R EQ2 : blocking_bound ts tsk + rbf tsk (A + 1 ) +
total_ohep_rbf FF <=
SBF FF
FF <= A + R
+ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched A : duration SP : search_space.is_in_search_space L
(fun A Δ : duration =>
task_request_bound_function tsk (A + 1 ) -
task_cost tsk +
task_intra_IBF
(fun => blocking_bound ts tsk)
(fun => [eta
total_ohep_request_bound_function_FP ts tsk])
A Δ) A FF : duration EQ1 : A <= FF <= A + R EQ2 : blocking_bound ts tsk + rbf tsk (A + 1 ) +
total_ohep_rbf FF <=
SBF FF
FF <= A + R
lia .
+ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched A : duration SP : search_space.is_in_search_space L
(fun A Δ : duration =>
task_request_bound_function tsk (A + 1 ) -
task_cost tsk +
task_intra_IBF
(fun => blocking_bound ts tsk)
(fun => [eta
total_ohep_request_bound_function_FP ts tsk])
A Δ) A FF : duration EQ1 : A <= FF <= A + R EQ2 : blocking_bound ts tsk + rbf tsk (A + 1 ) +
total_ohep_rbf FF <=
SBF FF
task_request_bound_function tsk (A + 1 ) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF (fun => blocking_bound ts tsk)
(fun => [eta total_ohep_request_bound_function_FP ts
tsk]) A FF <= SBF FF
by move : EQ2; rewrite /task_intra_IBF -/rbf -/total_ohep_rbf; lia .
+ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task Job : JobType H2 : JobTask Job Task H3 : JobCost Job H4 : JobArrival Job H5 : JobPreemptionPoints Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_task_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (rs_processor_state Job) H_valid_schedule : valid_schedule sched arr_seq H_work_conserving : work_conserving arr_seq sched H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy_at_preemption_point : respects_FP_policy_at_preemption_point
arr_seq sched
FP SBF : SupplyBoundFunction H_SBF_monotone : sbf_is_monotone SBF H_unit_SBF : unit_supply_bound_function SBF H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF rbf := task_request_bound_function : Task -> duration -> nat total_hep_rbf := total_hep_request_bound_function_FP ts
tsk : duration -> nat total_ohep_rbf := total_ohep_request_bound_function_FP
ts tsk : duration -> nat L : duration H_L_positive : 0 < LH_fixed_point : blocking_bound ts tsk +
total_hep_rbf L <=
SBF L R : duration SOL : rta_recurrence_solution R js : Job ARRs : arrives_in arr_seq js TSKs : job_of_task tsk js VAL1 : valid_preemption_model arr_seq sched POS : 0 < job_cost jsREAD : work_bearing_readiness arr_seq sched A : duration SP : search_space.is_in_search_space L
(fun A Δ : duration =>
task_request_bound_function tsk (A + 1 ) -
task_cost tsk +
task_intra_IBF
(fun => blocking_bound ts tsk)
(fun => [eta
total_ohep_request_bound_function_FP ts tsk])
A Δ) A FF : duration EQ1 : A <= FF <= A + R EQ2 : blocking_bound ts tsk + rbf tsk (A + 1 ) +
total_ohep_rbf FF <=
SBF FF
SBF FF + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
by rewrite subnn addn0; apply H_SBF_monotone; lia .
Qed .
End RTAforFloatingFPModelwithArrivalCurves .