Library prosa.analysis.facts.model.dbf

Require Export prosa.model.task.absolute_deadline.
Require Export prosa.analysis.definitions.demand_bound_function.
Require Export prosa.analysis.facts.model.rbf.
Require Export prosa.analysis.facts.model.workload.

Facts about the Demand Bound Function (DBF)

In this file we establish some properties of DBFs.

Section ProofDemandBoundDefinition.

Consider any type of task with relative deadlines and any type of jobs associated with such tasks.

Context {Task : TaskType} `{TaskDeadline Task}
{Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

Consider a valid arrival sequence.

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

First, we establish a relation between a task's arrivals in a given interval and those arrivals that also have a deadline contained within the given interval.

  Lemma task_arrivals_with_deadline_within_eq:
    ∀ (tsk : Task) (t : instant) (delta : duration),
      task_arrivals_with_deadline_within arr_seq tsk t (t + delta)
      = task_arrivals_between arr_seq tsk t (t + (delta - (task_deadline tsk -1))).

As a corollary, we also show a much more useful result that arises when we count these jobs.

  Corollary num_task_arrivals_with_deadline_within_eq:
    ∀ (tsk : Task) (t : instant) (delta : duration),
      number_of_task_arrivals_with_deadline_within arr_seq tsk t (t + delta)
      = number_of_task_arrivals arr_seq tsk t (t + (delta - (task_deadline tsk - 1))).

In the following, assume we are given a valid WCET bound for each task.

Context `{TaskCost Task} `{JobCost Job}.
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.

A task's demand in a given interval is the sum of the execution costs (i.e., the workload) of the task's jobs that both arrive in the interval and have a deadline within it.

  Definition task_demand_within (tsk : Task) (t1 t2 : instant) :=
    let
      causing_demand (j : Job) := (job_deadline j ≤ t2 ) && (job_of_task tsk j )
    in
      workload_of_jobs causing_demand (arrivals_between arr_seq t1 t2).

Consider a task set ts.

Variable ts : seq Task.

Let max_arrivals be any arrival curve.

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

The task's processor demand task_demand_within is upper-bounded by the task's DBF task_demand_bound_function.

  Lemma task_demand_within_le_task_dbf:
    ∀ (tsk : Task) t delta,
      tsk \in ts →
      task_demand_within tsk t (t + delta) ≤ task_demand_bound_function tsk delta.

We also prove that task_demand_within is less than shifted RBF.

  Corollary task_demand_within_le_task_rbf_shifted:
    ∀ (tsk : Task) t delta,
      tsk \in ts →
      task_demand_within tsk t (t + delta) ≤ task_request_bound_function tsk (delta - (task_deadline tsk - 1)).

Next, we define the total workload of all jobs that arrives in a given interval that also have a deadline within the interval.

  Definition total_demand_within (t1 t2 : instant) :=
    let
      causing_demand (j : Job) := job_deadline j ≤ t2
    in
      workload_of_jobs causing_demand (arrivals_between arr_seq t1 t2).

Assume that all jobs come from the task set ts.

Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

We relate total_demand_within to the sum of each task's demand task_demand_within.

  Lemma total_demand_within_le_sum_over_partitions:
    ∀ (t : instant) (delta : duration),
      total_demand_within t (t + delta) ≤ \sum_(tsk <- ts ) task_demand_within tsk t (t + delta).

Here we prove a stronger version of the above lemma by assuming that the task set ts is indeed a set.

  Lemma total_demand_within_partitioned_by_tasks:
    ∀ (t : instant) (delta : duration),
      uniq ts →
      total_demand_within t (t + delta) = \sum_(tsk <- ts ) task_demand_within tsk t (t + delta).

Finally we establish that total_demand_within is bounded by total_demand_bound_function.

  Lemma total_demand_within_le_total_dbf:
    ∀ (t : instant) (delta : duration),
      total_demand_within t (t + delta) ≤ total_demand_bound_function ts delta.

As a corollary, we also note that total_demand_within is less than the sum of each task's shifted RBF.

  Corollary total_demand_within_le_sum_task_rbf_shifted:
    ∀ (t : instant ) (delta : instant),
      total_demand_within t (t + delta)
      ≤ \sum_(tsk <- ts ) task_request_bound_function tsk (delta - (task_deadline tsk - 1)).

End ProofDemandBoundDefinition.