Library prosa.model.task.arrival.periodic

Require Export prosa.model.task.arrival.sporadic.
Require Export prosa.model.task.arrival.task_max_inter_arrival.
Require Export prosa.model.task.offset.
Require Export prosa.analysis.facts.job_index.

The Periodic Task Model

In the following, we define the classic Liu & Layland arrival process, i.e., the arrival process commonly known as the periodic task model, wherein the arrival times of consecutive jobs of a periodic task are separated by the task's period.

Task Model Parameter for Periods

Under the periodic task model, each task is characterized by its period, which we denote as task_period.

Class PeriodicModel (Task : TaskType) := task_period : Task → duration.

Model Validity

Next, we define the semantics of the periodic task model.
Section ValidPeriodicTaskModel.

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

A valid periodic task has a non-zero period.
  Definition valid_period (tsk : Task) := task_period tsk > 0.

Next, consider any type of jobs stemming from these tasks ...
  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

... and an arbitrary arrival sequence of such jobs.
  Variable arr_seq : arrival_sequence Job.

We say that a task respects the periodic task model if every job j (except the first one) has a predecessor j' that arrives exactly one task period before it.
  Definition respects_periodic_task_model (tsk : Task) :=
    ∀ j,
      arrives_in arr_seq j →
      job_index arr_seq j > 0 →
      job_task j = tsk →
      ∃ j',
        arrives_in arr_seq j' ∧
        job_index arr_seq j' = job_index arr_seq j - 1 ∧
        job_task j' = tsk ∧
        job_arrival j = job_arrival j' + task_period tsk.

Further, in the context of a set of periodic tasks, ...
  Variable ts : TaskSet Task.

... every task in the set must have a valid period ...
  Definition valid_periods := ∀ tsk : Task, tsk \in ts → valid_period tsk.

... and all jobs of every task in a set of periodic tasks must respect the period constraint on arrival times.
  Definition taskset_respects_periodic_task_model :=
    ∀ tsk, tsk \in ts → respects_periodic_task_model tsk.

End ValidPeriodicTaskModel.