Library prosa.classic.analysis.uni.jitter.workload_bound_fp
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.priority.
Require Import prosa.classic.model.arrival.jitter.job
prosa.classic.model.arrival.jitter.task_arrival
prosa.classic.model.arrival.jitter.arrival_bounds.
Require Import prosa.classic.model.schedule.uni.workload.
Require Import prosa.classic.model.schedule.uni.jitter.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
Module WorkloadBoundFP.
Import JobWithJitter SporadicTaskset UniprocessorScheduleWithJitter Priority Workload
TaskArrivalWithJitter ArrivalBounds.
Section SingleTask.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
Variable tsk: Task.
Variable delta: time.
Definition max_jobs := div_ceil (delta + task_jitter tsk) (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 task_jitter: 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 task_jitter 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 task_jitter: 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 task_jitter 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 task_jitter
tsk (task_cost tsk) × task_cost tsk);
last by apply leq_addr.
rewrite -{1}[task_cost tsk]mul1n leq_mul2r; apply/orP; right.
apply ceil_neq0; last by done.
by apply leq_trans with (n := task_cost tsk); last by apply leq_addr.
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.
by apply leq_divceil2r; [by apply H_period_positive | by rewrite leq_add2r].
Qed.
End NonDecreasing.
End BasicLemmas.
Section ProofWorkloadBound.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → Task.
Variable ts: seq Task.
Hypothesis H_positive_periods:
∀ tsk, tsk \in ts → task_period tsk > 0.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
Let actual_arrivals := actual_arrivals_between job_arrival job_jitter arr_seq.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_job_cost_le_task_cost:
∀ j,
arrives_in arr_seq j →
job_cost j ≤ task_cost (job_task j).
Hypothesis H_job_jitter_le_task_jitter:
∀ j,
arrives_in arr_seq j →
job_jitter j ≤ task_jitter (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 actual_hp_workload t1 t2 :=
workload_of_higher_or_equal_priority_tasks job_cost job_task (actual_arrivals t1 t2)
higher_eq_priority tsk.
Let workload_bound :=
total_workload_bound_fp task_cost task_period task_jitter higher_eq_priority ts tsk.
Variable R: time.
Hypothesis H_fixed_point: R = workload_bound R.
Lemma fp_workload_bound_holds:
∀ t,
actual_hp_workload t (t + R) ≤ R.
Proof.
rename H_fixed_point into FIX, H_all_jobs_from_taskset into FROMTS,
H_arrival_times_are_consistent into CONS, H_arrival_sequence_is_a_set into SET.
unfold actual_hp_workload, workload_of_higher_or_equal_priority_tasks,
valid_sporadic_job_with_jitter, valid_sporadic_job, valid_realtime_job,
valid_sporadic_taskset, is_valid_sporadic_task in ×.
have BOUND := sporadic_task_with_jitter_arrival_bound task_period task_jitter job_arrival
job_jitter job_task arr_seq CONS SET.
feed_n 2 BOUND; (try by done).
intro t.
rewrite {2}FIX /workload_bound /total_workload_bound_fp.
set l := actual_arrivals_between job_arrival job_jitter 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.
rewrite mem_filter in IN0; move: IN0 ⇒ /andP [_ ARR0].
by apply in_arrivals_implies_arrived in ARR0; apply FROMTS.
}
apply leq_sum_seq; intros tsk0 IN0 HP0.
apply leq_trans with (n := num_actual_arrivals_of_task job_arrival job_jitter job_task arr_seq
tsk0 t (t + R) × task_cost tsk0).
{
rewrite /num_actual_arrivals_of_task -sum1_size big_distrl /= big_filter.
apply leq_sum_seq; move ⇒ j1 IN1 /eqP EQ.
rewrite -EQ mul1n; apply H_job_cost_le_task_cost.
rewrite mem_filter in IN1; move: IN1 ⇒ /andP [_ ARR1].
by apply in_arrivals_implies_arrived in ARR1.
}
rewrite /task_workload_bound_FP leq_mul2r; apply/orP; right.
feed (BOUND t (t + R) tsk0); first by apply H_positive_periods.
by rewrite -addnA addKn in BOUND.
Qed.
End ProofWorkloadBound.
End WorkloadBoundFP.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.priority.
Require Import prosa.classic.model.arrival.jitter.job
prosa.classic.model.arrival.jitter.task_arrival
prosa.classic.model.arrival.jitter.arrival_bounds.
Require Import prosa.classic.model.schedule.uni.workload.
Require Import prosa.classic.model.schedule.uni.jitter.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
Module WorkloadBoundFP.
Import JobWithJitter SporadicTaskset UniprocessorScheduleWithJitter Priority Workload
TaskArrivalWithJitter ArrivalBounds.
Section SingleTask.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
Variable tsk: Task.
Variable delta: time.
Definition max_jobs := div_ceil (delta + task_jitter tsk) (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 task_jitter: 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 task_jitter 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 task_jitter: 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 task_jitter 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 task_jitter
tsk (task_cost tsk) × task_cost tsk);
last by apply leq_addr.
rewrite -{1}[task_cost tsk]mul1n leq_mul2r; apply/orP; right.
apply ceil_neq0; last by done.
by apply leq_trans with (n := task_cost tsk); last by apply leq_addr.
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.
by apply leq_divceil2r; [by apply H_period_positive | by rewrite leq_add2r].
Qed.
End NonDecreasing.
End BasicLemmas.
Section ProofWorkloadBound.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → Task.
Variable ts: seq Task.
Hypothesis H_positive_periods:
∀ tsk, tsk \in ts → task_period tsk > 0.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
Let actual_arrivals := actual_arrivals_between job_arrival job_jitter arr_seq.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_job_cost_le_task_cost:
∀ j,
arrives_in arr_seq j →
job_cost j ≤ task_cost (job_task j).
Hypothesis H_job_jitter_le_task_jitter:
∀ j,
arrives_in arr_seq j →
job_jitter j ≤ task_jitter (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 actual_hp_workload t1 t2 :=
workload_of_higher_or_equal_priority_tasks job_cost job_task (actual_arrivals t1 t2)
higher_eq_priority tsk.
Let workload_bound :=
total_workload_bound_fp task_cost task_period task_jitter higher_eq_priority ts tsk.
Variable R: time.
Hypothesis H_fixed_point: R = workload_bound R.
Lemma fp_workload_bound_holds:
∀ t,
actual_hp_workload t (t + R) ≤ R.
Proof.
rename H_fixed_point into FIX, H_all_jobs_from_taskset into FROMTS,
H_arrival_times_are_consistent into CONS, H_arrival_sequence_is_a_set into SET.
unfold actual_hp_workload, workload_of_higher_or_equal_priority_tasks,
valid_sporadic_job_with_jitter, valid_sporadic_job, valid_realtime_job,
valid_sporadic_taskset, is_valid_sporadic_task in ×.
have BOUND := sporadic_task_with_jitter_arrival_bound task_period task_jitter job_arrival
job_jitter job_task arr_seq CONS SET.
feed_n 2 BOUND; (try by done).
intro t.
rewrite {2}FIX /workload_bound /total_workload_bound_fp.
set l := actual_arrivals_between job_arrival job_jitter 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.
rewrite mem_filter in IN0; move: IN0 ⇒ /andP [_ ARR0].
by apply in_arrivals_implies_arrived in ARR0; apply FROMTS.
}
apply leq_sum_seq; intros tsk0 IN0 HP0.
apply leq_trans with (n := num_actual_arrivals_of_task job_arrival job_jitter job_task arr_seq
tsk0 t (t + R) × task_cost tsk0).
{
rewrite /num_actual_arrivals_of_task -sum1_size big_distrl /= big_filter.
apply leq_sum_seq; move ⇒ j1 IN1 /eqP EQ.
rewrite -EQ mul1n; apply H_job_cost_le_task_cost.
rewrite mem_filter in IN1; move: IN1 ⇒ /andP [_ ARR1].
by apply in_arrivals_implies_arrived in ARR1.
}
rewrite /task_workload_bound_FP leq_mul2r; apply/orP; right.
feed (BOUND t (t + R) tsk0); first by apply H_positive_periods.
by rewrite -addnA addKn in BOUND.
Qed.
End ProofWorkloadBound.
End WorkloadBoundFP.