Library probsa.util.prosa.arrival_bound
Require Import prosa.util.all.
Require Export prosa.model.task.arrival.sporadic.
Require Export prosa.analysis.facts.model.task_arrivals.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
Require Export prosa.model.task.arrival.sporadic.
Require Export prosa.analysis.facts.model.task_arrivals.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
Lemma div_ceil_multiple :
∀ Δ T n,
T > 0 →
(T × n) < Δ →
n < div_ceil Δ T.
Proof.
move⇒ delta T n GT0 LT.
rewrite /div_ceil.
case DIV: (T %| delta);
first by rewrite -(ltn_pmul2l GT0) [_ × (_ %/ _)]mulnC divnK.
rewrite -[(_ %/ _).+1]addn1 -divnDMl // -(ltn_pmul2l GT0) [_ × (_ %/ _)]mulnC mul1n.
rewrite divnDr // mulnDl (@divnK _ T) //.
rewrite -{4}[T]mul1n -mulnDl addn1.
apply: leq_ltn_trans; last first.
{ by apply ltn_ceil. }
{ by apply ltnW. }
Qed.
∀ Δ T n,
T > 0 →
(T × n) < Δ →
n < div_ceil Δ T.
Proof.
move⇒ delta T n GT0 LT.
rewrite /div_ceil.
case DIV: (T %| delta);
first by rewrite -(ltn_pmul2l GT0) [_ × (_ %/ _)]mulnC divnK.
rewrite -[(_ %/ _).+1]addn1 -divnDMl // -(ltn_pmul2l GT0) [_ × (_ %/ _)]mulnC mul1n.
rewrite divnDr // mulnDl (@divnK _ T) //.
rewrite -{4}[T]mul1n -mulnDl addn1.
apply: leq_ltn_trans; last first.
{ by apply ltn_ceil. }
{ by apply ltnW. }
Qed.
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_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence 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.
Section ArrivalTimes.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Section ArrivalTimes.
Similarly, to simplify subsequent proofs, we restate the
H_consistent_arrival_times assumption as a trivial
corollary.
Lemma job_arrival_at :
∀ {j t},
j \in arrivals_at arr_seq t → job_arrival j = t.
Proof. by apply H_valid_arrival_sequence. Qed.
∀ {j t},
j \in arrivals_at arr_seq t → job_arrival j = t.
Proof. by apply H_valid_arrival_sequence. Qed.
We observe that, by construction, the sequence of arrivals is
sorted by arrival times. To this end, we first define the
order relation.
Trivially, the arrivals at any one point in time are ordered
w.r.t. arrival times.
Lemma arrivals_at_sorted :
∀ t,
sorted by_arrival_times (arrivals_at arr_seq t).
Proof.
move⇒ t.
have AT_t : ∀ j, j \in (arrivals_at arr_seq t) → job_arrival j = t
by move⇒ j; apply job_arrival_at.
case: (arrivals_at arr_seq t) AT_t ⇒ // j' js AT_t.
apply /(pathP j') ⇒ i LT.
rewrite /by_arrival_times !AT_t //;
last by apply mem_nth; auto.
rewrite in_cons; apply /orP; right.
by exact: mem_nth.
Qed.
∀ t,
sorted by_arrival_times (arrivals_at arr_seq t).
Proof.
move⇒ t.
have AT_t : ∀ j, j \in (arrivals_at arr_seq t) → job_arrival j = t
by move⇒ j; apply job_arrival_at.
case: (arrivals_at arr_seq t) AT_t ⇒ // j' js AT_t.
apply /(pathP j') ⇒ i LT.
rewrite /by_arrival_times !AT_t //;
last by apply mem_nth; auto.
rewrite in_cons; apply /orP; right.
by exact: mem_nth.
Qed.
By design, the list of arrivals in any interval is sorted.
Lemma arrivals_between_sorted :
∀ t1 t2,
sorted by_arrival_times (arrivals_between arr_seq t1 t2).
Proof.
move⇒ t1 t2.
rewrite /arrivals_between.
elim: t2 ⇒ [|t2 SORTED];
first by rewrite big_nil.
case: (leqP t1 t2) ⇒ T1T2;
last by rewrite big_geq.
rewrite (big_cat_nat _ _ _ T1T2 _) //=.
case A1: (\cat_(t1≤t<t2)arrivals_at arr_seq t) ⇒ [|j js];
first by rewrite cat0s big_nat1; exact: arrivals_at_sorted.
have CAT : path by_arrival_times j (\cat_(t1≤t<t2)arrivals_at arr_seq t ++ \cat_(t2≤i<t2.+1)arrivals_at arr_seq i).
{ rewrite cat_path; apply /andP; split.
{ move: SORTED. rewrite /sorted A1 ⇒ PATH_js.
by rewrite /path -/(path _ _ js) /by_arrival_times; apply /andP; split. }
{ rewrite big_nat1.
case A2: (arrivals_at arr_seq t2) ⇒ // [j' js'].
have path_le: ∀ (T : eqType) (leT : rel T) (leT_tr : transitive leT) x x' s,
leT x x' → path leT x' s → path leT x s.
{ clear; intros ? ? ? ? ? ?; case: s ⇒ [//| x'' s xlex' /= /andP[x'lex'' ->]].
by rewrite andbT; apply: leT_tr; eauto 1. }
apply path_le with (x' := j').
{ rewrite /transitive/by_arrival_times. intros *; apply leq_trans. }
{ rewrite /by_arrival_times.
have → : job_arrival j' = t2
by apply job_arrival_at; rewrite A2; apply mem_head.
set L := (last j (\cat_(t1≤t<t2)arrivals_at arr_seq t)).
have EX : ∃ t', L \in arrivals_at arr_seq t' ∧ t1 ≤ t' < t2
by apply mem_bigcat_nat_exists; rewrite /L A1 last_cons; exact: mem_last.
move: EX ⇒ [t' [IN /andP [t1t' t't2]]].
have → : job_arrival L = t' by apply job_arrival_at.
by apply ltnW.
}
{ move: (arrivals_at_sorted t2); rewrite /sorted A2 ⇒ PATH'.
rewrite /path -/(path _ _ js') {1}/by_arrival_times.
by apply /andP; split ⇒ //. } } }
by move: CAT; rewrite /sorted A1 cat_cons {1}/path -/(path _ _ (js ++ _)) ⇒ /andP [_ CAT].
Qed.
Corollary task_arrivals_between_sorted :
∀ t1 t2,
sorted by_arrival_times (task_arrivals_between arr_seq tsk t1 t2).
Proof.
move⇒ t1 t2. apply sorted_filter;
first by rewrite /by_arrival_times /transitive; intros *; apply leq_trans.
exact: arrivals_between_sorted.
Qed.
End ArrivalTimes.
∀ t1 t2,
sorted by_arrival_times (arrivals_between arr_seq t1 t2).
Proof.
move⇒ t1 t2.
rewrite /arrivals_between.
elim: t2 ⇒ [|t2 SORTED];
first by rewrite big_nil.
case: (leqP t1 t2) ⇒ T1T2;
last by rewrite big_geq.
rewrite (big_cat_nat _ _ _ T1T2 _) //=.
case A1: (\cat_(t1≤t<t2)arrivals_at arr_seq t) ⇒ [|j js];
first by rewrite cat0s big_nat1; exact: arrivals_at_sorted.
have CAT : path by_arrival_times j (\cat_(t1≤t<t2)arrivals_at arr_seq t ++ \cat_(t2≤i<t2.+1)arrivals_at arr_seq i).
{ rewrite cat_path; apply /andP; split.
{ move: SORTED. rewrite /sorted A1 ⇒ PATH_js.
by rewrite /path -/(path _ _ js) /by_arrival_times; apply /andP; split. }
{ rewrite big_nat1.
case A2: (arrivals_at arr_seq t2) ⇒ // [j' js'].
have path_le: ∀ (T : eqType) (leT : rel T) (leT_tr : transitive leT) x x' s,
leT x x' → path leT x' s → path leT x s.
{ clear; intros ? ? ? ? ? ?; case: s ⇒ [//| x'' s xlex' /= /andP[x'lex'' ->]].
by rewrite andbT; apply: leT_tr; eauto 1. }
apply path_le with (x' := j').
{ rewrite /transitive/by_arrival_times. intros *; apply leq_trans. }
{ rewrite /by_arrival_times.
have → : job_arrival j' = t2
by apply job_arrival_at; rewrite A2; apply mem_head.
set L := (last j (\cat_(t1≤t<t2)arrivals_at arr_seq t)).
have EX : ∃ t', L \in arrivals_at arr_seq t' ∧ t1 ≤ t' < t2
by apply mem_bigcat_nat_exists; rewrite /L A1 last_cons; exact: mem_last.
move: EX ⇒ [t' [IN /andP [t1t' t't2]]].
have → : job_arrival L = t' by apply job_arrival_at.
by apply ltnW.
}
{ move: (arrivals_at_sorted t2); rewrite /sorted A2 ⇒ PATH'.
rewrite /path -/(path _ _ js') {1}/by_arrival_times.
by apply /andP; split ⇒ //. } } }
by move: CAT; rewrite /sorted A1 cat_cons {1}/path -/(path _ _ (js ++ _)) ⇒ /andP [_ CAT].
Qed.
Corollary task_arrivals_between_sorted :
∀ t1 t2,
sorted by_arrival_times (task_arrivals_between arr_seq tsk t1 t2).
Proof.
move⇒ t1 t2. apply sorted_filter;
first by rewrite /by_arrival_times /transitive; intros *; apply leq_trans.
exact: arrivals_between_sorted.
Qed.
End ArrivalTimes.
The same observation applies to task_arrivals_between.
Lemma task_arrivals_between_uniq :
∀ t1 t2,
arrival_sequence_uniq arr_seq →
uniq (task_arrivals_between arr_seq tsk t1 t2).
Proof. move⇒ t1 t2 UNIQ. apply/filter_uniq/arrivals_uniq; apply H_valid_arrival_sequence. Qed.
∀ t1 t2,
arrival_sequence_uniq arr_seq →
uniq (task_arrivals_between arr_seq tsk t1 t2).
Proof. move⇒ t1 t2 UNIQ. apply/filter_uniq/arrivals_uniq; apply H_valid_arrival_sequence. Qed.
For convenience, we restate the left bound of the above lemma...
Corollary job_arrival_between_ge :
∀ {j t1 t2},
j \in arrivals_between arr_seq t1 t2 → t1 ≤ job_arrival j.
Proof.
move ⇒ ? ? ? IN.
apply in_arrivals_implies_arrived_between in IN; last apply H_valid_arrival_sequence.
by move: IN ⇒ /andP [].
Qed.
Corollary job_arrival_between_lt :
∀ {j t1 t2},
j \in arrivals_between arr_seq t1 t2 → job_arrival j < t2.
Proof.
move ⇒ ? ? ? IN.
apply in_arrivals_implies_arrived_between in IN; last apply H_valid_arrival_sequence.
by move: IN ⇒ /andP [].
Qed.
∀ {j t1 t2},
j \in arrivals_between arr_seq t1 t2 → t1 ≤ job_arrival j.
Proof.
move ⇒ ? ? ? IN.
apply in_arrivals_implies_arrived_between in IN; last apply H_valid_arrival_sequence.
by move: IN ⇒ /andP [].
Qed.
Corollary job_arrival_between_lt :
∀ {j t1 t2},
j \in arrivals_between arr_seq t1 t2 → job_arrival j < t2.
Proof.
move ⇒ ? ? ? IN.
apply in_arrivals_implies_arrived_between in IN; last apply H_valid_arrival_sequence.
by move: IN ⇒ /andP [].
Qed.
Any job j in task_arrivals_between arr_seq tsk t1 t2 is also
contained in arrivals_between arr_seq t1 t2.
Lemma task_arrivals_between_subset:
∀ t1 t2 j,
j \in task_arrivals_between arr_seq tsk t1 t2 →
j \in arrivals_between arr_seq t1 t2.
Proof. move⇒ t1 t2 j. by rewrite mem_filter; move ⇒ /andP [/eqP TSK JB_IN]. Qed.
∀ t1 t2 j,
j \in task_arrivals_between arr_seq tsk t1 t2 →
j \in arrivals_between arr_seq t1 t2.
Proof. move⇒ t1 t2 j. by rewrite mem_filter; move ⇒ /andP [/eqP TSK JB_IN]. Qed.
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 ⇒ //.
apply: (task_arrivals_between_subset _ 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 ⇒ //; apply ltnW.
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, ltnW.
apply: H_sporadic_model ⇒ //=.
{ rewrite JOB /prev_j ⇒ /eqP; rewrite nth_uniq //.
{ by move⇒ /eqP EQ; apply n_Sn in EQ. }
{ by apply ltnW. }
{ by rewrite -ARR; apply task_arrivals_between_uniq, H_valid_arrival_sequence. }
}
{ by apply/in_arrivals_implies_arrived/(task_arrivals_between_subset t1 t2). }
{ by apply/in_arrivals_implies_arrived/(task_arrivals_between_subset t1 t2). }
{ by move: IN_prev; rewrite mem_filter ⇒ /andP [/eqP IN _]. }
{ by move: IN_j; rewrite mem_filter ⇒ /andP [/eqP IN _]. }
{ 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).
- by rewrite unfold_in simpl_predE; apply ltnW.
- by rewrite unfold_in simpl_predE.
- by done. } }
Unshelve.
- rewrite /by_arrival_times/transitive/reflexive; intros *; apply leq_trans.
- by rewrite /by_arrival_times/transitive/reflexive; intros *; done.
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 ⇒ //.
apply: (task_arrivals_between_subset _ 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 ⇒ //; apply ltnW.
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, ltnW.
apply: H_sporadic_model ⇒ //=.
{ rewrite JOB /prev_j ⇒ /eqP; rewrite nth_uniq //.
{ by move⇒ /eqP EQ; apply n_Sn in EQ. }
{ by apply ltnW. }
{ by rewrite -ARR; apply task_arrivals_between_uniq, H_valid_arrival_sequence. }
}
{ by apply/in_arrivals_implies_arrived/(task_arrivals_between_subset t1 t2). }
{ by apply/in_arrivals_implies_arrived/(task_arrivals_between_subset t1 t2). }
{ by move: IN_prev; rewrite mem_filter ⇒ /andP [/eqP IN _]. }
{ by move: IN_j; rewrite mem_filter ⇒ /andP [/eqP IN _]. }
{ 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).
- by rewrite unfold_in simpl_predE; apply ltnW.
- by rewrite unfold_in simpl_predE.
- by done. } }
Unshelve.
- rewrite /by_arrival_times/transitive/reflexive; intros *; apply leq_trans.
- by rewrite /by_arrival_times/transitive/reflexive; intros *; done.
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.
destruct (task_arrivals_between arr_seq tsk t1 t2) as [|j js] eqn:ARR.
{ move: ARR H_num_arrivals H_many_jobs; rewrite /number_of_task_arrivals ⇒ → //= →.
intros.
apply ltnW in H_many_jobs.
rewrite ltnn in H_many_jobs.
by done.
}
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 ⇒ //.
apply: task_arrivals_between_subset.
apply mem_nth.
move: H_num_arrivals; rewrite /number_of_task_arrivals ⇒ →.
destruct n. by done.
by done.
}
have DIST : t1 + task_min_inter_arrival_time tsk × n.-1 ≤ job_arrival j_last.
{ apply: arrival_of_nth_job; auto;
first rewrite [number_of_task_arrivals arr_seq tsk t1 _]H_num_arrivals.
{ by destruct n. }
by []. }
apply: leq_ltn_trans.
apply DIST.
apply LAST.
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.
destruct (task_arrivals_between arr_seq tsk t1 t2) as [|j js] eqn:ARR.
{ move: ARR H_num_arrivals H_many_jobs; rewrite /number_of_task_arrivals ⇒ → //= →.
intros.
apply ltnW in H_many_jobs.
rewrite ltnn in H_many_jobs.
by done.
}
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 ⇒ //.
apply: task_arrivals_between_subset.
apply mem_nth.
move: H_num_arrivals; rewrite /number_of_task_arrivals ⇒ →.
destruct n. by done.
by done.
}
have DIST : t1 + task_min_inter_arrival_time tsk × n.-1 ≤ job_arrival j_last.
{ apply: arrival_of_nth_job; auto;
first rewrite [number_of_task_arrivals arr_seq tsk t1 _]H_num_arrivals.
{ by destruct n. }
by []. }
apply: leq_ltn_trans.
apply DIST.
apply LAST.
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.
{
apply div_ceil_gt0 ⇒ //; rewrite subn_gt0.
move_neq_up LE; move: NARR.
rewrite /number_of_task_arrivals /task_arrivals_between /arrivals_between.
by rewrite big_geq.
}
{
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.
{
apply div_ceil_gt0 ⇒ //; rewrite subn_gt0.
move_neq_up LE; move: NARR.
rewrite /number_of_task_arrivals /task_arrivals_between /arrivals_between.
by rewrite big_geq.
}
{
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.