Library rt.model.arrival.basic.arrival_bounds

Require Import rt.util.all.
Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival
Require Import rt.model.schedule.uni.basic.busy_interval.

(* Properties of job arrival. *)
Module ArrivalBounds.

  Import ArrivalSequence SporadicTaskset TaskArrival Priority BusyInterval.

  Section Lemmas.

    Context {Task: eqType}.
    Variable task_period: Task time.

    Context {Job: eqType}.
    Variable job_arrival: Job time.
    Variable job_cost: Job time.
    Variable job_task: Job Task.

    (* Consider any job arrival sequence with consistent, duplicate-free arrivals. *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
    Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.

    (* In this section, we upper bound the number of jobs that can arrive in any interval. *)
    Section BoundOnSporadicArrivals.

      (* Assume that jobs are sporadic. *)
      Hypothesis H_sporadic_tasks: sporadic_task_model task_period job_arrival job_task arr_seq.

      (* Consider any time interval [t1, t2)... *)
      Variable t1 t2: time.

      (* ...and let tsk be any task with period > 0. *)
      Variable tsk: Task.
      Hypothesis H_period_gt_zero: task_period tsk > 0.

      (* Recall the jobs of tsk during [t1, t2), along with the number of arrivals. *)
      Let arriving_jobs := arrivals_of_task_between job_task arr_seq tsk t1 t2.
      Let num_arrivals := num_arrivals_of_task job_task arr_seq tsk t1 t2.

      (* We will establish an upper bound on the number of arriving jobs of tsk.
         The proof follows by case analysis. *)

      (* Case 1: Assume that no jobs of tsk arrive in the interval. *)
      Section NoJobs.

        (* If there are no arriving jobs in [t1, t2), ...*)
        Hypothesis H_no_jobs: num_arrivals = 0.

        (* ...then the arrival bound trivially holds. *)
        Lemma sporadic_arrival_bound_no_jobs:
          num_arrivals div_ceil (t2 - t1) (task_period tsk).

      End NoJobs.

      (* Case 2: Assume that a single job of tsk arrives in the interval. *)
      Section OneJob.

        (* First, note that since the interval is open at time t2,
           t2 must be larger than t1. *)

        Lemma sporadic_arrival_bound_more_than_one_point:
          num_arrivals > 0
          t1 < t2.

        (* Therefore, if there is one job of tsk arriving during [t1, t2), ... *)
        Hypothesis H_no_jobs: num_arrivals = 1.

        (* ...then (t2 - t1) > 0 and the arrival bound also holds. *)
        Lemma sporadic_arrival_bound_one_job:
          num_arrivals div_ceil (t2 - t1) (task_period tsk).

      End OneJob.

      (* Case 3: There are at least two arriving jobs. *)
      Section AtLeastTwoJobs.

        (* Assume that there are at least two jobs of tsk arriving in [t1,t2). *)
        Hypothesis H_at_least_two_jobs: num_arrivals 2.

        (* We prove the arrival bound by contradiction. *)
        Section DerivingContradiction.

          (* Suppose that the number of arrivals is larger than the bound. *)
          Hypothesis H_many_arrivals: div_ceil (t2 - t1) (task_period tsk) < num_arrivals.

          (* Consider the list of jobs ordered by arrival times. *)
          Let by_arrival_time j j' := job_arrival j job_arrival j'.
          Let sorted_jobs := sort by_arrival_time arriving_jobs.

          (* Based on the notation for the n-th job in the sorted list of arrivals, ... *)
          Variable elem: Job.
          Let nth_job := nth elem sorted_jobs.

          (* ...we identify the first and last jobs and their respective arrival times. *)
          Let j_first := nth_job 0.
          Let j_last := nth_job (num_arrivals.-1).
          Let a_first := job_arrival j_first.
          Let a_last := job_arrival j_last.

          (* Recall from task_arrival.v the properties of the n-th job ...*)
          Corollary sporadic_arrival_bound_properties_of_nth:
              idx < num_arrivals
              t1 job_arrival (nth_job idx) < t2
              job_task (nth_job idx) = tsk
              arrives_in arr_seq (nth_job idx).

          (* ...and the distance between the first and last jobs. *)
          Corollary sporadic_arrival_bound_distance_between_first_and_last:
            a_last a_first + (num_arrivals-1) × task_period tsk.

          (* Because the number of arrivals is larger than the ceiling term,
             it follows that the first and last jobs are separated by at
             least the length of the interval, ... *)

          Lemma sporadic_arrival_bound_last_job_too_far:
            a_first + t2 - t1 a_last.

          (* ...which implies that the last job arrives after the interval. *)
          Lemma sporadic_arrival_bound_last_arrives_too_late:
            a_last t2.

          (* However, the last job must lie within [t1, t2). Contradiction! *)
          Lemma sporadic_arrival_bound_case_3_contradiction: False.

        End DerivingContradiction.

        (* From the contradiction above, we prove that the arrival bound
           is correct for case 3 (i.e., at least two arriving jobs). *)

        Lemma sporadic_task_arrival_bound_at_least_two_jobs:
          num_arrivals div_ceil (t2 - t1) (task_period tsk).

      End AtLeastTwoJobs.

      (* Using the case analysis, we prove that the number of job arrivals of tsk
         can be upper-bounded using the length of the interval as follows. *)

      Theorem sporadic_task_arrival_bound:
        num_arrivals div_ceil (t2 - t1) (task_period tsk).

    End BoundOnSporadicArrivals.

  End Lemmas.

End ArrivalBounds.