Library prosa.analysis.facts.hyperperiod

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.
In this section we show a property of hyperperiod in context of task sets with valid periods.
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.
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.
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.
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.
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.

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).

We generalize the above lemma by lifting the condition on n1 and n2.
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.
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.
We show that job j1 arrives in its own hyperperiod.
We show that the corresponding_job_in_hyperperiod of j1 in j2's hyperperiod arrives in task arrivals up to job_arrival j2 + HP.
Finally, we show that the corresponding_job_in_hyperperiod of j1 in j2's hyperperiod arrives in the arrival sequence arr_seq.