# Library prosa.classic.model.arrival.jitter.arrival_bounds

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.jitter.job
prosa.classic.model.arrival.jitter.arrival_sequence
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path div.

(* In this file, we prove bounds on the number of actual task arrivals, i.e,
taking release jitter into account. *)

Module ArrivalBounds.

Section BoundingActualArrivals.

Context {Job: eqType}.
Variable job_arrival: Job time.
Variable job_cost: Job time.
Variable job_jitter: Job time.

(* 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.

(* ...where the jitter of each job is bounded by the jitter of its task. *)
Hypothesis H_job_jitter_bounded:
j,
arrives_in arr_seq j

(* For simplicity, let's define some local names. *)
Let actual_job_arrival := actual_arrival job_arrival job_jitter.

(* In this section, we prove an upper bound on the number of jobs with actual arrival time
in a given interval. *)

Section UpperBoundOn.

(* Assume that jobs are sporadic. *)

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

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

(* Recall the jobs of tsk with actual arrival time in t1, t2), along with the corresponding number of arrivals. *)
Let actual_arrivals := actual_arrivals_of_task_between job_arrival job_jitter
arr_seq tsk t1 t2.

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

(* Case 1: Assume that there are no jobs of tsk with actual arrival time in the interval. *)
Section NoJobs.

(* If there are no actual arrivals in t1, t2), *)
Hypothesis... H_no_jobs: num_actual_arrivals = 0.

(* ...then the arrival bound trivially holds. *)

End NoJobs.

(* Case 2: Assume that a single job of tsk has actual arrival time in the interval. *)
Section OneJob.

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

num_actual_arrivals > 0
t1 < t2.

(* Therefore, if there is one job of tsk with actual arrival time in t1, t2), ... *)
Hypothesis H_no_jobs: num_actual_arrivals = 1.

(* ...then (t2 - t1) > 0 and the arrival bound also holds. *)

End OneJob.

(* Case 3: There are at least two actual job arrivals. *)
Section AtLeastTwoJobs.

(* Assume that there are at least two jobs of tsk with actual arrival in t1,t2). *)
Hypothesis H_at_least_two_jobs: num_actual_arrivals 2.

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

(* Suppose that the number of arrivals is larger than the bound. *)
Hypothesis H_many_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 actual_arrivals.

(* 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_actual_arrivals.-1).
Let a_first := job_arrival j_first.
Let a_last := job_arrival j_last.

(* Next, we recall from task_arrival.v the properties of the n-th job in
the sequence... *)

idx,
idx < num_actual_arrivals
t1 actual_job_arrival (nth_job idx) < t2
arrives_in arr_seq (nth_job idx).

(* ...and that the first and last jobs are separated by at least
(num_actual_arrivals - 1) periods. *)

a_last a_first + (num_actual_arrivals - 1) × task_period tsk.

(* Next, because the number of actual 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 plus the jitter of the task, ... *)

a_first + t2 + task_jitter tsk - t1 a_last.

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

(* However, the actual arrival time of the last job must lie within t1, t2). Contradiction! *)

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

End AtLeastTwoJobs.

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