# Library prosa.analysis.facts.model.rbf

Require Export prosa.model.job.properties.
Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.facts.model.arrival_curves.
Require Export prosa.analysis.facts.model.task_cost.
Require Export prosa.analysis.definitions.request_bound_function.
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.util.tactics.
Require Export prosa.analysis.definitions.workload.bounded.

# Facts about Request-Bound Functions (RBFs)

In this file, we prove some lemmas about RBFs.

## RBF is a Bound on Workload

Section ProofRequestBoundFunction.
Consider any type of tasks characterized by WCETs and arrival curves ...
Context {Task : TaskType}.
Context `{TaskCost Task} `{MaxArrivals Task}.
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any valid arrival sequence ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
... and any schedule corresponding to this arrival sequence.
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
Assume that the job costs are no larger than the task costs.
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
In this section, we establish that a task's RBF is indeed an upper bound on the task's workload.
Section RBF.
Consider a given task tsk.
Variable tsk : Task.
First, as a stepping stone, we observe that any sequence of jobs of the task jointly satisfy the task's WCET.
Lemma task_workload_between_bounded :
∀ t1 t2,
task_workload_between arr_seq tsk t1 t2
≤ task_cost tsk × number_of_task_arrivals arr_seq tsk t1 t2.
Next, suppose that task tsk respects its arrival curve max_arrivals.
Hypothesis H_tsk_arrivals_bounded : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
From this assumption, we establish the RBF spec: In any interval of any length, the RBF upper-bounds the task's actual workload.
Lemma rbf_spec :
∀ t Δ,
task_workload_between arr_seq tsk t (t + Δ)
≤ task_request_bound_function tsk Δ.
End RBF.
In this section, we prove a trivial corollary stating that the RBF still upper-bounds the workload when considering only a subset of a task's jobs (namely those satisfying a filter predicate).
Section SubsetOfJobs.
Consider any predicate P on jobs.
Variable P : pred Job.
Consider any task tsk that respects its arrival curve max_arrivals
Variable tsk : Task.
Hypothesis H_tsk_arrivals_bounded : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
Assume that all jobs that satisfy P come from task tsk.
Hypothesis H_jobs_of_tsk : ∀ j, P j → job_of_task tsk j.
Trivially, the workload of jobs from task tsk that satisfy the predicate P is bounded by the task's RBF.
Corollary rbf_spec' :
∀ t Δ,
workload_of_jobs P
(arrivals_between arr_seq t (t + Δ))
≤ task_request_bound_function tsk Δ.
End SubsetOfJobs.
Now, consider a task set ts ...
Variable ts : seq Task.
... and assume that all jobs come from the task set.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
Assume that all tasks in the task set respect max_arrivals.
Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
Next, we prove that total workload is upper-bounded by the total RBF.
Lemma total_workload_le_total_rbf :
∀ t Δ,
total_workload_between arr_seq t (t + Δ) ≤ total_request_bound_function ts Δ.
In this section, we prove a more general result about the workload of arbitrary sets of jobs.
Section SumRBF.
Consider two predicates, one on jobs and one on tasks.
Variable pred1 : pred Job.
Variable pred2 : pred Task.
Assume that for all jobs satisfying pred1, the task it belongs to satisfies pred2.
Hypothesis H_also_satisfied : ∀ j, pred1 j → pred2 (job_task j).
We prove that the workload of all jobs satisfying predicate pred1 is bounded by the sum of task RBFs over tasks that satisfy the predicate pred2.
Lemma workload_of_jobs_bounded :
∀ t Δ,
workload_of_jobs (pred1) (arrivals_between arr_seq t (t + Δ))
≤ \sum_(tsk' <- ts | pred2 tsk') task_request_bound_function tsk' Δ.
End SumRBF.
Next, we establish bounds specific to fixed-priority scheduling.
Section FP.
Consider an arbitrary fixed-priority policy ...
Context {FP : FP_policy Task}.
... and any given task.
Variable tsk : Task.
The athep_workload_is_bounded predicate used below allows the workload bound to depend on two arguments: the relative offset A (w.r.t. the beginning of the corresponding busy interval) of a job to be analyzed and the length of an interval Δ. In the case of FP scheduling, the relative offset (A) does not play a role and is therefore ignored.
Let's abbreviate total_ohep_request_bound_function_FP such that the A argument is ignored.
Let total_ohep_rbf (_A Δ : duration) :=
total_ohep_request_bound_function_FP ts tsk Δ.
We next prove that the higher-or-equal-priority workload of tasks different from tsk is bounded by total_ohep_rbf.
Lemma athep_workload_le_total_ohep_rbf :
athep_workload_is_bounded arr_seq sched tsk total_ohep_rbf.
Consider any job j of tsk.
Variable j : Job.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Using lemma workload_of_jobs_bounded, we prove that the workload of higher-or-equal priority jobs (w.r.t. task tsk) is no larger than the total request-bound function of higher-or-equal priority tasks.
Lemma hep_workload_le_total_hep_rbf :
∀ t Δ,
workload_of_hep_jobs arr_seq j t (t + Δ)
≤ total_hep_request_bound_function_FP ts tsk Δ.
End FP.
In this section, we show that the total RBF is a bound on higher-or-equal priority workload under any JLFP policy.
Section JLFP.
Consider a JLFP policy that indicates a higher-or-equal priority relation ...
Context `{JLFP_policy Job}.
... and any job j.
Variable j : Job.
A simple consequence of lemma hep_workload_le_total_hep_rbf is that the workload of higher-or-equal priority jobs is bounded by the total request-bound function.
Corollary hep_workload_le_total_rbf :
∀ t Δ,
workload_of_hep_jobs arr_seq j t (t + Δ)
≤ total_request_bound_function ts Δ.
End JLFP.
End ProofRequestBoundFunction.

## RBF Properties

In this section, we prove simple properties and identities of RBFs.
Section RequestBoundFunctions.
Consider any type of tasks ...
Context {Task : TaskType}.
Context `{TaskCost Task}.
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Consider any arrival sequence.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent :
consistent_arrival_times arr_seq.
Let tsk be any task.
Variable tsk : Task.
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.
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
We prove that task_request_bound_function 0 is equal to 0.
Lemma task_rbf_0_zero :
task_request_bound_function tsk 0 = 0.
We prove that task_request_bound_function is monotone.
Lemma task_rbf_monotone :
monotone leq (task_request_bound_function tsk).
In the following, we assume that tsk has a positive cost ...
Hypothesis H_positive_cost : 0 < task_cost tsk.
... and max_arrivals tsk ε is positive.
Hypothesis H_arrival_curve_positive : max_arrivals tsk ε > 0.
Then we prove that task_request_bound_function at ε is greater than or equal to the task's WCET.
Lemma task_rbf_1_ge_task_cost :
task_request_bound_function tsk ε ≥ task_cost tsk.
As a corollary, we prove that the task_request_bound_function at any point A greater than 0 is no less than the task's WCET.
Lemma task_rbf_ge_task_cost :
∀ A,
A > 0 →
task_request_bound_function tsk A ≥ task_cost tsk.
Then, we prove that task_request_bound_function at ε is greater than 0.
Lemma task_rbf_epsilon_gt_0 : 0 < task_request_bound_function tsk ε.
Consider a set of tasks ts containing the task tsk.
Variable ts : seq Task.
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.
Lemma task_cost_le_sum_rbf :
∀ t,
t > 0 →
task_cost tsk ≤ total_request_bound_function ts t.
End RequestBoundFunctions.

## Monotonicity of the Total RBF

In the following section, we note some trivial facts about the monotonicity of various total RBF variants.
Section TotalRBFMonotonic.
Consider a set of tasks characterized by WCETs and arrival curves.
Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.
Variable ts : seq Task.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
We observe that the total RBF is monotonically increasing.
Lemma total_rbf_monotone :
monotone leq (total_request_bound_function ts).
Furthermore, for any fixed-priority policy, ...
Context `{FP_policy Task}.
... 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).
... 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).
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 ε.
Section DegenerateTotalRBFs.
Consider a set of tasks characterized by WCETs and arrival curves ...
Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.
Variable ts : seq Task.
... and any consistent arrival sequence of valid jobs of these tasks.
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job} `{JobCost Job}.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
Suppose the arrival curves are correct.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
Consider any valid schedule corresponding to this arrival sequence.
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Hypothesis H_jobs_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq.
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 →
task_request_bound_function tsk ε = 0 →
task_response_time_bound arr_seq sched tsk 0.
Second, given a fixed-priority policy with reflexive priorities, ...
Context {FP : FP_policy Task}.
Hypothesis H_reflexive : reflexive_task_priorities FP.
... 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 →
task_response_time_bound arr_seq sched tsk 0.
Thus 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,
task_response_time_bound arr_seq sched tsk R.
End DegenerateTotalRBFs.
In this section, we establish results about the task-wise partitioning of total RBFs of multiple tasks.
Section FP_RBF_partitioning.
Consider any type of tasks ...
Context {Task : TaskType} `{TaskCost Task}.
... and any type of jobs associated with these tasks, where each task has a cost and an associated arrival curve.
Context {Job : JobType} `{JobTask Job Task} `{JobCost Job} `{MaxArrivals Task}.
Consider an FP policy that indicates a higher-or-equal priority relation.
Context `{FP : FP_policy Task}.
Consider a task set ts...
Variable ts : seq Task.
...and let tsk be any task that serves as the reference point for "higher or equal priority" (usually, but not necessarily, from ts).
Variable tsk : Task.
We establish that the bound on the total workload due to higher-or-equal-priority tasks can be partitioned task-wise. In other words, it is equal to the sum of the bound on the total workload due to higher-priority tasks and the bound on the total workload due to equal- priority tasks.
Lemma hep_rbf_taskwise_partitioning :
∀ L,
total_hep_request_bound_function_FP ts tsk L
= total_hp_request_bound_function_FP ts tsk L
+ total_ep_request_bound_function_FP ts tsk L.
Now, assume that the priorities are reflexive.
Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
If the task set does not contain duplicates, then the total higher-or-equal-priority RBF for any task can be split as the sum of the total other higher-or-equal-priority workload and the RBF of the task itself.
Lemma split_hep_rbf :
∀ Δ,
tsk \in ts →
uniq ts →
total_hep_request_bound_function_FP ts tsk Δ
= total_ohep_request_bound_function_FP ts tsk Δ
+ task_request_bound_function tsk Δ.
If the task set may contain duplicates, then the we can only say that the sum of other higher-or-equal-priority RBF and task tsk's RBF is at most the total higher-or-equal-priority workload.
Lemma split_hep_rbf_weaken :
∀ Δ,
tsk \in ts →
total_ohep_request_bound_function_FP ts tsk Δ + task_request_bound_function tsk Δ
≤ total_hep_request_bound_function_FP ts tsk Δ.
End FP_RBF_partitioning.
In this section, we state a few facts for RBFs in the context of a fixed-priority policy.
Section RBFFOrFP.
Consider a set of tasks characterized by WCETs and arrival curves.
Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.
Variable ts : seq Task.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
For any fixed-priority policy, ...
Context `{FP_policy Task}.
... total_ohep_request_bound_function_FP at 0 is always 0.
Lemma total_ohep_rbf0 :
∀ (tsk : Task),
total_ohep_request_bound_function_FP ts tsk 0 = 0.
Next we show how total_ohep_request_bound_function_FP can bound the workload of jobs in a given interval.
Consider any types of jobs.
Context `{Job : JobType} `{JobTask Job Task} `{JobCost Job}.
Consider any arrival sequence that only has jobs from the task set and where all arrivals have a valid job cost.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
Assume there exists an arrival curve and that the arrival sequence respects this curve.
Context `{MaxArrivals Task}.
Hypothesis H_respects_max_arrivals : taskset_respects_max_arrivals arr_seq ts.
Consider any task tsk and any job j of the task tsk.
Variable j : Job.
Variable tsk : Task.
Hypothesis H_job_of_task : job_of_task tsk j.
For any interval `[t1, t1 + Δ)`, the workload of jobs that have higher task priority than the task priority of j is bounded by total_ohep_request_bound_function_FP for the duration Δ.
Lemma ohep_workload_le_rbf :
∀ Δ t1,
workload_of_jobs (another_task_hep_job^~ j) (arrivals_between arr_seq t1 (t1 + Δ))
≤ total_ohep_request_bound_function_FP ts tsk Δ.
End RBFFOrFP.
We know that the workload of a task in any interval must be bounded by the task's RBF in that interval. However, in the proofs of several lemmas, we are required to reason about the workload of a task in an interval excluding the cost of a particular job (usually the job under analysis). Such a workload can be tightly bounded by the task's RBF for the interval excluding the cost of one task.
Notice, however, that this is not a trivial result since a naive approach to proving it would fail. Suppose we want to prove that some quantity A - B is upper bounded by some quantity C - D. This usually requires us to prove that A is upper bounded by C and D is upper bounded by B. In our case, this would be equivalent to proving that the task cost is upper-bounded by the job cost, which of course is not true.
So, a different approach is needed, which we show in this section.
Section TaskWorkload.
Consider any type of tasks ...
Context {Task : TaskType}.
Context `{TaskCost Task}.
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any arrival sequence ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent :
consistent_arrival_times arr_seq.
... and assume that WCETs are respected.
Hypothesis H_arrivals_have_valid_job_costs :
arrivals_have_valid_job_costs arr_seq.
Let tsk be any task ...
Variable tsk : Task.
... characterized by a valid arrival curve.
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
Consider any job j of tsk ...
Variable j : Job.
Hypothesis H_job_of_task : job_of_task tsk j.
... that arrives in the given arrival sequence.
Hypothesis H_j_arrives_in : arrives_in arr_seq j.
Consider any time instant t1 and duration Δ such that j arrives before t1 + Δ.
Variables (t1 : instant) (Δ : duration).
Hypothesis H_job_arrival_lt : job_arrival j < t1 + Δ.
As a preparatory step, we restrict our attention to the sub-interval containing the job's arrival. We know that the job's arrival necessarily happens in the interval (`[job_arrival j], t1 + Δ`). This allows us to show that the task workload excluding the task cost can be bounded by the cost of the arrivals in the interval as follows.
Lemma task_rbf_without_job_under_analysis_from_arrival :
task_workload_between arr_seq tsk (job_arrival j) (t1 + Δ) - job_cost j
≤ task_cost tsk × number_of_task_arrivals arr_seq tsk (job_arrival j) (t1 + Δ)
- task_cost tsk.
To use the above lemma in our final theorem, we require that the arrival of the job under analysis necessarily happens in the interval we are considering.
Hypothesis H_j_arrives_after_t : t1 ≤ job_arrival j.
Under the above assumption, we can finally establish the desired bound.
Lemma task_rbf_without_job_under_analysis :
task_workload_between arr_seq tsk t1 (t1 + Δ) - job_cost j
≤ task_request_bound_function tsk Δ - task_cost tsk.
End TaskWorkload.