Library probsa.rt.model.carry_in
From probsa.rt.behavior Require Export service.
From probsa.rt.model Require Export workload.
Local Open Scope nat_scope.
Section BeforeDeadline.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_deadline : JobDeadlineRV Job Ω μ}.
Definition before_deadline (j : Job) (ω : Ω) (t : instant) :=
t < odflt0 (job_deadline j) ω.
Lemma before_deadline_monotone :
∀ (t1 t2 : instant) (j : Job) (ω : Ω),
t1 ≥ t2 →
before_deadline j ω t1 →
before_deadline j ω t2.
Proof.
by intros × LE; apply leq_trans.
Qed.
End BeforeDeadline.
Section PrPendWorkload.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_deadline : JobDeadlineRV Job Ω μ}
{job_task : JobTask Job Task}.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Definition pr_pend_workload (P : pred Job) (t : instant) : rvar μ [eqType of work] :=
mkRvar
μ (
fun ω ⇒
\sum_(j <- pr_arrivals_between 0 t.+1 ω | before_deadline j ω t && P j)
pr_remaining_service pr_sched j t ω
).
Definition pr_pend_workload_of_task (tsk : Task) (t : instant) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ pr_pend_workload (job_of_task tsk) t ω).
Definition pr_pend_workload_of_hep_jobs (tsk : Task) (t : instant) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ pr_pend_workload (fun j ⇒ hep_task (job_task j) tsk) t ω).
End PrPendWorkload.
Section PrCarryInWorkload.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_deadline : JobDeadlineRV Job Ω μ}
{job_task : JobTask Job Task}.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Definition pr_carry_in_workload (P : pred Job) (t : instant) : rvar μ [eqType of work] :=
mkRvar
μ (
fun ω ⇒
\sum_(j <- pr_arrivals_between 0 t ω | before_deadline j ω t && P j)
pr_remaining_service pr_sched j t ω
).
Definition pr_carry_in_workload_of_task (tsk : Task) (t : instant) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ pr_carry_in_workload (job_of_task tsk) t ω).
Definition pr_carry_in_workload_of_hep_jobs (tsk : Task) (t : instant) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ pr_carry_in_workload (fun j ⇒ hep_task (job_task j) tsk) t ω).
End PrCarryInWorkload.
Section PrCarryInWorkloadFacts.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{D : TaskDeadline Task}
{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.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Hypothesis H_arrivals_from_ts : arrivals_from_task_set ts.
Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.
Lemma pr_hep_carry_in_workload_split :
∀ (t : instant) (ω : Ω),
pr_carry_in_workload_of_hep_jobs pr_sched tsk t ω
≤ \sum_(tsko <- ts | hep_task tsko tsk)
pr_carry_in_workload_of_task pr_sched tsko t ω.
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.
unfold arrivals_between. simpl.
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.
move: IHjs; destruct (hep_task _ _ ) ⇒ NEQ; last by rewrite andbF //.
by destruct (before_deadline _ _ _)%nat ⇒ //=; rewrite leq_add2l.
}
{ rewrite andbF; move: IHjs; destruct (hep_task _ _ ) ⇒ NEQ ⇒ //.
by rewrite /job_of_task EQ andbF.
}
}
}
Qed.
Lemma pr_carry_in_workload_bounded_pr_pend_workload :
∀ (t : instant) (ω : Ω),
pr_carry_in_workload_of_task pr_sched tsk t ω
≤ pr_workload_of_task tsk (t - D tsk) t ω.
Proof.
intros.
rewrite /pr_carry_in_workload_of_task /pr_workload_of_task ⇒ //=.
rewrite big_mkcond //= /workload_of_jobs [in X in (_ ≤ X)%nat]big_mkcond //=.
rewrite (arrivals_between_cat _ _ (t - D tsk)%nat); [ | by done | by rewrite leq_subr ].
rewrite big_cat //= -[X in (_ ≤ X)%nat]add0n leq_add //.
{ rewrite leqn0; apply/eqP; rewrite big1_seq // ⇒ j /andP [_ IN].
destruct (before_deadline _ _ _)%nat eqn:DDLN ⇒ //.
destruct (job_of_task tsk _) eqn:TSK ⇒ //.
move: (IN) (IN) ⇒ LE NEQ; apply in_arrivals_implies_arrived in IN.
apply mem_bigcat_nat_exists in LE; move: LE ⇒ [A [EQA /andP [_ NEQA]]].
apply H_arrivals_consistent in EQA.
rewrite /before_deadline //= EQA //= in DDLN.
move_neq_down NEQA.
rewrite leq_subLR addnC ltnW //.
by move: TSK DDLN ; rewrite /task_deadline ⇒ /eqP →.
}
{ apply leq_sum ⇒ j _.
unfold prosa.behavior.job.job_cost, sample0_costs.
destruct (before_deadline _ _ _)%nat eqn:DD ⇒ //=.
destruct (job_of_task tsk _) eqn:TSK ⇒ //=.
by destruct (job_cost j ω) as [C | ] eqn:EQ; rewrite EQ //= leq_subr.
}
Qed.
End PrCarryInWorkloadFacts.
Section SporadicFacts.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{D : TaskDeadline Task}
{P : SporadicModel 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.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.
Hypothesis H_sporadic_tasks : pr_taskset_respects_sporadic_task_model ts.
Hypothesis H_constrained_deadlines : constrained_deadlines ts.
Lemma no_carry_in_at_task_arrival :
∀ (j : Job) (A : duration) (ω : Ω),
job_arrival j ω = Some A →
job_of_task tsk j →
pr_carry_in_workload_of_task pr_sched tsk A ω = 0.
Proof.
intros j a ω EQ TSK; unfold pr_carry_in_workload_of_task.
apply big1_seq. rewrite //= ⇒ s /andP [/andP [A B] IN]; exfalso.
apply mem_bigcat_nat_exists in IN; move: IN ⇒ [a' [IN /andP [_ NEQ]]].
apply H_arrivals_consistent in IN.
rewrite /before_deadline //= IN //= in A.
specialize (H_sporadic_tasks ω _ H_tsk_in_ts s j).
feed_n 6%nat H_sporadic_tasks.
{ intros EQjs; subst s.
rewrite EQ in IN; inversion IN; subst a'.
by rewrite ltnn in NEQ. }
{ 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 EQ IN //= ltnW. }
move: (H_sporadic_tasks) ⇒ SP.
rewrite //= /prosa.behavior.job.job_arrival /sample0_arrivals EQ IN //= in SP.
move: (leq_ltn_trans SP A); rewrite ltn_add2l ltnNge; move: B ⇒ /eqP →.
by rewrite /task_deadline H_constrained_deadlines //=.
Qed.
End SporadicFacts.
Global Opaque pr_carry_in_workload_of_hep_jobs.
From probsa.rt.model Require Export workload.
Local Open Scope nat_scope.
Section BeforeDeadline.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_deadline : JobDeadlineRV Job Ω μ}.
Definition before_deadline (j : Job) (ω : Ω) (t : instant) :=
t < odflt0 (job_deadline j) ω.
Lemma before_deadline_monotone :
∀ (t1 t2 : instant) (j : Job) (ω : Ω),
t1 ≥ t2 →
before_deadline j ω t1 →
before_deadline j ω t2.
Proof.
by intros × LE; apply leq_trans.
Qed.
End BeforeDeadline.
Section PrPendWorkload.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_deadline : JobDeadlineRV Job Ω μ}
{job_task : JobTask Job Task}.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Definition pr_pend_workload (P : pred Job) (t : instant) : rvar μ [eqType of work] :=
mkRvar
μ (
fun ω ⇒
\sum_(j <- pr_arrivals_between 0 t.+1 ω | before_deadline j ω t && P j)
pr_remaining_service pr_sched j t ω
).
Definition pr_pend_workload_of_task (tsk : Task) (t : instant) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ pr_pend_workload (job_of_task tsk) t ω).
Definition pr_pend_workload_of_hep_jobs (tsk : Task) (t : instant) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ pr_pend_workload (fun j ⇒ hep_task (job_task j) tsk) t ω).
End PrPendWorkload.
Section PrCarryInWorkload.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{FP : FP_policy Task}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_deadline : JobDeadlineRV Job Ω μ}
{job_task : JobTask Job Task}.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Definition pr_carry_in_workload (P : pred Job) (t : instant) : rvar μ [eqType of work] :=
mkRvar
μ (
fun ω ⇒
\sum_(j <- pr_arrivals_between 0 t ω | before_deadline j ω t && P j)
pr_remaining_service pr_sched j t ω
).
Definition pr_carry_in_workload_of_task (tsk : Task) (t : instant) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ pr_carry_in_workload (job_of_task tsk) t ω).
Definition pr_carry_in_workload_of_hep_jobs (tsk : Task) (t : instant) : rvar μ [eqType of work] :=
mkRvar μ (fun ω ⇒ pr_carry_in_workload (fun j ⇒ hep_task (job_task j) tsk) t ω).
End PrCarryInWorkload.
Section PrCarryInWorkloadFacts.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{D : TaskDeadline Task}
{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.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Hypothesis H_arrivals_from_ts : arrivals_from_task_set ts.
Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.
Lemma pr_hep_carry_in_workload_split :
∀ (t : instant) (ω : Ω),
pr_carry_in_workload_of_hep_jobs pr_sched tsk t ω
≤ \sum_(tsko <- ts | hep_task tsko tsk)
pr_carry_in_workload_of_task pr_sched tsko t ω.
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.
unfold arrivals_between. simpl.
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.
move: IHjs; destruct (hep_task _ _ ) ⇒ NEQ; last by rewrite andbF //.
by destruct (before_deadline _ _ _)%nat ⇒ //=; rewrite leq_add2l.
}
{ rewrite andbF; move: IHjs; destruct (hep_task _ _ ) ⇒ NEQ ⇒ //.
by rewrite /job_of_task EQ andbF.
}
}
}
Qed.
Lemma pr_carry_in_workload_bounded_pr_pend_workload :
∀ (t : instant) (ω : Ω),
pr_carry_in_workload_of_task pr_sched tsk t ω
≤ pr_workload_of_task tsk (t - D tsk) t ω.
Proof.
intros.
rewrite /pr_carry_in_workload_of_task /pr_workload_of_task ⇒ //=.
rewrite big_mkcond //= /workload_of_jobs [in X in (_ ≤ X)%nat]big_mkcond //=.
rewrite (arrivals_between_cat _ _ (t - D tsk)%nat); [ | by done | by rewrite leq_subr ].
rewrite big_cat //= -[X in (_ ≤ X)%nat]add0n leq_add //.
{ rewrite leqn0; apply/eqP; rewrite big1_seq // ⇒ j /andP [_ IN].
destruct (before_deadline _ _ _)%nat eqn:DDLN ⇒ //.
destruct (job_of_task tsk _) eqn:TSK ⇒ //.
move: (IN) (IN) ⇒ LE NEQ; apply in_arrivals_implies_arrived in IN.
apply mem_bigcat_nat_exists in LE; move: LE ⇒ [A [EQA /andP [_ NEQA]]].
apply H_arrivals_consistent in EQA.
rewrite /before_deadline //= EQA //= in DDLN.
move_neq_down NEQA.
rewrite leq_subLR addnC ltnW //.
by move: TSK DDLN ; rewrite /task_deadline ⇒ /eqP →.
}
{ apply leq_sum ⇒ j _.
unfold prosa.behavior.job.job_cost, sample0_costs.
destruct (before_deadline _ _ _)%nat eqn:DD ⇒ //=.
destruct (job_of_task tsk _) eqn:TSK ⇒ //=.
by destruct (job_cost j ω) as [C | ] eqn:EQ; rewrite EQ //= leq_subr.
}
Qed.
End PrCarryInWorkloadFacts.
Section SporadicFacts.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}
{D : TaskDeadline Task}
{P : SporadicModel 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.
Context {PState : ProcessorState Job}.
Variable pr_sched : pr_schedule μ PState.
Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.
Hypothesis H_sporadic_tasks : pr_taskset_respects_sporadic_task_model ts.
Hypothesis H_constrained_deadlines : constrained_deadlines ts.
Lemma no_carry_in_at_task_arrival :
∀ (j : Job) (A : duration) (ω : Ω),
job_arrival j ω = Some A →
job_of_task tsk j →
pr_carry_in_workload_of_task pr_sched tsk A ω = 0.
Proof.
intros j a ω EQ TSK; unfold pr_carry_in_workload_of_task.
apply big1_seq. rewrite //= ⇒ s /andP [/andP [A B] IN]; exfalso.
apply mem_bigcat_nat_exists in IN; move: IN ⇒ [a' [IN /andP [_ NEQ]]].
apply H_arrivals_consistent in IN.
rewrite /before_deadline //= IN //= in A.
specialize (H_sporadic_tasks ω _ H_tsk_in_ts s j).
feed_n 6%nat H_sporadic_tasks.
{ intros EQjs; subst s.
rewrite EQ in IN; inversion IN; subst a'.
by rewrite ltnn in NEQ. }
{ 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 EQ IN //= ltnW. }
move: (H_sporadic_tasks) ⇒ SP.
rewrite //= /prosa.behavior.job.job_arrival /sample0_arrivals EQ IN //= in SP.
move: (leq_ltn_trans SP A); rewrite ltn_add2l ltnNge; move: B ⇒ /eqP →.
by rewrite /task_deadline H_constrained_deadlines //=.
Qed.
End SporadicFacts.
Global Opaque pr_carry_in_workload_of_hep_jobs.