Library prosa.model.task.arrival.curves


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

Welcome to Coq 8.11.2 (June 2020)

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

Require Export prosa.util.rel.
Require Export prosa.model.task.arrivals.

The Arbitrary Arrival Curves Model

In the following, we define the notion of arbitrary arrival curves, which can be used to reason about the frequency of job arrivals. In contrast to the sporadic task model, the arbitrary arrival curves model is well-suited to expressing bursty and irregular arrival processes.

Task Parameters for the Arrival Curves Model

The arrival curves model describes tasks by giving an upper bound and, optionally, a lower bound on the number of new job arrivals during any given interval. These bounds are typically called arrival curves.
We let [max_arrivals tsk Δ] denote a bound on the maximum number of arrivals of jobs of task [tsk] in any interval of length [Δ].
Class MaxArrivals (Task : TaskType) := max_arrivals : Task → duration → nat.

Conversely, we let [min_arrivals tsk Δ] denote a bound on the minimum number of arrivals of jobs of task [tsk] in any interval of length [Δ].
Class MinArrivals (Task : TaskType) := min_arrivals : Task → duration → nat.

Alternatively, it is also possible to describe arbitrary arrival processes by specifying the minimum and maximum lengths of an interval in which a given number of jobs arrive. Such bounds are typically called minimum- and maximum-distance functions.
We let [min_separation tsk N] denote the minimal length of an interval in which exactly [N] jobs of task [tsk] arrive.
Class MinSeparation (Task : TaskType) := min_separation : Task → nat → duration.

Conversely, we let [max_separation tsk N] denote the maximal length of an interval in which exactly [N] jobs of task [tsk] arrive.
Class MaxSeparation (Task : TaskType) := max_separation : Task → nat → duration.

Parameter Semantics

In the following, we precisely define the semantics of the arrival curves model.
Section ArrivalCurves.

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

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.

Consider any job arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Definition of Arrival Curves

First, what constitutes a valid arrival bound for a task?
  Section ArrivalCurves.

We say that a given curve [num_arrivals] is a valid arrival curve for task [tsk] iff [num_arrivals] is a monotonic function that equals 0 for the empty interval [delta = 0].
    Definition valid_arrival_curve (num_arrivals : duration → nat) :=
      num_arrivals 0 = 0 ∧
      monotone num_arrivals leq.

We say that [max_arrivals] is an upper arrival bound for task [tsk] iff, for any interval [t1, t2), [max_arrivals (t2 - t1)] bounds the number of jobs of [tsk] that arrive in that interval.
    Definition respects_max_arrivals (tsk : Task) (max_arrivals : duration → nat) :=
      ∀ (t1 t2 : instant),
        t1 ≤ t2 →
        number_of_task_arrivals arr_seq tsk t1 t2 ≤ max_arrivals (t2 - t1).

We analogously define the lower arrival bound..
    Definition respects_min_arrivals (tsk : Task) (min_arrivals : duration → nat) :=
      ∀ (t1 t2 : instant),
        t1 ≤ t2 →
        min_arrivals (t2 - t1) ≤ number_of_task_arrivals arr_seq tsk t1 t2.

  End ArrivalCurves.

Definition of Minimum Distance Bounds

Next, we define the semantics of minimum-distance bounds.
  Section SeparationBound.

We say that a given function [min_separation] is a lower separation bound iff, for any number of jobs of task [tsk], [min_separation] lower-bounds the minimum interval length in which that many jobs can arrive.
    Definition respects_min_separation (tsk : Task) (min_separation: nat → duration) :=
      ∀ t1 t2,
          t1 ≤ t2 →
          min_separation (number_of_task_arrivals arr_seq tsk t1 t2) ≤ t2 - t1.

We analogously define in upper separation bounds.
    Definition respects_max_separation (tsk : Task) (max_separation: nat → duration):=
      ∀ t1 t2,
        t1 ≤ t2 →
        t2 - t1 ≤ max_separation (number_of_task_arrivals arr_seq tsk t1 t2).

  End SeparationBound.

End ArrivalCurves.

Model Validity

Based on the just-established semantics, we define the properties of a valid arrival curves model.

Section ArrivalCurvesModel.

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

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.

Consider any job arrival sequence...
  Variable arr_seq : arrival_sequence Job.

..and all kinds of arrival and separation curves.
  Context `{MaxArrivals Task}
          `{MinArrivals Task}
          `{MaxSeparation Task}
          `{MinSeparation Task}.

Let [ts] be an arbitrary task set.
  Variable ts : TaskSet Task.

We say that [arrivals] is a valid arrival curve for a task set if it is valid for any task in the task set
  Definition valid_taskset_arrival_curve (arrivals : Task → duration → nat) :=
    ∀ (tsk : Task), tsk \in ts → valid_arrival_curve (arrivals tsk).

Finally, we lift the per-task semantics of the respective arrival and separation curves to the entire task set.

  Definition taskset_respects_max_arrivals :=
    ∀ (tsk : Task), tsk \in ts → respects_max_arrivals arr_seq tsk (max_arrivals tsk).

  Definition taskset_respects_min_arrivals :=
    ∀ (tsk : Task), tsk \in ts → respects_min_arrivals arr_seq tsk (min_arrivals tsk).

  Definition taskset_respects_max_separation :=
    ∀ (tsk : Task), tsk \in ts → respects_max_separation arr_seq tsk (max_separation tsk).

  Definition taskset_respects_min_separation :=
    ∀ (tsk : Task), tsk \in ts → respects_min_separation arr_seq tsk (min_separation tsk).

End ArrivalCurvesModel.