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].
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').
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 ω.
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 ω.
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 ω).
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].
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').
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 ω.
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 ω.
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 ω).
End TaskWorkloadBounded.