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.results.fixed_priority.rta.bounded_nps.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
Require Export prosa.analysis.facts.readiness.sequential.
Require Export prosa.model.task.preemption.fully_nonpreemptive.
(** * RTA for Fully Non-Preemptive FP Model *)
(** In this module we prove the RTA theorem for the fully non-preemptive FP model. *)
(** ** Setup and Assumptions *)
Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves .
(** We assume ideal uni-processor schedules. *)
#[local] Existing Instance ideal .processor_state.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context {tc : TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** We assume that jobs and tasks are fully nonpreemptive. *)
#[local] Existing Instance fully_nonpreemptive_job_model .
#[local] Existing Instance fully_nonpreemptive_task_model .
#[local] Existing Instance fully_nonpreemptive_rtc_threshold .
(** 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.
(** Consider an arbitrary task set ts, ... *)
Variable ts : list Task.
(** ... assume that all jobs come from the task set, ... *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and the cost of a job cannot be larger than the task cost. *)
Hypothesis H_valid_job_cost :
arrivals_have_valid_job_costs arr_seq.
(** Let max_arrivals be a family of valid arrival curves, i.e., for
any task [tsk] in ts [max_arrival tsk] is (1) an arrival bound of
[tsk], and (2) it is a monotonic function that equals [0] for the
empty interval [delta = 0]. *)
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
(** Let [tsk] be any task in ts that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Recall that we assume sequential readiness. *)
#[local] Instance sequential_readiness : JobReady _ _ :=
sequential_ready_instance arr_seq.
(** Next, consider any ideal non-preemptive uniprocessor schedule of
this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule 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.
(** Next, we assume that the schedule is a work-conserving schedule ... *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** ... and the schedule respects the scheduling policy. *)
Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.
(** ** Total Workload and Length of Busy Interval *)
(** 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 [task_rbf] as an abbreviation
for the task request bound function of task [tsk]. *)
Let task_rbf := rbf tsk.
(** Using the sum of individual request bound functions, we define
the request bound function of all tasks with higher priority
... *)
Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
(** ... and the request bound function of all tasks with higher
priority other than task [tsk]. *)
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
(** Next, we define a bound for the priority inversion caused by tasks of lower priority. *)
Let blocking_bound :=
\max_(tsk_other <- ts | ~~ hep_task tsk_other tsk) (task_cost tsk_other - ε).
(** Let L be any positive fixed point of the busy interval recurrence, determined by
the sum of blocking and higher-or-equal-priority workload. *)
Variable L : duration.
Hypothesis H_L_positive : L > 0 .
Hypothesis H_fixed_point : L = blocking_bound + total_hep_rbf L.
(** ** Response-Time Bound *)
(** To reduce the time complexity of the analysis, recall the notion of search space. *)
Let is_in_search_space := is_in_search_space tsk L.
(** Next, consider any value [R], and assume that for any given
arrival [A] from search space there is a solution of the
response-time bound recurrence which is bounded by [R]. *)
Variable R : duration.
Hypothesis H_R_is_maximum :
forall (A : duration),
is_in_search_space A ->
exists (F : duration),
A + F >= blocking_bound
+ (task_rbf (A + ε) - (task_cost tsk - ε))
+ total_ohep_rbf (A + F) /\
R >= F + (task_cost tsk - ε).
(** Now, we can leverage the results for the abstract model with
bounded nonpreemptive segments to establish a response-time
bound for the more concrete model of fully nonpreemptive
scheduling. *)
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
Theorem uniprocessor_response_time_bound_fully_nonpreemptive_fp :
response_time_bounded_by tsk R.Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop
response_time_bounded_by tsk R
Proof .Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop
response_time_bounded_by tsk R
move : (posnP (@task_cost _ tc tsk)) => [ZERO|POS].Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop ZERO : task_cost tsk = 0
response_time_bounded_by tsk R
{ Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop ZERO : task_cost tsk = 0
response_time_bounded_by tsk R
intros j ARR TSK.Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop ZERO : task_cost tsk = 0 j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j
job_response_time_bound sched j R
have ZEROj: job_cost j = 0 .Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop ZERO : task_cost tsk = 0 j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j
job_cost j = 0
{ Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop ZERO : task_cost tsk = 0 j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j
job_cost j = 0
move : (H_valid_job_cost j ARR) => NEQ.Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop ZERO : task_cost tsk = 0 j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j NEQ : valid_job_cost j
job_cost j = 0
rewrite /valid_job_cost in NEQ.Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop ZERO : task_cost tsk = 0 j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j NEQ : job_cost j <= task_cost (job_task j)
job_cost j = 0
move : TSK => /eqP -> in NEQ.Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop ZERO : task_cost tsk = 0 j : Job ARR : arrives_in arr_seq j NEQ : job_cost j <= task_cost tsk
job_cost j = 0
rewrite ZERO in NEQ.Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop ZERO : task_cost tsk = 0 j : Job ARR : arrives_in arr_seq j NEQ : job_cost j <= 0
job_cost j = 0
by apply /eqP; rewrite -leqn0.
} Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop ZERO : task_cost tsk = 0 j : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j ZEROj : job_cost j = 0
job_response_time_bound sched j R
by rewrite /job_response_time_bound /completed_by ZEROj.
} Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop POS : 0 < task_cost tsk
response_time_bounded_by tsk R
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
(L := L) => //.Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop POS : 0 < task_cost tsk
work_bearing_readiness arr_seq sched
- Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop POS : 0 < task_cost tsk
work_bearing_readiness arr_seq sched
exact : sequential_readiness_implies_work_bearing_readiness.
- Task : TaskType tc : TaskCost Task Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H2 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_nonpreemptive_sched : nonpreemptive_schedule sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_work_conserving : work_conserving arr_seq sched H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP rbf := task_request_bound_function : Task -> duration -> nat task_rbf := rbf tsk : 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 blocking_bound := \max_(tsk_other <- ts | ~~
hep_task
tsk_other tsk)
(task_cost tsk_other - 1 ) : nat L : duration H_L_positive : 0 < LH_fixed_point : L = blocking_bound + total_hep_rbf L is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
blocking_bound +
(task_rbf (A + 1 ) -
(task_cost tsk - 1 )) +
total_ohep_rbf (A + F) <=
A + F /\
F + (task_cost tsk - 1 ) <= Rresponse_time_bounded_by := task_response_time_bound
arr_seq sched : Task -> duration -> Prop POS : 0 < task_cost tsk
sequential_tasks arr_seq sched
exact : sequential_readiness_implies_sequential_tasks.
Qed .
End RTAforFullyNonPreemptiveFPModelwithArrivalCurves .