Library rt.restructuring.model.arrival.arrival_curves
In this section, we define the notion of arrival curves, which can
be used to reason about the frequency of job arrivals.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Consider any job arrival sequence.
First, we define what constitutes an arrival bound for a task.
We say that 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 (tsk : Task) (num_arrivals : duration → nat) :=
num_arrivals 0 = 0 ∧
monotone num_arrivals leq.
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).
∀ (t1 t2 : instant),
t1 ≤ t2 →
number_of_task_arrivals arr_seq tsk t1 t2 ≤ max_arrivals (t2 - t1).
We define in the same way lower arrival bounds.
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.
Section SeparationBound.
∀ (t1 t2 : instant),
t1 ≤ t2 →
min_arrivals (t2 - t1) ≤ number_of_task_arrivals arr_seq tsk t1 t2.
End ArrivalCurves.
Section SeparationBound.
Then, we say that 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 number
of jobs can be spawned.
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.
∀ t1 t2,
t1 ≤ t2 →
min_separation (number_of_task_arrivals arr_seq tsk t1 t2) ≤ t2 - t1.
We define in the same way 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.
∀ t1 t2,
t1 ≤ t2 →
t2 - t1 ≤ max_separation (number_of_task_arrivals arr_seq tsk t1 t2).
End SeparationBound.
End ArrivalCurves.
We define generic classes for arrival curves
Class MaxArrivals (Task : TaskType) := max_arrivals : Task → duration → nat.
Class MinArrivals (Task : TaskType) := min_arrivals : Task → duration → nat.
Class MaxSeparation (Task : TaskType) := max_separation : Task → nat → duration.
Class MinSeparation (Task : TaskType) := min_separation : Task → nat → duration.
Section ArrivalCurvesModel.
Class MinArrivals (Task : TaskType) := min_arrivals : Task → duration → nat.
Class MaxSeparation (Task : TaskType) := max_separation : Task → nat → duration.
Class MinSeparation (Task : TaskType) := min_separation : Task → nat → duration.
Section ArrivalCurvesModel.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Consider any job arrival sequence...
..and all the classes of arrival curves.
Let ts be an arbitrary task set.
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 tsk (arrivals tsk).
∀ (tsk : Task), tsk \in ts → valid_arrival_curve tsk (arrivals tsk).
We say that max_arrivals is an arrival bound for a task set
ts iff max_arrivals is an arrival bound for any task in
ts.
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.
∀ (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.