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.

Constrained Offsets

Constrained offsets ensure that every task begins releasing jobs within its first period, simplifying bounds on the initial transient.
Section ConstrainedOffsets.

Consider periodic tasks with offsets.
  Context {Task : TaskType} `{PeriodicModel Task} `{TaskOffset Task}.

We say a task's offset is constrained if its offset is less than its period ...
  Definition constrained_offset (tsk : Task) :=
    task_offset tsk < task_period tsk.

... and lift this notion to task sets.
  Definition constrained_offsets (ts : TaskSet Task) :=
    ∀ tsk,
      tsk \in ts →
      constrained_offset tsk.

End ConstrainedOffsets.