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.
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 ω.
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 ω.
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.
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.
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 ω.
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 ω.
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.
End SporadicFacts.
Global Opaque pr_carry_in_workload_of_hep_jobs.