Library prosa.analysis.abstract.restricted_supply.abstract_rta
Require Export prosa.analysis.facts.behavior.supply.
Require Export prosa.analysis.facts.SBF.
Require Export prosa.analysis.abstract.abstract_rta.
Require Export prosa.analysis.abstract.iw_auxiliary.
Require Export prosa.analysis.abstract.IBF.supply.
Require Export prosa.analysis.abstract.restricted_supply.busy_sbf.
Require Export prosa.analysis.facts.SBF.
Require Export prosa.analysis.abstract.abstract_rta.
Require Export prosa.analysis.abstract.iw_auxiliary.
Require Export prosa.analysis.abstract.IBF.supply.
Require Export prosa.analysis.abstract.restricted_supply.busy_sbf.
Abstract Response-Time Analysis for Restricted-Supply Processors (aRSA)
In this section we propose a general framework for response-time analysis (RTA) for real-time tasks with arbitrary arrival models under uni-processor scheduling subject to supply restrictions, characterized by a given SBF.
Consider any type of tasks with a run-to-completion threshold ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
Consider any kind of fully supply-consuming unit-supply
processor state model.
Context `{PState : ProcessorState Job}.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
Consider any valid arrival sequence.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Consider any restricted supply uniprocessor schedule of this
arrival sequence ...
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
... where jobs do not execute before their arrival nor after completion.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Assume we are given valid WCETs for all tasks.
Consider a task set ts...
Consider a valid preemption model ...
...and a valid task run-to-completion threshold function. That
is, task_rtc tsk is (1) no bigger than tsk's cost and (2)
for any job j of task tsk job_rtct j is bounded by
task_rtct tsk.
Hypothesis H_valid_run_to_completion_threshold :
valid_task_run_to_completion_threshold arr_seq tsk.
valid_task_run_to_completion_threshold arr_seq tsk.
Assume we are provided with abstract functions for Interference
and Interfering Workload.
We assume that the scheduler is work-conserving.
Variable L : duration.
Hypothesis H_busy_interval_exists :
busy_intervals_are_bounded_by arr_seq sched tsk L.
Hypothesis H_busy_interval_exists :
busy_intervals_are_bounded_by arr_seq sched tsk L.
Consider a unit SBF valid in busy intervals (w.r.t. task
tsk). That is, (1) SBF 0 = 0, (2) for any duration Δ, the
supply produced during a busy-interval prefix of length Δ is
at least SBF Δ, and (3) SBF makes steps of at most one.
Context {SBF : SupplyBoundFunction}.
Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
Variable intra_IBF : duration → duration → duration.
Hypothesis H_intra_supply_interference_is_bounded :
intra_interference_is_bounded_by arr_seq sched tsk intra_IBF.
Hypothesis H_intra_supply_interference_is_bounded :
intra_interference_is_bounded_by arr_seq sched tsk intra_IBF.
Given any job j of task tsk that arrives exactly A units
after the beginning of the busy interval, the bound on the
interference incurred by j within an interval of length Δ is
no greater than (Δ - SBF Δ) + intra_IBF A Δ.
Next, we instantiate function IBF_NP, which is a function that
bounds interference in a non-preemptive stage of execution. We
prove that this function can be instantiated as λ tsk F Δ ⟹ (F
- task_rtct tsk) + (Δ - SBF Δ - (F - SBF F)).
Let us reiterate on the intuitive interpretation of this
function. Since F is a solution to the first equation
task_rtct tsk + IBF_P A F ≤ F, we know that by time
instant t1 + F a job receives task_rtct tsk units of service
and, hence, it becomes non-preemptive. Knowing this information,
how can we bound the job's interference in an interval
[t1, t1
+ Δ)>>? Note that this interval starts with the beginning of
the busy interval. We know that the job receives F - task_rtct
tsk units of interference. In the non-preemptive mode, a job
under analysis can still experience some interference due to a
lack of supply. This interference is bounded by (Δ - SBF Δ) -
(F - SBF F) since part of this interference has already been
accounted for in the preemptive part of the execution (F - SBF
F).
In the next section, we prove a few helper lemmas.
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Consider the busy interval
[t1, t2)
of job j.
Consider an arbitrary time Δ ...
First, we show that blackout is counted as interference.
Lemma blackout_impl_interference :
∀ t,
t1 ≤ t < t2 →
is_blackout sched t →
interference j t.
Proof.
move⇒ t /andP [LE1 LE2].
apply contraLR ⇒ /negP INT.
eapply H_work_conserving in INT =>//; last by lia.
by apply/negPn; eapply pos_service_impl_pos_supply.
Qed.
∀ t,
t1 ≤ t < t2 →
is_blackout sched t →
interference j t.
Proof.
move⇒ t /andP [LE1 LE2].
apply contraLR ⇒ /negP INT.
eapply H_work_conserving in INT =>//; last by lia.
by apply/negPn; eapply pos_service_impl_pos_supply.
Qed.
Next, we show that interference is equal to a sum of two
functions: is_blackout and intra_interference.
Lemma blackout_plus_local_is_interference :
∀ t,
t1 ≤ t < t2 →
is_blackout sched t + intra_interference sched j t
= interference j t.
Proof.
move⇒ t t_INT.
rewrite /intra_interference /cond_interference.
destruct (is_blackout sched t) eqn:BLACKOUT; rewrite (negbRL BLACKOUT) //.
by rewrite blackout_impl_interference.
Qed.
∀ t,
t1 ≤ t < t2 →
is_blackout sched t + intra_interference sched j t
= interference j t.
Proof.
move⇒ t t_INT.
rewrite /intra_interference /cond_interference.
destruct (is_blackout sched t) eqn:BLACKOUT; rewrite (negbRL BLACKOUT) //.
by rewrite blackout_impl_interference.
Qed.
As a corollary, cumulative interference during a time
interval
[t1, t1 + Δ)
can be split into a sum of total
blackouts in [t1, t1 + Δ)
and cumulative intra-supply
interference during [t1, t1 + Δ)
.
Corollary blackout_plus_local_is_interference_cumul :
blackout_during sched t1 (t1 + Δ) + cumul_intra_interference sched j t1 (t1 + Δ)
= cumulative_interference j t1 (t1 + Δ).
Proof.
rewrite -big_split; apply eq_big_nat ⇒ //=.
move⇒ t /andP [t_GEQ t_LTN_td].
move: (ltn_trans t_LTN_td H_inside_busy_interval) ⇒ t_LTN_t2.
by apply blackout_plus_local_is_interference; apply /andP.
Qed.
blackout_during sched t1 (t1 + Δ) + cumul_intra_interference sched j t1 (t1 + Δ)
= cumulative_interference j t1 (t1 + Δ).
Proof.
rewrite -big_split; apply eq_big_nat ⇒ //=.
move⇒ t /andP [t_GEQ t_LTN_td].
move: (ltn_trans t_LTN_td H_inside_busy_interval) ⇒ t_LTN_t2.
by apply blackout_plus_local_is_interference; apply /andP.
Qed.
Moreover, since the total blackout duration in an interval
of length Δ is bounded by Δ - SBF Δ, the cumulative
interference during the time interval
[t1, t1 + Δ)
is
bounded by the sum of Δ - SBF Δ and cumulative
intra-supply interference during [t1, t1 + Δ)
.
Corollary cumulative_job_interference_bound :
cumulative_interference j t1 (t1 + Δ)
≤ (Δ - SBF Δ) + cumul_intra_interference sched j t1 (t1 + Δ).
Proof.
rewrite -blackout_plus_local_is_interference_cumul leq_add2r.
by eapply blackout_during_bound with (t2 := t2) ⇒ //.
Qed.
cumulative_interference j t1 (t1 + Δ)
≤ (Δ - SBF Δ) + cumul_intra_interference sched j t1 (t1 + Δ).
Proof.
rewrite -blackout_plus_local_is_interference_cumul leq_add2r.
by eapply blackout_during_bound with (t2 := t2) ⇒ //.
Qed.
Next, consider a duration F such that F ≤ Δ and job j
has enough service to become non-preemptive by time instant
t1 + F.
Variable F : duration.
Hypothesis H_F_le_Δ : F ≤ Δ.
Hypothesis H_enough_service : task_rtct tsk ≤ service sched j (t1 + F).
Hypothesis H_F_le_Δ : F ≤ Δ.
Hypothesis H_enough_service : task_rtct tsk ≤ service sched j (t1 + F).
Then, we show that job j does not experience any
intra-supply interference in the time interval
[t1 + F, t1 +
Δ)>>.
Lemma no_intra_interference_after_F :
cumul_intra_interference sched j (t1 + F) (t1 + Δ) = 0.
Proof.
rewrite /cumul_intra_interference/ cumul_cond_interference big_nat.
apply big1; move ⇒ t /andP [GE__t LT__t].
apply/eqP; rewrite eqb0; apply/negP.
move ⇒ /andP [P /negPn /negP D]; apply: D; apply/negP.
eapply H_work_conserving with (t1 := t1) (t2 := t2); eauto 2.
{ by apply/andP; split; lia. }
eapply progress_inside_supplies; eauto.
eapply job_nonpreemptive_after_run_to_completion_threshold; eauto 2.
- rewrite -(leqRW H_enough_service).
by apply H_valid_run_to_completion_threshold.
- move: H_job_j_is_not_completed; apply contra.
by apply completion_monotonic; lia.
Qed.
End AuxiliaryLemmas.
cumul_intra_interference sched j (t1 + F) (t1 + Δ) = 0.
Proof.
rewrite /cumul_intra_interference/ cumul_cond_interference big_nat.
apply big1; move ⇒ t /andP [GE__t LT__t].
apply/eqP; rewrite eqb0; apply/negP.
move ⇒ /andP [P /negPn /negP D]; apply: D; apply/negP.
eapply H_work_conserving with (t1 := t1) (t2 := t2); eauto 2.
{ by apply/andP; split; lia. }
eapply progress_inside_supplies; eauto.
eapply job_nonpreemptive_after_run_to_completion_threshold; eauto 2.
- rewrite -(leqRW H_enough_service).
by apply H_valid_run_to_completion_threshold.
- move: H_job_j_is_not_completed; apply contra.
by apply completion_monotonic; lia.
Qed.
End AuxiliaryLemmas.
For clarity, let's define a local name for the search space.
We use the following equation to bound the response-time of a
job of task tsk. Consider any value R that upper-bounds the
solution of each response-time recurrence, i.e., for any
relative arrival time A in the search space, there exists a
corresponding solution F such that (1) F ≤ A + R,
(2) task_rtct tsk + intra_IBF tsk A F ≤ SBF F and SBF F +
(task_cost tsk - task_rtct tsk) ≤ SBF (A + R).
Note that, compared to "ideal RTA," there is an additional requirement
F ≤ A + R. Intuitively, it is needed to rule out a nonsensical
situation when the non-preemptive stage completes earlier than
the preemptive stage.
Variable R : duration.
Hypothesis H_R_is_maximum_rs :
∀ (A : duration),
is_in_search_space_rs A →
∃ (F : duration),
F ≤ A + R
∧ task_rtct tsk + intra_IBF A F ≤ SBF F
∧ SBF F + (task_cost tsk - task_rtct tsk) ≤ SBF (A + R).
Hypothesis H_R_is_maximum_rs :
∀ (A : duration),
is_in_search_space_rs A →
∃ (F : duration),
F ≤ A + R
∧ task_rtct tsk + intra_IBF A F ≤ SBF F
∧ SBF F + (task_cost tsk - task_rtct tsk) ≤ SBF (A + R).
In the following section we prove that all the premises of
abstract RTA are satisfied.
First, we show that IBF_P correctly upper-bounds
interference in the preemptive stage of execution.
Lemma IBF_P_bounds_interference :
job_interference_is_bounded_by
arr_seq sched tsk IBF_P (relative_arrival_time_of_job_is_A sched).
Proof.
move⇒ t1 t2 Δ j ARR TSK BUSY LT NCOM A PAR; move: (PAR _ _ BUSY) ⇒ EQ.
rewrite fold_cumul_interference.
rewrite (leqRW (cumulative_job_interference_bound _ _ _ _ _ t2 _ _ _ _)) ⇒ //.
- rewrite leq_add2l /cumul_intra_interference.
by apply: H_intra_supply_interference_is_bounded ⇒ //.
- by eapply incomplete_implies_positive_cost ⇒ //.
- by apply BUSY.
Qed.
job_interference_is_bounded_by
arr_seq sched tsk IBF_P (relative_arrival_time_of_job_is_A sched).
Proof.
move⇒ t1 t2 Δ j ARR TSK BUSY LT NCOM A PAR; move: (PAR _ _ BUSY) ⇒ EQ.
rewrite fold_cumul_interference.
rewrite (leqRW (cumulative_job_interference_bound _ _ _ _ _ t2 _ _ _ _)) ⇒ //.
- rewrite leq_add2l /cumul_intra_interference.
by apply: H_intra_supply_interference_is_bounded ⇒ //.
- by eapply incomplete_implies_positive_cost ⇒ //.
- by apply BUSY.
Qed.
Next, we prove that IBF_NP correctly bounds interference in
the non-preemptive stage given a solution to the preemptive
stage F.
Lemma IBF_NP_bounds_interference :
job_interference_is_bounded_by
arr_seq sched tsk IBF_NP (relative_time_to_reach_rtct sched tsk IBF_P).
Proof.
have USER : unit_service_proc_model PState by apply unit_supply_is_unit_service.
move⇒ t1 t2 Δ j ARR TSK BUSY LT NCOM F RT.
have POS := incomplete_implies_positive_cost _ _ _ NCOM.
move: (RT _ _ BUSY) (BUSY) ⇒ [FIX RTC] [[/andP [LE1 LE2] _] _].
have RleF : task_rtct tsk ≤ F.
{ apply cumulative_service_ge_delta with (j := j) (t := t1) (sched := sched) ⇒ //.
rewrite -[X in _ ≤ X]add0n.
by erewrite <-cumulative_service_before_job_arrival_zero;
first erewrite service_during_cat with (t1 := 0) ⇒ //; auto; lia. }
rewrite /IBF_NP addnBAC // leq_subRL_impl // addnC.
have [NEQ1|NEQ1] := leqP t2 (t1 + F); last have [NEQ2|NEQ2] := leqP F Δ.
{ rewrite -leq_subLR in NEQ1.
rewrite -{1}(leqRW NEQ1) (leqRW RTC) (leqRW (service_at_most_cost _ _ _ _ _)) ⇒ //.
rewrite (leqRW (cumulative_interference_sub _ _ _ _ t1 t2 _ _)) ⇒ //.
rewrite (leqRW (service_within_busy_interval_ge_job_cost _ _ _ _ _ _ _)) ⇒ //.
have LLL : (t1 < t2) by lia.
interval_to_duration t1 t2 k.
by rewrite addnC (leqRW (service_and_interference_bound _ _ _ _ _ _ _ _ _ _ _ _)) ⇒ //; lia. }
{ rewrite addnC -{1}(leqRW FIX) -addnA leq_add2l /IBF_P.
rewrite (@addnC (_ - _) _) -addnA subnKC; last by apply complement_SBF_monotone.
rewrite -/(cumulative_interference _ _ _).
erewrite <-blackout_plus_local_is_interference_cumul with (t2 := t2) ⇒ //; last by apply BUSY.
rewrite addnC leq_add //; last first.
{ by eapply blackout_during_bound with (t2 := t2) ⇒ //; split; [ | apply BUSY]. }
rewrite /cumul_intra_interference (cumulative_interference_cat _ j (t1 + F)) //=; last by lia.
rewrite -!/(cumul_intra_interference _ _ _ _).
rewrite (no_intra_interference_after_F _ _ _ _ _ t2) //; last by move: BUSY ⇒ [].
rewrite addn0 //; eapply H_intra_supply_interference_is_bounded ⇒ //.
- by move : NCOM; apply contra, completion_monotonic; lia.
- move ⇒ t1' t2' BUSY'.
have [EQ1 E2] := busy_interval_is_unique _ _ _ _ _ _ BUSY BUSY'.
by subst; lia. }
{ rewrite addnC (leqRW RTC); eapply leq_trans.
- by erewrite leq_add2l; apply cumulative_interference_sub with (bl := t1) (br := t1 + F); lia.
- erewrite no_service_before_busy_interval ⇒ //.
by rewrite (leqRW (service_and_interference_bound _ _ _ _ _ _ _ _ _ _ _ _)) ⇒ //; lia. }
Qed.
job_interference_is_bounded_by
arr_seq sched tsk IBF_NP (relative_time_to_reach_rtct sched tsk IBF_P).
Proof.
have USER : unit_service_proc_model PState by apply unit_supply_is_unit_service.
move⇒ t1 t2 Δ j ARR TSK BUSY LT NCOM F RT.
have POS := incomplete_implies_positive_cost _ _ _ NCOM.
move: (RT _ _ BUSY) (BUSY) ⇒ [FIX RTC] [[/andP [LE1 LE2] _] _].
have RleF : task_rtct tsk ≤ F.
{ apply cumulative_service_ge_delta with (j := j) (t := t1) (sched := sched) ⇒ //.
rewrite -[X in _ ≤ X]add0n.
by erewrite <-cumulative_service_before_job_arrival_zero;
first erewrite service_during_cat with (t1 := 0) ⇒ //; auto; lia. }
rewrite /IBF_NP addnBAC // leq_subRL_impl // addnC.
have [NEQ1|NEQ1] := leqP t2 (t1 + F); last have [NEQ2|NEQ2] := leqP F Δ.
{ rewrite -leq_subLR in NEQ1.
rewrite -{1}(leqRW NEQ1) (leqRW RTC) (leqRW (service_at_most_cost _ _ _ _ _)) ⇒ //.
rewrite (leqRW (cumulative_interference_sub _ _ _ _ t1 t2 _ _)) ⇒ //.
rewrite (leqRW (service_within_busy_interval_ge_job_cost _ _ _ _ _ _ _)) ⇒ //.
have LLL : (t1 < t2) by lia.
interval_to_duration t1 t2 k.
by rewrite addnC (leqRW (service_and_interference_bound _ _ _ _ _ _ _ _ _ _ _ _)) ⇒ //; lia. }
{ rewrite addnC -{1}(leqRW FIX) -addnA leq_add2l /IBF_P.
rewrite (@addnC (_ - _) _) -addnA subnKC; last by apply complement_SBF_monotone.
rewrite -/(cumulative_interference _ _ _).
erewrite <-blackout_plus_local_is_interference_cumul with (t2 := t2) ⇒ //; last by apply BUSY.
rewrite addnC leq_add //; last first.
{ by eapply blackout_during_bound with (t2 := t2) ⇒ //; split; [ | apply BUSY]. }
rewrite /cumul_intra_interference (cumulative_interference_cat _ j (t1 + F)) //=; last by lia.
rewrite -!/(cumul_intra_interference _ _ _ _).
rewrite (no_intra_interference_after_F _ _ _ _ _ t2) //; last by move: BUSY ⇒ [].
rewrite addn0 //; eapply H_intra_supply_interference_is_bounded ⇒ //.
- by move : NCOM; apply contra, completion_monotonic; lia.
- move ⇒ t1' t2' BUSY'.
have [EQ1 E2] := busy_interval_is_unique _ _ _ _ _ _ BUSY BUSY'.
by subst; lia. }
{ rewrite addnC (leqRW RTC); eapply leq_trans.
- by erewrite leq_add2l; apply cumulative_interference_sub with (bl := t1) (br := t1 + F); lia.
- erewrite no_service_before_busy_interval ⇒ //.
by rewrite (leqRW (service_and_interference_bound _ _ _ _ _ _ _ _ _ _ _ _)) ⇒ //; lia. }
Qed.
Next, we prove that F is bounded by task_cost tsk + IBF_NP
F Δ for any F and Δ. As explained in file
analysis/abstract/abstract_rta, this shows that the second
stage indeed takes into account service received in the first
stage.
Lemma IBF_P_sol_le_IBF_NP :
∀ (F Δ : duration),
F ≤ task_cost tsk + IBF_NP F Δ.
Proof.
move⇒ F Δ.
have [NEQ|NEQ] := leqP F (task_rtct tsk).
- apply: leq_trans; [apply NEQ | ].
by apply: leq_trans; [apply H_valid_run_to_completion_threshold | lia].
- rewrite addnA (@addnBCA _ F _); try lia.
by apply H_valid_run_to_completion_threshold; lia.
Qed.
∀ (F Δ : duration),
F ≤ task_cost tsk + IBF_NP F Δ.
Proof.
move⇒ F Δ.
have [NEQ|NEQ] := leqP F (task_rtct tsk).
- apply: leq_trans; [apply NEQ | ].
by apply: leq_trans; [apply H_valid_run_to_completion_threshold | lia].
- rewrite addnA (@addnBCA _ F _); try lia.
by apply H_valid_run_to_completion_threshold; lia.
Qed.
Next we prove that H_R_is_maximum_rs implies H_R_is_maximum.
Lemma max_in_rs_hypothesis_impl_max_in_arta_hypothesis :
∀ (A : duration),
is_in_search_space L IBF_P A →
∃ (F : duration),
task_rtct tsk + (F - SBF F + intra_IBF A F) ≤ F
∧ task_cost tsk + (F - task_rtct tsk + (A + R - SBF (A + R) - (F - SBF F))) ≤ A + R.
Proof.
move⇒ A SP.
case: (H_R_is_maximum_rs A SP) ⇒ [F [EQ0 [EQ1 EQ2]]].
∃ F; split.
{ have → : ∀ a b c, a + (b + c) = (a + c) + b by lia.
have -T : ∀ a b c, c ≥ b → (a ≤ c - b) → (a + b ≤ c); [by lia | apply: T; first by lia].
have LE : SBF F ≤ F by eapply sbf_bounded_by_duration; eauto.
by rewrite (leqRW EQ1); lia.
}
{ have JJ := IBF_P_sol_le_IBF_NP F (A + R); rewrite /IBF_NP in JJ.
rewrite addnA; rewrite addnA in JJ.
have T: ∀ a b c, c ≥ b → (a ≤ c - b) → (a + b ≤ c); [by lia | apply: T; first by lia].
rewrite subnA; [ | by apply complement_SBF_monotone | by lia].
have LE : ∀ Δ, SBF Δ ≤ Δ by move ⇒ ?; eapply sbf_bounded_by_duration; eauto.
rewrite subKn; last by eauto.
have T: ∀ a b c d e, b ≥ e → b ≥ c → e + (a - c) ≤ d → a + (b - c) ≤ d + (b - e) by lia.
apply : T ⇒ //.
eapply leq_trans; last by apply LE.
by rewrite -(leqRW EQ1); lia.
}
Qed.
End RSaRTAPremises.
∀ (A : duration),
is_in_search_space L IBF_P A →
∃ (F : duration),
task_rtct tsk + (F - SBF F + intra_IBF A F) ≤ F
∧ task_cost tsk + (F - task_rtct tsk + (A + R - SBF (A + R) - (F - SBF F))) ≤ A + R.
Proof.
move⇒ A SP.
case: (H_R_is_maximum_rs A SP) ⇒ [F [EQ0 [EQ1 EQ2]]].
∃ F; split.
{ have → : ∀ a b c, a + (b + c) = (a + c) + b by lia.
have -T : ∀ a b c, c ≥ b → (a ≤ c - b) → (a + b ≤ c); [by lia | apply: T; first by lia].
have LE : SBF F ≤ F by eapply sbf_bounded_by_duration; eauto.
by rewrite (leqRW EQ1); lia.
}
{ have JJ := IBF_P_sol_le_IBF_NP F (A + R); rewrite /IBF_NP in JJ.
rewrite addnA; rewrite addnA in JJ.
have T: ∀ a b c, c ≥ b → (a ≤ c - b) → (a + b ≤ c); [by lia | apply: T; first by lia].
rewrite subnA; [ | by apply complement_SBF_monotone | by lia].
have LE : ∀ Δ, SBF Δ ≤ Δ by move ⇒ ?; eapply sbf_bounded_by_duration; eauto.
rewrite subKn; last by eauto.
have T: ∀ a b c d e, b ≥ e → b ≥ c → e + (a - c) ≤ d → a + (b - c) ≤ d + (b - e) by lia.
apply : T ⇒ //.
eapply leq_trans; last by apply LE.
by rewrite -(leqRW EQ1); lia.
}
Qed.
End RSaRTAPremises.
Finally, we apply the uniprocessor_response_time_bound
theorem, and using the lemmas above, we prove that all the
requirements are satisfied. So, R is a response time bound.
Theorem uniprocessor_response_time_bound_restricted_supply :
task_response_time_bound arr_seq sched tsk R.
Proof.
eapply uniprocessor_response_time_bound ⇒ //.
{ by apply IBF_P_bounds_interference. }
{ by apply IBF_NP_bounds_interference. }
{ by apply IBF_P_sol_le_IBF_NP. }
{ by apply max_in_rs_hypothesis_impl_max_in_arta_hypothesis. }
Qed.
End AbstractRTARestrictedSupply.
task_response_time_bound arr_seq sched tsk R.
Proof.
eapply uniprocessor_response_time_bound ⇒ //.
{ by apply IBF_P_bounds_interference. }
{ by apply IBF_NP_bounds_interference. }
{ by apply IBF_P_sol_le_IBF_NP. }
{ by apply max_in_rs_hypothesis_impl_max_in_arta_hypothesis. }
Qed.
End AbstractRTARestrictedSupply.