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 δ].
  Proof.
    intros.
    apply: indep_irr; last erewrite map_comp with
      (f1 := fun o ⇒ match o with Some j ⇒ odflt0 (job_cost j) | None ⇒ rvar_const _ 0 end)
      (f2 := fun i ⇒ task_job tsk i); first by reflexivity.
    set (f1 := fun o ⇒ match o with Some j ⇒ job_cost j | None ⇒ rvar_const _ None end).
    set (f2 := Some : Job → option Job).
    have IND := @H_job_costs_independent.
    eapply indep_irr in IND; last by reflexivity.
    erewrite map_comp with (f1 := f1) (f2 := f2) in IND.
    eapply indep_comp with (f := odflt 0) in IND.
    eapply indep_subset with (xs := [seq task_job tsk i | i <- iota a δ]) in IND.
    { eapply indep_irr in IND; first by apply IND.
      by intros [j | ] ω IN POS; reflexivity. }
    { intros [j | ] IN.
      - by rewrite mem_map; [apply mem_index_enum | intros ? ? E; inversion E].
      - exfalso; move: IN ⇒ /mapP [i IN EQ].
        have jd : Job.
        { destruct δ; first by move: IN.
          by destruct (index_enum Job) as [ | s]; [ move: H; rewrite addnS | exact s].
        }
        rewrite /task_job (nth_map jd) in EQ; first by inversion EQ.
        apply: leq_trans; first by move: IN; rewrite mem_iota ⇒ /andP [_ T2]; apply T2.
        by apply: leq_trans; [apply H | rewrite size_map].
    }
    { rewrite map_inj_in_uniq; [by apply iota_uniq | ] ⇒ i1 i2 IN1 IN2 EQ.
      apply: nth_seq_eq; last by apply EQ.
      { apply: leq_trans; last by apply H.
        by move: IN1; rewrite mem_iota ⇒ /andP [_ T2]. }
      { apply: leq_trans; last by apply H.
        by move: IN2; rewrite mem_iota ⇒ /andP [_ T2]. }
      { rewrite map_inj_uniq; last by intros ? ? E; inversion E.
        by apply filter_uniq, index_enum_uniq. }
    }
    { rewrite map_inj_uniq.
      - by apply index_enum_uniq.
      - by intros ? ? E; inversion E.
    }
  Qed.

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].
  Proof.
    intros a b.
    have ->: iota a b = index_iota a (a + b).
    { by rewrite /index_iota addKn. }
    set(n := size [seq Some j | j <- index_enum Job & job_of_task tsk j]).
    have [NEQ|[NEQ|NEQ]] : n ≤ a ∨ a < n ≤ a + b ∨ a + b < n.
    { have [NEQ1|NEQ1] := leqP n a; [by left | right].
      by have [NEQ2|NEQ2] := leqP n (a + b); [left | right].
    }
    { apply indep_consts ⇒ i; rewrite mem_index_iota ⇒ /andP [LE1 LE2].
      ∃ 0 ⇒ ω; rewrite /nth_cost /task_job nth_default; first by reflexivity.
      by apply: leq_trans; first apply NEQ.
    }
    { rewrite /index_iota addKn.
      move: NEQ ⇒ /andP [NEQ1 NEQ2].
      have [δ [EQ POS]] : ∃ δ, n = a + δ ∧ δ > 0.
      { ∃ (n - a); split.
        - by rewrite -maxnE; symmetry; apply/maxn_idPr; apply ltnW.
        - by rewrite subn_gt0.
      }
      rewrite EQ in NEQ1, NEQ2; clear NEQ1; rewrite leq_add2l in NEQ2.
      rewrite (iotaD_impl δ) //; apply indep_extend_consts.
      { move ⇒ i; rewrite mem_iota ⇒ /andP [LE1 LE2].
        ∃ 0 ⇒ ω; rewrite /nth_cost /task_job nth_default; first by reflexivity.
        apply: leq_trans; last by apply leqnn.
        by rewrite -EQ in LE1; apply LE1.
      }
      { by apply task_job_cost_independence_aux; rewrite -EQ. }
    }
    { by apply task_job_cost_independence_aux;
        rewrite addKn; apply: leq_trans; [apply ltnW, NEQ | rewrite leqnn].
    }
  Qed.

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))].
  Proof. by intros; apply task_job_cost_independence. Qed.

End NthCostLemmas.