Library prosa.analysis.facts.model.rbf

Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.facts.model.arrival_curves.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.request_bound_function.
Require Export prosa.analysis.definitions.schedulability.

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.

Section ProofWorkloadBound.

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

Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

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

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

Context `{FP_policy Task}.

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

Hypothesis H_valid_job_cost :
arrivals_have_valid_job_costs arr_seq.

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

Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

Let max_arrivals be any arrival bound for task-set ts.

Context `{MaxArrivals Task}.
Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.

Next, recall the notions of total workload of jobs...

Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between arr_seq t1 t2).

... and the workload of jobs of the same task as job j.

Let task_workload t1 t2 :=
workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2).

Finally, let us define some local names for clarity.

Let task_rbf := task_request_bound_function tsk.
Let total_rbf := total_request_bound_function ts.

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.

    Lemma task_workload_le_num_of_arrivals_times_cost:
      task_workload t (t + Δ)
      ≤ task_cost tsk × number_of_task_arrivals arr_seq tsk t (t + Δ).

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_job_of_tsk : job_of_task tsk j.

Consider any general predicate defined on tasks.

Variable pred : pred Task.

We prove that the sum of job cost of jobs whose corresponding task satisfies the predicate pred is bound by the RBF of these tasks.

    Lemma sum_of_jobs_le_sum_rbf:
      \sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred (job_task j'))
        job_cost j' ≤
        \sum_(tsk' <- ts | pred tsk')
          task_request_bound_function tsk' Δ.

  End WorkloadIsBoundedByRBF.

End ProofWorkloadBound.

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

Let's define some local names for clarity.

Let task_rbf := task_request_bound_function tsk.

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.

Lemma task_rbf_1_ge_task_cost:
task_rbf ε ≥ task_cost tsk.

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.

Lemma task_rbf_epsilon_gt_0 : 0 < task_rbf ε.

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

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