Library prosa.analysis.facts.model.arrival_curves
Require Export prosa.util.epsilon.
Require Export prosa.model.priority.classes.
Require Export prosa.model.task.arrival.curves.
Require Export prosa.analysis.facts.model.task_arrivals.
Require Export prosa.model.priority.classes.
Require Export prosa.model.task.arrival.curves.
Require Export prosa.analysis.facts.model.task_arrivals.
Facts About Arrival Curves
Consider any kind of tasks characterized by an upper-bounding arrival curve...
... and the corresponding type of jobs.
Consider an arbitrary task ...
... and an arrival sequence ...
... that is compliant with the upper-bounding arrival curve.
If we have evidence that a job of the task tsk ...
... arrives at any point in time, ...
... then the maximum number of job arrivals in a non-empty interval cannot
be zero.
We add the above lemma to the global hints database.
Global Hint Resolve non_pathological_max_arrivals : basic_rt_facts.
In the following section, we prove a bound on the number of
arrivals within a given interval under an arbitrary JLFP
policy.
Consider any type of tasks ...
... and the corresponding type of jobs.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JLFP_policy Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JLFP_policy Job}.
Consider any kind of processor state model...
... and arrival sequence.
We consider an arbitrary task set ts ...
... and assume that all jobs stem from tasks in this task set.
We assume that max_arrivals is a family of valid arrival
curves that constrains the arrival sequence arr_seq, i.e., for
any task tsk in ts, max_arrival tsk is an arrival bound of
tsk.
We prove that the number of jobs that arrive in the interval
[t1, t1 + Δ)
and have higher-or-equal priority than a given
job j is bounded by the sum of arrival curves for all tasks in
ts.
Lemma jlfp_hep_arrivals_bounded_by_sum_max_arrivals :
∀ (j : Job) (t1 : instant) (Δ : duration),
size [seq jhp <- arrivals_between arr_seq t1 (t1 + Δ) | hep_job jhp j]
≤ \sum_(tsk <- ts) max_arrivals tsk Δ.
End JLFPArrivalBounds.
∀ (j : Job) (t1 : instant) (Δ : duration),
size [seq jhp <- arrivals_between arr_seq t1 (t1 + Δ) | hep_job jhp j]
≤ \sum_(tsk <- ts) max_arrivals tsk Δ.
End JLFPArrivalBounds.
In this section, we prove a bound on the number of arrivals within
a given interval under an FP policy.
Consider any type of tasks ...
Context {Task : TaskType}.
Context `{MaxArrivals Task}.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{FP_policy Task}.
Context `{MaxArrivals Task}.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{FP_policy Task}.
Consider any kind of processor state model...
... and arrival sequence.
We consider an arbitrary task set ts ...
... and assume that all jobs stem from tasks in this task set.
We assume that max_arrivals is a family of valid arrival
curves that constrains the arrival sequence arr_seq, i.e., for
any task tsk in ts, max_arrival tsk is an arrival bound of
tsk.