Library probsa.rt.model.workload
From prosa.model Require Export aggregate.workload.
From prosa.analysis Require Export facts.model.workload.
From probsa.util Require Export misc.
From probsa.probability Require Export pred pmf.
From probsa.rt.behavior Require Export schedule.
From probsa.rt.model Require Export assumptions.basic.
Local Open Scope nat_scope.
Section PrWorkload.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Definition pr_workload_of_jobs (P : pred Job) (jobs : seq Job) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ @workload_of_jobs Job (sample0_costs ω) P jobs).
Definition pr_workload_of_task (tsk : Task) (t1 t2 : instant) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ pr_workload_of_jobs (job_of_task tsk) (pr_arrivals_between t1 t2 ω) ω).
Definition pr_workload_of_hep_tasks (tsk : Task) (t1 t2 : instant) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ pr_workload_of_jobs
(fun j ⇒ hep_task (job_task j) tsk)
(pr_arrivals_between t1 t2 ω)
ω
).
End PrWorkload.
Section WorkloadLemmasDetCostStocArr.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_cost : JobCost Job}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Variable tsk : Task.
Lemma workload_of_jobs_xpredT :
∀ (P : pred Job) (jobs : seq Job),
workload_of_jobs P jobs = workload_of_jobs xpredT [seq j <- jobs | P j].
Proof.
induction jobs.
{ by rewrite /workload_of_jobs big_nil //= big_nil. }
{ move: IHjobs; rewrite /workload_of_jobs big_cons ⇒ → ⇒ //=.
by destruct (P a) eqn:EQ; first rewrite big_cons. }
Qed.
Lemma workload_of_jobs_widen :
∀ (t1 t2 t1' t2' : nat) (ω : Ω),
t1' ≤ t1 →
t2 ≤ t2' →
workload_of_jobs (job_of_task tsk) (arrivals_between (arr_seq ω) t1 t2)
≤ workload_of_jobs (job_of_task tsk) (arrivals_between (arr_seq ω) t1' t2').
Proof.
intros.
have [LE|LE] := leqP t1 t2; last first.
{ rewrite /arrivals_between big_geq; try by apply ltnW.
by rewrite /workload_of_jobs big_nil.
}
rewrite [in X in (_ ≤ X)%nat](workload_of_jobs_cat _ t1); last first.
{ by apply/andP; split; [done | apply: leq_trans; eauto 1]. }
rewrite -[X in (X ≤ _)%nat]addn0 addnC leq_add //.
rewrite [in X in (_ ≤ X)%nat](workload_of_jobs_cat _ t2); last first.
{ apply/andP; split; [apply: leq_trans; eauto 1 | done]. }
by rewrite -[X in (X ≤ _)%nat]addn0 leq_add //.
Qed.
End WorkloadLemmasDetCostStocArr.
Section PrWorkloadCat.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Variable tsk : Task.
Lemma pr_workload_of_task_cat :
∀ (t1 t2 t : instant) (ω : Ω),
t1 ≤ t ≤ t2 →
pr_workload_of_task tsk t1 t2 ω
= pr_workload_of_task tsk t1 t ω + pr_workload_of_task tsk t t2 ω.
Proof.
intros; rewrite /pr_workload_of_task //=.
by erewrite workload_of_jobs_cat; last by eassumption.
Qed.
End PrWorkloadCat.
Section PrWorkloadFacts.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Variable ts : seq Task.
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
Hypothesis H_arrivals_from_ts : arrivals_from_task_set ts.
Lemma pr_hep_workload_pr_task_workload_split :
∀ (t1 t2 : instant) (ω : Ω),
pr_workload_of_hep_tasks tsk t1 t2 ω
≤ \sum_(tsko <- ts | hep_task tsko tsk) pr_workload_of_task tsko t1 t2 ω.
Proof.
intros; apply: leq_trans.
apply sum_over_partitions_le with (x_to_y := job_task) (ys := ts).
{ move ⇒ j.
rewrite /pr_arrivals_between //= ⇒ IN.
apply in_arrivals_implies_arrived in IN.
by apply: H_arrivals_from_ts; apply IN.
}
{ rewrite [in X in (_ ≤ X)%nat]big_mkcond //=; apply leq_sum ⇒ tsko _.
set (js := arrivals_between _ _ _).
induction js as [ | j js].
{ by rewrite big_nil. }
{ rewrite /workload_of_jobs !big_cons.
destruct (_ == _) eqn:EQ.
{ rewrite andbT /job_of_task EQ.
move: EQ ⇒ /eqP EQ; rewrite EQ.
by move: IHjs; destruct (hep_task _ _ ) ⇒ NEQ; first rewrite leq_add2l.
}
{ by rewrite andbF /job_of_task EQ; apply IHjs. }
}
}
Qed.
End PrWorkloadFacts.
Section TaskWorkloadBounded.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{P : SporadicModel Task}
{D : TaskDeadline Task}
{FP : FP_policy Task}.
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_arrivals_cost_consistent : arrivals_cost_consistent.
Hypothesis H_arrival_sequence_uniq : pr_arrival_sequence_uniq.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Variable (ts : seq Task) (tsk : Task).
Hypothesis H_tsk_in_ts : tsk \in ts.
Hypothesis H_arrivals_from_ts : arrivals_from_task_set ts.
Hypothesis H_inter_arrival_pos : valid_taskset_inter_arrival_times ts.
Hypothesis H_sporadic_arrivals : pr_taskset_respects_sporadic_task_model ts.
Hypothesis H_constrained_deadlines : constrained_deadlines ts.
Variable j : Job.
Variable ω : Ω.
Hypothesis H_arrives_in : arrives_in (arr_seq ω) j.
Hypothesis H_job_of_task : job_of_task tsk j.
Variable A : instant.
Hypothesis H_j_arrives_at_A : job_arrival j ω = Some A.
Lemma at_most_one_job_pending :
∀ t,
t ≤ D tsk →
pr_workload_of_task tsk A (A + t) ω ≤ odflt 0 (job_cost j ω).
Proof.
intros × LE; move: (H_arrives_in) ⇒ E.
destruct (D tsk) as [| d] eqn:EQD.
{ move: LE; rewrite leqn0 ⇒ /eqP EQ; subst t.
rewrite addn0 /pr_workload_of_task //=.
by rewrite /arrivals_between big_geq // /workload_of_jobs //= big_nil. }
apply H_arrivals_cost_consistent in H_arrives_in;
destruct (job_cost j _ ) as [c| ] eqn:EQC; [clear H_arrives_in | done].
apply: leq_trans; first apply workload_of_jobs_widen with (t1' := A) (t2' := (A + D tsk)%nat).
{ by done. }
{ by rewrite leq_add2l EQD. }
clear t LE; rewrite workload_of_jobs_xpredT.
have → :
[seq j0 <- arrivals_between (arr_seq ω) A (A + D tsk)%nat | job_of_task tsk j0] = [::j]; last first.
{ by rewrite /workload_of_jobs big_seq1 /prosa.behavior.job.job_cost /sample0_costs //= EQC. }
rewrite /arrivals_between EQD addnS big_nat_recl; last by rewrite leq_addr.
rewrite filter_cat -[RHS]cats0; f_equal.
{ clear d EQD c EQC; apply seq_filter_singleton.
{ by apply H_arrival_sequence_uniq. }
{ by done. }
{ by apply H_arrivals_consistent; rewrite H_j_arrives_at_A. }
{ intros s IN TSKs.
apply H_arrivals_consistent in IN.
apply/eqP/negPn/negP ⇒ /eqP NEQ.
move: (H_sporadic_arrivals) ⇒ SP.
specialize (SP ω _ H_tsk_in_ts _ _ NEQ).
feed_n 5%nat SP.
{ by eexists; apply H_arrivals_consistent; eassumption. }
{ by eexists; apply H_arrivals_consistent; eassumption. }
{ by apply/eqP. }
{ by apply/eqP. }
{ by rewrite //= /prosa.behavior.job.job_arrival /sample0_arrivals H_j_arrives_at_A IN //= ltnW. }
rewrite //= /prosa.behavior.job.job_arrival /sample0_arrivals H_j_arrives_at_A IN //= in SP.
move_neq_down SP.
rewrite -addn1 leq_add2l.
by apply H_inter_arrival_pos.
}
}
{ apply filter_in_pred0 ⇒ s IN.
apply mem_bigcat_nat_exists in IN; move: IN ⇒ [a [IN /andP [NEQA1 NEQA2]]].
apply H_arrivals_consistent in IN.
apply/negP ⇒ TSKs; move_neq_down NEQA2.
rewrite -(leq_add2r 1%nat) -addnA addn1 -EQD.
destruct (j == s) eqn:EQ.
{ move: EQ ⇒ /eqP EQ; subst s.
move: (H_j_arrives_at_A); rewrite IN ⇒ EQN; inversion EQN; subst A.
by rewrite ltnn in NEQA1.
}
{ move: (H_sporadic_arrivals) ⇒ SP.
specialize (SP ω _ H_tsk_in_ts j s).
feed_n 6%nat SP.
{ by apply/eqP; rewrite EQ. }
{ by eexists; apply H_arrivals_consistent; eassumption. }
{ by eexists; apply H_arrivals_consistent; eassumption. }
{ by apply/eqP. }
{ by apply/eqP. }
{ by rewrite //= /prosa.behavior.job.job_arrival /sample0_arrivals IN H_j_arrives_at_A //= ltnW //. }
rewrite //= /prosa.behavior.job.job_arrival /sample0_arrivals IN H_j_arrives_at_A //= in SP.
rewrite addn1; apply: leq_trans; last by apply SP.
by rewrite leq_add2l; apply H_constrained_deadlines.
}
}
Qed.
End TaskWorkloadBounded.
From prosa.analysis Require Export facts.model.workload.
From probsa.util Require Export misc.
From probsa.probability Require Export pred pmf.
From probsa.rt.behavior Require Export schedule.
From probsa.rt.model Require Export assumptions.basic.
Local Open Scope nat_scope.
Section PrWorkload.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Definition pr_workload_of_jobs (P : pred Job) (jobs : seq Job) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ @workload_of_jobs Job (sample0_costs ω) P jobs).
Definition pr_workload_of_task (tsk : Task) (t1 t2 : instant) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ pr_workload_of_jobs (job_of_task tsk) (pr_arrivals_between t1 t2 ω) ω).
Definition pr_workload_of_hep_tasks (tsk : Task) (t1 t2 : instant) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ pr_workload_of_jobs
(fun j ⇒ hep_task (job_task j) tsk)
(pr_arrivals_between t1 t2 ω)
ω
).
End PrWorkload.
Section WorkloadLemmasDetCostStocArr.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_cost : JobCost Job}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Variable tsk : Task.
Lemma workload_of_jobs_xpredT :
∀ (P : pred Job) (jobs : seq Job),
workload_of_jobs P jobs = workload_of_jobs xpredT [seq j <- jobs | P j].
Proof.
induction jobs.
{ by rewrite /workload_of_jobs big_nil //= big_nil. }
{ move: IHjobs; rewrite /workload_of_jobs big_cons ⇒ → ⇒ //=.
by destruct (P a) eqn:EQ; first rewrite big_cons. }
Qed.
Lemma workload_of_jobs_widen :
∀ (t1 t2 t1' t2' : nat) (ω : Ω),
t1' ≤ t1 →
t2 ≤ t2' →
workload_of_jobs (job_of_task tsk) (arrivals_between (arr_seq ω) t1 t2)
≤ workload_of_jobs (job_of_task tsk) (arrivals_between (arr_seq ω) t1' t2').
Proof.
intros.
have [LE|LE] := leqP t1 t2; last first.
{ rewrite /arrivals_between big_geq; try by apply ltnW.
by rewrite /workload_of_jobs big_nil.
}
rewrite [in X in (_ ≤ X)%nat](workload_of_jobs_cat _ t1); last first.
{ by apply/andP; split; [done | apply: leq_trans; eauto 1]. }
rewrite -[X in (X ≤ _)%nat]addn0 addnC leq_add //.
rewrite [in X in (_ ≤ X)%nat](workload_of_jobs_cat _ t2); last first.
{ apply/andP; split; [apply: leq_trans; eauto 1 | done]. }
by rewrite -[X in (X ≤ _)%nat]addn0 leq_add //.
Qed.
End WorkloadLemmasDetCostStocArr.
Section PrWorkloadCat.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Variable tsk : Task.
Lemma pr_workload_of_task_cat :
∀ (t1 t2 t : instant) (ω : Ω),
t1 ≤ t ≤ t2 →
pr_workload_of_task tsk t1 t2 ω
= pr_workload_of_task tsk t1 t ω + pr_workload_of_task tsk t t2 ω.
Proof.
intros; rewrite /pr_workload_of_task //=.
by erewrite workload_of_jobs_cat; last by eassumption.
Qed.
End PrWorkloadCat.
Section PrWorkloadFacts.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Variable ts : seq Task.
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
Hypothesis H_arrivals_from_ts : arrivals_from_task_set ts.
Lemma pr_hep_workload_pr_task_workload_split :
∀ (t1 t2 : instant) (ω : Ω),
pr_workload_of_hep_tasks tsk t1 t2 ω
≤ \sum_(tsko <- ts | hep_task tsko tsk) pr_workload_of_task tsko t1 t2 ω.
Proof.
intros; apply: leq_trans.
apply sum_over_partitions_le with (x_to_y := job_task) (ys := ts).
{ move ⇒ j.
rewrite /pr_arrivals_between //= ⇒ IN.
apply in_arrivals_implies_arrived in IN.
by apply: H_arrivals_from_ts; apply IN.
}
{ rewrite [in X in (_ ≤ X)%nat]big_mkcond //=; apply leq_sum ⇒ tsko _.
set (js := arrivals_between _ _ _).
induction js as [ | j js].
{ by rewrite big_nil. }
{ rewrite /workload_of_jobs !big_cons.
destruct (_ == _) eqn:EQ.
{ rewrite andbT /job_of_task EQ.
move: EQ ⇒ /eqP EQ; rewrite EQ.
by move: IHjs; destruct (hep_task _ _ ) ⇒ NEQ; first rewrite leq_add2l.
}
{ by rewrite andbF /job_of_task EQ; apply IHjs. }
}
}
Qed.
End PrWorkloadFacts.
Section TaskWorkloadBounded.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{P : SporadicModel Task}
{D : TaskDeadline Task}
{FP : FP_policy Task}.
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_arrivals_cost_consistent : arrivals_cost_consistent.
Hypothesis H_arrival_sequence_uniq : pr_arrival_sequence_uniq.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Variable (ts : seq Task) (tsk : Task).
Hypothesis H_tsk_in_ts : tsk \in ts.
Hypothesis H_arrivals_from_ts : arrivals_from_task_set ts.
Hypothesis H_inter_arrival_pos : valid_taskset_inter_arrival_times ts.
Hypothesis H_sporadic_arrivals : pr_taskset_respects_sporadic_task_model ts.
Hypothesis H_constrained_deadlines : constrained_deadlines ts.
Variable j : Job.
Variable ω : Ω.
Hypothesis H_arrives_in : arrives_in (arr_seq ω) j.
Hypothesis H_job_of_task : job_of_task tsk j.
Variable A : instant.
Hypothesis H_j_arrives_at_A : job_arrival j ω = Some A.
Lemma at_most_one_job_pending :
∀ t,
t ≤ D tsk →
pr_workload_of_task tsk A (A + t) ω ≤ odflt 0 (job_cost j ω).
Proof.
intros × LE; move: (H_arrives_in) ⇒ E.
destruct (D tsk) as [| d] eqn:EQD.
{ move: LE; rewrite leqn0 ⇒ /eqP EQ; subst t.
rewrite addn0 /pr_workload_of_task //=.
by rewrite /arrivals_between big_geq // /workload_of_jobs //= big_nil. }
apply H_arrivals_cost_consistent in H_arrives_in;
destruct (job_cost j _ ) as [c| ] eqn:EQC; [clear H_arrives_in | done].
apply: leq_trans; first apply workload_of_jobs_widen with (t1' := A) (t2' := (A + D tsk)%nat).
{ by done. }
{ by rewrite leq_add2l EQD. }
clear t LE; rewrite workload_of_jobs_xpredT.
have → :
[seq j0 <- arrivals_between (arr_seq ω) A (A + D tsk)%nat | job_of_task tsk j0] = [::j]; last first.
{ by rewrite /workload_of_jobs big_seq1 /prosa.behavior.job.job_cost /sample0_costs //= EQC. }
rewrite /arrivals_between EQD addnS big_nat_recl; last by rewrite leq_addr.
rewrite filter_cat -[RHS]cats0; f_equal.
{ clear d EQD c EQC; apply seq_filter_singleton.
{ by apply H_arrival_sequence_uniq. }
{ by done. }
{ by apply H_arrivals_consistent; rewrite H_j_arrives_at_A. }
{ intros s IN TSKs.
apply H_arrivals_consistent in IN.
apply/eqP/negPn/negP ⇒ /eqP NEQ.
move: (H_sporadic_arrivals) ⇒ SP.
specialize (SP ω _ H_tsk_in_ts _ _ NEQ).
feed_n 5%nat SP.
{ by eexists; apply H_arrivals_consistent; eassumption. }
{ by eexists; apply H_arrivals_consistent; eassumption. }
{ by apply/eqP. }
{ by apply/eqP. }
{ by rewrite //= /prosa.behavior.job.job_arrival /sample0_arrivals H_j_arrives_at_A IN //= ltnW. }
rewrite //= /prosa.behavior.job.job_arrival /sample0_arrivals H_j_arrives_at_A IN //= in SP.
move_neq_down SP.
rewrite -addn1 leq_add2l.
by apply H_inter_arrival_pos.
}
}
{ apply filter_in_pred0 ⇒ s IN.
apply mem_bigcat_nat_exists in IN; move: IN ⇒ [a [IN /andP [NEQA1 NEQA2]]].
apply H_arrivals_consistent in IN.
apply/negP ⇒ TSKs; move_neq_down NEQA2.
rewrite -(leq_add2r 1%nat) -addnA addn1 -EQD.
destruct (j == s) eqn:EQ.
{ move: EQ ⇒ /eqP EQ; subst s.
move: (H_j_arrives_at_A); rewrite IN ⇒ EQN; inversion EQN; subst A.
by rewrite ltnn in NEQA1.
}
{ move: (H_sporadic_arrivals) ⇒ SP.
specialize (SP ω _ H_tsk_in_ts j s).
feed_n 6%nat SP.
{ by apply/eqP; rewrite EQ. }
{ by eexists; apply H_arrivals_consistent; eassumption. }
{ by eexists; apply H_arrivals_consistent; eassumption. }
{ by apply/eqP. }
{ by apply/eqP. }
{ by rewrite //= /prosa.behavior.job.job_arrival /sample0_arrivals IN H_j_arrives_at_A //= ltnW //. }
rewrite //= /prosa.behavior.job.job_arrival /sample0_arrivals IN H_j_arrives_at_A //= in SP.
rewrite addn1; apply: leq_trans; last by apply SP.
by rewrite leq_add2l; apply H_constrained_deadlines.
}
}
Qed.
End TaskWorkloadBounded.