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...
... and any ideal uni-processor schedule of this arrival sequence.
Consider an FP policy that indicates a higher-or-equal priority relation.
Consider a task set ts...
  Variable ts : list 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.
Next, we assume that all jobs come from the task set.
Let max_arrivals be any arrival bound for task-set ts.
Let's define some local names for clarity.
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_task j = tsk.

Next, 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.
Next, we recall the notions of total workload of jobs...
...notions of workload of higher or equal priority jobs...
... workload of other higher or equal priority jobs...
... and the workload of jobs of the same task as job j.
In this section we prove that the workload of any jobs is no larger than the request bound function.
  Section WorkloadIsBoundedByRBF.

Consider any time t and any interval of length delta.
    Variable t : instant.
    Variable delta : 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 + delta) task_rbf delta.

Next, 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 tasks with higher-or-equal priority is no larger than the total request bound function.
Next, we prove that total workload of tasks 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 delta = 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 task_rbf leq.

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_task j = tsk.

Then we prove that task_rbf 1 is greater than or equal to task cost.