Library probsa.rt.analysis.independent.cost_and_workload

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice fintype bigop seq.

From probsa.rt.model Require Export events workload assumptions.basic.

Section JobCostWorkloadIndependent.

  Context {Ω} {μ : measure Ω}.

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

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

  Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.

  Variable (ts : seq Task) (tsk : Task).
  Hypothesis H_tsk_in_ts : tsk \in ts.

Consider a job of task tsk.

Variable j : Job.
Hypothesis H_job_of_task : job_of_task tsk j.

Assume that job costs conditioned on an arrival sequence are independent.

  Hypothesis H_job_costs_cond_independent :
    let ξpart := partition_on_ξ μ : Ω_partition in
    ∀ (ξ : I ξpart) `(!PosProb μ (ξpart ◁{ξ })),
      independent [
          seq mkRvar (restrict μ (ξpart ◁{ξ })) (job_cost j)
        | j <- index_enum Job].

  Let ξpart := partition_on_ξ μ : Ω_partition.
  Variable (ξ : I ξpart) (ω : Ω).
  Hypothesis IN ω ξ : ξpart ◁{ξ } ω.
  Hypothesis POS : PosProb μ (ξpart ◁{ξ }).

  Variable (t : instant) (Δ : duration).

We define two random variables on the restricted probability space (conditioned on a fixed arrival sequence ξ):

𝓒 - The cost of job j (defaulting to 0 if the job doesn't arrive). This represents the workload contribution of our specific job.

𝓦 - The total workload of all tasks with higher or equal priority than tsk distinct from tsk over the interval [t - D tsko, t + Δ) for each such task tsko. This represents the interfering workload from higher-priority tasks. Note: The specific interval

[t - D

tsko, t + Δ)>> is used because it's later required for the pRTA proof.

  Let 𝓒 :=
        mkRvar _ [eta odflt0 (job_cost j)]
        : rvar (restrict μ (ξpart ◁{ξ })) [eqType of work].

  Let 𝓦 :=
        mkRvar _ (fun ω ⇒
                    \sum_(tsko <- ts | hep_task tsko tsk && (tsko != tsk ))
                     pr_workload_of_task tsko (t - D tsko) (t + Δ) ω
                 )
        : rvar (restrict μ (ξpart ◁{ξ })) [eqType of work].

We show that these two random variables are independent: the cost of job j does not depend on the costs of jobs from higher-priority tasks.

  Local Lemma job_cost_and_ohep_workload_indep2 :
    indep2 𝓒 𝓦.

  Corollary job_cost_and_ohep_workload_independent :
    ∀ (c w : work),
      ℙ <μ >{[ (𝓒 ⟨=⟩ c ) ∩ (𝓦 ⟨=⟩ w ) | ξpart ◁{ξ } ]}
      = ℙ <μ >{[ 𝓒 ⟨=⟩ c | ξpart ◁{ξ } ]} × ℙ <μ >{[ 𝓦 ⟨=⟩ w | ξpart ◁{ξ } ]}.

End JobCostWorkloadIndependent.