Library prosa.results.fixed_priority.rta.bounded_pi_non_seq
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.abstract.ideal.iw_instantiation.
Require Export prosa.analysis.abstract.IBF.task.
Require Export prosa.analysis.facts.busy_interval.existence.
Require Export prosa.analysis.abstract.ideal.cumulative_bounds.
Require Export prosa.analysis.abstract.ideal.abstract_rta.
Require Export prosa.analysis.abstract.ideal.iw_instantiation.
Require Export prosa.analysis.abstract.IBF.task.
Require Export prosa.analysis.facts.busy_interval.existence.
Require Export prosa.analysis.abstract.ideal.cumulative_bounds.
Require Export prosa.analysis.abstract.ideal.abstract_rta.
Abstract RTA Instantiation for FP-Schedulers with Bounded Priority Inversion
In this module we instantiate the abstract response-time analysis (aRTA) for FP-schedulers assuming the ideal uni-processor model and real-time tasks with arbitrary arrival models.
We consider tasks and jobs with the listed parameters.
Context {Task : TaskType}
`{TaskCost Task}
`{TaskRunToCompletionThreshold Task}
`{!MaxArrivals Task}.
Context {Job : JobType}
`{JobTask Job Task}
`{Arrival : !JobArrival Job}
`{Cost : !JobCost Job}
`{!JobPreemptable Job}.
`{TaskCost Task}
`{TaskRunToCompletionThreshold Task}
`{!MaxArrivals Task}.
Context {Job : JobType}
`{JobTask Job Task}
`{Arrival : !JobArrival Job}
`{Cost : !JobCost Job}
`{!JobPreemptable Job}.
We allow for any work-bearing readiness model.
(The work_bearing_readiness restriction is introduced further down
because it requires a schedule to be introduced first; see H_job_ready below.)
A. Defining the System Model
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
Next, we consider any fixed-priority policy that is reflexive.
We consider a valid, ideal uniprocessor schedule that follows a
work-bearing readiness model.
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
We model the tasks in the system using a task set ts.
We assume that all jobs in the system come from this task set.
We assume that the task set respects the arrival curve
defined by max_arrivals.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
While we do not assume an explicit preemption model,
we require that any preemption model under consideration
is valid. We also assume that the run-to-completion-threshold
of the task tsk is valid.
Hypothesis H_valid_preemption_model:
valid_preemption_model arr_seq sched.
Hypothesis H_valid_run_to_completion_threshold:
valid_task_run_to_completion_threshold arr_seq tsk.
valid_preemption_model arr_seq sched.
Hypothesis H_valid_run_to_completion_threshold:
valid_task_run_to_completion_threshold arr_seq tsk.
As mentioned, we assume that the duration of priority inversion
incurred by the task tsk is bounded by priority_inversion_bound.
Variable priority_inversion_bound : duration.
Hypothesis H_priority_inversion_is_bounded:
priority_inversion_is_bounded_by arr_seq sched tsk (constant priority_inversion_bound).
Hypothesis H_priority_inversion_is_bounded:
priority_inversion_is_bounded_by arr_seq sched tsk (constant priority_inversion_bound).
B. Encoding the Scheduling Policy and Preemption Model
Next, we encode the scheduling policy and preemption model using the functions interference and interfering_workload. To this end, we simply reuse the general definitions of interference and interfering workload that apply to any JLFP policy, as defined in the module analysis.abstract.ideal.iw_instantiation.
#[local] Instance ideal_jlfp_interference : Interference Job :=
ideal_jlfp_interference arr_seq sched.
#[local] Instance ideal_jlfp_interfering_workload : InterferingWorkload Job :=
ideal_jlfp_interfering_workload arr_seq sched.
ideal_jlfp_interference arr_seq sched.
#[local] Instance ideal_jlfp_interfering_workload : InterferingWorkload Job :=
ideal_jlfp_interfering_workload arr_seq sched.
C. Abstract Work Conservation
Let us recall the abstract and classic notations of work conservation.
Let work_conserving_ab := definitions.work_conserving arr_seq sched.
Let work_conserving_cl := work_conserving.work_conserving arr_seq sched.
Let work_conserving_cl := work_conserving.work_conserving arr_seq sched.
We assume that the schedule is work-conserving in the classic sense,
which allows us to apply instantiated_i_and_w_are_coherent_with_schedule
to conclude that abstract work-conservation also holds.
Let task_rbf := task_request_bound_function tsk.
Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
Next, we define L as a positive fixed point of the given equation ...
Variable L : duration.
Hypothesis H_L_positive : L > 0.
Hypothesis H_fixed_point :
L = priority_inversion_bound + total_hep_rbf L.
Hypothesis H_L_positive : L > 0.
Hypothesis H_fixed_point :
L = priority_inversion_bound + total_hep_rbf L.
... and prove that it is a bound on the maximum length of a busy interval.
Lemma instantiated_busy_intervals_are_bounded :
busy_intervals_are_bounded_by arr_seq sched tsk L.
Proof.
move ⇒ j ARR TSK POS.
edestruct (exists_busy_interval) with
(delta := L) (priority_inversion_bound := (fun (d : duration) ⇒ priority_inversion_bound))
as [t1 [t2 [T1 [T2 BI]]]] ⇒ //; last first.
{ ∃ t1, t2; split⇒ [//|]; split⇒ [//|].
by eapply instantiated_busy_interval_equivalent_busy_interval. }
{ intros; rewrite {2}H_fixed_point leq_add //.
by apply: hep_workload_le_total_hep_rbf. }
Qed.
busy_intervals_are_bounded_by arr_seq sched tsk L.
Proof.
move ⇒ j ARR TSK POS.
edestruct (exists_busy_interval) with
(delta := L) (priority_inversion_bound := (fun (d : duration) ⇒ priority_inversion_bound))
as [t1 [t2 [T1 [T2 BI]]]] ⇒ //; last first.
{ ∃ t1, t2; split⇒ [//|]; split⇒ [//|].
by eapply instantiated_busy_interval_equivalent_busy_interval. }
{ intros; rewrite {2}H_fixed_point leq_add //.
by apply: hep_workload_le_total_hep_rbf. }
Qed.
E. Defining the Interference Bound Function (IBF)
Next, we define task_IBF and prove that task_IBF bounds the interference incurred by any job of tsk. Note that the maxn here is required to avoid the case in which the interval under consideration is shorter than A. While intuitively it might seem that this case is irrelevant, aRTA does not allow for this case to be ignored.
Definition IBF (A: instant) (Δ : duration) :=
priority_inversion_bound
+ (task_rbf (maxn (A + ε) Δ) - task_cost tsk)
+ total_ohep_rbf (Δ).
priority_inversion_bound
+ (task_rbf (maxn (A + ε) Δ) - task_cost tsk)
+ total_ohep_rbf (Δ).
First we prove bounds on self-interference, that is, interference
incurred from other jobs of the same task. Note that since we do not
require a sequential task model, we need to account for the case of later jobs
of the same task causing interference.
Consider any interval
[t1, t1 + Δ)
.
Next, consider any job j of the task tsk that has a positive cost
and arrives in the arrival sequence after the interval under
consideration has started.
Variable j : Job.
Hypothesis H_job_cost_positive : job_cost_positive j.
Hypothesis H_job_of_task : job_of_task tsk j.
Hypothesis H_j_in_arr_seq : arrives_in arr_seq j.
Hypothesis H_t1_le_job_arrival : t1 ≤ job_arrival j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Hypothesis H_job_of_task : job_of_task tsk j.
Hypothesis H_j_in_arr_seq : arrives_in arr_seq j.
Hypothesis H_t1_le_job_arrival : t1 ≤ job_arrival j.
First, we consider the case where the job arrives before the end of
the interval under consideration.
In this case, we bound the interference caused by the task under
consideration itself by the cost of the workload released by the tasks in the
interval (given by the RBF). However, we do not want to account for the job under
consideration itself as interference and hence we subtract the cost
of the task.
Lemma self_intf_bound_case1:
workload_of_jobs
(another_hep_job_of_same_task^~ j)
(arrivals_between arr_seq t1 (t1 + Δ))
≤ task_rbf Δ - task_cost (tsk).
Proof.
eapply leq_trans; last eapply leq_trans;
last eapply task_rbf_without_job_under_analysis ⇒ //=.
- rewrite (workload_of_jobs_equiv_pred _ _
(another_hep_job_of_same_task^~ j));
last by move ⇒ jo IN1; lia.
set (hep_job_of_same_task := (fun x : Job ⇒ hep_job x j && (job_task x == tsk))).
rewrite (workload_of_jobs_equiv_pred _ _ (fun x ⇒ hep_job_of_same_task x && (x != j) ));
last first.
{ move ⇒ j' _.
rewrite /another_hep_job_of_same_task /hep_job_of_same_task /another_hep_job.
move : H_job_of_task ⇒ /eqP →.
lia. }
rewrite workload_minus_job_cost'; [apply leqnn| by done|].
rewrite job_arrival_in_bounds //=.
by split; [| apply /andP; split] ⇒ //=.
- rewrite /task_workload_between /task_workload.
move : H_job_of_task ⇒ TSK.
move : TSK ⇒ /eqP TSK.
rewrite /hep_job /FP_to_JLFP H_priority_is_reflexive andTb TSK eq_refl //=.
apply leq_sub; last by done.
apply workload_of_jobs_weaken.
move ⇒ ? /andP[_ /eqP EQ].
by apply /eqP.
Qed.
End SelfInterferenceBoundCase1.
workload_of_jobs
(another_hep_job_of_same_task^~ j)
(arrivals_between arr_seq t1 (t1 + Δ))
≤ task_rbf Δ - task_cost (tsk).
Proof.
eapply leq_trans; last eapply leq_trans;
last eapply task_rbf_without_job_under_analysis ⇒ //=.
- rewrite (workload_of_jobs_equiv_pred _ _
(another_hep_job_of_same_task^~ j));
last by move ⇒ jo IN1; lia.
set (hep_job_of_same_task := (fun x : Job ⇒ hep_job x j && (job_task x == tsk))).
rewrite (workload_of_jobs_equiv_pred _ _ (fun x ⇒ hep_job_of_same_task x && (x != j) ));
last first.
{ move ⇒ j' _.
rewrite /another_hep_job_of_same_task /hep_job_of_same_task /another_hep_job.
move : H_job_of_task ⇒ /eqP →.
lia. }
rewrite workload_minus_job_cost'; [apply leqnn| by done|].
rewrite job_arrival_in_bounds //=.
by split; [| apply /andP; split] ⇒ //=.
- rewrite /task_workload_between /task_workload.
move : H_job_of_task ⇒ TSK.
move : TSK ⇒ /eqP TSK.
rewrite /hep_job /FP_to_JLFP H_priority_is_reflexive andTb TSK eq_refl //=.
apply leq_sub; last by done.
apply workload_of_jobs_weaken.
move ⇒ ? /andP[_ /eqP EQ].
by apply /eqP.
Qed.
End SelfInterferenceBoundCase1.
Next, we consider the case where the job arrives after the
interval under consideration has ended.
In this case we proceed similarly to the first case.
However in order to safely subtract the task cost from the RBF, we need
to consider the interval up to the arrival of the job under consideration.
Lemma self_intf_bound_case2 :
workload_of_jobs
(another_hep_job_of_same_task^~ j)
(arrivals_between arr_seq t1 (t1 + Δ))
≤ task_rbf ((job_arrival j - t1) + ε) - task_cost tsk.
Proof.
eapply leq_trans with
(workload_of_jobs (another_hep_job_of_same_task^~ j)
(arrivals_between arr_seq t1 ( (job_arrival j) + 1)));
first by apply workload_of_jobs_reduce_range ⇒ //=;lia.
eapply leq_trans; last first.
- eapply task_rbf_without_job_under_analysis with (t1 := t1) ⇒ //=.
lia.
-
set (hep_job_of_same_task := (fun x : Job ⇒ hep_job x j && (job_task x == tsk))).
rewrite (workload_of_jobs_equiv_pred _ _ (fun x ⇒ hep_job_of_same_task x && (x != j) ));
last first.
{ move ⇒ j' _.
rewrite /another_hep_job_of_same_task /hep_job_of_same_task /another_hep_job.
move : H_job_of_task ⇒ /eqP →.
lia. }
rewrite workload_minus_job_cost' //=.
+ apply leq_sub; last first.
× rewrite /hep_job_of_same_task.
case (hep_job j j && (job_task j == tsk)) eqn: EQ1; try done.
contradict EQ1.
move : H_job_of_task ⇒ /eqP TSK.
by rewrite /hep_job /FP_to_JLFP H_priority_is_reflexive TSK eq_refl //=.
× rewrite /task_workload_between /task_workload addnA.
have → :t1 + (job_arrival j - t1) + ε = job_arrival j + ε by lia.
apply workload_of_jobs_weaken.
move : H_job_of_task ⇒ /eqP TSK.
by move ⇒ jo /andP[_ /eqP TSK']; apply /eqP; rewrite -TSK TSK'.
+ apply arrived_between_implies_in_arrivals ⇒ //=.
apply /andP; split; [done| lia].
Qed.
End SelfInterferenceBoundCase2.
workload_of_jobs
(another_hep_job_of_same_task^~ j)
(arrivals_between arr_seq t1 (t1 + Δ))
≤ task_rbf ((job_arrival j - t1) + ε) - task_cost tsk.
Proof.
eapply leq_trans with
(workload_of_jobs (another_hep_job_of_same_task^~ j)
(arrivals_between arr_seq t1 ( (job_arrival j) + 1)));
first by apply workload_of_jobs_reduce_range ⇒ //=;lia.
eapply leq_trans; last first.
- eapply task_rbf_without_job_under_analysis with (t1 := t1) ⇒ //=.
lia.
-
set (hep_job_of_same_task := (fun x : Job ⇒ hep_job x j && (job_task x == tsk))).
rewrite (workload_of_jobs_equiv_pred _ _ (fun x ⇒ hep_job_of_same_task x && (x != j) ));
last first.
{ move ⇒ j' _.
rewrite /another_hep_job_of_same_task /hep_job_of_same_task /another_hep_job.
move : H_job_of_task ⇒ /eqP →.
lia. }
rewrite workload_minus_job_cost' //=.
+ apply leq_sub; last first.
× rewrite /hep_job_of_same_task.
case (hep_job j j && (job_task j == tsk)) eqn: EQ1; try done.
contradict EQ1.
move : H_job_of_task ⇒ /eqP TSK.
by rewrite /hep_job /FP_to_JLFP H_priority_is_reflexive TSK eq_refl //=.
× rewrite /task_workload_between /task_workload addnA.
have → :t1 + (job_arrival j - t1) + ε = job_arrival j + ε by lia.
apply workload_of_jobs_weaken.
move : H_job_of_task ⇒ /eqP TSK.
by move ⇒ jo /andP[_ /eqP TSK']; apply /eqP; rewrite -TSK TSK'.
+ apply arrived_between_implies_in_arrivals ⇒ //=.
apply /andP; split; [done| lia].
Qed.
End SelfInterferenceBoundCase2.
Combining the above two bounds, we obtain the final bound on the
self-interference incurred by any job j of task tsk.
Lemma self_intf_bound :
workload_of_jobs
(another_hep_job_of_same_task^~ j)
(arrivals_between arr_seq t1 (t1 + Δ))
≤ task_rbf (maxn ((job_arrival j - t1) + ε) Δ) - (task_cost tsk).
Proof.
case ((t1 + Δ) > (job_arrival j)) eqn: MAX.
- have ->: maxn ((job_arrival j - t1) + ε) Δ = Δ by lia.
by apply self_intf_bound_case1 ⇒ //=.
- have ->: maxn ((job_arrival j - t1) + ε) Δ = ((job_arrival j - t1) + ε) by lia.
apply self_intf_bound_case2 ⇒ //=.
by lia.
Qed.
End SelfInterferenceBound.
workload_of_jobs
(another_hep_job_of_same_task^~ j)
(arrivals_between arr_seq t1 (t1 + Δ))
≤ task_rbf (maxn ((job_arrival j - t1) + ε) Δ) - (task_cost tsk).
Proof.
case ((t1 + Δ) > (job_arrival j)) eqn: MAX.
- have ->: maxn ((job_arrival j - t1) + ε) Δ = Δ by lia.
by apply self_intf_bound_case1 ⇒ //=.
- have ->: maxn ((job_arrival j - t1) + ε) Δ = ((job_arrival j - t1) + ε) by lia.
apply self_intf_bound_case2 ⇒ //=.
by lia.
Qed.
End SelfInterferenceBound.
Next, we use the above bound on self-interference to state a bound on the
total interference incurred by any job j of task tsk.
Lemma instantiated_task_interference_is_bounded :
job_interference_is_bounded_by arr_seq sched tsk IBF
(relative_arrival_time_of_job_is_A sched).
Proof.
move ⇒ t1 t2 Δ j ARR TSK BUSY LT NCOMPL A OFF.
rewrite /IBF.
move: (posnP (@job_cost _ Cost j)) ⇒ [ZERO''|POS];
first by exfalso; rewrite /completed_by ZERO'' in NCOMPL.
have X := cumulative_interference_split.
rewrite /cumulative_interference in X.
rewrite X //=.
clear X.
rewrite /IBF -addnA leq_add //.
- pose PI_fun :duration → duration := fun⇒ priority_inversion_bound.
have: cumulative_priority_inversion arr_seq sched j t1 (t1 + Δ) ≤ PI_fun 0;
last by apply.
apply: cumulative_priority_inversion_is_bounded ⇒ //.
- erewrite cumulative_i_ohep_eq_service_of_ohep ⇒ //;
last by eauto 6 with basic_rt_facts.
apply: leq_trans; first by apply service_of_jobs_le_workload ⇒ //=.
rewrite workload_of_other_jobs_split.
rewrite -[leqLHS]addnC.
apply leq_add.
+ specialize (OFF t1 t2 BUSY).
rewrite OFF.
by eapply self_intf_bound ⇒ //=.
+ by apply ohep_workload_le_rbf ⇒ //.
Qed.
job_interference_is_bounded_by arr_seq sched tsk IBF
(relative_arrival_time_of_job_is_A sched).
Proof.
move ⇒ t1 t2 Δ j ARR TSK BUSY LT NCOMPL A OFF.
rewrite /IBF.
move: (posnP (@job_cost _ Cost j)) ⇒ [ZERO''|POS];
first by exfalso; rewrite /completed_by ZERO'' in NCOMPL.
have X := cumulative_interference_split.
rewrite /cumulative_interference in X.
rewrite X //=.
clear X.
rewrite /IBF -addnA leq_add //.
- pose PI_fun :duration → duration := fun⇒ priority_inversion_bound.
have: cumulative_priority_inversion arr_seq sched j t1 (t1 + Δ) ≤ PI_fun 0;
last by apply.
apply: cumulative_priority_inversion_is_bounded ⇒ //.
- erewrite cumulative_i_ohep_eq_service_of_ohep ⇒ //;
last by eauto 6 with basic_rt_facts.
apply: leq_trans; first by apply service_of_jobs_le_workload ⇒ //=.
rewrite workload_of_other_jobs_split.
rewrite -[leqLHS]addnC.
apply leq_add.
+ specialize (OFF t1 t2 BUSY).
rewrite OFF.
by eapply self_intf_bound ⇒ //=.
+ by apply ohep_workload_le_rbf ⇒ //.
Qed.
F. Defining the Search Space
Let is_in_abstract_search_space A := search_space.is_in_search_space L IBF A.
Section ConcreteSearchSpace.
Section ConcreteSearchSpace.
We begin by defining the concrete search space as follows.
To rule out pathological cases with the concrete search space,
we assume that the task cost is positive and the arrival curve
is non-pathological.
Hypothesis H_task_cost_pos : 0 < task_cost tsk.
Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
Then, for any relative arrival time A, we prove that, ...
... if A is in the abstract search space, ...
... then A is also in the concrete search space.
Lemma A_is_in_concrete_search_space :
is_in_concrete_search_space A.
Proof.
move: H_A_is_in_abstract_search_space ⇒ [INSP | [/andP [POSA LTL] [x [LTx INSP2]]]].
- rewrite INSP.
apply/andP; split; first by done.
rewrite neq_ltn; apply/orP; left.
rewrite {1}/task_rbf; erewrite task_rbf_0_zero; eauto 2; try done.
rewrite add0n /task_rbf; apply leq_trans with (task_cost tsk); try lia.
exact: task_rbf_1_ge_task_cost.
- apply/andP; split; first by done.
apply/negP; intros EQ; move: EQ ⇒ /eqP EQ.
rewrite /IBF subn1 addn1 prednK // in INSP2.
apply INSP2.
case (A < x) eqn: EQ1.
+ have ->: maxn A x = x by lia.
by have ->: maxn (A + ε) x = x by lia.
+ have ->: maxn A x = A by lia.
by have ->: maxn (A + ε) x = (A + ε) by lia.
Qed.
End ConcreteSearchSpace.
is_in_concrete_search_space A.
Proof.
move: H_A_is_in_abstract_search_space ⇒ [INSP | [/andP [POSA LTL] [x [LTx INSP2]]]].
- rewrite INSP.
apply/andP; split; first by done.
rewrite neq_ltn; apply/orP; left.
rewrite {1}/task_rbf; erewrite task_rbf_0_zero; eauto 2; try done.
rewrite add0n /task_rbf; apply leq_trans with (task_cost tsk); try lia.
exact: task_rbf_1_ge_task_cost.
- apply/andP; split; first by done.
apply/negP; intros EQ; move: EQ ⇒ /eqP EQ.
rewrite /IBF subn1 addn1 prednK // in INSP2.
apply INSP2.
case (A < x) eqn: EQ1.
+ have ->: maxn A x = x by lia.
by have ->: maxn (A + ε) x = x by lia.
+ have ->: maxn A x = A by lia.
by have ->: maxn (A + ε) x = (A + ε) by lia.
Qed.
End ConcreteSearchSpace.
G. Stating the Response-Time Bound R
Variable R : duration.
Hypothesis H_R_is_maximum:
∀ (A : duration),
is_in_concrete_search_space A →
∃ (F : duration),
0 < F
∧ A + F ≥ priority_inversion_bound + total_hep_rbf (A + F)
- (task_cost tsk - task_rtct tsk)
∧ R ≥ F + (task_cost tsk - task_rtct tsk).
Hypothesis H_R_is_maximum:
∀ (A : duration),
is_in_concrete_search_space A →
∃ (F : duration),
0 < F
∧ A + F ≥ priority_inversion_bound + total_hep_rbf (A + F)
- (task_cost tsk - task_rtct tsk)
∧ R ≥ F + (task_cost tsk - task_rtct tsk).
Next, in this section, we prove that, if a solution to the above equation
exists, then a solution to the response-time equation as stated in aRTA
also exists.
To rule out pathological cases with the concrete search space,
we assume that the task cost is positive and the arrival curve
is non-pathological.
Hypothesis H_task_cost_pos : 0 < task_cost tsk.
Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
We know that, if A is in the abstract search, then it is in the concrete search space, too.
We also know that, if A is in the concrete search space, then there exists an R that
satisfies H_R_is_maximum. Using these facts, here we prove that, if A
is in the abstract search space then, there exists a solution to the response-time
equation as stated in the aRTA.
Corollary correct_search_space :
∀ A,
is_in_abstract_search_space A →
∃ F : nat,
task_rtct tsk + IBF A (A + F) ≤ A + F
∧ F + (task_cost tsk - task_rtct tsk) ≤ R.
Proof.
move ⇒ A IN.
move: (H_R_is_maximum A) ⇒ FIX.
feed FIX; first by apply A_is_in_concrete_search_space.
move: FIX ⇒ [F [GE1 [FIX NEQ]]].
rewrite /IBF.
∃ F.
split; last by done.
rewrite /IBF.
eapply leq_trans; last by apply FIX.
move: H_valid_run_to_completion_threshold ⇒ [BOUND _].
rewrite /task_rtc_bounded_by_cost in BOUND.
have F2 : task_rbf (maxn (A + ε) (A + F)) ≥ task_cost tsk.
{ eapply (task_rbf_ge_task_cost _ _ _ _) ⇒ //=.
lia. }
have MAXX : maxn (A + 1) (A + F) = A + F by lia.
rewrite MAXX in F2.
rewrite MAXX.
have SPLITLE : total_hep_rbf (A + F) ≥ total_ohep_rbf (A + F) + task_rbf (A + F).
{ apply split_hep_rbf_weaken ⇒ //. }
by lia.
Unshelve.
all: by done.
Qed.
End ResponseTimeReccurence.
∀ A,
is_in_abstract_search_space A →
∃ F : nat,
task_rtct tsk + IBF A (A + F) ≤ A + F
∧ F + (task_cost tsk - task_rtct tsk) ≤ R.
Proof.
move ⇒ A IN.
move: (H_R_is_maximum A) ⇒ FIX.
feed FIX; first by apply A_is_in_concrete_search_space.
move: FIX ⇒ [F [GE1 [FIX NEQ]]].
rewrite /IBF.
∃ F.
split; last by done.
rewrite /IBF.
eapply leq_trans; last by apply FIX.
move: H_valid_run_to_completion_threshold ⇒ [BOUND _].
rewrite /task_rtc_bounded_by_cost in BOUND.
have F2 : task_rbf (maxn (A + ε) (A + F)) ≥ task_cost tsk.
{ eapply (task_rbf_ge_task_cost _ _ _ _) ⇒ //=.
lia. }
have MAXX : maxn (A + 1) (A + F) = A + F by lia.
rewrite MAXX in F2.
rewrite MAXX.
have SPLITLE : total_hep_rbf (A + F) ≥ total_ohep_rbf (A + F) + task_rbf (A + F).
{ apply split_hep_rbf_weaken ⇒ //. }
by lia.
Unshelve.
all: by done.
Qed.
End ResponseTimeReccurence.
H. Soundness of the Response-Time Bound
Theorem uniprocessor_response_time_bound_fp :
task_response_time_bound arr_seq sched tsk R.
Proof.
intros js ARRs TSKs.
move: (posnP (@job_cost _ Cost js)) ⇒ [ZERO|POS].
{ by rewrite /job_response_time_bound /completed_by ZERO. }
eapply uniprocessor_response_time_bound_ideal ⇒ //.
- exact: instantiated_i_and_w_are_coherent_with_schedule.
- exact: instantiated_busy_intervals_are_bounded.
- exact: instantiated_task_interference_is_bounded.
- by apply : correct_search_space ⇒ //.
Qed.
End AbstractRTAforFPwithArrivalCurves.
task_response_time_bound arr_seq sched tsk R.
Proof.
intros js ARRs TSKs.
move: (posnP (@job_cost _ Cost js)) ⇒ [ZERO|POS].
{ by rewrite /job_response_time_bound /completed_by ZERO. }
eapply uniprocessor_response_time_bound_ideal ⇒ //.
- exact: instantiated_i_and_w_are_coherent_with_schedule.
- exact: instantiated_busy_intervals_are_bounded.
- exact: instantiated_task_interference_is_bounded.
- by apply : correct_search_space ⇒ //.
Qed.
End AbstractRTAforFPwithArrivalCurves.