Library prosa.analysis.facts.model.arrival_curves

Facts About Arrival Curves

We observe that tasks that exhibit job arrivals must have non-pathological arrival curves. This allows excluding pathological cases in higher-level proofs.
Consider any kind of tasks characterized by an upper-bounding arrival curve...
  Context {Task : TaskType} `{MaxArrivals Task}.
... and the corresponding type of jobs.
  Context {Job : JobType} `{JobTask Job Task}.

Consider an arbitrary task ...
  Variable tsk : Task.

... and an arrival sequence ...
  Variable arr_seq : arrival_sequence Job.

... that is compliant with the upper-bounding arrival curve.
If we have evidence that a job of the task tsk ...
  Variable j : Job.
  Hypothesis H_job_of_tsk : job_of_task tsk j.

... arrives at any point in time, ...
  Hypothesis H_arrives : arrives_in arr_seq j.

... 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 ...
  Context {Task : TaskType}.
  Context `{MaxArrivals Task}.

... and the corresponding type of jobs.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JLFP_policy Job}.

Consider any kind of processor state model...
  Context {PState : ProcessorState Job}.

... and arrival sequence.
  Variable arr_seq : arrival_sequence Job.

We consider an arbitrary task set ts ...
  Variable ts : seq Task.

... 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.
In this section, we prove a bound on the number of arrivals within a given interval under an FP policy.
Section FPArrivalBounds.

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}.

Consider any kind of processor state model...
  Context {PState : ProcessorState Job}.

... and arrival sequence.
  Variable arr_seq : arrival_sequence Job.

We consider an arbitrary task set ts ...
  Variable ts : seq Task.

... 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 of all tasks in ts whose priority is higher than or equal to that of j’s task.