Library probsa.rt.analysis.pRTA.pRTA
From probsa.util.prosa Require Export sporadic_as_curve.
From probsa.rt.model Require Export axiomatic_pWCET scheduler rt_monotonic pRBF assumptions.pr_cost.
From probsa.rt.analysis Require Export work_bound.
From probsa.rt.analysis.independent Require Export cost_and_workload task_workload.
From probsa.rt.model Require Export axiomatic_pWCET scheduler rt_monotonic pRBF assumptions.pr_cost.
From probsa.rt.analysis Require Export work_bound.
From probsa.rt.analysis.independent Require Export cost_and_workload task_workload.
TDFP ≤ WCA-TDFP
In this section, we prove that if the worst-case-arrival TDFP is bounded by a constant Λ, then TDFP is bounded by Λ as well.
Section WCATDFPtoTDFP.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{D : TaskDeadline Task}
{P : SporadicModel Task}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Variable h : instant.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{D : TaskDeadline Task}
{P : SporadicModel Task}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Variable h : instant.
Consider any scheduler.
Variable ζ : @scheduler𝗔𝗖 Job.
Let sched := @compute_pr_schedule Ω μ Job _ _ ζ.
Let 𝓡 j := response_time sched (Some h) j.
Variable ts : seq Task.
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
Variable j : Job.
Hypothesis H_job_of_task : job_of_task tsk j.
Variable Λ : R.
Hypothesis H_Λ_bounded : 0 ≤ Λ ≤ 1.
Let sched := @compute_pr_schedule Ω μ Job _ _ ζ.
Let 𝓡 j := response_time sched (Some h) j.
Variable ts : seq Task.
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
Variable j : Job.
Hypothesis H_job_of_task : job_of_task tsk j.
Variable Λ : R.
Hypothesis H_Λ_bounded : 0 ≤ Λ ≤ 1.
We assume that the TDFP is bounded by Λ for every possible arrival
sequence ξ. The conditioning on ξpart◁{ξ} represents fixing a specific
arrival pattern. Worst-case arrival (WCA-TDFP) means this bound holds for
all possible arrival patterns, not just on average.
Hypothesis H_WCA_TDFP_bounded :
let ξpart := partition_on_ξ μ in
∀ (ξ : I ξpart) (ρ : PosProb μ (ξpart◁{ξ})),
ℙ<μ,ρ>{[ D tsk ⟨<⟩ 𝓡 j | ξpart◁{ξ} ]} ≤ Λ.
let ξpart := partition_on_ξ μ in
∀ (ξ : I ξpart) (ρ : PosProb μ (ξpart◁{ξ})),
ℙ<μ,ρ>{[ D tsk ⟨<⟩ 𝓡 j | ξpart◁{ξ} ]} ≤ Λ.
If WCA-TDFP is bounded by Λ for every arrival sequence, then the
unconditional TDFP (averaging over all possible arrival sequences) is also
bounded by Λ. This holds because the unconditional probability is a
weighted average of the conditional probabilities, where each conditional
probability is at most Λ. Therefore, their average cannot exceed Λ.
Lemma WCA_TDFP_bounded_implies_TDFP_bounded :
ℙ<μ>{[ D tsk ⟨<⟩ 𝓡 j ]} ≤ Λ.
Proof.
set (ξpart := partition_on_ξ μ).
intros; rewrite -[Λ]Rmult_1_r -(pr_xpredT μ).
rewrite /cdf (law_of_total_probability_prod _ _ ξpart)
(law_of_total_probability_prod _ _ ξpart).
rewrite -bigop_inf.SeriesC_scal_l.
apply SeriesC_le; last first.
{ eapply ex_seriesC_le; last by eapply ex_series_pr_eq_over_partition.
intros ?; split.
- by apply Rmult_le_0_compat; [apply H_Λ_bounded | apply Rge_le, ge_pr_0].
- rewrite -[X in _ ≤ X]Rmult_1_l.
by apply Rmult_le_compat;
[ apply H_Λ_bounded
| apply Rge_le, ge_pr_0
| apply H_Λ_bounded
| apply pr_leq_intersectionr].
}
move ⇒ ξ; split; first by apply Rge_le, ge_pr_0.
have A : (∀ ω, ¬ ξpart◁{ξ} ω ∨ μ ω = 0)
∨ (∃ ω, ξpart◁{ξ} ω ∧ μ ω > 0).
{ destruct (ClassicalEpsilon.excluded_middle_informative
(∃ ω, p ξpart ξ ω ∧ μ ω > 0)).
- by right.
- left; move: n ⇒ /forallNP ALL.
intros ω; specialize (ALL ω); move: ALL ⇒ /not_andP [L|R]; first by left.
right; apply Rnot_gt_le in R.
have FE := @pmf_pos Ω μ ω.
by rewrite //=; nra.
}
destruct A as [ZERO | POS].
{ replace (pr _ _) with 0;
first by apply Rmult_le_0_compat; [apply H_Λ_bounded | apply Rge_le, ge_pr_0].
symmetry; apply SeriesC_0 ⇒ ω.
specialize (ZERO ω); destruct ZERO as [NP | Z].
- by rewrite /intersection /pred.pred_intersection;
move: NP ⇒ /negP NP; apply negbTE in NP; rewrite NP andb_false_r.
- by rewrite Z; case: (_ ∩ _ ).
}
destruct POS as [ω [INωξ POSμω]].
have POS: PosProb μ (ξpart◁{ξ}).
{ by eapply pr_pos; eauto. }
rewrite pr_cond_axiomatic' [X in _ ≤ X]Rmult_comm;
apply Rmult_le_compat; try apply Rge_le, ge_pr_0.
{ by apply pr_mono_pred ⇒ ω' IN; apply/andP; split. }
by apply: H_WCA_TDFP_bounded; eauto 1.
Qed.
End WCATDFPtoTDFP.
ℙ<μ>{[ D tsk ⟨<⟩ 𝓡 j ]} ≤ Λ.
Proof.
set (ξpart := partition_on_ξ μ).
intros; rewrite -[Λ]Rmult_1_r -(pr_xpredT μ).
rewrite /cdf (law_of_total_probability_prod _ _ ξpart)
(law_of_total_probability_prod _ _ ξpart).
rewrite -bigop_inf.SeriesC_scal_l.
apply SeriesC_le; last first.
{ eapply ex_seriesC_le; last by eapply ex_series_pr_eq_over_partition.
intros ?; split.
- by apply Rmult_le_0_compat; [apply H_Λ_bounded | apply Rge_le, ge_pr_0].
- rewrite -[X in _ ≤ X]Rmult_1_l.
by apply Rmult_le_compat;
[ apply H_Λ_bounded
| apply Rge_le, ge_pr_0
| apply H_Λ_bounded
| apply pr_leq_intersectionr].
}
move ⇒ ξ; split; first by apply Rge_le, ge_pr_0.
have A : (∀ ω, ¬ ξpart◁{ξ} ω ∨ μ ω = 0)
∨ (∃ ω, ξpart◁{ξ} ω ∧ μ ω > 0).
{ destruct (ClassicalEpsilon.excluded_middle_informative
(∃ ω, p ξpart ξ ω ∧ μ ω > 0)).
- by right.
- left; move: n ⇒ /forallNP ALL.
intros ω; specialize (ALL ω); move: ALL ⇒ /not_andP [L|R]; first by left.
right; apply Rnot_gt_le in R.
have FE := @pmf_pos Ω μ ω.
by rewrite //=; nra.
}
destruct A as [ZERO | POS].
{ replace (pr _ _) with 0;
first by apply Rmult_le_0_compat; [apply H_Λ_bounded | apply Rge_le, ge_pr_0].
symmetry; apply SeriesC_0 ⇒ ω.
specialize (ZERO ω); destruct ZERO as [NP | Z].
- by rewrite /intersection /pred.pred_intersection;
move: NP ⇒ /negP NP; apply negbTE in NP; rewrite NP andb_false_r.
- by rewrite Z; case: (_ ∩ _ ).
}
destruct POS as [ω [INωξ POSμω]].
have POS: PosProb μ (ξpart◁{ξ}).
{ by eapply pr_pos; eauto. }
rewrite pr_cond_axiomatic' [X in _ ≤ X]Rmult_comm;
apply Rmult_le_compat; try apply Rge_le, ge_pr_0.
{ by apply pr_mono_pred ⇒ ω' IN; apply/andP; split. }
by apply: H_WCA_TDFP_bounded; eauto 1.
Qed.
End WCATDFPtoTDFP.
Section TDFPBound.
Context {Task : TaskType}
{pWCET_pmf : ProbWCET Task}
{D : TaskDeadline Task}
{T : SporadicModel Task}
{FP : FP_policy Task}.
Variables (ts : seq Task) (tsk : Task).
Context {Task : TaskType}
{pWCET_pmf : ProbWCET Task}
{D : TaskDeadline Task}
{T : SporadicModel Task}
{FP : FP_policy Task}.
Variables (ts : seq Task) (tsk : Task).
The interference distribution for task tsk in an interval of length t
is the convolution of workload distributions from all tasks with
higher-or-equal priority to tsk, excluding tsk itself. Each task
tsko contributes workload over the interval t + D tsko.
Definition interference_distrib (t : nat) : distrib [countType of nat] :=
⨁_{tsko <- ts | (hep_task tsko tsk) && (tsko != tsk)}
pRBF tsko (t + D tsko)%nat.
⨁_{tsko <- ts | (hep_task tsko tsk) && (tsko != tsk)}
pRBF tsko (t + D tsko)%nat.
The total demand distribution in an interval of length t combines the
job's own cost with interference from higher-or-equal priority tasks.
Definition demand_distrib (t : nat) : distrib [countType of nat] :=
to_distrib pWCET_pmf tsk ⊕ interference_distrib t.
to_distrib pWCET_pmf tsk ⊕ interference_distrib t.
The TDFP bound Λ is the minimum probability, over all interval lengths
t ∈ [1, D tsk], that the total workload of higher-or-equal priority jobs
exceeds the length t of the interval.
The key insight: ℙ{demand_distrib t > t} gives the probability that
workload generated in an interval of length t exceeds t itself,
meaning the work cannot be completed within the interval. Taking the
minimum over all t identifies the interval length where the workload is
most likely to be consumed, thereby providing an upper bound on the
deadline miss probability.
Definition Λ : R :=
min1 [ seq ℙ<demand_distrib t>{[ltn t]}
| t <- index_iota 1 (D tsk + 1) ].
Remark lims_Λ : 0 ≤ Λ ≤ 1.
Proof.
split; last by apply seq_ext.foldl_Rmin.
have Re : ∀ xs d, 0 ≤ d → (∀ x, x \in xs → 0 ≤ x) → 0 ≤ foldl Rmin d xs.
{ clear; induction xs; intros × POSd POS.
{ by apply POSd. }
{ apply IHxs.
{ apply Rmin_glb ⇒ //.
by apply POS; rewrite in_cons eq_refl orTb. }
{ by intros; apply POS; rewrite in_cons; apply/orP; right. }
}
}
apply Re; try apply Rle_0_1.
move ⇒ p /mapP2 [idx IN EQ]; subst p.
by apply Rge_le, ge_pr_0.
Qed.
End TDFPBound.
min1 [ seq ℙ<demand_distrib t>{[ltn t]}
| t <- index_iota 1 (D tsk + 1) ].
Remark lims_Λ : 0 ≤ Λ ≤ 1.
Proof.
split; last by apply seq_ext.foldl_Rmin.
have Re : ∀ xs d, 0 ≤ d → (∀ x, x \in xs → 0 ≤ x) → 0 ≤ foldl Rmin d xs.
{ clear; induction xs; intros × POSd POS.
{ by apply POSd. }
{ apply IHxs.
{ apply Rmin_glb ⇒ //.
by apply POS; rewrite in_cons eq_refl orTb. }
{ by intros; apply POS; rewrite in_cons; apply/orP; right. }
}
}
apply Re; try apply Rle_0_1.
move ⇒ p /mapP2 [idx IN EQ]; subst p.
by apply Rge_le, ge_pr_0.
Qed.
End TDFPBound.
Step-by-Step Proof of Probabilistic Response-Time Analysis: TDFP Bound
Section TDFPIsBounded.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{pWCET_pmf : ProbWCET Task}
{D : TaskDeadline Task}
{T : SporadicModel Task}
{FP : FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive hep_task.
Hypothesis H_transitive_priorities : transitive hep_task.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{pWCET_pmf : ProbWCET Task}
{D : TaskDeadline Task}
{T : SporadicModel Task}
{FP : FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive hep_task.
Hypothesis H_transitive_priorities : transitive hep_task.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Let us assume that the pWCET is axiomatic.
Assume the system terminates at some distant time h.
Variable h : instant.
Hypothesis H_horizon_far_enough :
∀ (j : Job) (ω : Ω), (odflt0 (job_deadline j) ω < h)%nat.
Hypothesis H_horizon_far_enough :
∀ (j : Job) (ω : Ω), (odflt0 (job_deadline j) ω < h)%nat.
Consider a scheduler ...
Variable ζ : @scheduler𝗔𝗖 Job.
Let sched := @compute_pr_schedule Ω μ Job _ _ ζ.
Let 𝓡 j := response_time sched (Some h) j.
Let sched := @compute_pr_schedule Ω μ Job _ _ ζ.
Let 𝓡 j := response_time sched (Some h) j.
... and assume that it is work conserving and respects the FP-FP policy.
Hypothesis H_work_conserving : pr_work_conserving sched pr_abort_ready_instance.
Hypothesis H_respects_policy_at_preemption_point :
pr_respects_policy_at_preemption_point sched pr_abort_ready_instance fully_preemptive_model.
Hypothesis H_jobs_come_from_arrival_sequence : pr_jobs_come_from_arrival_sequence sched.
Hypothesis H_completed_jobs_dont_execute : pr_completed_jobs_dont_execute sched.
Hypothesis H_jobs_must_arrive_to_execute : pr_jobs_must_arrive_to_execute sched.
Hypothesis H_jobs_must_be_ready_to_execute :
pr_jobs_must_be_ready_to_execute sched pr_abort_ready_instance.
Variable ts : seq Task.
Hypothesis H_ts_uniq : uniq ts.
Hypothesis H_jobs_from_ts : ∀ (j : Job), job_task j \in ts.
Hypothesis H_arrivals_and_costs_consistent : arrivals_cost_consistent.
Hypothesis H_arrivals_from_ts : arrivals_from_task_set ts.
Hypothesis H_sporadic_arrivals : pr_taskset_respects_sporadic_task_model ts.
Hypothesis H_task_min_inter_arrival_time_valid : valid_taskset_inter_arrival_times ts.
Hypothesis H_constrained_deadlines : constrained_deadlines ts.
Hypothesis H_respects_policy_at_preemption_point :
pr_respects_policy_at_preemption_point sched pr_abort_ready_instance fully_preemptive_model.
Hypothesis H_jobs_come_from_arrival_sequence : pr_jobs_come_from_arrival_sequence sched.
Hypothesis H_completed_jobs_dont_execute : pr_completed_jobs_dont_execute sched.
Hypothesis H_jobs_must_arrive_to_execute : pr_jobs_must_arrive_to_execute sched.
Hypothesis H_jobs_must_be_ready_to_execute :
pr_jobs_must_be_ready_to_execute sched pr_abort_ready_instance.
Variable ts : seq Task.
Hypothesis H_ts_uniq : uniq ts.
Hypothesis H_jobs_from_ts : ∀ (j : Job), job_task j \in ts.
Hypothesis H_arrivals_and_costs_consistent : arrivals_cost_consistent.
Hypothesis H_arrivals_from_ts : arrivals_from_task_set ts.
Hypothesis H_sporadic_arrivals : pr_taskset_respects_sporadic_task_model ts.
Hypothesis H_task_min_inter_arrival_time_valid : valid_taskset_inter_arrival_times ts.
Hypothesis H_constrained_deadlines : constrained_deadlines ts.
The sporadic task model implies that the task set respects arrival curves.
Local Remark respects_arrival_curve :
∀ ω,
taskset_respects_max_arrivals (arr_seq ω) ts.
Proof.
intros.
apply: sporadic_task_sets_respects_max_arrivals.
{ split.
{ by apply pr_consistent_arrival_times. }
{ by intros ?; apply arr_seq_uniq. }
}
{ by apply H_task_min_inter_arrival_time_valid. }
{ by apply H_sporadic_arrivals. }
Qed.
Local Remark valid_arrival_curve :
valid_taskset_arrival_curve ts max_arrivals.
Proof.
by apply sporadic_task_sets_arrival_curve_valid.
Qed.
∀ ω,
taskset_respects_max_arrivals (arr_seq ω) ts.
Proof.
intros.
apply: sporadic_task_sets_respects_max_arrivals.
{ split.
{ by apply pr_consistent_arrival_times. }
{ by intros ?; apply arr_seq_uniq. }
}
{ by apply H_task_min_inter_arrival_time_valid. }
{ by apply H_sporadic_arrivals. }
Qed.
Local Remark valid_arrival_curve :
valid_taskset_arrival_curve ts max_arrivals.
Proof.
by apply sporadic_task_sets_arrival_curve_valid.
Qed.
In this proof, we assume the job cost properties established by the
axiomatic-pWCET transformation.
Hypothesis H_job_costs_independent : job_costs_independent.
Hypothesis H_job_costs_bounded_by_pWCET : job_costs_bounded_by_pWCET.
Hypothesis H_job_costs_identically_distr : job_costs_identically_distributed.
Hypothesis H_job_costs_independent_cond_arr_seq : job_costs_independent_cond_arr_seq.
Hypothesis H_job_costs_independent_arr_seq : job_costs_independent_of_arrival_sequence.
Hypothesis H_conditional_cost_bounded_by_pWCET : conditional_cost_bounded_by_pWCET.
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
Variable j : Job.
Hypothesis H_job_of_task : job_of_task tsk j.
Hypothesis H_job_costs_bounded_by_pWCET : job_costs_bounded_by_pWCET.
Hypothesis H_job_costs_identically_distr : job_costs_identically_distributed.
Hypothesis H_job_costs_independent_cond_arr_seq : job_costs_independent_cond_arr_seq.
Hypothesis H_job_costs_independent_arr_seq : job_costs_independent_of_arrival_sequence.
Hypothesis H_conditional_cost_bounded_by_pWCET : conditional_cost_bounded_by_pWCET.
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
Variable j : Job.
Hypothesis H_job_of_task : job_of_task tsk j.
Step-by-Step Proof Sketch
Section StepByStep.
Let ξpart := partition_on_ξ μ : Ω_partition.
Let V := pr_carry_in_workload_of_hep_jobs sched tsk : instant → rvar μ [eqType of work].
Let ξpart := partition_on_ξ μ : Ω_partition.
Let V := pr_carry_in_workload_of_hep_jobs sched tsk : instant → rvar μ [eqType of work].
Consider an arbitrary arrival sequence that has positive probability.
Step 1: Handle the case where job j doesn't arrive.
Local Lemma job_either_arrives_or_not :
(∀ ω, (ξpart◁{ξ}) ω → job_arrival j ω = None)
∨ (∃ A, ∀ ω, (ξpart◁{ξ}) ω → job_arrival j ω = Some A).
Proof.
move: (pr_pos_inv _ ρ) ⇒ [ω [INωξ FE]].
{ destruct (job_arrival j ω) as [A | ] eqn:EQ; last first.
{ left ⇒ ωo INωoξ.
inversion INωξ as [IN1]; inversion INωoξ as [IN2].
move: IN1 IN2 ⇒ /eqP <- /eqP EQξ.
rewrite -EQ; eapply eq_arr_seq_impl_eq_job_arrival.
by move ⇒ t; rewrite EQξ.
}
{ right; ∃ A ⇒ ωo INωoξ.
inversion INωξ as [IN1]; inversion INωoξ as [IN2].
move: IN1 IN2 ⇒ /eqP <- /eqP EQξ.
rewrite -EQ; eapply eq_arr_seq_impl_eq_job_arrival.
by move ⇒ t; rewrite EQξ.
}
}
Qed.
(∀ ω, (ξpart◁{ξ}) ω → job_arrival j ω = None)
∨ (∃ A, ∀ ω, (ξpart◁{ξ}) ω → job_arrival j ω = Some A).
Proof.
move: (pr_pos_inv _ ρ) ⇒ [ω [INωξ FE]].
{ destruct (job_arrival j ω) as [A | ] eqn:EQ; last first.
{ left ⇒ ωo INωoξ.
inversion INωξ as [IN1]; inversion INωoξ as [IN2].
move: IN1 IN2 ⇒ /eqP <- /eqP EQξ.
rewrite -EQ; eapply eq_arr_seq_impl_eq_job_arrival.
by move ⇒ t; rewrite EQξ.
}
{ right; ∃ A ⇒ ωo INωoξ.
inversion INωξ as [IN1]; inversion INωoξ as [IN2].
move: IN1 IN2 ⇒ /eqP <- /eqP EQξ.
rewrite -EQ; eapply eq_arr_seq_impl_eq_job_arrival.
by move ⇒ t; rewrite EQξ.
}
}
Qed.
If job j doesn't arrive in arrival sequence ξ, then the conditional
TDFP is 0 (no deadline to miss).
Lemma tdfp_zero_when_job_does_not_arrive :
(∀ ω, (ξpart◁{ξ}) ω → job_arrival j ω = None) →
ℙ<μ>{[ D tsk ⟨<⟩ response_time (compute_pr_schedule ζ) (Some h) j | ξpart◁{ξ} ]} = 0.
Proof.
intros ZERO; eapply pr_cond_eq_pred_0 ⇒ ωo IN.
unfold 𝓡, response_time, "⟨<⟩", dominance_relation.nat_etimervar_pred_ltop.
by rewrite //= ZERO //.
Qed.
(∀ ω, (ξpart◁{ξ}) ω → job_arrival j ω = None) →
ℙ<μ>{[ D tsk ⟨<⟩ response_time (compute_pr_schedule ζ) (Some h) j | ξpart◁{ξ} ]} = 0.
Proof.
intros ZERO; eapply pr_cond_eq_pred_0 ⇒ ωo IN.
unfold 𝓡, response_time, "⟨<⟩", dominance_relation.nat_etimervar_pred_ltop.
by rewrite //= ZERO //.
Qed.
Step 2: Relate deadline miss to workload demand
Variable ω : Ω.
Hypothesis H_ω_in_ξ : ξpart◁{ξ} ω.
Variable A : nat.
Hypothesis H_job_arrives_at :
∀ ω, ξpart◁{ξ} ω → job_arrival j ω = Some A.
Hypothesis H_ω_in_ξ : ξpart◁{ξ} ω.
Variable A : nat.
Hypothesis H_job_arrives_at :
∀ ω, ξpart◁{ξ} ω → job_arrival j ω = Some A.
We consider interval lengths from 1 to the task deadline.
Next, we define a predicate that is true iff the workload demand exceeds
available time in an interval of length Δ in an evolution ω.
Let workload_exceeds_time (ω : Ω) (Δ : duration) :=
(V A ω + pr_workload_of_hep_tasks tsk A (A + Δ) ω > Δ)%nat.
(V A ω + pr_workload_of_hep_tasks tsk A (A + Δ) ω > Δ)%nat.
We prove a probabilistic version of an intuitive statement: if the
response time exceeds the deadline, then workload demand must exceed the
available time in ALL intervals of length Δ ∈ [1, D tsk].
Lemma deadline_miss_implies_workload_exceeds_time :
ℙ<μ>{[ D tsk ⟨<⟩ 𝓡 j | ξpart◁{ξ} ]}
≤ ℙ<μ>{[ λ ω, all (workload_exceeds_time ω) lengths | ξpart◁{ξ} ]}.
Proof.
apply pr_cond_mono_pred ⇒ ωo INξ LT.
apply/allP ⇒ t; rewrite mem_index_iota ⇒ IN //=.
unfold workload_exceeds_time; move_neq_up LE; rewrite addn1 ltnS in IN.
eapply completion_time_exists in LE; first last; try by done.
{ by ssrlia. }
{ by apply arr_seq_consistent. }
move: LE ⇒ [δ [NEQ EQ]]; specialize (EQ j).
feed_n 3%nat EQ.
{ by move: H_job_of_task ⇒ /eqP <-; apply H_priority_is_reflexive. }
{ by apply H_job_arrives_at. }
{ rewrite /job_deadline //= H_job_arrives_at //= leq_add2l.
move: H_job_of_task ⇒ /eqP →.
move: IN ⇒ /andP [_ ]; move: NEQ ⇒ /andP [_ ].
by clear; intros; eapply leq_trans; eauto 1. }
move: LT; unfold 𝓡, response_time, "⟨<⟩", nat_etimervar_pred_ltop; rewrite //= H_job_arrives_at //=.
destruct (min_completion_time sched ωo j) eqn:CT; last first.
{ by exfalso; eapply n; apply EQ. }
{ move: s CT ⇒ [tmin [COMP NCOMP]] _ EXC.
have TMIN : (tmin ≤ A + δ)%nat by move_neq_up GT; eapply NCOMP; [ | apply EQ]; ssrlia.
have F : (h ≤ tmin)%N = false.
{ apply/negP ⇒ NEGP; move: (H_horizon_far_enough j ω) ⇒ BIG.
move_neq_down BIG.
eapply leq_trans; first apply NEGP.
eapply leq_trans; first apply TMIN.
rewrite //= H_job_arrives_at //= leq_add2l; move: NEQ ⇒ /andP [_ NEQ].
eapply leq_trans; first apply NEQ.
move: IN ⇒ /andP [_ IN]; eapply leq_trans; first apply IN.
by move: H_job_of_task ⇒ /eqP →.
}
move: EXC; rewrite F /exceeds ⇒ EXC.
by move_neq_down EXC; ssrlia.
}
Qed.
ℙ<μ>{[ D tsk ⟨<⟩ 𝓡 j | ξpart◁{ξ} ]}
≤ ℙ<μ>{[ λ ω, all (workload_exceeds_time ω) lengths | ξpart◁{ξ} ]}.
Proof.
apply pr_cond_mono_pred ⇒ ωo INξ LT.
apply/allP ⇒ t; rewrite mem_index_iota ⇒ IN //=.
unfold workload_exceeds_time; move_neq_up LE; rewrite addn1 ltnS in IN.
eapply completion_time_exists in LE; first last; try by done.
{ by ssrlia. }
{ by apply arr_seq_consistent. }
move: LE ⇒ [δ [NEQ EQ]]; specialize (EQ j).
feed_n 3%nat EQ.
{ by move: H_job_of_task ⇒ /eqP <-; apply H_priority_is_reflexive. }
{ by apply H_job_arrives_at. }
{ rewrite /job_deadline //= H_job_arrives_at //= leq_add2l.
move: H_job_of_task ⇒ /eqP →.
move: IN ⇒ /andP [_ ]; move: NEQ ⇒ /andP [_ ].
by clear; intros; eapply leq_trans; eauto 1. }
move: LT; unfold 𝓡, response_time, "⟨<⟩", nat_etimervar_pred_ltop; rewrite //= H_job_arrives_at //=.
destruct (min_completion_time sched ωo j) eqn:CT; last first.
{ by exfalso; eapply n; apply EQ. }
{ move: s CT ⇒ [tmin [COMP NCOMP]] _ EXC.
have TMIN : (tmin ≤ A + δ)%nat by move_neq_up GT; eapply NCOMP; [ | apply EQ]; ssrlia.
have F : (h ≤ tmin)%N = false.
{ apply/negP ⇒ NEGP; move: (H_horizon_far_enough j ω) ⇒ BIG.
move_neq_down BIG.
eapply leq_trans; first apply NEGP.
eapply leq_trans; first apply TMIN.
rewrite //= H_job_arrives_at //= leq_add2l; move: NEQ ⇒ /andP [_ NEQ].
eapply leq_trans; first apply NEQ.
move: IN ⇒ /andP [_ IN]; eapply leq_trans; first apply IN.
by move: H_job_of_task ⇒ /eqP →.
}
move: EXC; rewrite F /exceeds ⇒ EXC.
by move_neq_down EXC; ssrlia.
}
Qed.
By Fréchet's inequality, the probability that workload exceeds time in
ALL intervals is bounded by the minimum probability across
intervals. This allows us to focus on a single interval length at a
time.
Lemma frechet_bound_on_all_intervals :
ℙ<μ>{[ λ ω, all (workload_exceeds_time ω) lengths | ξpart◁{ξ} ]}
≤ min1 [
seq ℙ<μ>{[ λ ω, workload_exceeds_time ω t | ξpart◁{ξ} ]}
| t <- lengths].
Proof.
by apply frechet_min.
Qed.
ℙ<μ>{[ λ ω, all (workload_exceeds_time ω) lengths | ξpart◁{ξ} ]}
≤ min1 [
seq ℙ<μ>{[ λ ω, workload_exceeds_time ω t | ξpart◁{ξ} ]}
| t <- lengths].
Proof.
by apply frechet_min.
Qed.
Step 3: Bound workload for a single interval
Define random variables for the workload components (conditioned on ξ)...
Let interfering_workload :=
mkRvar
(restrict μ (ξpart◁{ξ}))
(fun ω ⇒
\sum_(tsko <- ts | (hep_task tsko tsk) && (tsko != tsk))
pr_workload_of_task (μ := μ) tsko (A - D tsko) (A + Δ) ω
).
mkRvar
(restrict μ (ξpart◁{ξ}))
(fun ω ⇒
\sum_(tsko <- ts | (hep_task tsko tsk) && (tsko != tsk))
pr_workload_of_task (μ := μ) tsko (A - D tsko) (A + Δ) ω
).
Let cond_cost_j :=
mkRvar (restrict μ (ξpart◁{ξ})) (fun ω ⇒ odflt0 (job_cost j) ω).
Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.
Hypothesis H_arrivals_unique : pr_arrival_sequence_uniq.
mkRvar (restrict μ (ξpart◁{ξ})) (fun ω ⇒ odflt0 (job_cost j) ω).
Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.
Hypothesis H_arrivals_unique : pr_arrival_sequence_uniq.
The probability that the total workload exceeds Δ is bounded by the
probability that the sum of job j's cost and interference exceeds Δ.
This uses the carry-in workload decomposition and properties of the
abort-ready model (at most one job of each task is pending).
Lemma workload_bounded_by_cost_plus_interference :
ℙ<μ>{[ λ ω, workload_exceeds_time ω Δ | ξpart◁{ξ} ]}
≤ ℙ<μ>{[ λ ω, (Δ < cond_cost_j ω + interfering_workload ω)%nat | ξpart◁{ξ} ]}.
Proof.
apply pr_cond_mono_pred ⇒ ωo INωo LE.
apply: leq_trans; first by apply LE.
unfold cond_cost_j, interfering_workload in × ⇒ //=.
erewrite eq_bigr; last first.
{ intros; apply pr_workload_of_task_cat with (t := A).
by apply/andP; split; [rewrite leq_subr // | rewrite leq_addr]. }
rewrite big_split //= [X in (_ ≤ X)%nat]addnC -addnA leq_add //.
{ eapply leq_trans; first by apply pr_hep_carry_in_workload_split, H_arrivals_from_ts.
have → :
(\sum_(tsko <- ts | hep_task tsko tsk) pr_carry_in_workload_of_task sched tsko A ωo
= pr_carry_in_workload_of_task sched tsk A ωo
+ \sum_(tsko <- ts | hep_task tsko tsk && (tsko != tsk))
pr_carry_in_workload_of_task sched tsko A ωo)%nat
by erewrite bigD1_seq_pred; eauto 2.
rewrite -[\sum_(i <- ts | _) pr_workload_of_task _ _ _ _ ]add0n.
rewrite leq_add //.
{ by erewrite no_carry_in_at_task_arrival; eauto 2. }
{ rewrite big_seq_cond [in X in (_ ≤ X)%nat]big_seq_cond.
rewrite leq_sum // ⇒ tsko /andP [INo /andP [HEP NEQ]].
by apply: pr_carry_in_workload_bounded_pr_pend_workload; eauto 1.
}
}
{ apply: leq_trans.
{ by apply pr_hep_workload_pr_task_workload_split ⇒ //; eauto 2. }
{ erewrite bigD1_seq_pred ⇒ //=; rewrite addnC //= leq_add //=.
apply: at_most_one_job_pending; eauto 2; last first.
{ by move: H_Δ_in_range ⇒ /andP [_ LT]; rewrite addn1 ltnS in LT. }
∃ A; inversion H_ω_in_ξ as [IN1]; inversion INωo as [IN2].
by move: IN1 IN2 ⇒ /eqP <- /eqP ->; apply arr_seq_consistent; apply H_job_arrives_at.
}
}
Qed.
ℙ<μ>{[ λ ω, workload_exceeds_time ω Δ | ξpart◁{ξ} ]}
≤ ℙ<μ>{[ λ ω, (Δ < cond_cost_j ω + interfering_workload ω)%nat | ξpart◁{ξ} ]}.
Proof.
apply pr_cond_mono_pred ⇒ ωo INωo LE.
apply: leq_trans; first by apply LE.
unfold cond_cost_j, interfering_workload in × ⇒ //=.
erewrite eq_bigr; last first.
{ intros; apply pr_workload_of_task_cat with (t := A).
by apply/andP; split; [rewrite leq_subr // | rewrite leq_addr]. }
rewrite big_split //= [X in (_ ≤ X)%nat]addnC -addnA leq_add //.
{ eapply leq_trans; first by apply pr_hep_carry_in_workload_split, H_arrivals_from_ts.
have → :
(\sum_(tsko <- ts | hep_task tsko tsk) pr_carry_in_workload_of_task sched tsko A ωo
= pr_carry_in_workload_of_task sched tsk A ωo
+ \sum_(tsko <- ts | hep_task tsko tsk && (tsko != tsk))
pr_carry_in_workload_of_task sched tsko A ωo)%nat
by erewrite bigD1_seq_pred; eauto 2.
rewrite -[\sum_(i <- ts | _) pr_workload_of_task _ _ _ _ ]add0n.
rewrite leq_add //.
{ by erewrite no_carry_in_at_task_arrival; eauto 2. }
{ rewrite big_seq_cond [in X in (_ ≤ X)%nat]big_seq_cond.
rewrite leq_sum // ⇒ tsko /andP [INo /andP [HEP NEQ]].
by apply: pr_carry_in_workload_bounded_pr_pend_workload; eauto 1.
}
}
{ apply: leq_trans.
{ by apply pr_hep_workload_pr_task_workload_split ⇒ //; eauto 2. }
{ erewrite bigD1_seq_pred ⇒ //=; rewrite addnC //= leq_add //=.
apply: at_most_one_job_pending; eauto 2; last first.
{ by move: H_Δ_in_range ⇒ /andP [_ LT]; rewrite addn1 ltnS in LT. }
∃ A; inversion H_ω_in_ξ as [IN1]; inversion INωo as [IN2].
by move: IN1 IN2 ⇒ /eqP <- /eqP ->; apply arr_seq_consistent; apply H_job_arrives_at.
}
}
Qed.
Define workload random variable for a single higher-priority task.
Let task_workload : Task → rvar (restrict μ (ξpart◁{ξ})) [eqType of work] :=
λ tsko,
mkRvar (restrict μ (ξpart◁{ξ}))
[eta pr_workload_of_task tsko (A - D tsko)%N (A + Δ)%N].
λ tsko,
mkRvar (restrict μ (ξpart◁{ξ}))
[eta pr_workload_of_task tsko (A - D tsko)%N (A + Δ)%N].
The sum of task workloads (as random variables) stochastically dominates
the interference workload (monotonicity of sums).
Lemma interference_bounded_by_task_workload_sum :
interfering_workload
⪯ ∑[rv]_{tsko <- ts| hep_task tsko tsk && (tsko != tsk)} task_workload tsko .
Proof.
intros k ⇒ //=.
apply Rle_ge, pr_mono_pred ⇒ ωo; apply leq_trans ⇒ //=.
clear H_tsk_in_ts interfering_workload H_ts_uniq H_arrivals_from_ts H_jobs_from_ts.
clear H_sporadic_arrivals H_constrained_deadlines H_task_min_inter_arrival_time_valid .
induction ts; first by rewrite !big_nil //=.
rewrite !big_cons //=; case: (hep_task a tsk && (a != tsk)).
rewrite leq_add ⇒ //.
by apply IHl.
Qed.
interfering_workload
⪯ ∑[rv]_{tsko <- ts| hep_task tsko tsk && (tsko != tsk)} task_workload tsko .
Proof.
intros k ⇒ //=.
apply Rle_ge, pr_mono_pred ⇒ ωo; apply leq_trans ⇒ //=.
clear H_tsk_in_ts interfering_workload H_ts_uniq H_arrivals_from_ts H_jobs_from_ts.
clear H_sporadic_arrivals H_constrained_deadlines H_task_min_inter_arrival_time_valid .
induction ts; first by rewrite !big_nil //=.
rewrite !big_cons //=; case: (hep_task a tsk && (a != tsk)).
rewrite leq_add ⇒ //.
by apply IHl.
Qed.
Step 4: Bound each task's workload by a sum of job costs
Variable tsko : Task.
Hypothesis H_tsko_in_ts : tsko \in ts.
Hypothesis H_tsko_hep : hep_task tsko tsk.
Hypothesis H_neq : tsko != tsk.
Hypothesis H_tsko_in_ts : tsko \in ts.
Hypothesis H_tsko_hep : hep_task tsko tsk.
Hypothesis H_neq : tsko != tsk.
Task workload is bounded by the sum of nth_cost over the maximum
number of arrivals in the interval (given by the arrival curve).
Lemma task_workload_bounded_by_nth_cost_sum :
task_workload tsko
⪯ ∑[rv]_{i < max_arrivals tsko (Δ + D tsko)%nat} nth_cost tsko i.
Proof.
move ⇒ k.
have EQj :
ℙ<μ>{[ task_workload tsko ⟨<=⟩ k | ξpart◁{ξ} ]}
= ℙ<μ>{[ pr_workload_of_task tsko (A - D tsko)%nat (A + Δ)%nat ⟨<=⟩ k | ξpart◁{ξ} ]}.
{ by apply pr_cond_eq_pred ⇒ ω' INωξ'; reflexivity. }
have EX :
∃ n, ∀ ω,
ξpart◁{ξ} ω →
size (pr_arrivals_task_between tsko (A - D tsko)%nat (A + Δ)%nat ω)
= n.
{
∃ (size (pr_arrivals_task_between tsko (A - D tsko)%nat (A + Δ)%nat ω)).
move ⇒ ω1 IN1; f_equal.
by apply: pr_arrivals_task_between_eq; eauto 2.
}
edestruct EX as [n EQ] ⇒ //.
rewrite /cdf fold_prob_to_cond_prob /task_workload.
apply Rle_ge, Rle_trans with (r2 := ℙ<μ>{[ ∑[rv]_{i < n} nth_cost tsko i ⟨<=⟩ k ]}).
{ apply: nth_cost_sum_monotone; erewrite <-EQ; eauto 1.
apply: leq_trans.
{ apply: pr_arrivals_task_between_respect_arrival_curve_mid ⇒ //.
{ by apply H_tsko_in_ts. }
{ by apply respects_arrival_curve. }
{ by apply valid_arrival_curve. }
}
{ by rewrite addnC. }
}
{ rewrite EQj; apply: pr_workload_bounded_by_nth_cost_sum; eauto 1.
by intros; rewrite EQ.
}
Qed.
task_workload tsko
⪯ ∑[rv]_{i < max_arrivals tsko (Δ + D tsko)%nat} nth_cost tsko i.
Proof.
move ⇒ k.
have EQj :
ℙ<μ>{[ task_workload tsko ⟨<=⟩ k | ξpart◁{ξ} ]}
= ℙ<μ>{[ pr_workload_of_task tsko (A - D tsko)%nat (A + Δ)%nat ⟨<=⟩ k | ξpart◁{ξ} ]}.
{ by apply pr_cond_eq_pred ⇒ ω' INωξ'; reflexivity. }
have EX :
∃ n, ∀ ω,
ξpart◁{ξ} ω →
size (pr_arrivals_task_between tsko (A - D tsko)%nat (A + Δ)%nat ω)
= n.
{
∃ (size (pr_arrivals_task_between tsko (A - D tsko)%nat (A + Δ)%nat ω)).
move ⇒ ω1 IN1; f_equal.
by apply: pr_arrivals_task_between_eq; eauto 2.
}
edestruct EX as [n EQ] ⇒ //.
rewrite /cdf fold_prob_to_cond_prob /task_workload.
apply Rle_ge, Rle_trans with (r2 := ℙ<μ>{[ ∑[rv]_{i < n} nth_cost tsko i ⟨<=⟩ k ]}).
{ apply: nth_cost_sum_monotone; erewrite <-EQ; eauto 1.
apply: leq_trans.
{ apply: pr_arrivals_task_between_respect_arrival_curve_mid ⇒ //.
{ by apply H_tsko_in_ts. }
{ by apply respects_arrival_curve. }
{ by apply valid_arrival_curve. }
}
{ by rewrite addnC. }
}
{ rewrite EQj; apply: pr_workload_bounded_by_nth_cost_sum; eauto 1.
by intros; rewrite EQ.
}
Qed.
Technical lemma: rewrite sum using iota notation.
Lemma nth_cost_sum_rewrite :
∑[rv]_{i < max_arrivals tsko (Δ + D tsko)%nat} nth_cost tsko i
⪯ ∑[rv]_{x<-iota 0 (max_arrivals tsko (Δ + D tsko)%nat)|xpredT x} nth_cost tsko x.
Proof.
move ⇒ k; apply Rle_ge, pr_mono_pred ⇒ ωo.
by rewrite /index_iota subn0.
Qed.
∑[rv]_{i < max_arrivals tsko (Δ + D tsko)%nat} nth_cost tsko i
⪯ ∑[rv]_{x<-iota 0 (max_arrivals tsko (Δ + D tsko)%nat)|xpredT x} nth_cost tsko x.
Proof.
move ⇒ k; apply Rle_ge, pr_mono_pred ⇒ ωo.
by rewrite /index_iota subn0.
Qed.
Step 5: Bound individual job costs by pWCET
The cost of the i-th job of task tsko is stochastically dominated by
the pWCET distribution of tsko. This is the leaf-level bound that
allows us to "replace" random job costs with deterministic pWCET
distributions.
Lemma nth_job_cost_bounded_by_pWCET :
nth_cost tsko i ⪯ to_distrib pWCET_pmf tsko.
Proof.
by apply H_job_costs_bounded_by_pWCET.
Qed.
End StepByStep.
nth_cost tsko i ⪯ to_distrib pWCET_pmf tsko.
Proof.
by apply H_job_costs_bounded_by_pWCET.
Qed.
End StepByStep.
Theorem probabilistic_rta_fp :
ℙ<μ>{[ D tsk ⟨<⟩ 𝓡 j ]} ≤ Λ ts tsk.
Proof.
set (ξpart := partition_on_ξ μ).
set (V := pr_carry_in_workload_of_hep_jobs sched tsk : instant → rvar μ [eqType of work]).
apply WCA_TDFP_bounded_implies_TDFP_bounded; [by apply lims_Λ | intros ξprt ξ ρ].
move: (pr_pos_inv _ ρ) ⇒ [ω [INωξ FE]].
have [ZERO|[A ARR]] := job_either_arrives_or_not.
{ by replace (pr_cond _ _ _ ) with 0;
[apply lims_Λ | symmetry; apply: tdfp_zero_when_job_does_not_arrive]. }
apply: Rle_trans; first by apply deadline_miss_implies_workload_exceeds_time with ω; eauto 1.
have ARRCON: arr_seq_job_arrival_consistent by apply arr_seq_consistent.
have ARRUNIQ: pr_arrival_sequence_uniq by intros ? ?; apply arr_seq_uniq.
eapply Rle_trans; first by apply frechet_bound_on_all_intervals.
apply pointwise_min1_zip; first by rewrite !size_map /range.
apply pointwise_leq_zip_impl_in_leq ⇒ t; rewrite mem_index_iota ⇒ IN.
set (𝓢 := mkRvar
(restrict μ (ξpart◁{ξ}))
(fun ω ⇒
\sum_(tsko <- ts | (hep_task tsko tsk) && (tsko != tsk))
pr_workload_of_task (μ := μ) tsko (A - D tsko) (A + t) ω
)
).
set (𝓒j := mkRvar (restrict μ (ξpart◁{ξ})) (fun ω ⇒ odflt0 (job_cost j) ω)).
set (S :=
(fun ω t ⇒
V A ω + pr_workload_of_hep_tasks tsk A (A + t) ω > t
)%nat
).
have F3 : ℙ<μ>{[ S^~ t | ξpart◁{ξ} ]} ≤ ℙ<μ>{[ fun ω ⇒ (𝓒j ω + 𝓢 ω > t)%nat | ξpart◁{ξ} ]}.
{ by apply: workload_bounded_by_cost_plus_interference; try apply INωξ. }
apply: Rle_trans; [by apply: F3 | clear F3].
apply addrv_addmpf_respect_ltn ⇒ //.
{ intros Cj W; rewrite Rmult_comm !fold_prob_to_cond_prob.
apply: eq_tr3;
[ by apply: job_cost_and_ohep_workload_independent; eauto 1
| by rewrite Rmult_comm; apply Rmult_eq_compat ].
}
{ by apply: H_conditional_cost_bounded_by_pWCET; eauto 1. }
set (F := fun tsko ⇒
mkRvar
(restrict μ (ξpart◁{ξ}))
(fun ω ⇒ pr_workload_of_task tsko (A - D tsko)%nat (A + t)%nat ω)).
have F4 :
𝓢 ⪯ ∑[rv]_{x<-ts|(λ x0 : Task, hep_task x0 tsk && (x0 != tsk)) x} F x .
{ apply: interference_bounded_by_task_workload_sum ⇒ //. }
eapply func_dom_trans; [by apply F4 | clear F4].
apply: sumrv_sumpmf_respect_stochastic_order.
{ by apply: pr_task_workload_independence; eauto 1. }
move ⇒ tsko INo /andP [HEPo NEQo].
have F5 : F tsko ⪯ ∑[rv]_{i< max_arrivals tsko (t + D tsko)%nat} nth_cost tsko i.
{ by apply: task_workload_bounded_by_nth_cost_sum; eauto. }
apply: func_dom_trans; [ by apply F5 | clear F5 ].
have F6 :
∑[rv]_{i< max_arrivals tsko (t + D tsko)%nat} nth_cost tsko i
⪯ ∑[rv]_{x<-iota 0 (max_arrivals tsko (t + D tsko)%nat)|xpredT x} nth_cost tsko x.
{ by apply nth_cost_sum_rewrite. }
eapply func_dom_trans; [by apply F6 | clear F6].
move ⇒ k.
apply sumrv_sumpmf_respect_stochastic_order.
{ by apply: task_job_cost_independence_ac; eassumption. }
by intros; apply nth_job_cost_bounded_by_pWCET.
Qed.
End TDFPIsBounded.
ℙ<μ>{[ D tsk ⟨<⟩ 𝓡 j ]} ≤ Λ ts tsk.
Proof.
set (ξpart := partition_on_ξ μ).
set (V := pr_carry_in_workload_of_hep_jobs sched tsk : instant → rvar μ [eqType of work]).
apply WCA_TDFP_bounded_implies_TDFP_bounded; [by apply lims_Λ | intros ξprt ξ ρ].
move: (pr_pos_inv _ ρ) ⇒ [ω [INωξ FE]].
have [ZERO|[A ARR]] := job_either_arrives_or_not.
{ by replace (pr_cond _ _ _ ) with 0;
[apply lims_Λ | symmetry; apply: tdfp_zero_when_job_does_not_arrive]. }
apply: Rle_trans; first by apply deadline_miss_implies_workload_exceeds_time with ω; eauto 1.
have ARRCON: arr_seq_job_arrival_consistent by apply arr_seq_consistent.
have ARRUNIQ: pr_arrival_sequence_uniq by intros ? ?; apply arr_seq_uniq.
eapply Rle_trans; first by apply frechet_bound_on_all_intervals.
apply pointwise_min1_zip; first by rewrite !size_map /range.
apply pointwise_leq_zip_impl_in_leq ⇒ t; rewrite mem_index_iota ⇒ IN.
set (𝓢 := mkRvar
(restrict μ (ξpart◁{ξ}))
(fun ω ⇒
\sum_(tsko <- ts | (hep_task tsko tsk) && (tsko != tsk))
pr_workload_of_task (μ := μ) tsko (A - D tsko) (A + t) ω
)
).
set (𝓒j := mkRvar (restrict μ (ξpart◁{ξ})) (fun ω ⇒ odflt0 (job_cost j) ω)).
set (S :=
(fun ω t ⇒
V A ω + pr_workload_of_hep_tasks tsk A (A + t) ω > t
)%nat
).
have F3 : ℙ<μ>{[ S^~ t | ξpart◁{ξ} ]} ≤ ℙ<μ>{[ fun ω ⇒ (𝓒j ω + 𝓢 ω > t)%nat | ξpart◁{ξ} ]}.
{ by apply: workload_bounded_by_cost_plus_interference; try apply INωξ. }
apply: Rle_trans; [by apply: F3 | clear F3].
apply addrv_addmpf_respect_ltn ⇒ //.
{ intros Cj W; rewrite Rmult_comm !fold_prob_to_cond_prob.
apply: eq_tr3;
[ by apply: job_cost_and_ohep_workload_independent; eauto 1
| by rewrite Rmult_comm; apply Rmult_eq_compat ].
}
{ by apply: H_conditional_cost_bounded_by_pWCET; eauto 1. }
set (F := fun tsko ⇒
mkRvar
(restrict μ (ξpart◁{ξ}))
(fun ω ⇒ pr_workload_of_task tsko (A - D tsko)%nat (A + t)%nat ω)).
have F4 :
𝓢 ⪯ ∑[rv]_{x<-ts|(λ x0 : Task, hep_task x0 tsk && (x0 != tsk)) x} F x .
{ apply: interference_bounded_by_task_workload_sum ⇒ //. }
eapply func_dom_trans; [by apply F4 | clear F4].
apply: sumrv_sumpmf_respect_stochastic_order.
{ by apply: pr_task_workload_independence; eauto 1. }
move ⇒ tsko INo /andP [HEPo NEQo].
have F5 : F tsko ⪯ ∑[rv]_{i< max_arrivals tsko (t + D tsko)%nat} nth_cost tsko i.
{ by apply: task_workload_bounded_by_nth_cost_sum; eauto. }
apply: func_dom_trans; [ by apply F5 | clear F5 ].
have F6 :
∑[rv]_{i< max_arrivals tsko (t + D tsko)%nat} nth_cost tsko i
⪯ ∑[rv]_{x<-iota 0 (max_arrivals tsko (t + D tsko)%nat)|xpredT x} nth_cost tsko x.
{ by apply nth_cost_sum_rewrite. }
eapply func_dom_trans; [by apply F6 | clear F6].
move ⇒ k.
apply sumrv_sumpmf_respect_stochastic_order.
{ by apply: task_job_cost_independence_ac; eassumption. }
by intros; apply nth_job_cost_bounded_by_pWCET.
Qed.
End TDFPIsBounded.