Library probsa.rt.analysis.work_bound

From prosa.classic Require Export util.list.

From probsa.rt.analysis Require Export nth_cost arrivals completion_time.
From probsa.rt.model.assumptions Require Export pr_cost.

Section PrTaskWorkloadBoundedNthCost.

  Context {Ω} {μ : measure Ω}.

  Context {Task : TaskType}.
  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.
  Hypothesis H_arrival_sequence_uniq : pr_arrival_sequence_uniq.

  Variable tsk : Task.

  Lemma nth_cost_sum_monotone :
    ∀ (k : work) (n_small n_big : nat),
      (n_small ≤ n_big)%nat →
      ℙ <μ >{[ ∑[rv ]_{i < n_big } nth_cost tsk i ⟨<=⟩ k ]}
      ≤ ℙ <μ >{[ ∑[rv ]_{i < n_small } nth_cost tsk i ⟨<=⟩ k ]}.

We assume job costs are independent of the probabilistic arrival sequence.

  Hypothesis H_job_costs_independent_arr_seq :
    job_costs_independent_of_arrival_sequence.

  Let ξpart := partition_on_ξ μ : Ω_partition.
  Variable ξ : I ξpart.
  Context `{!PosProb μ (ξpart ◁{ξ })}.

  Lemma job_cost_sum_condition_arrival_seq :
    ∀ (k : work) (jobs : seq Job),
      ℙ <μ >{[ ∑[rv ]_{i <-jobs } odflt0 (job_cost i) ⟨<=⟩ k ]}
      = ℙ <μ >{[ ∑[rv ]_{i <-jobs } odflt0 (job_cost i) ⟨<=⟩ k | ξpart ◁{ξ } ]}.

Next, assume that job costs are IID.

  Hypothesis H_job_costs_independent : independent [seq job_cost j | j <- index_enum Job].
  Hypothesis H_job_costs_identically_distr :
    ∀ j1 j2, job_task j1 = job_task j2 → odflt0 (job_cost j1) ⪯ odflt0 (job_cost j2).

If at most n jobs of task tsk arrive in an interval [t1, t2) for arrival sequence ξ, then the probability that the sum of the first n job costs of tsk is at most k is less than or equal to the conditional probability that the actual workload in [t1, t2) is at most k.

Equivalently: the sum of nth_cost terms stochastically dominates (upper- bounds) the actual workload conditioned on arrival sequence ξ.

This inequality allows us to bound workload probabilities using a fixed-size sum of nth_cost terms, even though the actual number of arrivals is random.

  Lemma pr_workload_bounded_by_nth_cost_sum :
    ∀ (n : nat) (k : work) (t1 t2 : instant),
      (∀ ω, (ξpart ◁{ξ }) ω → size (pr_arrivals_task_between tsk t1 t2 ω) ≤ n)%nat →
      ℙ <μ >{[ ∑[rv ]_{i < n } nth_cost tsk i ⟨<=⟩ k ]}
      ≤ ℙ <μ >{[ pr_workload_of_task tsk t1 t2 ⟨<=⟩ k | ξpart ◁{ξ } ]}.
End PrTaskWorkloadBoundedNthCost.