Library probsa.util.prosa.arrival_bound

Require Import prosa.util.all.
Require Export prosa.model.task.arrival.sporadic.
Require Export prosa.analysis.facts.model.task_arrivals.

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.

We observe that when dividing a value exceeding T × n, then the ceiling exceeds n.
Lemma div_ceil_multiple :
  ∀ Δ T n,
    T > 0 →
    (T × n) < Δ →
    n < div_ceil Δ T.

Sporadic Arrival Bound

In the following, we upper bound the number of jobs that can arrive in any interval as constrained by the sporadic task model's minimum inter-arrival time task_min_inter_arrival_time.
Section SporadicArrivalBound.

Consider any sporadic tasks ...
  Context {Task : TaskType} `{SporadicModel Task}.

... and their jobs.
  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

We define the classic "ceiling of the interval length divided by minimum inter-arrival time", which we prove to be correct in the following.
  Definition max_sporadic_arrivals (tsk : Task) (delta : duration) :=
    div_ceil delta (task_min_inter_arrival_time tsk).

To establish the bound's soundness, consider any well-formed arrival sequence, ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any valid sporadic task tsk to be analyzed.
  Variable tsk : Task.
  Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
  Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.

  Section ArrivalTimes.

Similarly, to simplify subsequent proofs, we restate the H_consistent_arrival_times assumption as a trivial corollary.
    Lemma job_arrival_at :
      ∀ {j t},
        j \in arrivals_at arr_seq t → job_arrival j = t.

We observe that, by construction, the sequence of arrivals is sorted by arrival times. To this end, we first define the order relation.
    Definition by_arrival_times (j1 j2 : Job) : bool := job_arrival j1 ≤ job_arrival j2.

Trivially, the arrivals at any one point in time are ordered w.r.t. arrival times.
    Lemma arrivals_at_sorted :
      ∀ t,
        sorted by_arrival_times (arrivals_at arr_seq t).

By design, the list of arrivals in any interval is sorted.
    Lemma arrivals_between_sorted :
      ∀ t1 t2,
        sorted by_arrival_times (arrivals_between arr_seq t1 t2).

    Corollary task_arrivals_between_sorted :
      ∀ t1 t2,
        sorted by_arrival_times (task_arrivals_between arr_seq tsk t1 t2).

  End ArrivalTimes.

The same observation applies to task_arrivals_between.
  Lemma task_arrivals_between_uniq :
    ∀ t1 t2,
      arrival_sequence_uniq arr_seq →
      uniq (task_arrivals_between arr_seq tsk t1 t2).

For convenience, we restate the left bound of the above lemma...
  Corollary job_arrival_between_ge :
    ∀ {j t1 t2},
      j \in arrivals_between arr_seq t1 t2 → t1 ≤ job_arrival j.

  Corollary job_arrival_between_lt :
    ∀ {j t1 t2},
      j \in arrivals_between arr_seq t1 t2 → job_arrival j < t2.

Any job j in task_arrivals_between arr_seq tsk t1 t2 is also contained in arrivals_between arr_seq t1 t2.
  Lemma task_arrivals_between_subset:
    ∀ t1 t2 j,
      j \in task_arrivals_between arr_seq tsk t1 t2 →
            j \in arrivals_between arr_seq t1 t2.

Before we can establish the bound, we require two auxiliary bounds, which we derive next. First, we consider minimum offset of the n-th job of the task that arrives in a given interval.
  Section NthJob.

For technical reasons, we require a "dummy" job in scope to use the nth function. In the proofs, we establish that the dummy job is never used, i.e., it is an irrelevant artifact induced by the ssreflect API. It may be safely ignored.
    Variable dummy : Job.

We observe that the i-th job to arrive in an interval [t1,t2) arrives no earlier than (task_min_inter_arrival_time tsk) ×i time units after the beginning of the interval due the minimum inter-arrival time of the sporadic task.
    Lemma arrival_of_nth_job :
      ∀ t1 t2 n i j,
        n = number_of_task_arrivals arr_seq tsk t1 t2 →
        i < n →
        j = nth dummy (task_arrivals_between arr_seq tsk t1 t2) i →
        job_arrival j ≥ t1 + (task_min_inter_arrival_time tsk) × i.

  End NthJob.

As a second auxiliary lemma, we establish a minimum length on the interval for a given number of arrivals by applying the previous lemma to the last job in the interval. We consider only the case of "many" jobs, i.e., n ≥ 2, which ensures that the interval [t1, t2) spans at least one inter-arrival time.
  Lemma minimum_distance_for_n_sporadic_arrivals:
    ∀ t1 t2 n,
      number_of_task_arrivals arr_seq tsk t1 t2 = n →
      n ≥ 2 →
      t2 > t1 + (task_min_inter_arrival_time tsk) × n.-1.

Based on the above lemma, it is easy to see that max_sporadic_arrivals is indeed a correct upper bound on the maximum number of arrivals in a given interval.
  Theorem sporadic_task_arrivals_bound:
    ∀ t1 t2,
      number_of_task_arrivals arr_seq tsk t1 t2 ≤ max_sporadic_arrivals tsk (t2 - t1).

End SporadicArrivalBound.