Library prosa.classic.analysis.uni.basic.workload_bound_fp
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.priority
prosa.classic.model.arrival.basic.task_arrival prosa.classic.model.arrival.basic.arrival_bounds.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.workload.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
Module WorkloadBoundFP.
Import Job SporadicTaskset UniprocessorSchedule Priority Workload
TaskArrival ArrivalBounds.
Section SingleTask.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable tsk: Task.
Variable delta: time.
Definition max_jobs := div_ceil delta (task_period tsk).
Definition task_workload_bound_FP := max_jobs × task_cost tsk.
End SingleTask.
Section AllTasks.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable higher_eq_priority: FP_policy Task.
Variable ts: list Task.
Variable tsk: Task.
Variable delta: time.
Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
Let W tsk_other :=
task_workload_bound_FP task_cost task_period tsk_other delta.
Definition total_workload_bound_fp :=
\sum_(tsk_other <- ts | is_hep_task tsk_other) W tsk_other.
End AllTasks.
Section BasicLemmas.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_deadline: Task → time.
Variable higher_eq_priority: FP_policy Task.
Variable ts: list Task.
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Let workload_bound :=
total_workload_bound_fp task_cost task_period higher_eq_priority ts tsk.
Section NoSmallerThanCost.
Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
Hypothesis H_cost_positive: task_cost tsk > 0.
Hypothesis H_period_positive: task_period tsk > 0.
Lemma total_workload_bound_fp_ge_cost:
workload_bound (task_cost tsk) ≥ task_cost tsk.
Proof.
rename H_priority_is_reflexive into REFL.
unfold workload_bound, total_workload_bound_fp.
rewrite big_mkcond (big_rem tsk) /=; last by done.
rewrite REFL /task_workload_bound_FP.
apply leq_trans with (n := max_jobs task_period tsk (task_cost tsk) × task_cost tsk);
last by apply leq_addr.
rewrite -{1}[task_cost tsk]mul1n leq_mul2r; apply/orP; right.
by apply ceil_neq0.
Qed.
End NoSmallerThanCost.
Section NonDecreasing.
Hypothesis H_period_positive:
∀ tsk,
tsk \in ts →
task_period tsk > 0.
Lemma total_workload_bound_fp_non_decreasing:
∀ delta1 delta2,
delta1 ≤ delta2 →
workload_bound delta1 ≤ workload_bound delta2.
Proof.
unfold workload_bound, total_workload_bound_fp; intros d1 d2 LE.
apply leq_sum_seq; intros tsk' IN HP.
rewrite leq_mul2r; apply/orP; right.
apply leq_divceil2r; last by done.
by apply H_period_positive.
Qed.
End NonDecreasing.
End BasicLemmas.
Section ProofWorkloadBound.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_deadline: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → Task.
Variable ts: seq Task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Hypothesis H_sporadic_arrivals:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Variable higher_eq_priority: FP_policy Task.
Let arrivals_between := jobs_arrived_between arr_seq.
Let hp_workload t1 t2:=
workload_of_higher_or_equal_priority_tasks job_cost job_task (arrivals_between t1 t2)
higher_eq_priority tsk.
Let workload_bound :=
total_workload_bound_fp task_cost task_period higher_eq_priority ts tsk.
Variable R: time.
Hypothesis H_fixed_point: R = workload_bound R.
Lemma fp_workload_bound_holds:
∀ t,
hp_workload t (t + R) ≤ R.
Proof.
have BOUND := sporadic_task_arrival_bound task_period job_arrival job_task arr_seq.
feed_n 3 BOUND; try (by done).
rename H_fixed_point into FIX, H_all_jobs_from_taskset into FROMTS,
H_valid_job_parameters into JOBPARAMS,
H_valid_task_parameters into PARAMS.
unfold hp_workload, workload_of_higher_or_equal_priority_tasks,
valid_sporadic_job, valid_realtime_job,
valid_sporadic_taskset, is_valid_sporadic_task in ×.
intro t.
rewrite {2}FIX /workload_bound /total_workload_bound_fp.
set l := jobs_arrived_between arr_seq t (t + R).
set hep := higher_eq_priority.
apply leq_trans with (n := \sum_(tsk' <- ts | hep tsk' tsk)
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{
have EXCHANGE := exchange_big_dep (fun x ⇒ hep (job_task x) tsk).
rewrite EXCHANGE /=; last by move ⇒ tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ ≤ X]big_seq_cond.
apply leq_sum; move ⇒ j0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=;
first by rewrite HP0 andTb eq_refl; apply leq_addr.
by apply in_arrivals_implies_arrived in IN0; apply FROMTS.
}
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply leq_trans with (n := num_arrivals_of_task job_task arr_seq
tsk0 t (t + R) × task_cost tsk0).
{
rewrite /num_arrivals_of_task -sum1_size big_distrl /= big_filter.
apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.
rewrite -EQ mul1n.
feed (JOBPARAMS j0); first by eapply in_arrivals_implies_arrived; eauto 1.
by move: JOBPARAMS ⇒ [_ [LE _]].
}
rewrite /task_workload_bound_FP leq_mul2r; apply/orP; right.
feed (BOUND t (t + R) tsk0); first by feed (PARAMS tsk0); last by des.
by rewrite addKn in BOUND.
Qed.
End ProofWorkloadBound.
End WorkloadBoundFP.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.priority
prosa.classic.model.arrival.basic.task_arrival prosa.classic.model.arrival.basic.arrival_bounds.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.workload.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
Module WorkloadBoundFP.
Import Job SporadicTaskset UniprocessorSchedule Priority Workload
TaskArrival ArrivalBounds.
Section SingleTask.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable tsk: Task.
Variable delta: time.
Definition max_jobs := div_ceil delta (task_period tsk).
Definition task_workload_bound_FP := max_jobs × task_cost tsk.
End SingleTask.
Section AllTasks.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable higher_eq_priority: FP_policy Task.
Variable ts: list Task.
Variable tsk: Task.
Variable delta: time.
Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
Let W tsk_other :=
task_workload_bound_FP task_cost task_period tsk_other delta.
Definition total_workload_bound_fp :=
\sum_(tsk_other <- ts | is_hep_task tsk_other) W tsk_other.
End AllTasks.
Section BasicLemmas.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_deadline: Task → time.
Variable higher_eq_priority: FP_policy Task.
Variable ts: list Task.
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Let workload_bound :=
total_workload_bound_fp task_cost task_period higher_eq_priority ts tsk.
Section NoSmallerThanCost.
Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
Hypothesis H_cost_positive: task_cost tsk > 0.
Hypothesis H_period_positive: task_period tsk > 0.
Lemma total_workload_bound_fp_ge_cost:
workload_bound (task_cost tsk) ≥ task_cost tsk.
Proof.
rename H_priority_is_reflexive into REFL.
unfold workload_bound, total_workload_bound_fp.
rewrite big_mkcond (big_rem tsk) /=; last by done.
rewrite REFL /task_workload_bound_FP.
apply leq_trans with (n := max_jobs task_period tsk (task_cost tsk) × task_cost tsk);
last by apply leq_addr.
rewrite -{1}[task_cost tsk]mul1n leq_mul2r; apply/orP; right.
by apply ceil_neq0.
Qed.
End NoSmallerThanCost.
Section NonDecreasing.
Hypothesis H_period_positive:
∀ tsk,
tsk \in ts →
task_period tsk > 0.
Lemma total_workload_bound_fp_non_decreasing:
∀ delta1 delta2,
delta1 ≤ delta2 →
workload_bound delta1 ≤ workload_bound delta2.
Proof.
unfold workload_bound, total_workload_bound_fp; intros d1 d2 LE.
apply leq_sum_seq; intros tsk' IN HP.
rewrite leq_mul2r; apply/orP; right.
apply leq_divceil2r; last by done.
by apply H_period_positive.
Qed.
End NonDecreasing.
End BasicLemmas.
Section ProofWorkloadBound.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_deadline: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → Task.
Variable ts: seq Task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Hypothesis H_sporadic_arrivals:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Variable higher_eq_priority: FP_policy Task.
Let arrivals_between := jobs_arrived_between arr_seq.
Let hp_workload t1 t2:=
workload_of_higher_or_equal_priority_tasks job_cost job_task (arrivals_between t1 t2)
higher_eq_priority tsk.
Let workload_bound :=
total_workload_bound_fp task_cost task_period higher_eq_priority ts tsk.
Variable R: time.
Hypothesis H_fixed_point: R = workload_bound R.
Lemma fp_workload_bound_holds:
∀ t,
hp_workload t (t + R) ≤ R.
Proof.
have BOUND := sporadic_task_arrival_bound task_period job_arrival job_task arr_seq.
feed_n 3 BOUND; try (by done).
rename H_fixed_point into FIX, H_all_jobs_from_taskset into FROMTS,
H_valid_job_parameters into JOBPARAMS,
H_valid_task_parameters into PARAMS.
unfold hp_workload, workload_of_higher_or_equal_priority_tasks,
valid_sporadic_job, valid_realtime_job,
valid_sporadic_taskset, is_valid_sporadic_task in ×.
intro t.
rewrite {2}FIX /workload_bound /total_workload_bound_fp.
set l := jobs_arrived_between arr_seq t (t + R).
set hep := higher_eq_priority.
apply leq_trans with (n := \sum_(tsk' <- ts | hep tsk' tsk)
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{
have EXCHANGE := exchange_big_dep (fun x ⇒ hep (job_task x) tsk).
rewrite EXCHANGE /=; last by move ⇒ tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ ≤ X]big_seq_cond.
apply leq_sum; move ⇒ j0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=;
first by rewrite HP0 andTb eq_refl; apply leq_addr.
by apply in_arrivals_implies_arrived in IN0; apply FROMTS.
}
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply leq_trans with (n := num_arrivals_of_task job_task arr_seq
tsk0 t (t + R) × task_cost tsk0).
{
rewrite /num_arrivals_of_task -sum1_size big_distrl /= big_filter.
apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.
rewrite -EQ mul1n.
feed (JOBPARAMS j0); first by eapply in_arrivals_implies_arrived; eauto 1.
by move: JOBPARAMS ⇒ [_ [LE _]].
}
rewrite /task_workload_bound_FP leq_mul2r; apply/orP; right.
feed (BOUND t (t + R) tsk0); first by feed (PARAMS tsk0); last by des.
by rewrite addKn in BOUND.
Qed.
End ProofWorkloadBound.
End WorkloadBoundFP.