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 ].
  Proof.
    move⇒ j ARR.
    set arrivals := task_arrivals_up_to_job_arrival arr_seq j.
    have IN : j \in arrivals
      by apply: arrives_in_task_arrivals_up_to.
    ∃ (job_arrival j), (take (index j arrivals) arrivals),
      (drop (index j arrivals).+1 arrivals).
    change (arrivals = take (index j arrivals) arrivals
                       ++ [:: j] ++ drop (index j arrivals).+1 arrivals).
    have TAIL : drop (index j arrivals) arrivals
                = [:: j] ++ drop (index j arrivals).+1 arrivals.
    { rewrite /= (@drop_nth _ j); last by rewrite index_mem.
      by rewrite (nth_index j IN). }
    by rewrite -TAIL cat_take_drop.
  Qed.

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).
  Proof.
    move⇒ tsk t1 t2 LEQ.
    ∃ t2, (task_arrivals_before arr_seq tsk t1),
      (task_arrivals_between arr_seq tsk t2 t2.+1).
    rewrite /task_arrivals_up_to /task_arrivals_before
            /task_arrivals_between.
    rewrite (arrivals_between_cat _ 0 t2 t2.+1) //=
            (arrivals_between_cat _ 0 t1 t2) //=.
    by rewrite !filter_cat catA.
  Qed.

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.
  Proof.
    move⇒ tsk RESP j ARR TSK.
    rewrite /valid_job_cost /task_cost /=.
    have COST : \sum_(j0 <- [:: j]) job_cost j0
                ≤ task_cumulative_cost (job_task j) (size [:: j]).
    { move: TSK; rewrite /job_of_task ⇒ /eqP TSK; rewrite TSK.
      apply: RESP; rewrite -TSK.
      by apply: arriving_job_is_consecutive_task_arrival. }
    by rewrite big_seq1 in COST.
  Qed.

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.
  Proof.
    move⇒ FROM j ARR.
    apply: valid_job_cost_from_cumulative_cost_bound ⇒ //=.
    by rewrite /job_of_task.
  Qed.

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.
  Proof.
    move⇒ tsk.
    split; first by rewrite /task_cumulative_cost /= mul0n.
    move⇒ x y LEQ.
    rewrite /task_cumulative_cost /=.
    case: (task_cost tsk) ⇒ [|c]; first by rewrite !muln0.
    by rewrite leq_pmul2r.
  Qed.

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.
  Proof.
    move⇒ VALID tsk js [t [prefix [suffix ARR]]].
    rewrite /task_cumulative_cost /= mulnC -sum1_size big_distrr //= muln1.
    apply: leq_sum_seq ⇒ j IN _.
    have: j \in task_arrivals_up_to arr_seq tsk t by rewrite ARR !mem_cat IN !orbT.
    rewrite /task_arrivals_up_to ⇒ IN'.
    have /eqP <- : job_of_task tsk j by (move: IN'; rewrite mem_filter ⇒ /andP [TSK _]).
    by apply/VALID/arrives_in_task_arrivals_implies_arrived.
  Qed.

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.
  Proof. by move⇒ tsk IN; apply: trivial_cumulative_cost_valid. Qed.

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.
  Proof. by move⇒ VALID tsk IN; apply: trivial_cumulative_cost_respected. Qed.

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.