Library prosa.model.task.arrival.sporadic_as_curve

Arrival Curve for Sporadic Tasks
Any analysis that supports arbitrary arrival curves can also be used to analyze sporadic tasks. We establish this link below.
Consider any type of sporadic tasks.
  Context {Task : TaskType} `{SporadicModel Task}.

The bound on the maximum number of arrivals in a given interval max_sporadic_arrivals is in fact a valid arrival curve, which we note with the following arrival-curve declaration.
  Global Program Instance MaxArrivalsSporadic : MaxArrivals Task := max_sporadic_arrivals.

It remains to be shown that max_sporadic_arrivals satisfies all expectations placed on arrival curves. First, we observe that the bound is structurally sound.
  Lemma sporadic_arrival_curve_valid :
      valid_arrival_curve (max_sporadic_arrivals tsk).
    movetsk; split; first exact: div_ceil0.
    movedelta1 delta2 LEQ.
    exact: div_ceil_monotone1.

For convenience, we lift the preceding observation to the level of entire task sets.
  Remark sporadic_task_sets_arrival_curve_valid :
      valid_taskset_arrival_curve ts max_arrivals.
  Proof. move⇒ ? ? ?; exact: sporadic_arrival_curve_valid. Qed.

Next, we note that it is indeed an arrival bound. To this end, consider any type of jobs stemming from these tasks ...
  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

... and any well-formed arrival sequence of such jobs.
We establish the validity of the defined curve.
  Section Validity.

Let tsk denote any valid sporadic task to be analyzed.
We observe that max_sporadic_arrivals is indeed an upper bound on the maximum number of arrivals.
    Lemma sporadic_arrival_curve_respects_max_arrivals :
      respects_max_arrivals arr_seq tsk (max_sporadic_arrivals tsk).
    Proof. by movet1 t2 LEQ; apply: sporadic_task_arrivals_bound. Qed.

  End Validity.

For convenience, we lift the preceding observation to the level of entire task sets.
  Remark sporadic_task_sets_respects_max_arrivals :
      valid_taskset_inter_arrival_times ts
      taskset_respects_sporadic_task_model ts arr_seq
      taskset_respects_max_arrivals arr_seq ts.
    movets VAL SPO tsk IN.
    apply: sporadic_arrival_curve_respects_max_arrivals.
    - exact: SPO.
    - exact: VAL.

End SporadicArrivalCurve.

We add the lemmas into the "Hint Database" basic_rt_facts so that they become available for proof automation.
Global Hint Resolve
  : basic_rt_facts.