Library prosa.analysis.facts.model.rbf

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 ...
  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 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...
  Variable ts : seq Task.

... and let tsk be any task in ts.
  Variable tsk : Task.
  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.
  Section WorkloadIsBoundedByRBF.

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.
As a corollary, we prove that workload of task is no larger the than task request bound function.
    Corollary task_workload_le_task_rbf:
      task_workload t (t + Δ) task_rbf Δ.

Next, we prove that total workload of tasks is no larger than the total request bound function.
    Lemma total_workload_le_total_rbf:
      total_workload t (t + Δ) total_rbf Δ.
Next, we consider any job j of tsk.
    Variable j : Job.
    Hypothesis H_j_arrives : arrives_in arr_seq j.
    Hypothesis H_job_of_tsk : job_of_task tsk j.

We say that two jobs j1 and j2 are in relation other_higher_eq_priority, iff j1 has higher or equal priority than j2 and is produced by a different task.
Recall the notion of workload of higher or equal priority jobs...
    Let total_hep_workload t1 t2 :=
      workload_of_jobs (fun j_otherjlfp_higher_eq_priority j_other j)
                       (arrivals_between arr_seq t1 t2).

... and workload of other higher or equal priority jobs.
    Let total_ohep_workload t1 t2 :=
      workload_of_jobs (fun j_otherother_higher_eq_priority j_other j)
                       (arrivals_between arr_seq t1 t2).

We prove that total workload of other tasks with higher-or-equal priority is no larger than the total request bound function.
Next, we prove that total workload of all tasks with higher-or-equal priority is no larger than the total request bound function.

RBF Properties

In this section, we prove simple properties and identities of RBFs.
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.
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.
Let's define some local names for clarity.
We prove that task_rbf 0 is equal to 0.
  Lemma task_rbf_0_zero:
    task_rbf 0 = 0.

We prove that task_rbf is monotone.
  Lemma task_rbf_monotone:
    monotone leq task_rbf.

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.
As a corollary, we prove that the task_rbf 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_rbf A task_cost tsk.

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.
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.
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, ...
  Context `{FP_policy Task}.

... 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 ...
  Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.
  Variable ts : seq Task.

... 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, ...
  Context `{FP_policy Task}.
  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.
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,
        task_response_time_bound arr_seq sched tsk R.

End DegenerateTotalRBFs.