# Library prosa.analysis.facts.hyperperiod

Require Export prosa.analysis.definitions.hyperperiod.
Require Export prosa.analysis.facts.periodic.task_arrivals_size.
Require Export prosa.util.div_mod.
Require Export prosa.util.tactics.
In this file we prove some simple properties of hyperperiods of periodic tasks.
Section Hyperperiod.
Consider any type of periodic tasks, ...
Context {Task : TaskType} `{PeriodicModel Task}.
... any task set ts, ...
Variable ts : TaskSet Task.
... and any task tsk that belongs to this task set.
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
A task set's hyperperiod is an integral multiple of each task's period in the task set.
Lemma hyperperiod_int_mult_of_any_task :
∃ (k : nat),
hyperperiod ts = k × task_period tsk.
Proof. by apply/dvdnP; apply lcm_seq_is_mult_of_all_ints, map_f, H_tsk_in_ts. Qed.
End Hyperperiod.
In this section we show a property of hyperperiod in context of task sets with valid periods.
Section ValidPeriodsImplyPositiveHP.
Consider any type of periodic tasks ...
Context {Task : TaskType} `{PeriodicModel Task}.
... and any task set ts ...
Variable ts : TaskSet Task.
... such that all tasks in ts have valid periods.
Hypothesis H_valid_periods : valid_periods ts.
We show that the hyperperiod of task set ts is positive.
Lemma valid_periods_imply_pos_hp :
hyperperiod ts > 0.
Proof.
apply all_pos_implies_lcml_pos.
move ⇒ b /mapP [x IN EQ]; subst b.
now apply H_valid_periods.
Qed.
End ValidPeriodsImplyPositiveHP.
In this section we prove some lemmas about the hyperperiod in context of the periodic model.
Section PeriodicLemmas.
Consider any type of tasks, ...
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{PeriodicModel Task}.
... any type of jobs, ...
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
... and a consistent arrival sequence with non-duplicate arrivals.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Consider a task set ts such that all tasks in ts have valid periods.
Variable ts : TaskSet Task.
Hypothesis H_valid_periods : valid_periods ts.
Let tsk be any periodic task in ts with a valid offset and period.
Variable tsk : Task.
Hypothesis H_task_in_ts : tsk \in ts.
Hypothesis H_valid_offset : valid_offset arr_seq tsk.
Hypothesis H_valid_period : valid_period tsk.
Hypothesis H_periodic_task : respects_periodic_task_model arr_seq tsk.
Assume we have an infinite sequence of jobs in the arrival sequence.
Hypothesis H_infinite_jobs : infinite_jobs arr_seq.
Let O_max denote the maximum task offset in ts and let HP denote the hyperperiod of all tasks in ts.
Let O_max := max_task_offset ts.
Let HP := hyperperiod ts.
We show that the job corresponding to any job j1 in any other hyperperiod is of the same task as j1.
Lemma corresponding_jobs_have_same_task :
∀ j1 j2,
job_task (corresponding_job_in_hyperperiod ts arr_seq j1
(starting_instant_of_corresponding_hyperperiod ts j2) (job_task j1)) = job_task j1.
Proof.
clear H_task_in_ts H_valid_period.
move⇒ j1 j2.
set ARRIVALS := (task_arrivals_between arr_seq (job_task j1) (starting_instant_of_hyperperiod ts (job_arrival j2))
(starting_instant_of_hyperperiod ts (job_arrival j2) + HP)).
set IND := (job_index_in_hyperperiod ts arr_seq j1 (starting_instant_of_hyperperiod ts (job_arrival j1)) (job_task j1)).
have SIZE_G : size ARRIVALS ≤ IND → job_task (nth j1 ARRIVALS IND) = job_task j1 by intro SG; rewrite nth_default.
case: (boolP (size ARRIVALS == IND)) ⇒ [/eqP EQ|NEQ]; first by apply SIZE_G; lia.
move : NEQ; rewrite neq_ltn ⇒ /orP [LT | G]; first by apply SIZE_G; lia.
set jb := nth j1 ARRIVALS IND.
have JOB_IN : jb \in ARRIVALS by apply mem_nth.
rewrite /ARRIVALS /task_arrivals_between mem_filter in JOB_IN.
now move : JOB_IN ⇒ /andP [/eqP TSK JB_IN].
Qed.
We show that if a job j lies in the hyperperiod starting at instant t then j arrives in the interval `[t, t + HP)`.
Lemma all_jobs_arrive_within_hyperperiod :
∀ j t,
j \in jobs_in_hyperperiod ts arr_seq t tsk →
t ≤ job_arrival j < t + HP.
Proof.
intros × JB_IN_HP.
rewrite mem_filter in JB_IN_HP.
move : JB_IN_HP ⇒ /andP [/eqP TSK JB_IN]; apply mem_bigcat_nat_exists in JB_IN.
destruct JB_IN as [i [JB_IN INEQ]].
apply job_arrival_at in JB_IN ⇒ //.
by rewrite JB_IN.
Qed.
We show that the number of jobs in a hyperperiod starting at n1 × HP + O_max is the same as the number of jobs in a hyperperiod starting at n2 × HP + O_max given that n1 is less than or equal to n2.
Lemma eq_size_hyp_lt :
∀ n1 n2,
n1 ≤ n2 →
size (jobs_in_hyperperiod ts arr_seq (n1 × HP + O_max) tsk)
= size (jobs_in_hyperperiod ts arr_seq (n2 × HP + O_max) tsk).
Proof.
move⇒ n1 n2 N1_LT.
have → : n2 × HP + O_max = n1 × HP + O_max + (n2 - n1) × HP.
{ by rewrite -[in LHS](subnKC N1_LT) mulnDl addnAC. }
destruct (hyperperiod_int_mult_of_any_task ts tsk H_task_in_ts) as [k HYP]; rewrite !/HP.
rewrite [in X in _ = size (_ (n1 × HP + O_max + _ × X) tsk)]HYP.
rewrite mulnA /HP /jobs_in_hyperperiod !size_of_task_arrivals_between.
erewrite big_sum_eq_in_eq_sized_intervals ⇒ //; intros g G_LT.
have OFF_G : task_offset tsk ≤ O_max by apply max_offset_g.
have FG : ∀ v b n, v + b + n = v + n + b by intros *; lia.
erewrite eq_size_of_task_arrivals_seperated_by_period ⇒ //; last lia.
by rewrite FG.
Qed.
We generalize the above lemma by lifting the condition on n1 and n2.
Lemma eq_size_of_arrivals_in_hyperperiod :
∀ n1 n2,
size (jobs_in_hyperperiod ts arr_seq (n1 × HP + O_max) tsk)
= size (jobs_in_hyperperiod ts arr_seq (n2 × HP + O_max) tsk).
Proof.
move⇒ n1 n2.
case : (boolP (n1 == n2)) ⇒ [/eqP EQ | NEQ]; first by rewrite EQ.
move : NEQ; rewrite neq_ltn ⇒ /orP [LT | LT].
+ by apply eq_size_hyp_lt ⇒ //; lia.
+ move : (eq_size_hyp_lt n2 n1) ⇒ EQ_S.
by feed_n 1 EQ_S ⇒ //; lia.
Qed.
Consider any two jobs j1 and j2 that stem from the arrival sequence arr_seq such that j1 is of task tsk.
Variable j1 : Job.
Variable j2 : Job.
Hypothesis H_j1_from_arr_seq : arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq : arrives_in arr_seq j2.
Hypothesis H_j1_task : job_task j1 = tsk.
Assume that both j1 and j2 arrive after O_max.
Hypothesis H_j1_arr_after_O_max : O_max ≤ job_arrival j1.
Hypothesis H_j2_arr_after_O_max : O_max ≤ job_arrival j2.
We show that any job j that arrives in task arrivals in the same hyperperiod as j2 also arrives in task arrivals up to job_arrival j2 + HP.
Lemma job_in_hp_arrives_in_task_arrivals_up_to :
∀ j,
j \in jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP × HP + O_max) tsk →
j \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).
Proof.
intros j J_IN.
rewrite /task_arrivals_up_to.
set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP × HP + O_max) tsk).
move : (J_IN) ⇒ J_ARR; apply all_jobs_arrive_within_hyperperiod in J_IN.
rewrite /jobs_in_hp /jobs_in_hyperperiod /task_arrivals_up_to /task_arrivals_between mem_filter in J_ARR.
move : J_ARR ⇒ /andP [/eqP TSK' NTH_IN].
apply job_in_task_arrivals_between ⇒ //;
first by apply in_arrivals_implies_arrived in NTH_IN.
apply mem_bigcat_nat_exists in NTH_IN.
apply /andP; split ⇒ //.
rewrite ltnS.
apply leq_trans with (n := (job_arrival j2 - O_max) %/ HP × HP + O_max + HP); first by lia.
rewrite leq_add2r.
have O_M : (job_arrival j2 - O_max) %/ HP × HP ≤ job_arrival j2 - O_max by apply leq_divM.
have ARR_G : job_arrival j2 ≥ O_max by [].
lia.
Qed.
We show that job j1 arrives in its own hyperperiod.
Lemma job_in_own_hp :
j1 \in jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP × HP + O_max) tsk.
Proof.
apply job_in_task_arrivals_between ⇒ //.
apply /andP; split.
+ rewrite addnC -leq_subRL ⇒ //.
by apply leq_divM.
+ specialize (div_floor_add_g (job_arrival j1 - O_max) HP) ⇒ AB.
feed_n 1 AB; first by apply valid_periods_imply_pos_hp ⇒ //.
rewrite ltn_subLR // in AB.
by rewrite -/(HP); lia.
Qed.
We show that the corresponding_job_in_hyperperiod of j1 in j2's hyperperiod arrives in task arrivals up to job_arrival j2 + HP.
Lemma corr_job_in_task_arrivals_up_to :
corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) tsk \in
task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).
Proof.
rewrite /corresponding_job_in_hyperperiod /starting_instant_of_corresponding_hyperperiod.
rewrite /job_index_in_hyperperiod /starting_instant_of_hyperperiod /hyperperiod_index.
set ind := (index j1 (jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP × HP + O_max) tsk)).
set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP × HP + O_max) tsk).
set nj := nth j1 jobs_in_hp ind.
apply job_in_hp_arrives_in_task_arrivals_up_to ⇒ //.
rewrite mem_nth /jobs_in_hp ⇒ //.
specialize (eq_size_of_arrivals_in_hyperperiod ((job_arrival j2 - O_max) %/ HP) ((job_arrival j1 - O_max) %/ HP)) ⇒ EQ.
rewrite EQ /ind index_mem.
by apply job_in_own_hp.
Qed.
Finally, we show that the corresponding_job_in_hyperperiod of j1 in j2's hyperperiod arrives in the arrival sequence arr_seq.
Lemma corresponding_job_arrives :
arrives_in arr_seq (corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) tsk).
Proof.
move : (corr_job_in_task_arrivals_up_to) ⇒ ARR_G.
rewrite /task_arrivals_up_to /task_arrivals_between mem_filter in ARR_G.
move : ARR_G ⇒ /andP [/eqP TSK' NTH_IN].
by apply in_arrivals_implies_arrived in NTH_IN.
Qed.
End PeriodicLemmas.