# Facts about Request Bound Functions (RBFs)

In this file, we prove some lemmas about request bound functions.

## RBF is a Bound on Workload

First, we show that a task's RBF is indeed an upper bound on its workload.
Consider any type of tasks ...

... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.

Consider any arrival sequence with consistent, non-duplicate arrivals, ...
... any schedule corresponding to this arrival sequence, ...
... and an FP policy that indicates a higher-or-equal priority relation.

Further, consider a task set ts...

... and let tsk be any task in ts.
Hypothesis H_tsk_in_ts : tsk \in ts.

Assume that the job costs are no larger than the task costs ...
... and that all jobs come from the task set.
Let max_arrivals be any arrival bound for task-set ts.
Next, recall the notions of total workload of jobs...
... and the workload of jobs of the same task as job j.
Finally, let us define some local names for clarity.
In this section, we prove that the workload of all jobs is no larger than the request bound function.

Consider any time t and any interval of length Δ.
Variable t : instant.
Variable Δ : instant.

First, we show that workload of task tsk is bounded by the number of arrivals of the task times the cost of the task.
Proof.
by rewrite -big_filter !TASK !big_nil. }
{ rewrite //= big_filter big_seq_cond [in X in _ X]big_seq_cond.
apply leq_sum.
movej' /andP [IN TSKj'].
rewrite muln1.
move: TSKj' ⇒ /eqP TSKj'; rewrite -TSKj'.
apply H_valid_job_cost.
by apply in_arrivals_implies_arrived in IN. }
Qed.

As a corollary, we prove that workload of task is no larger the than task request bound function.
Proof.
rewrite leq_mul2l; apply/orP; right.
by apply H_is_arrival_bound; last rewrite leq_addr.
Qed.

Next, we prove that total workload of tasks is no larger than the total request bound function.
total_workload t (t + Δ) total_rbf Δ.
Proof.
set l := arrivals_between arr_seq t (t + Δ).
apply (@leq_trans (\sum_(tsk' <- ts) (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0))).
have EXCHANGE := exchange_big_dep predT.
rewrite EXCHANGE /=; clear EXCHANGE; last by done.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ X]big_seq_cond.
apply leq_sum; movej0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=.
by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset. }
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply (@leq_trans (task_cost tsk0 × size (task_arrivals_between arr_seq tsk0 t (t + Δ)))).
{ rewrite -sum1_size big_distrr /= big_filter -/l /workload_of_jobs muln1.
apply leq_sum_seqj0 IN0 /eqP <-.
apply H_valid_job_cost.
by apply in_arrivals_implies_arrived in IN0. }
{ rewrite leq_mul2l; apply/orP; right.
by apply H_is_arrival_bound; last rewrite leq_addr. }
Qed.

Next, we consider any job j of tsk.
Variable j : Job.
Hypothesis H_job_of_tsk : job_of_task tsk j.

Consider any general predicate defined on tasks.

We prove that the sum of job cost of jobs whose corresponding task satisfies the predicate pred is bound by the RBF of these tasks.
Lemma sum_of_jobs_le_sum_rbf:
\sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred (job_task j'))
job_cost j'
\sum_(tsk' <- ts| pred tsk')
Proof.
apply (@leq_trans (\sum_(tsk' <- filter pred ts)
(\sum_(j' <- arrivals_between arr_seq t (t + Δ)
| job_task j' == tsk') job_cost j'))).
- move: (H_job_of_tsk) ⇒ /eqP TSK.
rewrite [X in _ X]big_filter.
set P := fun xpred (job_task x).
rewrite (exchange_big_dep P) //=; last by rewrite /P; move ⇒ ???/eqP→.
rewrite /P /workload_of_jobs big_seq_cond [X in _ X]big_seq_cond.
apply leq_sumj0 /andP [IN0 HP0].
+ by rewrite HP0 andTb eq_refl; apply leq_addr.
+ by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
- rewrite big_filter.
apply leq_sum_seqtsk0 INtsk0 HP0.
apply (@leq_trans (task_cost tsk0 × size (task_arrivals_between arr_seq tsk0 t (t + Δ)))).
+ rewrite -sum1_size big_distrr /= big_filter /workload_of_jobs.
rewrite muln1 /arrivals_between /arrival_sequence.arrivals_between.
apply leq_sum_seq; movej0 IN0 /eqP EQ.
by rewrite -EQ; apply H_valid_job_cost; apply in_arrivals_implies_arrived in IN0.
+ rewrite leq_mul2l; apply/orP; right.
by apply H_is_arrival_bound; last by rewrite leq_addr.
Qed.

## RBF Properties

In this section, we prove simple properties and identities of RBFs.
Consider any type of tasks ...

... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobArrival Job}.

Consider any arrival sequence.

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 Δ = 0.
Let's define some local names for clarity.
We prove that task_rbf 0 is equal to 0.
Proof.
apply/eqP; rewrite muln_eq0; apply/orP; right; apply/eqP.
by move: H_valid_arrival_curve ⇒ [T1 T2].
Qed.

We prove that task_rbf is monotone.
Proof.
rewrite /monotone; intros ? ? LE.
apply/orP; right.
by move: H_valid_arrival_curve ⇒ [_ T]; apply T.
Qed.

Consider any job j of tsk. This guarantees that there exists at least one job of task tsk.
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.

Then we prove that task_rbf at ε is greater than or equal to the task's WCET.
Proof.
have ALT: n, n = 0 n > 0 by clear; intros n; destruct n; [left | right].
specialize (ALT (task_cost tsk)); destruct ALT as [Z | POS]; first by rewrite Z.
rewrite leqNgt; apply/negP; intros CONTR.
move: H_is_arrival_curveARRB.
specialize (ARRB (job_arrival j) (job_arrival j + ε)).
feed ARRB; first by rewrite leq_addr.
rewrite -{2}[task_cost tsk]muln1 ltn_mul2l ⇒ /andP [_ CONTR].
move: ARRB; rewrite addKn CONTR leqn0 eqn0Ngt ⇒ /negP T; apply: T.
apply/hasP; j; last by done.
rewrite /arrivals_between addn1 big_nat_recl; last by done.
rewrite big_geq ?cats0 //= mem_filter.
apply/andP; split; first by done.
move: H_j_arrives ⇒ [t ARR]; move: (ARR) ⇒ CONS.
apply H_arrival_times_are_consistent in CONS.
by rewrite CONS.
Qed.

As a corollary, we prove that the task_rbf at any point A greater than 0 is no less than the task's WCET.
A,
A > 0
Proof.
case ⇒ // A GEQ.
Qed.

Assume that tsk has a positive cost.
Hypothesis H_positive_cost : 0 < task_cost tsk.

Then, we prove that task_rbf at ε is greater than 0.
Proof.
apply leq_trans with (task_cost tsk); first by done.
Qed.

Hypothesis H_tsk_in_ts : tsk \in ts.

Next, we prove that cost of tsk is less than or equal to the total_request_bound_function.
t,
t > 0
Proof.
movet GE.
destruct t; first by done.
rewrite /total_request_bound_function.
erewrite big_rem; last by exact H_tsk_in_ts.
Qed.

End RequestBoundFunctions.

## Monotonicity of the Total RBF

In the following section, we note some trivial facts about the monotonicity of various total RBF variants.
Consider a set of tasks characterized by WCETs and arrival curves.
We observe that the total RBF is monotonically increasing.
Lemma total_rbf_monotone :
monotone leq (total_request_bound_function ts).
Proof.
apply: sum_leq_monotsk IN.
Qed.

Furthermore, for any fixed-priority policy, ...

... the total RBF of higher- or equal-priority tasks is also monotonic, ...
Lemma total_hep_rbf_monotone :
tsk,
monotone leq (total_hep_request_bound_function_FP ts tsk).
Proof.
movetsk.
apply: sum_leq_monotsk' IN.
Qed.

... as is the variant that excludes the reference task.
Lemma total_ohep_rbf_monotone :
tsk,
monotone leq (total_ohep_request_bound_function_FP ts tsk).
Proof.
movetsk.
apply: sum_leq_monotsk' IN.
Qed.

End TotalRBFMonotonic.

## RBFs Equal to Zero for Duration ε

In the following section, we derive simple properties that follow in the pathological case of an RBF that yields zero for duration ε.
Consider a set of tasks characterized by WCETs and arrival curves ...

... and any consistent arrival sequence of valid jobs of these tasks.
Suppose the arrival curves are correct.
Consider any valid schedule corresponding to this arrival sequence.
First, we observe that, if a task's RBF is zero for a duration ε, then it trivially has a response-time bound of zero.
Lemma pathological_rbf_response_time_bound :
tsk,
tsk \in ts
Proof.
movetsk IN ZERO j ARR TASK.
rewrite /job_response_time_bound/completed_by.
move: ZERO. rewrite /task_request_bound_function ⇒ /eqP.
rewrite muln_eq0 ⇒ /orP [/eqP COST|/eqP NEVER].
{ apply: leq_trans.
- by apply: H_valid_job_cost.
by rewrite COST. }
{ exfalso.
have: 0 < max_arrivals tsk ε
by apply: (non_pathological_max_arrivals tsk arr_seq _ j); rt_auto.
by rewrite NEVER. }
Qed.

Second, given a fixed-priority policy with reflexive priorities, ...
Hypothesis H_reflexive : reflexive_priorities.

... if the total RBF of all equal- and higher-priority tasks is zero, then the reference task's response-time bound is also trivially zero.
Lemma pathological_total_hep_rbf_response_time_bound :
tsk,
tsk \in ts
total_hep_request_bound_function_FP ts tsk ε = 0
Proof.
movetsk IN ZERO j ARR TASK.
apply: pathological_rbf_response_time_bound; eauto.
apply /eqP.
move: ZERO ⇒ /eqP; rewrite sum_nat_eq0_nat ⇒ /allP; apply.
rewrite mem_filter; apply /andP; split ⇒ //.
move: (H_reflexive 0 j).
rewrite /hep_job_at/JLFP_to_JLDP/hep_job/FP_to_JLFP.
Qed.

Thus we we can prove any response-time bound from such a pathological case, which is useful to eliminate this case in higher-level analyses.
Corollary pathological_total_hep_rbf_any_bound :
tsk,
tsk \in ts
total_hep_request_bound_function_FP ts tsk ε = 0
R,