Library probsa.rt.analysis.valid_pWCET_remains_valid
From prosa.model Require Import processor.ideal.
From probsa.util Require Export misc bigop_inf.
From probsa.probability Require Export pred law_of_total_prob.
From probsa.rt.model Require Export task events axiomatic_pWCET scheduler rt_monotonic.
From probsa.rt.analysis Require Export pETs_to_pWCETs partition_transfer
axiomatic_pWCET_step.
From mathcomp Require Import finfun.
From probsa.util Require Export misc bigop_inf.
From probsa.probability Require Export pred law_of_total_prob.
From probsa.rt.model Require Export task events axiomatic_pWCET scheduler rt_monotonic.
From probsa.rt.analysis Require Export pETs_to_pWCETs partition_transfer
axiomatic_pWCET_step.
From mathcomp Require Import finfun.
Valid pWCET Remains Valid
We plan to replace every single job cost using the procedure replace_job_pET repeated for each job. However, note that the assumption axiomatic_pWCET (μ_of S) is stated only for the initial system S. After we apply the transformation, we create a new system S' := replace_job_pET j S. Thus, in order to be able to use axiomatic_pWCET again on S', we must ensure that the pWCET remains axiomatic in the new system S'. In this section, we show that this is indeed the case.
Assume horizon defines the termination time of the system. If
horizon = None, the system does not terminate; however, it
still has a finite number of jobs.
Consider any type of tasks with a notion of pWCET ...
...and their jobs.
Consider a response-time monotonic scheduling algorithm ζ,
where response-time monotonic means the following -- assuming
that all arrival times are fixed, an increase of the execution
cost of any job cannot cause a decrease of the response time of
any job. Recall that ζ receives two vectors: a vector of
arrival times 𝗔 and a vector of job costs 𝗖.
For simplicity, let 𝓡 denote a function that maps 𝗔 and 𝗖
to a function that computes the response time of any job ...
Auxiliary Lemmas
When we talk about axiomatic pWCET, we are interested in two properties: partition-independentness and partition-dominance. In this section, we prove two auxiliary lemmas which state that after transforming a system into a new system via function replace_job_pET, both properties are satisfied in the new system.
Variable Ω : countType.
Variable μ : measure Ω.
Variable 𝓐 : JobArrivalRV Job Ω μ.
Variable 𝓒 : JobCostRV Job Ω μ.
Variable μ : measure Ω.
Variable 𝓐 : JobArrivalRV Job Ω μ.
Variable 𝓒 : JobCostRV Job Ω μ.
Let us use these parameters to construct a system S.
Next, consider two arbitrary jobs: job j, for which we
compute the response time, and job j_rep, whose pET we
modify.
Suppose we use the construction replace_job_pET presented in
probsa/rt/analysis/pETs_to_pWCETs to replace the execution
cost of given job j_rep. Let S' denote the resulting system.
Similar to probsa/rt/analysis/axiomatic_pWCET_step.v,
consider an arrival sequence ξ and two events corresponding
to ω that realize this arrival sequence in systems S and
S', respectively.
Variable ξ : arrival_sequence Job.
Let ξf := ξ_fix (arr_seq (job_arrival := 𝓐_of S)) ξ.
Let ξf' := ξ_fix (arr_seq (job_arrival := 𝓐_of S')) ξ.
Let ξf := ξ_fix (arr_seq (job_arrival := 𝓐_of S)) ξ.
Let ξf' := ξ_fix (arr_seq (job_arrival := 𝓐_of S')) ξ.
In this section, we show that if partition-dominance holds for
S w.r.t. partition P, then partition-dominance holds for
S' w.r.t. partition P'.
Section ConditionalBoundedness.
Hypothesis H_job_cost_cond_bounded_by_pWCET :
∀ (i : I P) (ρ : PosProb (μ_of S) (ξf ∩ P◁{i})),
𝔽<μ_of S, ρ>{[ odflt0 (𝓒_of S j) | ξf ∩ P◁{i} ]} ⪯ pWCET_cdf (job_task j).
Lemma job_cost_cond_bounded_by_pWCET_respected :
∀ (i : I P') (ρ' : PosProb (μ_of S') (ξf' ∩ P'◁{i})),
𝔽<μ_of S', ρ'>{[ odflt0 (𝓒_of S' j) | ξf' ∩ P'◁{i} ]} ⪯ pWCET_cdf (job_task j).
Proof.
intros × c; unfold S in *; clear S ⇒ //=.
destruct pWCET_pmf as [pWCET nonneg sum1], P as [I p COV DISJ]; simpl in *; clear P P'.
set (μ_tsk := {| pmf := pWCET (job_task j_rep);
pmf_pos := nonneg (job_task j_rep);
pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
have ρ : PosProb μ (ξ_fix arr_seq ξ ∩ p i).
{ move: ρ'; unfold PosProb ⇒ //= ⇒ EQ.
erewrite (pr_joint_pred_eq μ μ_tsk) with (A2 := xpredT),
(pr_xpredT μ_tsk), Rmult_1_r in EQ.
apply: EQ.
by intros [ω n]; rewrite andb_true_r.
}
set (μp := distrib_prod _ _) in ×.
have EQ := cdf_cond_eq_cond
μp _
(ξf' ∩ (λ ω : Ω × nat, p i (let (ω0, _) := ω in ω0)))
(fun ω ⇒ ξf ω.1 && p i ω.1).
unshelve erewrite EQ;
[ by rewrite /PosProb /μp; erewrite pr_joint_pred_eq with (A2 := xpredT);
[ rewrite pr_xpredT Rmult_1_r; apply ρ
| intros []; rewrite andb_true_r]
| clear EQ
| by intros [ω n] ⇒ //= ].
destruct (j_rep == j) eqn:EQ.
{ unfold μp; move: EQ ⇒ /eqP EQ; subst j_rep.
have E := cdf_cond_marginal21
μ μ_tsk
(odflt0 {| rvar_fun := λ '(_, ω__j), Some ω__j |})
(mkRvar μ_tsk id)
(λ ω : _, ξf ω && p i ω).
unshelve erewrite E; [ clear E | by move ⇒ []].
rewrite cdf_cond_xpredT /cdf_cond /cdf -bigop_inf_cdf_le.
apply Rle_ge, SeriesC_le; last first.
{ eapply ex_seriesC_le with (fun n ⇒ ℙ<μ_tsk>{[ λ ω, ω == n ]}).
{ move ⇒ n; split.
{ destruct (n ≤ c)%nat ⇒ //=; [rewrite Rmult_1_l | rewrite Rmult_0_l].
- by apply Rge_le, ge_pr_0.
- by apply Rge_refl. }
destruct (n ≤ c)%nat ⇒ //=; [rewrite Rmult_1_l | rewrite Rmult_0_l].
- by apply Rge_refl.
- by apply Rge_le, ge_pr_0.
}
by apply ex_series_pr_eq_over_disjoint; move ⇒ ? ? ? /eqP → /eqP →.
}
move ⇒ n; split.
{ destruct (n ≤ c)%nat; last by apply Rge_refl.
by apply Rge_le.
}
{ unfold task.pWCET_pmf, μ_tsk, "I[ _ ]", pr ⇒ //=.
destruct (n ≤ c)%nat; [rewrite Rmult_1_l | by rewrite Rmult_0_l; apply Rge_refl].
by rewrite SeriesCf_bump; apply Rge_refl.
}
}
{ eapply Rge_trans; [clear H_job_cost_cond_bounded_by_pWCET | apply H_job_cost_cond_bounded_by_pWCET].
have E := cdf_cond_marginal11
μ μ_tsk
(odflt0 {| rvar_fun := λ '(ω, _), 𝓒 j ω |}) (odflt0 (𝓒 j))
(λ ω : _, ξf ω && p i ω).
erewrite E; clear E; last by intros [].
apply Req_le_sym, cdf_cond_eq_cond ⇒ ω.
by compute.
}
Qed.
End ConditionalBoundedness.
Hypothesis H_job_cost_cond_bounded_by_pWCET :
∀ (i : I P) (ρ : PosProb (μ_of S) (ξf ∩ P◁{i})),
𝔽<μ_of S, ρ>{[ odflt0 (𝓒_of S j) | ξf ∩ P◁{i} ]} ⪯ pWCET_cdf (job_task j).
Lemma job_cost_cond_bounded_by_pWCET_respected :
∀ (i : I P') (ρ' : PosProb (μ_of S') (ξf' ∩ P'◁{i})),
𝔽<μ_of S', ρ'>{[ odflt0 (𝓒_of S' j) | ξf' ∩ P'◁{i} ]} ⪯ pWCET_cdf (job_task j).
Proof.
intros × c; unfold S in *; clear S ⇒ //=.
destruct pWCET_pmf as [pWCET nonneg sum1], P as [I p COV DISJ]; simpl in *; clear P P'.
set (μ_tsk := {| pmf := pWCET (job_task j_rep);
pmf_pos := nonneg (job_task j_rep);
pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
have ρ : PosProb μ (ξ_fix arr_seq ξ ∩ p i).
{ move: ρ'; unfold PosProb ⇒ //= ⇒ EQ.
erewrite (pr_joint_pred_eq μ μ_tsk) with (A2 := xpredT),
(pr_xpredT μ_tsk), Rmult_1_r in EQ.
apply: EQ.
by intros [ω n]; rewrite andb_true_r.
}
set (μp := distrib_prod _ _) in ×.
have EQ := cdf_cond_eq_cond
μp _
(ξf' ∩ (λ ω : Ω × nat, p i (let (ω0, _) := ω in ω0)))
(fun ω ⇒ ξf ω.1 && p i ω.1).
unshelve erewrite EQ;
[ by rewrite /PosProb /μp; erewrite pr_joint_pred_eq with (A2 := xpredT);
[ rewrite pr_xpredT Rmult_1_r; apply ρ
| intros []; rewrite andb_true_r]
| clear EQ
| by intros [ω n] ⇒ //= ].
destruct (j_rep == j) eqn:EQ.
{ unfold μp; move: EQ ⇒ /eqP EQ; subst j_rep.
have E := cdf_cond_marginal21
μ μ_tsk
(odflt0 {| rvar_fun := λ '(_, ω__j), Some ω__j |})
(mkRvar μ_tsk id)
(λ ω : _, ξf ω && p i ω).
unshelve erewrite E; [ clear E | by move ⇒ []].
rewrite cdf_cond_xpredT /cdf_cond /cdf -bigop_inf_cdf_le.
apply Rle_ge, SeriesC_le; last first.
{ eapply ex_seriesC_le with (fun n ⇒ ℙ<μ_tsk>{[ λ ω, ω == n ]}).
{ move ⇒ n; split.
{ destruct (n ≤ c)%nat ⇒ //=; [rewrite Rmult_1_l | rewrite Rmult_0_l].
- by apply Rge_le, ge_pr_0.
- by apply Rge_refl. }
destruct (n ≤ c)%nat ⇒ //=; [rewrite Rmult_1_l | rewrite Rmult_0_l].
- by apply Rge_refl.
- by apply Rge_le, ge_pr_0.
}
by apply ex_series_pr_eq_over_disjoint; move ⇒ ? ? ? /eqP → /eqP →.
}
move ⇒ n; split.
{ destruct (n ≤ c)%nat; last by apply Rge_refl.
by apply Rge_le.
}
{ unfold task.pWCET_pmf, μ_tsk, "I[ _ ]", pr ⇒ //=.
destruct (n ≤ c)%nat; [rewrite Rmult_1_l | by rewrite Rmult_0_l; apply Rge_refl].
by rewrite SeriesCf_bump; apply Rge_refl.
}
}
{ eapply Rge_trans; [clear H_job_cost_cond_bounded_by_pWCET | apply H_job_cost_cond_bounded_by_pWCET].
have E := cdf_cond_marginal11
μ μ_tsk
(odflt0 {| rvar_fun := λ '(ω, _), 𝓒 j ω |}) (odflt0 (𝓒 j))
(λ ω : _, ξf ω && p i ω).
erewrite E; clear E; last by intros [].
apply Req_le_sym, cdf_cond_eq_cond ⇒ ω.
by compute.
}
Qed.
End ConditionalBoundedness.
In this section, we show that if partition-independentness holds for
S w.r.t. partition P, then partition-independentness holds for
S' w.r.t. partition P'.
Consider an arbitrary vector of job costs 𝗖...
... and two events corresponding to ωs that realize this
vector of job costs in systems S and S',
respectively.
Let 𝓒_fix := events.𝓒_fix (job_cost := 𝓒_of S) 𝗖.
Let 𝓒_fix' := events.𝓒_fix (job_cost := 𝓒_of S') 𝗖.
Hypothesis H_job_cost_cond_independent :
∀ (i : I P) (jobs : seq Job) (ρ : PosProb (μ_of S) (ξf ∩ P◁{i})),
j \notin jobs →
ℙ<μ_of S, ρ>{[ 𝓒_fix [:: j] ∩ 𝓒_fix jobs | ξf ∩ P◁{i} ]}
= ℙ<μ_of S>{[ 𝓒_fix [:: j] | ξf ∩ P◁{i} ]} × ℙ<μ_of S>{[ 𝓒_fix jobs | ξf ∩ P◁{i} ]}.
Lemma job_cost_cond_independent_respected :
∀ (i : I P') (jobs : seq Job) (ρ' : PosProb (μ_of S') (ξf' ∩ P'◁{i})),
j \notin jobs →
ℙ<μ_of S', ρ'>{[ 𝓒_fix' [:: j] ∩ 𝓒_fix' jobs | ξf' ∩ P'◁{i} ]}
= ℙ<μ_of S'>{[ 𝓒_fix' [:: j] | ξf' ∩ P'◁{i} ]} × ℙ<μ_of S'>{[ 𝓒_fix' jobs | ξf' ∩ P'◁{i} ]}.
Proof.
unfold proj1 in *; destruct pWCET_pmf as [pWCET nonneg sum1].
have L1 : ∀ a b c d, a = c → b = d → a × b = c × d by move ⇒ ? ? ? ? → →.
set (μ_tsk := {| pmf := pWCET (job_task j_rep);
pmf_pos := nonneg (job_task j_rep);
pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
unfold 𝓒_fix', events.𝓒_fix in ×.
intros × H_nin; unfold S in *; clear S ⇒ //=.
destruct P as [I p COV DISJ]; simpl in *; clear P P'.
set (μp := distrib_prod _ _) in ×.
have ρ : PosProb μ (ξ_fix arr_seq ξ ∩ p i).
{ move: ρ'; rewrite /μp /PosProb -/μ_tsk.
erewrite (pr_joint_pred_eq μ μ_tsk) with (A2 := xpredT);
[ by rewrite pr_xpredT Rmult_1_r ⇒ POS; apply: POS
| by intros []; rewrite andb_true_r].
}
destruct (j_rep == j) eqn:EQ, (j_rep \in jobs) eqn:IN.
{ by exfalso; move : EQ ⇒ /eqP EQ; subst j_rep; move: IN (H_nin) ⇒ →. }
{ clear IN; move : EQ ⇒ /eqP EQ; subst j_rep.
have Ex1 : ∃ P1, 𝓒_fix' jobs =1 (fun ω ⇒ P1 ω.1).
{ unshelve eexists (λ ω : Ω, all (λ j0 : Job, {| rvar_fun := λ ω0, 𝓒 j0 ω0 |} ω == 𝗖 j0) jobs).
{ by done. }
intros [ω c]; apply eq_in_all ⇒ s IN ⇒ //=; rewrite /sample_costs.
replace (j == s) with false; first by reflexivity.
symmetry; apply/negP ⇒ /eqP EQ; subst s.
by move: (H_nin); rewrite IN.
}
have Ex2 : ∃ P2, 𝓒_fix' [::j] =1 (fun ω ⇒ P2 ω.2).
{ unshelve eexists (fun (ω : nat) ⇒
sample_costs (job_cost := λ jo : Job,
{| rvar_fun := λ ω__j, Some ω__j |}) ω j == 𝗖 j).
{ by done. }
by rewrite /𝓒_fix' /events.𝓒_fix ⇒ //=; intros [ω c]; rewrite /sample_costs eq_refl andb_true_r.
}
destruct Ex1 as [P1 EQ1], Ex2 as [P2 EQ2]; rewrite /μp -/μ_tsk.
unshelve erewrite (pr_cond_joint_pred_eq_cond_eq μ _)
with (A1 := P1) (A2 := P2) (B2 := xpredT) ⇒ //; first last.
{ by intros [ω c]; rewrite andb_true_r. }
{ intros [ω c]; unfold "∩", pred.pred_intersection.
rewrite /𝓒_fix' //= in EQ1, EQ2.
by rewrite EQ1 EQ2 andb_comm.
}
unshelve erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk)
with (A1 := xpredT) (A2 := P2) (B2 := xpredT) ⇒ //; first last.
{ by intros [ω c]; rewrite andb_true_r. }
unshelve erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk)
with (A1 := P1) (A2 := xpredT) (B2 := xpredT) ⇒ //; first last.
{ by intros [ω c]; rewrite andb_true_r. }
{ by intros [ω c]; rewrite /𝓒_fix' //= in EQ1; rewrite andb_true_r EQ1. }
by rewrite ![pr_cond _ _ xpredT]/pr_cond !pr_xpredT ?Rmult_1_l ?Rmult_1_r Rmult_comm.
all: rewrite /PosProb pr_xpredT; apply Rlt_0_1.
}
{ set (jobs2 := filter (fun j ⇒ j_rep != j) jobs).
have NIN: j \notin jobs2.
{ by apply/negP; rewrite mem_filter; apply/negP; rewrite negb_and H_nin orbT. }
rewrite /μp -/μ_tsk; unshelve erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk)
with (B2 := xpredT) (A1 := 𝓒_fix [:: j] ∩ 𝓒_fix jobs2)
(A2 := events.𝓒_fix (job_cost := λ jo, {| rvar_fun := λ ωj, Some ωj |}) 𝗖 [::j_rep]);
first last; [ | | | by done].
{ by intros [ω c]; rewrite andb_true_r. }
{ intros [ω c]; rewrite /𝓒_fix /all_filter /sample_costs //= andb_true_r.
unfold "∩", pred.pred_intersection; rewrite !andb_true_r all_filter EQ.
destruct (𝓒 j ω == 𝗖 j) eqn:EQ3; rewrite EQ3 //=.
destruct (Some c == 𝗖 j_rep) eqn:EQ2.
{ rewrite EQ2 andb_true_r; apply eq_in_all ⇒ s INs ⇒ //=.
destruct (j_rep == s) eqn:EQs ⇒ //=.
by move: EQs ⇒ /eqP EQs; subst s.
}
{ rewrite EQ2 andb_false_r; apply/allPn.
by ∃ j_rep; [ | rewrite eq_refl; apply/negP; rewrite EQ2].
}
}
specialize (H_job_cost_cond_independent i jobs2 ρ NIN); unfold ξf in ×.
erewrite H_job_cost_cond_independent, Rmult_assoc; apply L1.
{ erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk)
with (A2 := xpredT) (B2 := xpredT);
[ by rewrite {3}/pr_cond pr_xpredT Rmult_1_r
| by intros []; rewrite /𝓒_fix' //= !andb_true_r //= /sample_costs EQ //=
| by intros []; rewrite andb_true_r].
}
{ symmetry; apply pr_cond_joint_pred_eq_cond_eq with (B2 := xpredT);
last by intros []; rewrite andb_true_r.
intros [ω c]; rewrite /𝓒_fix /all_filter /sample_costs //= andb_true_r all_filter.
destruct (Some c == 𝗖 j_rep) eqn:EQ2.
{ rewrite EQ2 andb_true_r; apply eq_in_all ⇒ s INs ⇒ //=.
destruct (j_rep == s) eqn:EQs ⇒ //=.
by move: EQs ⇒ /eqP EQs; subst s.
}
{ rewrite EQ2 andb_false_r; apply/allPn.
by ∃ j_rep; [ | rewrite eq_refl; apply/negP; rewrite EQ2].
}
}
}
{ rewrite /μp; erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk); first last.
{ by intros []; rewrite !andb_true_r. }
{ intros [ω c]; instantiate (1 := xpredT); rewrite andb_true_r.
instantiate (1 := (𝓒_fix [:: j] ∩ 𝓒_fix jobs)).
unfold "∩", pred.pred_intersection, sample_costs; rewrite EQ //=.
erewrite eq_in_all with (a2 := λ j0 : Job, 𝓒 j0 ω == 𝗖 j0); first by reflexivity.
intros ? IN2; destruct (j_rep == x) eqn:EQ2 ⇒ //.
by move: EQ2 ⇒ /eqP EQ2; subst x; rewrite IN2 in IN.
}
specialize (H_job_cost_cond_independent i jobs ρ H_nin); unfold ξf in *; erewrite H_job_cost_cond_independent.
rewrite Rmult_comm {1}/pr_cond pr_xpredT Rmult_1_l -/μ_tsk.
apply L1.
{ erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk) with (A2 := xpredT) (B2 := xpredT).
{ rewrite {3}/pr_cond pr_xpredT Rmult_1_r; reflexivity. }
{ rewrite /𝓒_fix' //=.
by intros []; rewrite !andb_true_r //= /sample_costs EQ. }
{ by intros []; rewrite andb_true_r. }
}
{ erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk) with (A2 := xpredT) (B2 := xpredT).
- by rewrite {3}/pr_cond pr_xpredT Rmult_1_r; reflexivity.
- intros [ω c]; rewrite andb_true_r /𝓒_fix /sample_costs.
apply eq_in_all ⇒ s INs ⇒ //=; destruct (j_rep == s) eqn:EQs; last by done.
by move: EQs ⇒ /eqP EQs; subst s; rewrite INs in IN.
- by intros [ω s]; rewrite andb_true_r.
}
}
Qed.
End ConditionalIndependence.
End ProofOfLemmas.
Let 𝓒_fix' := events.𝓒_fix (job_cost := 𝓒_of S') 𝗖.
Hypothesis H_job_cost_cond_independent :
∀ (i : I P) (jobs : seq Job) (ρ : PosProb (μ_of S) (ξf ∩ P◁{i})),
j \notin jobs →
ℙ<μ_of S, ρ>{[ 𝓒_fix [:: j] ∩ 𝓒_fix jobs | ξf ∩ P◁{i} ]}
= ℙ<μ_of S>{[ 𝓒_fix [:: j] | ξf ∩ P◁{i} ]} × ℙ<μ_of S>{[ 𝓒_fix jobs | ξf ∩ P◁{i} ]}.
Lemma job_cost_cond_independent_respected :
∀ (i : I P') (jobs : seq Job) (ρ' : PosProb (μ_of S') (ξf' ∩ P'◁{i})),
j \notin jobs →
ℙ<μ_of S', ρ'>{[ 𝓒_fix' [:: j] ∩ 𝓒_fix' jobs | ξf' ∩ P'◁{i} ]}
= ℙ<μ_of S'>{[ 𝓒_fix' [:: j] | ξf' ∩ P'◁{i} ]} × ℙ<μ_of S'>{[ 𝓒_fix' jobs | ξf' ∩ P'◁{i} ]}.
Proof.
unfold proj1 in *; destruct pWCET_pmf as [pWCET nonneg sum1].
have L1 : ∀ a b c d, a = c → b = d → a × b = c × d by move ⇒ ? ? ? ? → →.
set (μ_tsk := {| pmf := pWCET (job_task j_rep);
pmf_pos := nonneg (job_task j_rep);
pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
unfold 𝓒_fix', events.𝓒_fix in ×.
intros × H_nin; unfold S in *; clear S ⇒ //=.
destruct P as [I p COV DISJ]; simpl in *; clear P P'.
set (μp := distrib_prod _ _) in ×.
have ρ : PosProb μ (ξ_fix arr_seq ξ ∩ p i).
{ move: ρ'; rewrite /μp /PosProb -/μ_tsk.
erewrite (pr_joint_pred_eq μ μ_tsk) with (A2 := xpredT);
[ by rewrite pr_xpredT Rmult_1_r ⇒ POS; apply: POS
| by intros []; rewrite andb_true_r].
}
destruct (j_rep == j) eqn:EQ, (j_rep \in jobs) eqn:IN.
{ by exfalso; move : EQ ⇒ /eqP EQ; subst j_rep; move: IN (H_nin) ⇒ →. }
{ clear IN; move : EQ ⇒ /eqP EQ; subst j_rep.
have Ex1 : ∃ P1, 𝓒_fix' jobs =1 (fun ω ⇒ P1 ω.1).
{ unshelve eexists (λ ω : Ω, all (λ j0 : Job, {| rvar_fun := λ ω0, 𝓒 j0 ω0 |} ω == 𝗖 j0) jobs).
{ by done. }
intros [ω c]; apply eq_in_all ⇒ s IN ⇒ //=; rewrite /sample_costs.
replace (j == s) with false; first by reflexivity.
symmetry; apply/negP ⇒ /eqP EQ; subst s.
by move: (H_nin); rewrite IN.
}
have Ex2 : ∃ P2, 𝓒_fix' [::j] =1 (fun ω ⇒ P2 ω.2).
{ unshelve eexists (fun (ω : nat) ⇒
sample_costs (job_cost := λ jo : Job,
{| rvar_fun := λ ω__j, Some ω__j |}) ω j == 𝗖 j).
{ by done. }
by rewrite /𝓒_fix' /events.𝓒_fix ⇒ //=; intros [ω c]; rewrite /sample_costs eq_refl andb_true_r.
}
destruct Ex1 as [P1 EQ1], Ex2 as [P2 EQ2]; rewrite /μp -/μ_tsk.
unshelve erewrite (pr_cond_joint_pred_eq_cond_eq μ _)
with (A1 := P1) (A2 := P2) (B2 := xpredT) ⇒ //; first last.
{ by intros [ω c]; rewrite andb_true_r. }
{ intros [ω c]; unfold "∩", pred.pred_intersection.
rewrite /𝓒_fix' //= in EQ1, EQ2.
by rewrite EQ1 EQ2 andb_comm.
}
unshelve erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk)
with (A1 := xpredT) (A2 := P2) (B2 := xpredT) ⇒ //; first last.
{ by intros [ω c]; rewrite andb_true_r. }
unshelve erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk)
with (A1 := P1) (A2 := xpredT) (B2 := xpredT) ⇒ //; first last.
{ by intros [ω c]; rewrite andb_true_r. }
{ by intros [ω c]; rewrite /𝓒_fix' //= in EQ1; rewrite andb_true_r EQ1. }
by rewrite ![pr_cond _ _ xpredT]/pr_cond !pr_xpredT ?Rmult_1_l ?Rmult_1_r Rmult_comm.
all: rewrite /PosProb pr_xpredT; apply Rlt_0_1.
}
{ set (jobs2 := filter (fun j ⇒ j_rep != j) jobs).
have NIN: j \notin jobs2.
{ by apply/negP; rewrite mem_filter; apply/negP; rewrite negb_and H_nin orbT. }
rewrite /μp -/μ_tsk; unshelve erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk)
with (B2 := xpredT) (A1 := 𝓒_fix [:: j] ∩ 𝓒_fix jobs2)
(A2 := events.𝓒_fix (job_cost := λ jo, {| rvar_fun := λ ωj, Some ωj |}) 𝗖 [::j_rep]);
first last; [ | | | by done].
{ by intros [ω c]; rewrite andb_true_r. }
{ intros [ω c]; rewrite /𝓒_fix /all_filter /sample_costs //= andb_true_r.
unfold "∩", pred.pred_intersection; rewrite !andb_true_r all_filter EQ.
destruct (𝓒 j ω == 𝗖 j) eqn:EQ3; rewrite EQ3 //=.
destruct (Some c == 𝗖 j_rep) eqn:EQ2.
{ rewrite EQ2 andb_true_r; apply eq_in_all ⇒ s INs ⇒ //=.
destruct (j_rep == s) eqn:EQs ⇒ //=.
by move: EQs ⇒ /eqP EQs; subst s.
}
{ rewrite EQ2 andb_false_r; apply/allPn.
by ∃ j_rep; [ | rewrite eq_refl; apply/negP; rewrite EQ2].
}
}
specialize (H_job_cost_cond_independent i jobs2 ρ NIN); unfold ξf in ×.
erewrite H_job_cost_cond_independent, Rmult_assoc; apply L1.
{ erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk)
with (A2 := xpredT) (B2 := xpredT);
[ by rewrite {3}/pr_cond pr_xpredT Rmult_1_r
| by intros []; rewrite /𝓒_fix' //= !andb_true_r //= /sample_costs EQ //=
| by intros []; rewrite andb_true_r].
}
{ symmetry; apply pr_cond_joint_pred_eq_cond_eq with (B2 := xpredT);
last by intros []; rewrite andb_true_r.
intros [ω c]; rewrite /𝓒_fix /all_filter /sample_costs //= andb_true_r all_filter.
destruct (Some c == 𝗖 j_rep) eqn:EQ2.
{ rewrite EQ2 andb_true_r; apply eq_in_all ⇒ s INs ⇒ //=.
destruct (j_rep == s) eqn:EQs ⇒ //=.
by move: EQs ⇒ /eqP EQs; subst s.
}
{ rewrite EQ2 andb_false_r; apply/allPn.
by ∃ j_rep; [ | rewrite eq_refl; apply/negP; rewrite EQ2].
}
}
}
{ rewrite /μp; erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk); first last.
{ by intros []; rewrite !andb_true_r. }
{ intros [ω c]; instantiate (1 := xpredT); rewrite andb_true_r.
instantiate (1 := (𝓒_fix [:: j] ∩ 𝓒_fix jobs)).
unfold "∩", pred.pred_intersection, sample_costs; rewrite EQ //=.
erewrite eq_in_all with (a2 := λ j0 : Job, 𝓒 j0 ω == 𝗖 j0); first by reflexivity.
intros ? IN2; destruct (j_rep == x) eqn:EQ2 ⇒ //.
by move: EQ2 ⇒ /eqP EQ2; subst x; rewrite IN2 in IN.
}
specialize (H_job_cost_cond_independent i jobs ρ H_nin); unfold ξf in *; erewrite H_job_cost_cond_independent.
rewrite Rmult_comm {1}/pr_cond pr_xpredT Rmult_1_l -/μ_tsk.
apply L1.
{ erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk) with (A2 := xpredT) (B2 := xpredT).
{ rewrite {3}/pr_cond pr_xpredT Rmult_1_r; reflexivity. }
{ rewrite /𝓒_fix' //=.
by intros []; rewrite !andb_true_r //= /sample_costs EQ. }
{ by intros []; rewrite andb_true_r. }
}
{ erewrite (pr_cond_joint_pred_eq_cond_eq μ μ_tsk) with (A2 := xpredT) (B2 := xpredT).
- by rewrite {3}/pr_cond pr_xpredT Rmult_1_r; reflexivity.
- intros [ω c]; rewrite andb_true_r /𝓒_fix /sample_costs.
apply eq_in_all ⇒ s INs ⇒ //=; destruct (j_rep == s) eqn:EQs; last by done.
by move: EQs ⇒ /eqP EQs; subst s; rewrite INs in IN.
- by intros [ω s]; rewrite andb_true_r.
}
}
Qed.
End ConditionalIndependence.
End ProofOfLemmas.
Valid Axiomatic pWCET Remains Valid
We use the two auxiliary lemmas to prove a lemma that, given a system S, an axiomatic pWCET remains valid for a new system S' where pETs of an arbitrary set of jobs have been replaced by pWCETs.
Lemma valid_axiomatic_pWCET_remains_valid :
∀ (S : system) (jobs : seq Job),
let S' := foldr replace_job_pET S jobs in
axiomatic_pWCET (μ_of S) (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) →
axiomatic_pWCET (μ_of S') (job_arrival := 𝓐_of S') (job_cost := 𝓒_of S').
Proof.
intros [Ω μ 𝓐 𝓒]; induction jobs as [| j_rep jobs]; first by done.
simpl; simpl in IHjobs ⇒ PWCET; apply IHjobs in PWCET; clear IHjobs.
set (S := foldr _ _ _) in ×.
intros ? ξ .
unfold job_cost_partition_dominated, job_cost_partition_independence.
specialize (PWCET j ξ); destruct PWCET as [P [INDP BOUND]].
set (P' := extend_partition S P j_rep).
∃ P'; split.
{ intros ? ? jobs' IN; destruct S.
by apply job_cost_cond_independent_respected; eauto.
}
{ intros ? c x; destruct S as [Ω' μ' 𝓐' 𝓒'].
by apply job_cost_cond_bounded_by_pWCET_respected; intros; apply BOUND.
}
Qed.
∀ (S : system) (jobs : seq Job),
let S' := foldr replace_job_pET S jobs in
axiomatic_pWCET (μ_of S) (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) →
axiomatic_pWCET (μ_of S') (job_arrival := 𝓐_of S') (job_cost := 𝓒_of S').
Proof.
intros [Ω μ 𝓐 𝓒]; induction jobs as [| j_rep jobs]; first by done.
simpl; simpl in IHjobs ⇒ PWCET; apply IHjobs in PWCET; clear IHjobs.
set (S := foldr _ _ _) in ×.
intros ? ξ .
unfold job_cost_partition_dominated, job_cost_partition_independence.
specialize (PWCET j ξ); destruct PWCET as [P [INDP BOUND]].
set (P' := extend_partition S P j_rep).
∃ P'; split.
{ intros ? ? jobs' IN; destruct S.
by apply job_cost_cond_independent_respected; eauto.
}
{ intros ? c x; destruct S as [Ω' μ' 𝓐' 𝓒'].
by apply job_cost_cond_bounded_by_pWCET_respected; intros; apply BOUND.
}
Qed.
Iterative Application of Theorem 1
Consequently, one can use Theorem 1 iteratively to replace the pETs of all jobs in the system.
Theorem prob_rt_monotonic_axiomatic_pWCET_replace_all_pETs :
∀ (S : system),
let S' := replace_all_pETs S in
let sched S := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) in
axiomatic_pWCET (μ_of S) (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) →
probabilistic_response_time_monotone_transformation horizon
(sched S) (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S)
(sched S') (job_arrival_s := 𝓐_of S') (job_cost_s := 𝓒_of S').
Proof.
intros ? ? PWCET ?.
unfold S', replace_all_pETs, replace_all_jobs_pETs.
set (js := index_enum _) in ×.
induction js.
{ by intros ?; apply etime_dom_refl. }
{ intros ?. eapply etime_dom_trans; first apply: IHjs.
set (S'' := foldr replace_job_pET S js).
apply prob_rt_monotonic_axiomatic_pWCET_replace_pET ⇒ //.
by apply (valid_axiomatic_pWCET_remains_valid S).
}
Qed.
End ValidpWCETRemainsValid.
∀ (S : system),
let S' := replace_all_pETs S in
let sched S := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) in
axiomatic_pWCET (μ_of S) (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) →
probabilistic_response_time_monotone_transformation horizon
(sched S) (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S)
(sched S') (job_arrival_s := 𝓐_of S') (job_cost_s := 𝓒_of S').
Proof.
intros ? ? PWCET ?.
unfold S', replace_all_pETs, replace_all_jobs_pETs.
set (js := index_enum _) in ×.
induction js.
{ by intros ?; apply etime_dom_refl. }
{ intros ?. eapply etime_dom_trans; first apply: IHjs.
set (S'' := foldr replace_job_pET S js).
apply prob_rt_monotonic_axiomatic_pWCET_replace_pET ⇒ //.
by apply (valid_axiomatic_pWCET_remains_valid S).
}
Qed.
End ValidpWCETRemainsValid.