# Library prosa.model.task.cumulative_cost

Require Export prosa.model.task.arrivals.

# WCET(n): Cumulative Task Costs

In this module, we introduce a task parameter for cumulative execution-time bounds, which is commonly referred to as WCET(n). Whereas task_cost tsk bounds the cost of any one job of task tsk, task_cumulative_cost tsk n bounds the total cost of any n consecutive jobs of tsk.
We first define a task-model parameter that expresses each task's cumulative worst-case execution-time bound WCET(n).
Class TaskCumulativeCost (Task : TaskType) :=
{
task_cumulative_cost : Task → nat → work
}.
A cumulative cost parameter also induces the ordinary scalar WCET parameter by considering exactly one job, i.e., WCET(1). We make this conversion a local instance so that it needs explicit opt-in, as it is a rather rare case.
#[local,program] Instance task_cost_from_cumulative_cost
{Task : TaskType} `{TaskCumulativeCost Task} : TaskCost Task :=
{
task_cost tsk := task_cumulative_cost tsk 1
}.
Conversely, a legacy scalar WCET parameter induces a default cumulative bound by multiplying the scalar WCET by the number of arrivals. This is a compatibility fallback for contexts that provide only a scalar WCET and hence is made globally visible.
#[global,program] Instance task_cost_as_cumulative_cost
{Task : TaskType} `{TaskCost Task} : TaskCumulativeCost Task :=
{
task_cumulative_cost tsk n := n × task_cost tsk
}.
In the following section, we define basic validity conditions for cumulative task costs.
Section ValidTaskCumulativeCost.
Consider any type of tasks with cumulative cost bounds.
Context {Task : TaskType} `{TaskCumulativeCost Task}.
A cumulative cost bound is well-formed if it maps zero arrivals to zero cost and is monotonic in the number of arrivals.
Definition valid_task_cumulative_cost (tsk : Task) :=
task_cumulative_cost tsk 0 = 0
∧ monotone leq (task_cumulative_cost tsk).
We lift the constraint to task sets.
Definition taskset_has_valid_cumulative_cost_bounds (ts : TaskSet Task) :=
∀ tsk,
tsk \in ts →
valid_task_cumulative_cost tsk.
End ValidTaskCumulativeCost.
Next, we define what it means for an arrival sequence to respect a cumulative cost bound.
Section RespectsTaskCumulativeCost.
Consider any type of tasks with cumulative cost bounds ...
Context {Task : TaskType} `{TaskCumulativeCost Task}.
... and any type of jobs associated with these tasks.
Context {Job : JobType} `{JobTask Job Task}.
Context `{JobCost Job}.
Context `{JobArrival Job}.
Consider a given arrival sequence.
Variable arr_seq : arrival_sequence Job.
A sequence of jobs js is a consecutive block of arrivals of task tsk if it occurs contiguously in the list of task arrivals up to some time.
Definition consecutive_task_arrivals (tsk : Task) (js : seq Job) :=
∃ t prefix suffix,
task_arrivals_up_to arr_seq tsk t = prefix ++ js ++ suffix.
The arrival sequence respects the cumulative cost bound of task tsk if every consecutive block of jobs of tsk is bounded by task_cumulative_cost tsk.
Definition respects_task_cumulative_cost (tsk : Task) :=
∀ js,
consecutive_task_arrivals tsk js →
\sum_(j <- js) job_cost j ≤ task_cumulative_cost tsk (size js).
Finally, we lift the validity constraint to task sets.
Definition taskset_respects_cumulative_cost_bounds (ts : TaskSet Task) :=
∀ tsk,
tsk \in ts →
respects_task_cumulative_cost tsk.
End RespectsTaskCumulativeCost.