Library prosa.analysis.facts.sporadic.arrival_bound
Require Import prosa.util.all.
Require Export prosa.model.task.arrival.sporadic.
Require Export prosa.analysis.facts.model.task_arrivals.
Require Export prosa.model.task.arrival.sporadic.
Require Export prosa.analysis.facts.model.task_arrivals.
Sporadic Arrival Bound
Consider any sporadic tasks ...
... and their jobs.
We define the classic "ceiling of the interval length divided by
minimum inter-arrival time", which we prove to be correct in the
following.
Definition max_sporadic_arrivals (tsk : Task) (delta : duration) :=
div_ceil delta (task_min_inter_arrival_time tsk).
div_ceil delta (task_min_inter_arrival_time tsk).
To establish the bound's soundness, consider any well-formed
arrival sequence, ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
... and any valid sporadic task tsk to be analyzed.
Variable tsk : Task.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Before we can establish the bound, we require two auxiliary
bounds, which we derive next. First, we consider minimum offset
of the
n-th job of the task that arrives in a given interval.
For technical reasons, we require a "dummy" job in scope to
use the nth function. In the proofs, we establish that the
dummy job is never used, i.e., it is an irrelevant artifact
induced by the ssreflect API. It may be safely ignored.
We observe that the
i-th job to arrive in an interval [t1,t2)
arrives no earlier than (task_min_inter_arrival_time tsk) ×i
time units after the beginning of the interval due the minimum
inter-arrival time of the sporadic task.
Lemma arrival_of_nth_job :
∀ t1 t2 n i j,
n = number_of_task_arrivals arr_seq tsk t1 t2 →
i < n →
j = nth dummy (task_arrivals_between arr_seq tsk t1 t2) i →
job_arrival j ≥ t1 + (task_min_inter_arrival_time tsk) × i.
Proof.
move⇒ t1 t2 n i j. rewrite /number_of_task_arrivals.
case ARR : (task_arrivals_between arr_seq tsk t1 t2) ⇒ [|j' js'] → // LIM JOB.
elim: i LIM j JOB ⇒ [LIM j JOB|i IH LIM j JOB].
{ rewrite muln0 addn0.
apply: job_arrival_between_ge; eauto.
apply: (task_arrivals_between_subset _ tsk _ t2).
by rewrite JOB ARR; apply mem_nth. }
{ rewrite mulnSr addnA.
pose prev_j := nth dummy (j' :: js') i.
have prev_LIM : t1 + task_min_inter_arrival_time tsk × i + task_min_inter_arrival_time tsk
≤ job_arrival prev_j + task_min_inter_arrival_time tsk
by rewrite leq_add2r; apply IH ⇒ //; lia.
apply: (leq_trans prev_LIM).
have IN_j : j \in task_arrivals_between arr_seq tsk t1 t2
by rewrite JOB ARR; apply mem_nth.
have IN_prev : prev_j \in task_arrivals_between arr_seq tsk t1 t2
by rewrite /prev_j ARR; apply mem_nth; lia.
apply: H_sporadic_model ⇒ //=.
{ rewrite JOB /prev_j ⇒ /eqP.
rewrite nth_uniq; try lia; rewrite -ARR.
by apply: task_arrivals_between_uniq. }
{ by apply/in_arrivals_implies_arrived/(task_arrivals_between_subset _ tsk t1 t2). }
{ by apply/in_arrivals_implies_arrived/(task_arrivals_between_subset _ tsk t1 t2). }
{ apply: in_task_arrivals_between_implies_job_of_task.
exact IN_prev. }
{ apply: in_task_arrivals_between_implies_job_of_task.
exact: IN_j. }
{ rewrite /prev_j JOB.
have SORTED : sorted by_arrival_times (j' :: js')
by rewrite -ARR; apply task_arrivals_between_sorted.
eapply (sorted_leq_nth _ _ _ SORTED); try lia.
- rewrite unfold_in simpl_predE; lia.
- rewrite unfold_in simpl_predE; lia. } }
Unshelve. all: by rewrite /by_arrival_times/transitive/reflexive; lia.
Qed.
End NthJob.
∀ t1 t2 n i j,
n = number_of_task_arrivals arr_seq tsk t1 t2 →
i < n →
j = nth dummy (task_arrivals_between arr_seq tsk t1 t2) i →
job_arrival j ≥ t1 + (task_min_inter_arrival_time tsk) × i.
Proof.
move⇒ t1 t2 n i j. rewrite /number_of_task_arrivals.
case ARR : (task_arrivals_between arr_seq tsk t1 t2) ⇒ [|j' js'] → // LIM JOB.
elim: i LIM j JOB ⇒ [LIM j JOB|i IH LIM j JOB].
{ rewrite muln0 addn0.
apply: job_arrival_between_ge; eauto.
apply: (task_arrivals_between_subset _ tsk _ t2).
by rewrite JOB ARR; apply mem_nth. }
{ rewrite mulnSr addnA.
pose prev_j := nth dummy (j' :: js') i.
have prev_LIM : t1 + task_min_inter_arrival_time tsk × i + task_min_inter_arrival_time tsk
≤ job_arrival prev_j + task_min_inter_arrival_time tsk
by rewrite leq_add2r; apply IH ⇒ //; lia.
apply: (leq_trans prev_LIM).
have IN_j : j \in task_arrivals_between arr_seq tsk t1 t2
by rewrite JOB ARR; apply mem_nth.
have IN_prev : prev_j \in task_arrivals_between arr_seq tsk t1 t2
by rewrite /prev_j ARR; apply mem_nth; lia.
apply: H_sporadic_model ⇒ //=.
{ rewrite JOB /prev_j ⇒ /eqP.
rewrite nth_uniq; try lia; rewrite -ARR.
by apply: task_arrivals_between_uniq. }
{ by apply/in_arrivals_implies_arrived/(task_arrivals_between_subset _ tsk t1 t2). }
{ by apply/in_arrivals_implies_arrived/(task_arrivals_between_subset _ tsk t1 t2). }
{ apply: in_task_arrivals_between_implies_job_of_task.
exact IN_prev. }
{ apply: in_task_arrivals_between_implies_job_of_task.
exact: IN_j. }
{ rewrite /prev_j JOB.
have SORTED : sorted by_arrival_times (j' :: js')
by rewrite -ARR; apply task_arrivals_between_sorted.
eapply (sorted_leq_nth _ _ _ SORTED); try lia.
- rewrite unfold_in simpl_predE; lia.
- rewrite unfold_in simpl_predE; lia. } }
Unshelve. all: by rewrite /by_arrival_times/transitive/reflexive; lia.
Qed.
End NthJob.
As a second auxiliary lemma, we establish a minimum length on
the interval for a given number of arrivals by applying the
previous lemma to the last job in the interval. We consider only
the case of "many" jobs, i.e., n ≥ 2, which ensures that the
interval
[t1, t2) spans at least one inter-arrival time.
Lemma minimum_distance_for_n_sporadic_arrivals:
∀ t1 t2 n,
number_of_task_arrivals arr_seq tsk t1 t2 = n →
n ≥ 2 →
t2 > t1 + (task_min_inter_arrival_time tsk) × n.-1.
Proof.
move⇒ t1 t2 n H_num_arrivals H_many_jobs.
(* First, let us get ourselves a job so we can discharge the dummy job parameter. *)
destruct (task_arrivals_between arr_seq tsk t1 t2) as [|j js] eqn:ARR;
first by move: ARR H_num_arrivals H_many_jobs; rewrite /number_of_task_arrivals ⇒ → //= ->; lia.
(* Now that we can use nth, let's proceed with the actual proof. *)
set j_last := (nth j (task_arrivals_between arr_seq tsk t1 t2) n.-1).
have LAST : job_arrival j_last < t2.
{ apply: job_arrival_between_lt; eauto.
apply: task_arrivals_between_subset.
apply mem_nth.
by move: H_num_arrivals; rewrite /number_of_task_arrivals ⇒ ->; lia. }
have DIST : t1 + task_min_inter_arrival_time tsk × n.-1 ≤ job_arrival j_last.
{ apply: arrival_of_nth_job; auto;
first by rewrite [number_of_task_arrivals arr_seq tsk t1 _]H_num_arrivals; lia.
by rewrite /j_last //=. }
by lia.
Qed.
∀ t1 t2 n,
number_of_task_arrivals arr_seq tsk t1 t2 = n →
n ≥ 2 →
t2 > t1 + (task_min_inter_arrival_time tsk) × n.-1.
Proof.
move⇒ t1 t2 n H_num_arrivals H_many_jobs.
(* First, let us get ourselves a job so we can discharge the dummy job parameter. *)
destruct (task_arrivals_between arr_seq tsk t1 t2) as [|j js] eqn:ARR;
first by move: ARR H_num_arrivals H_many_jobs; rewrite /number_of_task_arrivals ⇒ → //= ->; lia.
(* Now that we can use nth, let's proceed with the actual proof. *)
set j_last := (nth j (task_arrivals_between arr_seq tsk t1 t2) n.-1).
have LAST : job_arrival j_last < t2.
{ apply: job_arrival_between_lt; eauto.
apply: task_arrivals_between_subset.
apply mem_nth.
by move: H_num_arrivals; rewrite /number_of_task_arrivals ⇒ ->; lia. }
have DIST : t1 + task_min_inter_arrival_time tsk × n.-1 ≤ job_arrival j_last.
{ apply: arrival_of_nth_job; auto;
first by rewrite [number_of_task_arrivals arr_seq tsk t1 _]H_num_arrivals; lia.
by rewrite /j_last //=. }
by lia.
Qed.
Based on the above lemma, it is easy to see that
max_sporadic_arrivals is indeed a correct upper bound on the
maximum number of arrivals in a given interval.
Theorem sporadic_task_arrivals_bound:
∀ t1 t2,
number_of_task_arrivals arr_seq tsk t1 t2 ≤ max_sporadic_arrivals tsk (t2 - t1).
Proof.
move⇒ t1 t2.
case COUNT: (number_of_task_arrivals arr_seq tsk t1 t2) ⇒ // [n'].
case COUNT: n' COUNT ⇒ // [|n] NARR.
{ (* one arrival *)
apply div_ceil_gt0 ⇒ //; rewrite subn_gt0.
by eapply number_of_task_arrivals_nonzero; eauto. }
{ (* two or more arrivals *)
clear n' COUNT.
move: NARR. set n' := n.+2 ⇒ NARR.
have SEP: t2 > t1 + (task_min_inter_arrival_time tsk) × n'.-1
by apply: minimum_distance_for_n_sporadic_arrivals.
move: SEP. rewrite -ltn_subRL ⇒ SEP.
by apply: div_ceil_multiple. }
Qed.
End SporadicArrivalBound.
∀ t1 t2,
number_of_task_arrivals arr_seq tsk t1 t2 ≤ max_sporadic_arrivals tsk (t2 - t1).
Proof.
move⇒ t1 t2.
case COUNT: (number_of_task_arrivals arr_seq tsk t1 t2) ⇒ // [n'].
case COUNT: n' COUNT ⇒ // [|n] NARR.
{ (* one arrival *)
apply div_ceil_gt0 ⇒ //; rewrite subn_gt0.
by eapply number_of_task_arrivals_nonzero; eauto. }
{ (* two or more arrivals *)
clear n' COUNT.
move: NARR. set n' := n.+2 ⇒ NARR.
have SEP: t2 > t1 + (task_min_inter_arrival_time tsk) × n'.-1
by apply: minimum_distance_for_n_sporadic_arrivals.
move: SEP. rewrite -ltn_subRL ⇒ SEP.
by apply: div_ceil_multiple. }
Qed.
End SporadicArrivalBound.