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 ]}.
Proof.
intros × GE.
interval_to_duration n_small n_big δ.
apply pr_mono_pred ⇒ ω.
unfold "⟨<=⟩", rvar_nat_pred_leqop; apply leq_trans.
rewrite !sum_nrvar_sum_nat (big_nat_widen _ _ (n_small + δ)%nat); last by apply leq_addr.
by rewrite big_mkcondr //=; apply leq_sum ⇒ i _; destruct (_ < _)%nat.
Qed.
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 ]}.
Proof.
intros × GE.
interval_to_duration n_small n_big δ.
apply pr_mono_pred ⇒ ω.
unfold "⟨<=⟩", rvar_nat_pred_leqop; apply leq_trans.
rewrite !sum_nrvar_sum_nat (big_nat_widen _ _ (n_small + δ)%nat); last by apply leq_addr.
by rewrite big_mkcondr //=; apply leq_sum ⇒ i _; destruct (_ < _)%nat.
Qed.
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◁{ξ} ]}.
Proof.
intros; symmetry; apply pr_cond_indep2.
eapply indep2_fn_extl with (f := fun x ⇒ (x ≤ k)%nat).
{ by intros ? POSω; reflexivity. }
have EQ :
rvar_comp
(mkRvar μ (fun ω ⇒ [seq job_cost j ω | j <- jobs]))
(fun xs ⇒ \sum_(x <- xs) (odflt 0%nat x))
=1 ∑[rv]_{i<-jobs}odflt0 (job_cost i).
{ intros ω; induction jobs.
{ by rewrite //= !big_nil //=. }
{ by rewrite //= in IHjobs; rewrite //= !big_cons //= IHjobs. }
}
eapply indep2_fn_extl; first by intros; apply: EQ.
by apply H_job_costs_independent_arr_seq, PosProb0.
Qed.
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◁{ξ} ]}.
Proof.
intros; symmetry; apply pr_cond_indep2.
eapply indep2_fn_extl with (f := fun x ⇒ (x ≤ k)%nat).
{ by intros ? POSω; reflexivity. }
have EQ :
rvar_comp
(mkRvar μ (fun ω ⇒ [seq job_cost j ω | j <- jobs]))
(fun xs ⇒ \sum_(x <- xs) (odflt 0%nat x))
=1 ∑[rv]_{i<-jobs}odflt0 (job_cost i).
{ intros ω; induction jobs.
{ by rewrite //= !big_nil //=. }
{ by rewrite //= in IHjobs; rewrite //= !big_cons //= IHjobs. }
}
eapply indep2_fn_extl; first by intros; apply: EQ.
by apply H_job_costs_independent_arr_seq, PosProb0.
Qed.
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).
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
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.
[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.
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◁{ξ} ]}.
Proof.
intros × GE.
have [jobs EQ] := pr_arrivals_between_fixed_in_partition _ _ tsk _ t1 t2.
apply: Rle_trans; last first.
{ apply pr_cond_mono_pred ⇒ ω IN; apply leq_trans.
by simpl; rewrite /workload_of_jobs -big_filter EQ; [apply leqnn | apply IN].
}
apply: Rle_trans; last first.
{ apply pr_cond_mono_pred ⇒ ω IN; apply leq_trans.
by rewrite -(sum_nrvar_sum_nat (fun j ⇒ odflt0 (job_cost j)) jobs ω); apply leqnn.
}
have [s SIZE] : ∃ n, size jobs = n by (∃ (size jobs)).
replace (pr_cond _ _ _) with (ℙ<μ>{[ ∑[rv]_{ i <- jobs } odflt0 (job_cost i) ⟨<=⟩ k ]}); last first.
{ by apply job_cost_sum_condition_arrival_seq. }
move: (PosProb0) ⇒ EX; apply pr_pos_inv in EX; destruct EX as [ωp POSωp].
apply Rle_trans with (ℙ<μ>{[ ∑[rv]_{ i <- iota 0 s } nth_cost tsk i ⟨<=⟩ k ]}).
{ apply: Rle_trans.
{ apply nth_cost_sum_monotone with (n_small := s).
apply: leq_trans; last by apply GE, POSωp.
by rewrite -SIZE //= EQ; last apply POSωp.
}
{ apply pr_mono_pred ⇒ ω; apply leq_trans.
by rewrite !sum_nrvar_sum_nat /index_iota subn0; apply leq_sum.
}
}
apply Rge_le, sumrv_respects_stochastic_order.
{ apply: indep_irr; last eapply indep_comp.
{ by intros; reflexivity. }
apply: indep_subset; last by apply H_job_costs_independent.
{ by intros; rewrite mem_index_enum. }
{ rewrite -(EQ ωp); last by apply POSωp.
apply filter_uniq; apply: arrivals_uniq; eauto 2.
{ by apply pr_consistent_arrival_times; apply H_arrivals_consistent. }
{ by apply H_arrival_sequence_uniq. }
}
{ by apply index_enum_uniq. }
}
{ by apply task_job_cost_independence ⇒ //. }
{ by rewrite SIZE size_iota. }
{ intros; intros f; rewrite /nth_cost.
have [j EQU]: ∃ j, task_job tsk y = Some j.
{ destruct (task_job)eqn:EX; first by (∃ s0).
exfalso; unfold task_job in EX.
have LT : (y < size [seq Some j | j <- index_enum Job & job_of_task tsk j])%nat.
{ apply mem_zip in H; last by rewrite size_iota.
move: H ⇒ [_ ]; rewrite mem_iota add0n ⇒ /andP [_ LT].
rewrite -SIZE in LT; apply: leq_trans; first by apply LT.
rewrite -(EQ ωp); last by apply POSωp.
rewrite size_map; apply: subseq_leq_size.
{ rewrite filter_uniq //; apply: arrivals_uniq; eauto 2.
{ by apply pr_consistent_arrival_times. }
{ by apply H_arrival_sequence_uniq. }
}
{ intros j; rewrite mem_filter ⇒ /andP [TSK _].
rewrite mem_filter; apply/andP; split ⇒ //=.
by rewrite mem_index_enum.
}
}
apply (mem_nth None) in LT; move: LT; rewrite EX ⇒ /mapP2 [v IN EQU].
by inversion EQU.
}
rewrite EQU; apply H_job_costs_identically_distr.
apply mem_zip in H; destruct H.
{ rewrite -(EQ ωp (fst POSωp)) in H.
rewrite mem_filter in H.
move: H ⇒ /andP [TSK _].
apply nth_mem_o in EQU.
destruct EQU as [_ TSKj].
move: TSKj ⇒ /eqP. rewrite /concept.job_task ⇒ →.
by apply/eqP.
}
{ by rewrite SIZE size_iota. }
}
Qed.
End PrTaskWorkloadBoundedNthCost.
∀ (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◁{ξ} ]}.
Proof.
intros × GE.
have [jobs EQ] := pr_arrivals_between_fixed_in_partition _ _ tsk _ t1 t2.
apply: Rle_trans; last first.
{ apply pr_cond_mono_pred ⇒ ω IN; apply leq_trans.
by simpl; rewrite /workload_of_jobs -big_filter EQ; [apply leqnn | apply IN].
}
apply: Rle_trans; last first.
{ apply pr_cond_mono_pred ⇒ ω IN; apply leq_trans.
by rewrite -(sum_nrvar_sum_nat (fun j ⇒ odflt0 (job_cost j)) jobs ω); apply leqnn.
}
have [s SIZE] : ∃ n, size jobs = n by (∃ (size jobs)).
replace (pr_cond _ _ _) with (ℙ<μ>{[ ∑[rv]_{ i <- jobs } odflt0 (job_cost i) ⟨<=⟩ k ]}); last first.
{ by apply job_cost_sum_condition_arrival_seq. }
move: (PosProb0) ⇒ EX; apply pr_pos_inv in EX; destruct EX as [ωp POSωp].
apply Rle_trans with (ℙ<μ>{[ ∑[rv]_{ i <- iota 0 s } nth_cost tsk i ⟨<=⟩ k ]}).
{ apply: Rle_trans.
{ apply nth_cost_sum_monotone with (n_small := s).
apply: leq_trans; last by apply GE, POSωp.
by rewrite -SIZE //= EQ; last apply POSωp.
}
{ apply pr_mono_pred ⇒ ω; apply leq_trans.
by rewrite !sum_nrvar_sum_nat /index_iota subn0; apply leq_sum.
}
}
apply Rge_le, sumrv_respects_stochastic_order.
{ apply: indep_irr; last eapply indep_comp.
{ by intros; reflexivity. }
apply: indep_subset; last by apply H_job_costs_independent.
{ by intros; rewrite mem_index_enum. }
{ rewrite -(EQ ωp); last by apply POSωp.
apply filter_uniq; apply: arrivals_uniq; eauto 2.
{ by apply pr_consistent_arrival_times; apply H_arrivals_consistent. }
{ by apply H_arrival_sequence_uniq. }
}
{ by apply index_enum_uniq. }
}
{ by apply task_job_cost_independence ⇒ //. }
{ by rewrite SIZE size_iota. }
{ intros; intros f; rewrite /nth_cost.
have [j EQU]: ∃ j, task_job tsk y = Some j.
{ destruct (task_job)eqn:EX; first by (∃ s0).
exfalso; unfold task_job in EX.
have LT : (y < size [seq Some j | j <- index_enum Job & job_of_task tsk j])%nat.
{ apply mem_zip in H; last by rewrite size_iota.
move: H ⇒ [_ ]; rewrite mem_iota add0n ⇒ /andP [_ LT].
rewrite -SIZE in LT; apply: leq_trans; first by apply LT.
rewrite -(EQ ωp); last by apply POSωp.
rewrite size_map; apply: subseq_leq_size.
{ rewrite filter_uniq //; apply: arrivals_uniq; eauto 2.
{ by apply pr_consistent_arrival_times. }
{ by apply H_arrival_sequence_uniq. }
}
{ intros j; rewrite mem_filter ⇒ /andP [TSK _].
rewrite mem_filter; apply/andP; split ⇒ //=.
by rewrite mem_index_enum.
}
}
apply (mem_nth None) in LT; move: LT; rewrite EX ⇒ /mapP2 [v IN EQU].
by inversion EQU.
}
rewrite EQU; apply H_job_costs_identically_distr.
apply mem_zip in H; destruct H.
{ rewrite -(EQ ωp (fst POSωp)) in H.
rewrite mem_filter in H.
move: H ⇒ /andP [TSK _].
apply nth_mem_o in EQU.
destruct EQU as [_ TSKj].
move: TSKj ⇒ /eqP. rewrite /concept.job_task ⇒ →.
by apply/eqP.
}
{ by rewrite SIZE size_iota. }
}
Qed.
End PrTaskWorkloadBoundedNthCost.