Facts about Request-Bound Functions (RBFs)

In this file, we prove some lemmas about RBFs.

RBF is a Bound on Workload

Consider any type of tasks characterized by WCETs and arrival curves ...

... and any type of jobs associated with these tasks.

Consider any valid arrival sequence ...

... and any schedule corresponding to this arrival sequence.

Assume that the job costs are no larger than the task costs.

In this section, we establish that a task's RBF is indeed an upper bound on the task's workload.

Consider a given task tsk.

First, as a stepping stone, we observe that any sequence of jobs of the task jointly satisfy the task's WCET.

Next, suppose that task tsk respects its arrival curve max_arrivals.

From this assumption, we establish the RBF spec: In any interval of any length, the RBF upper-bounds the task's actual workload.

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).

Consider any predicate P on jobs.

Consider any task tsk that respects its arrival curve max_arrivals

Assume that all jobs that satisfy P come from task tsk.

Trivially, the workload of jobs from task tsk that satisfy the predicate P is bounded by the task's RBF.

Now, consider a task set ts ...

... and assume that all jobs come from the task set.

Assume that all tasks in the task set respect max_arrivals.

Next, we prove that total workload is upper-bounded by the total RBF.

In this section, we prove a more general result about the workload of arbitrary sets of jobs.

Consider two predicates, one on jobs and one on tasks.

Assume that for all jobs satisfying pred1, the task it belongs to satisfies pred2.

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.

Next, we establish bounds specific to fixed-priority scheduling.

Consider an arbitrary fixed-priority policy ...

... and any given 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.

We next prove that the higher-or-equal-priority workload of tasks different from tsk is bounded by total_ohep_rbf.

Consider any job j of tsk.

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.

In this section, we show that the total RBF is a bound on higher-or-equal priority workload under any JLFP policy.

Consider a JLFP policy that indicates a higher-or-equal priority relation ...

... and any job j.

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.

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.

Consider any arrival sequence.

Let tsk be any 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.

We prove that task_request_bound_function 0 is equal to 0.

We prove that task_request_bound_function is monotone.

In the following, we assume that tsk has a positive cost ...

... and max_arrivals tsk ε is positive.

Then we prove that task_request_bound_function at ε is greater than or equal to the task's WCET.

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.

Then, we prove that task_request_bound_function at ε is greater than 0.

Consider a set of tasks ts containing the task tsk.

Next, we prove that cost of tsk is less than or equal to the total_request_bound_function.

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.

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

... the total RBF of higher- or equal-priority tasks is also monotonic, ...

... as is the variant that excludes the reference task.

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.

Second, given a fixed-priority policy with 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.

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.

In this section, we establish results about the task-wise partitioning of total RBFs of multiple tasks.

Consider any type of tasks ...

... and any type of jobs associated with these tasks, where each task has a cost and an associated arrival curve.

Consider an FP policy that indicates a higher-or-equal priority relation.

Consider a task set ts...

...and let tsk be any task that serves as the reference point for "higher or equal priority" (usually, but not necessarily, from ts).

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.

Now, assume that the priorities are reflexive.

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.

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.

In this section, we state a few facts for RBFs in the context of a fixed-priority policy.

Consider a set of tasks characterized by WCETs and arrival curves.

For any fixed-priority policy, ...

... total_ohep_request_bound_function_FP at 0 is always 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.

Consider any arrival sequence that only has jobs from the task set and where all arrivals have a valid job cost.

Assume there exists an arrival curve and that the arrival sequence respects this curve.

Consider any task tsk and any job j of the task tsk.

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 Δ.

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.

Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Consider any arrival sequence ...

... and assume that WCETs are respected.

Let tsk be any task ...

... characterized by a valid arrival curve.

Consider any job j of tsk ...

... that arrives in the given arrival sequence.

Consider any time instant t1 and duration Δ such that j arrives before 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.

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.

Under the above assumption, we can finally establish the desired bound.