Library probsa.rt.analysis.nth_cost

From prosa.model Require Import task.arrival.curves.

From probsa.rt.model Require Export workload.

Local Open Scope nat_scope.

In this file, we define the notion of the n-th job of a task and its associated cost random variable. It then proves that these costs are independent when the underlying job costs are independent.

Section NthCost.

  Context {Ω} {μ : measure Ω}.

  Context {Task : TaskType}.
  Context {Job : finType}
          {job_cost : JobCostRV Job Ω μ}
          {job_task : JobTask Job Task}.

Given a task tsk and an index i, task_job tsk i is the i-th job belonging to task tsk. Returns None if there are fewer than i+1 jobs for this task. Note that the order is arbitrary but fixed.

  Definition task_job : Task → nat → option Job :=
    fun tsk n ⇒
      nth None [seq Some j | j <- index_enum Job & job_of_task tsk j] n.

Given a task tsk and a constant i, nth_cost tsk i is the random variable for the cost of the i-th job of task tsk. If no such job exists, returns the constant random variable 0.

  Definition nth_cost : Task → nat → rvar μ [eqType of instant] :=
    λ (tsk : Task) (i : nat ),
      match task_job tsk i with
      | Some j ⇒ odflt0 (job_cost j)
      | None ⇒ rvar_const _ 0
      end.

End NthCost.

Section NthCostLemmas.

  Context {Ω} {μ : measure Ω}.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {α : MaxArrivals Task}
          {FP : FP_policy Task}.

  Context {Job : finType}
          {job_cost : JobCostRV Job Ω μ}
          {job_arrival : JobArrivalRV Job Ω μ}
          {job_task : JobTask Job Task}.

  Context {PState : ProcessorState Job}.
  Variable pr_sched : pr_schedule μ PState.

  Hypothesis H_arrival_sequence_uniq : pr_arrival_sequence_uniq.
  Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.

We assume all job costs are independent random variables.

Hypothesis H_job_costs_independent :
independent [seq job_cost j | j <- index_enum Job].

Consider an arbitrary task set ts ...

Variable ts : seq Task.
Hypothesis H_ts_uniq : uniq ts.

... and a task tsk ∈ ts.

Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.

We show that the costs of the jobs at indices in a range [a, a+δ) are independent, provided this range doesn't exceed the number of jobs belonging to task tsk.

  Lemma task_job_cost_independence_aux :
    ∀ (a δ : nat) ,
      a + δ ≤ size [seq Some j | j <- index_enum Job & job_of_task tsk j] →
      independent [seq nth_cost tsk x | x <- iota a δ].

Next, we extend the above lemma to arbitrary index ranges [a, b) by case analysis. (1) If [a, b) is beyond all jobs for tsk: all variables are constant 0, hence trivially independent. (2) If [a, b) partially overlaps: split into jobs [a, n) and constants [n, b), where n is the number of jobs. If [a, b) is entirely within jobs: apply the auxiliary lemma directly.

  Lemma task_job_cost_independence :
    ∀ (a b : nat),
      independent [seq nth_cost tsk i | i <- iota a b].

Finally, we instantiate the independence result for the specific range [0, α tsk (t + D tsk)), where α gives the maximum number of arrivals and D is the task deadline.

  Corollary task_job_cost_independence_ac :
    ∀ (t : instant),
      independent [seq nth_cost tsk x | x <- iota 0 (α tsk (t + D tsk))].

End NthCostLemmas.