Library prosa.analysis.definitions.hyperperiod


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


Require Export prosa.model.task.arrival.periodic.
Require Export prosa.util.lcmseq.
From mathcomp Require Import div.

In this file we define the notion of a hyperperiod for periodic tasks.
Section Hyperperiod.

Consider any type of periodic tasks ...
  Context {Task : TaskType} `{PeriodicModel Task}.

... and any task set [ts].
  Variable ts : TaskSet Task.

The hyperperiod of a task set is defined as the least common multiple (LCM) of the periods of all tasks in the task set.
  Definition hyperperiod : duration := lcml (map task_period ts).

End Hyperperiod.

In this section we provide basic definitions concerning the hyperperiod of all tasks in a task set.
Consider any type of periodic tasks ...
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{PeriodicModel Task}.

... and any type of jobs.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any task set [ts] ...
  Variable ts : TaskSet Task.

... and any arrival sequence [arr_seq].
  Variable arr_seq : arrival_sequence Job.

Let [O_max] denote the maximum offset of all tasks in [ts] ...
  Let O_max := max_task_offset ts.

... and let [HP] denote the hyperperiod of all tasks in [ts].
  Let HP := hyperperiod ts.

We define a hyperperiod index based on an instant [t] which lies in it. Note that we consider the first hyperperiod to start at time [O_max], i.e., shifted by the maximum offset (and not at time zero as can also be found sometimes in the literature)
  Definition hyperperiod_index (t : instant) :=
    (t - O_max) %/ HP.

Given an instant [t], we define the starting instant of the hyperperiod that contains [t].
Given a job [j], we define the starting instant of the hyperperiod in which [j] arrives.
We define the sequence of jobs of a task [tsk] that arrive in a hyperperiod given the starting instant [h] of the hyperperiod.
  Definition jobs_in_hyperperiod (h : instant) (tsk : Task) :=
    task_arrivals_between arr_seq tsk h (h + HP).

We define the index of a job [j] of task [tsk] in a hyperperiod starting at [h].
  Definition job_index_in_hyperperiod (j : Job) (h : instant) (tsk : Task) :=
    index j (jobs_in_hyperperiod h tsk).

Given a job [j] of task [tsk] and the hyperperiod starting at [h], we define a [corresponding_job_in_hyperperiod] which is the job that arrives in given hyperperiod and has the same [job_index] as [j].