# 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.
For convenience in subsequent proofs, we restate the RBF specification as two simple lemmas.
Section RBFSpec.
Consider any type of tasks characterized by RBFs ...
Context {Task : TaskType}.
Context `{MaxRequestBound Task}.
... and their associated jobs.
Context {Job : JobType} `{JobTask Job Task}
`{JobArrival Job} `{JobCost Job}.
Consider any valid arrival sequence.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Consider a given task tsk ...
Variable tsk : Task.
... with a sound RBF.
Hypothesis H_rbf_respected :
respects_max_request_bound arr_seq tsk (max_request_bound 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 Δ.
We next establish 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.
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.
End RBFSpec.
Section SumsOfRBFs.
Consider any type of tasks characterized by RBFs ...
Context {Task : TaskType}.
Context `{MaxRequestBound Task}.
... and their associated jobs.
Context {Job : JobType} `{JobTask Job Task}
`{JobArrival Job} `{JobCost Job}.
Now, consider a task set ts ...
Variable ts : seq Task.
... and a valid arrival sequence of this task set ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
... that respects the RBFs.
Hypothesis H_sound_RBF : taskset_respects_max_request_bound arr_seq ts.
First, we observe 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}.
... a given task, ...
Variable tsk : Task.
... and any schedule of the arriving jobs.
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
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 SumsOfRBFs.

## RBF Properties

In this section, we restate two simple properties and identities of RBFs.
Section RequestBoundFunctions.
Consider any type of tasks characterized by RBFs.
Context {Task : TaskType}.
Context `{MaxRequestBound Task}.
Let tsk be any task.
Variable tsk : Task.
Assume that tsk's RBF is a valid request-bound function.
Hypothesis H_valid_rbf :
valid_request_bound_function (max_request_bound tsk).
By definition task_request_bound_function 0 is equal to 0.
Lemma task_rbf_0_zero :
task_request_bound_function tsk 0 = 0.
By definition task_request_bound_function is monotone.
Lemma task_rbf_monotone :
monotone leq (task_request_bound_function tsk).
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 RBFs.
Context {Task : TaskType} `{MaxRequestBound Task}.
Variable ts : seq Task.
Hypothesis H_valid_rbf : valid_taskset_request_bound_function ts task_request_bound_function.
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 RBFs ...
Context {Task : TaskType} `{MaxRequestBound Task}.
Variable ts : seq Task.
... and any consistent arrival sequence of 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.
Suppose the RBFs are correct.
Hypothesis H_sound_rbf : taskset_respects_max_request_bound 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 characterized by RBFs.
Context {Task : TaskType} `{MaxRequestBound 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 RBFs.
Context {Task : TaskType} `{MaxRequestBound Task}.
Variable ts : seq Task.
Hypothesis H_valid_rbf : valid_taskset_request_bound_function ts max_request_bound.
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.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
Assume that the arrival sequence respects the RBFs.
Hypothesis H_respects_max_request_bound : taskset_respects_max_request_bound 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.

## Properties of Scalar RBFs

As a "compatibility layer", for the common case of linear WCET(n) approximations derived from a scalar WCET parameter, we establish a rewriting lemma to express the RBF as a simple scalar multiplication of the task's WCET and its arrival curve.
Section LinearRBF.
Consider any type of tasks characterized by WCETs and arrival curves.
Context {Task : TaskType}.
Context `{TaskCost Task} `{MaxArrivals Task}.
For such tasks, the RBF definition reduces to a simple multiplication.
Lemma scalar_rbf_def :
∀ tsk Δ,
task_request_bound_function tsk Δ = task_cost tsk × max_arrivals tsk Δ.
End LinearRBF.
In this section, we prove simple properties and identities of RBFs obtained from scalar WCETs.
Section ScalarRequestBoundFunctions.
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).
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 ScalarRequestBoundFunctions.
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).
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.
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.