Library prosa.analysis.facts.model.cumulative_cost

Require Export prosa.model.task.cumulative_cost.
Require Export prosa.analysis.facts.model.task_arrivals.

Facts About Cumulative Task Costs

In this file, we establish basic consequences of cumulative task-cost validity. In particular, a cumulative bound for singleton blocks implies the ordinary scalar job-cost validity assumption.

We first establish some basic facts about consecutive arrivals of a task.

Section ConsecutiveArrivals.

Consider any type of tasks and their jobs.

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

Consider any job arrival sequence with consistent arrival times.

Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.

Any arriving job j is trivially a "consecutive" block in the arrival sequence of job_task j.

  Lemma arriving_job_is_consecutive_task_arrival :
    ∀ j,
      arrives_in arr_seq j →
      consecutive_task_arrivals arr_seq (job_task j) [:: j ].

The arrivals of a given task in any half-open interval are consecutive.

  Lemma task_arrivals_between_is_consecutive_task_arrival :
    ∀ tsk t1 t2,
      t1 ≤ t2 →
      consecutive_task_arrivals arr_seq tsk
        (task_arrivals_between arr_seq tsk t1 t2).

End ConsecutiveArrivals.

Next, we derive ordinary scalar job-cost validity from cumulative cost validity.

Section ValidJobCosts.

Consider any type of tasks with cumulative cost bounds ...

Context {Task : TaskType} `{TaskCumulativeCost Task}.

... and their associated jobs with execution costs and arrival times.

Context {Job : JobType} `{JobTask Job Task} `{JobCost Job} `{JobArrival Job}.

Consider any job arrival sequence with consistent arrival times.

Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.

Let task_cost be defined by WCET(1).

#[local] Existing Instance task_cost_from_cumulative_cost.

Given a task that with a valid cumulative cost bound tsk, every arriving job j of the task has a valid scalar job cost.

  Lemma valid_job_cost_from_cumulative_cost_bound :
    ∀ tsk,
      respects_task_cumulative_cost arr_seq tsk →
      ∀ j,
        arrives_in arr_seq j →
        job_of_task tsk j →
        valid_job_cost j.

We next lift the above property to task sets. Consider any given task set with valid cumulative execution-time bounds.

Variable ts : seq Task.
Hypothesis H_bounds_respected : taskset_respects_cumulative_cost_bounds arr_seq ts.

All jobs in an arrival sequence of the task set have valid scalar job costs.

  Corollary valid_job_costs_from_cumulative_cost_bounds :
    all_jobs_from_taskset arr_seq ts →
    arrivals_have_valid_job_costs arr_seq.

End ValidJobCosts.

The trivial cumulative cost WCET(n) = n × WCET is valid for every task.

Section TrivialCumulativeCostValidity.

Consider any type of tasks with a scalar WCET ...

Context {Task : TaskType} `{ScalarCost : TaskCost Task}.

... and the induced trivial WCET(n) bound for such tasks.

Let TrivialCumulativeCost := (@task_cost_as_cumulative_cost Task ScalarCost).

The trivial cumulative bound induced by the scalar bound is well formed.

  Lemma trivial_cumulative_cost_valid :
    ∀ tsk,
      @valid_task_cumulative_cost Task TrivialCumulativeCost tsk.

Next, consider an arrival sequence of the jobs associated with these tasks.

Context {Job : JobType} `{JobTask Job Task} `{JobCost Job} `{JobArrival Job}.
Variable arr_seq : arrival_sequence Job.

Ordinary scalar job-cost validity implies that the induced trivial WCET(n) bound is respected.

  Lemma trivial_cumulative_cost_respected :
    arrivals_have_valid_job_costs arr_seq →
    ∀ tsk,
      @respects_task_cumulative_cost Task TrivialCumulativeCost
        Job _ _ arr_seq tsk.

For automation, we lift the two previous lemmas to task sets.

Variable ts : seq Task.

The induced trivial WCET(n) bound is valid for every task.

Fact taskset_trivial_cumulative_cost_valid :
taskset_has_valid_cumulative_cost_bounds ts.

The induced trivial WCET(n) bound is respected by every task if each task's WCET is valid.

  Fact taskset_trivial_cumulative_cost_bound_respected :
    arrivals_have_valid_job_costs arr_seq →
    taskset_respects_cumulative_cost_bounds arr_seq ts.

End TrivialCumulativeCostValidity.

We add the above lemmas about the induced trivial cost bound into the "Hint Database" basic_rt_facts so that they become available for proof automation.

Global Hint Resolve
  valid_job_cost_from_cumulative_cost_bound
  valid_job_costs_from_cumulative_cost_bounds
  trivial_cumulative_cost_valid
  trivial_cumulative_cost_respected
  taskset_trivial_cumulative_cost_valid
  taskset_trivial_cumulative_cost_bound_respected
  : basic_rt_facts.