Library prosa.analysis.facts.periodic.task_arrivals_size
Require Export prosa.analysis.facts.periodic.arrival_times.
Require Export prosa.analysis.definitions.infinite_jobs.
Require Export prosa.analysis.facts.sporadic.arrival_sequence.
Require Export prosa.analysis.definitions.infinite_jobs.
Require Export prosa.analysis.facts.sporadic.arrival_sequence.
In this file we prove some properties concerning the size
of task arrivals in context of the periodic model.
Consider any type of periodic tasks with an offset ...
... and any type of jobs associated with these tasks.
Consider any unique arrival sequence with consistent arrivals ...
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 periodic task tsk with a valid offset and period.
Variable tsk : Task.
Hypothesis H_valid_offset : valid_offset arr_seq tsk.
Hypothesis H_valid_period : valid_period tsk.
Hypothesis H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk.
Hypothesis H_valid_offset : valid_offset arr_seq tsk.
Hypothesis H_valid_period : valid_period tsk.
Hypothesis H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk.
We show that if an instant t is not an "arrival time" for
task tsk then task_arrivals_at arr_seq tsk t is an empty sequence.
Lemma task_arrivals_size_at_non_arrival:
∀ t,
(∀ n, t ≠ task_offset tsk + n × task_period tsk) →
task_arrivals_at arr_seq tsk t = [::].
Proof.
move⇒ t T.
have EMPT_OR_EXISTS : ∀ xs, xs = [::] ∨ ∃ a, a \in xs.
{ move⇒ t0; elim⇒ [|a xs IHxs]; first by left.
right; ∃ a.
by apply mem_head.
}
destruct (EMPT_OR_EXISTS Job (task_arrivals_at arr_seq tsk t)) as [EMPT | [a A_IN]] ⇒ //.
rewrite /task_arrivals_at mem_filter in A_IN; move : A_IN ⇒ /andP [/eqP TSK A_ARR].
move : H_valid_arrival_sequence ⇒ [CONSISTENT UNIQ].
move : (A_ARR) ⇒ A_IN; apply CONSISTENT in A_IN.
rewrite -A_IN in T; rewrite /arrivals_at in A_ARR.
apply in_arrseq_implies_arrives in A_ARR.
have EXISTS_N : ∃ n, job_arrival a = task_offset tsk + n × task_period tsk
by exact: (job_arrival_times arr_seq).
move : EXISTS_N ⇒ [n A_ARRIVAL].
by move : (T n) ⇒ T1.
Qed.
∀ t,
(∀ n, t ≠ task_offset tsk + n × task_period tsk) →
task_arrivals_at arr_seq tsk t = [::].
Proof.
move⇒ t T.
have EMPT_OR_EXISTS : ∀ xs, xs = [::] ∨ ∃ a, a \in xs.
{ move⇒ t0; elim⇒ [|a xs IHxs]; first by left.
right; ∃ a.
by apply mem_head.
}
destruct (EMPT_OR_EXISTS Job (task_arrivals_at arr_seq tsk t)) as [EMPT | [a A_IN]] ⇒ //.
rewrite /task_arrivals_at mem_filter in A_IN; move : A_IN ⇒ /andP [/eqP TSK A_ARR].
move : H_valid_arrival_sequence ⇒ [CONSISTENT UNIQ].
move : (A_ARR) ⇒ A_IN; apply CONSISTENT in A_IN.
rewrite -A_IN in T; rewrite /arrivals_at in A_ARR.
apply in_arrseq_implies_arrives in A_ARR.
have EXISTS_N : ∃ n, job_arrival a = task_offset tsk + n × task_period tsk
by exact: (job_arrival_times arr_seq).
move : EXISTS_N ⇒ [n A_ARRIVAL].
by move : (T n) ⇒ T1.
Qed.
We show that at any instant t, at most one job of task tsk
can arrive (i.e. size of task_arrivals_at arr_seq tsk t is at most one).
Lemma task_arrivals_at_size_cases:
∀ t,
size (task_arrivals_at arr_seq tsk t) = 0 ∨
size (task_arrivals_at arr_seq tsk t) = 1.
Proof.
intro t.
case: (ltngtP (size (task_arrivals_at arr_seq tsk t)) 1) ⇒ [LT|GT|EQ];
[by destruct (size (task_arrivals_at arr_seq tsk t)); left| |by lia].
specialize (exists_two (task_arrivals_at arr_seq tsk t)) ⇒ EXISTS_TWO.
move : H_valid_arrival_sequence ⇒ [CONSISTENT UNIQ].
destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by [] | by apply filter_uniq | ].
rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
move: A_IN B_IN ⇒ /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
move: (ARRA); move: (ARRB); rewrite /arrivals_at ⇒ A_IN B_IN.
apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
have SPO : respects_sporadic_task_model arr_seq tsk ⇒ [//|].
have EQ_ARR_A : (job_arrival a = t) by [].
have EQ_ARR_B : (job_arrival b = t) by [].
specialize (SPO a b); feed_n 6 SPO ⇒ //; first lia.
rewrite EQ_ARR_A EQ_ARR_B in SPO.
rewrite /task_min_inter_arrival_time /periodic_as_sporadic in SPO.
have POS : task_period tsk > 0 by [].
lia.
Qed.
∀ t,
size (task_arrivals_at arr_seq tsk t) = 0 ∨
size (task_arrivals_at arr_seq tsk t) = 1.
Proof.
intro t.
case: (ltngtP (size (task_arrivals_at arr_seq tsk t)) 1) ⇒ [LT|GT|EQ];
[by destruct (size (task_arrivals_at arr_seq tsk t)); left| |by lia].
specialize (exists_two (task_arrivals_at arr_seq tsk t)) ⇒ EXISTS_TWO.
move : H_valid_arrival_sequence ⇒ [CONSISTENT UNIQ].
destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by [] | by apply filter_uniq | ].
rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
move: A_IN B_IN ⇒ /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
move: (ARRA); move: (ARRB); rewrite /arrivals_at ⇒ A_IN B_IN.
apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
have SPO : respects_sporadic_task_model arr_seq tsk ⇒ [//|].
have EQ_ARR_A : (job_arrival a = t) by [].
have EQ_ARR_B : (job_arrival b = t) by [].
specialize (SPO a b); feed_n 6 SPO ⇒ //; first lia.
rewrite EQ_ARR_A EQ_ARR_B in SPO.
rewrite /task_min_inter_arrival_time /periodic_as_sporadic in SPO.
have POS : task_period tsk > 0 by [].
lia.
Qed.
We show that the size of task arrivals (strictly) between two consecutive arrival
times is zero.
Lemma size_task_arrivals_between_eq0:
∀ n,
let l := (task_offset tsk + n × task_period tsk).+1 in
let r := (task_offset tsk + n.+1 × task_period tsk) in
size (task_arrivals_between arr_seq tsk l r) = 0.
Proof.
intros n l r; rewrite /l /r.
rewrite size_of_task_arrivals_between big_nat_eq0 ⇒ //; intros t INEQ.
rewrite task_arrivals_size_at_non_arrival ⇒ //; intros n1 EQ.
rewrite EQ in INEQ.
move : INEQ ⇒ /andP [INEQ1 INEQ2].
rewrite ltn_add2l ltn_mul2r in INEQ1; rewrite ltn_add2l ltn_mul2r in INEQ2.
move : INEQ1 INEQ2 ⇒ /andP [A B] /andP [C D].
by lia.
Qed.
∀ n,
let l := (task_offset tsk + n × task_period tsk).+1 in
let r := (task_offset tsk + n.+1 × task_period tsk) in
size (task_arrivals_between arr_seq tsk l r) = 0.
Proof.
intros n l r; rewrite /l /r.
rewrite size_of_task_arrivals_between big_nat_eq0 ⇒ //; intros t INEQ.
rewrite task_arrivals_size_at_non_arrival ⇒ //; intros n1 EQ.
rewrite EQ in INEQ.
move : INEQ ⇒ /andP [INEQ1 INEQ2].
rewrite ltn_add2l ltn_mul2r in INEQ1; rewrite ltn_add2l ltn_mul2r in INEQ2.
move : INEQ1 INEQ2 ⇒ /andP [A B] /andP [C D].
by lia.
Qed.
In this section we show some properties of task arrivals in case
of an infinite sequence of jobs.
Assume that we have an infinite sequence of jobs.
We show that for any number n, there exists a job j of task tsk
such that job_index of j is equal to n and j arrives
at task_offset tsk + n × task_period tsk.
Lemma jobs_exists_later:
∀ n,
∃ j,
arrives_in arr_seq j ∧
job_task j = tsk ∧
job_arrival j = task_offset tsk + n × task_period tsk ∧
job_index arr_seq j = n.
Proof.
move⇒ n.
destruct (H_infinite_jobs tsk n) as [j [ARR [TSK IND]]].
∃ j; repeat split ⇒ //.
exact: (periodic_arrival_times arr_seq).
Qed.
∀ n,
∃ j,
arrives_in arr_seq j ∧
job_task j = tsk ∧
job_arrival j = task_offset tsk + n × task_period tsk ∧
job_index arr_seq j = n.
Proof.
move⇒ n.
destruct (H_infinite_jobs tsk n) as [j [ARR [TSK IND]]].
∃ j; repeat split ⇒ //.
exact: (periodic_arrival_times arr_seq).
Qed.
We show that the size of task arrivals at any arrival time is equal to one.
Lemma task_arrivals_at_size:
∀ n,
let l := (task_offset tsk + n × task_period tsk) in
size (task_arrivals_at arr_seq tsk l) = 1.
Proof.
intros n l; rewrite /l.
move : (jobs_exists_later n) ⇒ [j' [ARR [TSK [ARRIVAL IND]]]].
apply (only_j_in_task_arrivals_at_j
arr_seq H_valid_arrival_sequence tsk) in ARR ⇒ //.
rewrite /task_arrivals_at_job_arrival TSK in ARR.
by rewrite -ARRIVAL ARR.
Qed.
∀ n,
let l := (task_offset tsk + n × task_period tsk) in
size (task_arrivals_at arr_seq tsk l) = 1.
Proof.
intros n l; rewrite /l.
move : (jobs_exists_later n) ⇒ [j' [ARR [TSK [ARRIVAL IND]]]].
apply (only_j_in_task_arrivals_at_j
arr_seq H_valid_arrival_sequence tsk) in ARR ⇒ //.
rewrite /task_arrivals_at_job_arrival TSK in ARR.
by rewrite -ARRIVAL ARR.
Qed.
We show that the size of task arrivals up to task_offset tsk is equal to one.
Lemma size_task_arrivals_up_to_offset:
size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1.
Proof.
rewrite /task_arrivals_up_to.
specialize (task_arrivals_between_cat arr_seq tsk 0 (task_offset tsk) (task_offset tsk).+1) ⇒ CAT.
feed_n 2 CAT ⇒ //; rewrite CAT size_cat.
have Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0.
{ rewrite size_of_task_arrivals_between big_nat_eq0 ⇒ //; intros t T_EQ.
rewrite task_arrivals_size_at_non_arrival ⇒ //; intros n EQ.
by lia.
}
rewrite Z add0n /task_arrivals_between /arrivals_between big_nat1.
specialize (task_arrivals_at_size 0) ⇒ AT_SIZE.
by rewrite mul0n addn0 in AT_SIZE.
Qed.
size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1.
Proof.
rewrite /task_arrivals_up_to.
specialize (task_arrivals_between_cat arr_seq tsk 0 (task_offset tsk) (task_offset tsk).+1) ⇒ CAT.
feed_n 2 CAT ⇒ //; rewrite CAT size_cat.
have Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0.
{ rewrite size_of_task_arrivals_between big_nat_eq0 ⇒ //; intros t T_EQ.
rewrite task_arrivals_size_at_non_arrival ⇒ //; intros n EQ.
by lia.
}
rewrite Z add0n /task_arrivals_between /arrivals_between big_nat1.
specialize (task_arrivals_at_size 0) ⇒ AT_SIZE.
by rewrite mul0n addn0 in AT_SIZE.
Qed.
We show that for any number n, the number of jobs released by task tsk up to
task_offset tsk + n × task_period tsk is equal to n + 1.
Lemma task_arrivals_up_to_size:
∀ n,
let l := (task_offset tsk + n × task_period tsk) in
let r := (task_offset tsk + n.+1 × task_period tsk) in
size (task_arrivals_up_to arr_seq tsk l) = n + 1.
Proof.
elim⇒ [|n IHn].
- intros l r; rewrite /l mul0n add0n addn0.
by apply size_task_arrivals_up_to_offset.
- intros l r.
specialize (task_arrivals_cat arr_seq tsk (task_offset tsk + n × task_period tsk)
(task_offset tsk + n.+1 × task_period tsk)) ⇒ CAT.
feed_n 1 CAT; first by lia.
rewrite CAT size_cat IHn.
specialize (task_arrivals_between_cat arr_seq tsk (task_offset tsk + n × task_period tsk).+1
(task_offset tsk + n.+1 × task_period tsk) (task_offset tsk + n.+1 × task_period tsk).+1) ⇒ S_CAT.
feed_n 2 S_CAT; try by lia.
{ rewrite ltn_add2l ltn_mul2r.
by apply /andP; split ⇒ //.
}
rewrite S_CAT size_cat /task_arrivals_between /arrivals_between big_nat1.
rewrite size_task_arrivals_between_eq0 task_arrivals_at_size ⇒ //.
by lia.
Qed.
∀ n,
let l := (task_offset tsk + n × task_period tsk) in
let r := (task_offset tsk + n.+1 × task_period tsk) in
size (task_arrivals_up_to arr_seq tsk l) = n + 1.
Proof.
elim⇒ [|n IHn].
- intros l r; rewrite /l mul0n add0n addn0.
by apply size_task_arrivals_up_to_offset.
- intros l r.
specialize (task_arrivals_cat arr_seq tsk (task_offset tsk + n × task_period tsk)
(task_offset tsk + n.+1 × task_period tsk)) ⇒ CAT.
feed_n 1 CAT; first by lia.
rewrite CAT size_cat IHn.
specialize (task_arrivals_between_cat arr_seq tsk (task_offset tsk + n × task_period tsk).+1
(task_offset tsk + n.+1 × task_period tsk) (task_offset tsk + n.+1 × task_period tsk).+1) ⇒ S_CAT.
feed_n 2 S_CAT; try by lia.
{ rewrite ltn_add2l ltn_mul2r.
by apply /andP; split ⇒ //.
}
rewrite S_CAT size_cat /task_arrivals_between /arrivals_between big_nat1.
rewrite size_task_arrivals_between_eq0 task_arrivals_at_size ⇒ //.
by lia.
Qed.
We show that the number of jobs released by task tsk at any instant t
and t + n × task_period tsk is the same for any number n.
Lemma eq_size_of_task_arrivals_seperated_by_period:
∀ n t,
t ≥ task_offset tsk →
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n × task_period tsk)).
Proof.
move⇒ n t o_le_t.
have [tmo_eq0|tmo_neq0] :=
@eqP _ ((t - task_offset tsk) %% task_period tsk) 0.
- rewrite -(subnKC o_le_t) (divn_eq (t - _) (task_period tsk)).
by rewrite tmo_eq0 addn0 -addnA -mulnDl !task_arrivals_at_size.
- rewrite !task_arrivals_size_at_non_arrival// ⇒ n';
move⇒ /(f_equal (subn^~(task_offset tsk))); rewrite addKn;
move⇒ /(f_equal (modn^~(task_period tsk))).
+ by rewrite -addnBAC// addnC -[n' × _]addn0 !modnMDl mod0n.
+ by rewrite -[n' × _]addn0 modnMDl mod0n.
Qed.
End TaskArrivalsInCaseOfInfiniteJobs.
End TaskArrivalsSize.
∀ n t,
t ≥ task_offset tsk →
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n × task_period tsk)).
Proof.
move⇒ n t o_le_t.
have [tmo_eq0|tmo_neq0] :=
@eqP _ ((t - task_offset tsk) %% task_period tsk) 0.
- rewrite -(subnKC o_le_t) (divn_eq (t - _) (task_period tsk)).
by rewrite tmo_eq0 addn0 -addnA -mulnDl !task_arrivals_at_size.
- rewrite !task_arrivals_size_at_non_arrival// ⇒ n';
move⇒ /(f_equal (subn^~(task_offset tsk))); rewrite addKn;
move⇒ /(f_equal (modn^~(task_period tsk))).
+ by rewrite -addnBAC// addnC -[n' × _]addn0 !modnMDl mod0n.
+ by rewrite -[n' × _]addn0 modnMDl mod0n.
Qed.
End TaskArrivalsInCaseOfInfiniteJobs.
End TaskArrivalsSize.