Require Import prosa.classic.util.all.
prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.

(* Consider any task tsk with response-time bound R_tsk,
that is scheduled in an interval of length delta. *)

Variable R_tsk: time.
Variable delta: time.

(* Based on the number of jobs that execute completely in the interval, ... *)
Definition max_jobs :=

(* ... Bertogna and Cirinei's workload bound is defined as follows. *)
Definition W :=
let e_k := (task_cost tsk) in
let p_k := (task_period tsk) in
minn e_k (delta + R_tsk - e_k - max_jobs × p_k) + max_jobs × e_k.

Section BasicLemmas.

(* Let tsk be any task...*)

(* ... with period > 0. *)
Hypothesis H_period_positive: task_period tsk > 0.

(* Let R1 <= R2 be two response-time bounds that
are larger than the cost of the tsk. *)

Variable R1 R2: time.
Hypothesis H_R1_le_R2: R1 R2.

(* Then, Bertogna and Cirinei's workload bound is monotonically increasing. *)
Lemma W_monotonic :
t1 t2,
t1 t2

End BasicLemmas.

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

Variable arr_seq: arrival_sequence Job.

(* Assume that all jobs have valid parameters *)
Hypothesis H_jobs_have_valid_parameters :
j,
arrives_in arr_seq j

(* Consider any schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.

(* Assumption: jobs only execute if they arrived.
This is used to eliminate jobs that arrive after end of the interval t1 + delta. *)

Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.

(* Assumption: jobs do not execute after they completed.
This is used to eliminate jobs that complete before the start of the interval t1. *)

Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.

(* Assumption: Jobs are sequential.
This is required to use interval lengths as a measure of service. *)

Hypothesis H_sequential_jobs: sequential_jobs sched.

This is necessary to conclude that consecutive jobs ordered by arrival times
are separated by at least 'period' times units. *)

(* Before starting the proof, let's give simpler names to the definitions. *)
Let job_has_completed_by := completed job_cost sched.

(* Now we define the theorem. Let tsk be any task in the taskset. *)

(* Assumption: the task must have valid parameters:
a) period > 0 (used in divisions)
c) cost <= period
(used to prove that the distance between the first and last
jobs is at least (cost + n*period), where n is the number
of middle jobs. If cost >> period, the claim does not hold

This is required to prove that n_k (max_jobs) from Bertogna
and Cirinei's formula accounts for at least the number of
middle jobs (i.e., number of jobs - 2 in the worst case). *)

(* Consider an interval t1, t1 + delta). *)
Variable t1 delta: time.

(* Assume that a response-time bound R_tsk for that task in any
schedule of this processor platform is also given, ... *)

Variable R_tsk: time.

Hypothesis H_response_time_bound :
j,
arrives_in arr_seq j
job_arrival j + R_tsk < t1 + delta
job_has_completed_by j (job_arrival j + R_tsk).

Section MainProof.

(* In this section, we prove that the workload of a task in the
interval t1, t1 + delta) is bounded by W. *)

(* Let's simplify the names a bit. *)
Let t2 := t1 + delta.

(* Since we only care about the workload of tsk, we restrict
our view to the set of jobs of tsk scheduled in t1, t2). *)

Let scheduled_jobs :=

(* Now, let's consider the list of interfering jobs sorted by arrival time. *)
Let earlier_arrival := fun x yjob_arrival x job_arrival y.
Let sorted_jobs := sort earlier_arrival scheduled_jobs.

(* The first step consists in simplifying the sum corresponding

Section SimplifyJobSequence.

(* After switching to the definition of workload based on a list
of jobs, we show that sorting the list preserves the sum. *)

\sum_(i <- sorted_jobs) service_during sched i t1 t2.

(* Remember that both sequences have the same set of elements *)
j,
(j \in scheduled_jobs) = (j \in sorted_jobs).

(* Remember that all jobs in the sorted sequence is an
interfering job of task tsk. *)

j_i,
j_i \in sorted_jobs
arrives_in arr_seq j_i
service_during sched j_i t1 t2 != 0
j_i \in jobs_scheduled_between sched t1 t2.

(* Remember that consecutive jobs are ordered by arrival. *)
i elem,
i < (size sorted_jobs).-1
earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).

End SimplifyJobSequence.

(* Next, we show that if the number of jobs is no larger than n_k,
the workload bound trivially holds. *)

size sorted_jobs n_k
\sum_(i <- sorted_jobs) service_during sched i t1 t2

(* Otherwise, assume that the number of jobs is larger than n_k >= 0.
First, consider the simple case with only one job. *)

(* Assume that there's at least one job in the sorted list. *)
Hypothesis H_at_least_one_job: size sorted_jobs > 0.

Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.

(* The first job is an interfering job of task tsk. *)
arrives_in arr_seq j_fst
service_during sched j_fst t1 t2 != 0
j_fst \in jobs_scheduled_between sched t1 t2.

(* The workload bound holds for the single job. *)
\sum_(0 i < 1) service_during sched (nth elem sorted_jobs i) t1 t2

(* Next, consider the last case where there are at least two jobs:
the first job j_fst, and the last job j_lst. *)

(* There are at least two jobs. *)
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.

Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.

(* The last job is an interfering job of task tsk. *)
arrives_in arr_seq j_lst
service_during sched j_lst t1 t2 != 0
j_lst \in jobs_scheduled_between sched t1 t2.

(* The response time of the first job must fall inside the interval. *)
t1 job_arrival j_fst + R_tsk.

(* The arrival of the last job must also fall inside the interval. *)
job_arrival j_lst < t2.

(* Next, we upper-bound the service of the first and last jobs using their arrival times. *)
service_during sched j_fst t1 t2 +
service_during sched j_lst t1 t2
(job_arrival j_fst + R_tsk - t1) + (t2 - job_arrival j_lst).

(* Simplify the expression from the previous lemma. *)
job_arrival j_fst + R_tsk - t1 + (t2 - job_arrival j_lst) =
delta + R_tsk - (job_arrival j_lst - job_arrival j_fst).

(* Bound the service of the middle jobs. *)
\sum_(0 i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2

(* Conclude that the distance between first and last is at least num_mid_jobs + 1 periods. *)
job_arrival j_lst - job_arrival j_fst num_mid_jobs.+1 × (task_period tsk).

(* Prove that n_k is at least the number of the middle jobs *)
n_k num_mid_jobs.

(* If n_k = num_mid_jobs, then the workload bound holds. *)
num_mid_jobs = n_k
service_during sched j_lst t1 t2 +
service_during sched j_fst t1 t2 +
\sum_(0 i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2

(* If n_k = num_mid_jobs + 1, then the workload bound holds. *)
num_mid_jobs.+1 = n_k
service_during sched j_lst t1 t2 +
service_during sched j_fst t1 t2 +
\sum_(0 i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2