Project Page Index Table of Contents

# Library prosa.analysis.facts.periodic.max_inter_arrival

Require Export prosa.analysis.facts.periodic.arrival_separation.

## Periodic Task Model respects the Task Max Inter-Arrival model.

In this section, we show that the periodic task model respects the task max inter-arrival model (i.e. consecutive jobs of a task are separated at most by a certain duration specified by the task_max_inter_arrival_time parameter).
Section PeriodicTasksRespectMaxInterArrivalModel.
Consider any type of periodic tasks, ...
Context {Task : TaskType} `{PeriodicModel Task}.
... any type of jobs associated with the tasks, ...
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
... and any arrival sequence.
Variable arr_seq : arrival_sequence Job.
By using each task's period as its maximum inter-arrival time, ...
Global Instance max_inter_eq_period : TaskMaxInterArrival Task :=
{
task_max_inter_arrival_time := task_period
}.
... we observe that for any task tsk, task_max_inter_arrival_time tsk is positive, ...
Remark valid_period_is_valid_max_inter_arrival_time :
∀ tsk, valid_period tsk → positive_task_max_inter_arrival_time tsk.
Proof. trivial. Qed.
... and show that the periodic model respects the task max inter-arrival model.
Remark periodic_model_respects_max_inter_arrival_model :
∀ tsk,
valid_period tsk →
respects_periodic_task_model arr_seq tsk →
valid_task_max_inter_arrival_time arr_seq tsk.
Proof.
intros tsk VALID_PERIOD PERIODIC.
split; first by apply VALID_PERIOD ⇒ //.
intros j ARR TSK IND.
specialize (PERIODIC j); feed_n 3 PERIODIC ⇒ //.
move : PERIODIC ⇒ [j' [ARR' [IND' [TSK' ARRJ']]]].
∃ j'; repeat split ⇒ //.
{ case: (boolP (j == j')) ⇒ [/eqP EQ|NEQ].
- have EQ_IND : (job_index arr_seq j' = job_index arr_seq j) by apply f_equal ⇒ //.
now exfalso; lia.
- now apply /eqP. }
{ have NZ_PERIOD : (task_period tsk > 0) by apply VALID_PERIOD.
rewrite /max_inter_eq_period /task_max_inter_arrival_time ARRJ'.
now lia. }
Qed.
End PeriodicTasksRespectMaxInterArrivalModel.