Library prosa.analysis.abstract.ideal.cumulative_bounds

In this file, we prove some inequalities that always hold inside the busy interval of a job. Throughout this file we assume the ideal uniprocessor model.
Consider any kind of tasks and their jobs, each characterized by an arrival time, a cost, and an arbitrary notion of readiness.
  Context {Task : TaskType} {Job : JobType} `{JobTask Job Task}.
  Context `{JobArrival Job} `{JobCost Job} {JR :JobReady Job (ideal.processor_state Job)}.

Consider a JLFP policy that is reflexive and respects sequential tasks.
Consider a consistent arrival sequence that does not contain duplicates.
Consider any valid ideal uniprocessor schedule defined over this arrival sequence.
Consider a set of tasks ts that contains all the jobs in the arrival sequence.
  Variable ts : list Task.
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

Consider a task tsk.
  Variable tsk : Task.

Consider a job j of the task tsk that has a positive job cost.
  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_of_tsk : job_of_task tsk j.
  Hypothesis H_job_cost_positive: job_cost_positive j.

Consider the ideal JLFP definitions of interference and interfering workload.
Consider the busy interval for j is given by [t1,t2).
  Variable t1 t2 : duration.
  Hypothesis H_busy_interval : definitions.busy_interval sched j t1 t2.

Let us denote the relative arrival time by A.
  Let A := job_arrival j - t1.

Consider any arbitrary time Δ inside the busy interval.
  Variable Δ : duration.
  Hypothesis H_Δ_in_busy : t1 + Δ t2.

First, we prove that if the priority inversion is bounded then, the cumulative priority inversion is also bounded.
  Section PIBound.

Consider the priority inversion in any given interval is bounded by a constant.
Then, the cumulative priority inversion in any interval is also bounded.
    Lemma cumulative_priority_inversion_is_bounded:
      cumulative_priority_inversion arr_seq sched j t1 (t1 + Δ)
       priority_inversion_bound (job_arrival j - t1).
    Proof.
      apply leq_trans with (cumulative_priority_inversion arr_seq sched j t1 t2).
      - rewrite [X in _ X](@big_cat_nat _ _ _ (t1 + Δ)) //=; try by lia.
        by rewrite /priority_inversion leq_addr.
      - apply: H_priority_inversion_is_bounded ⇒ //.
        by move: H_busy_interval; rewrite -instantiated_busy_interval_equivalent_busy_interval // ⇒ -[PREF _].
    Qed.

  End PIBound.

Let jobs denote the arrivals in the interval Δ.
Next, we prove that the cumulative interference from higher priority jobs of other tasks in an interval is bounded by the total service received by the higher priority jobs of those tasks.
  Lemma cumulative_interference_is_bounded_by_total_service:
    cumulative_another_task_hep_job_interference arr_seq sched j t1 (t1 + Δ)
     service_of_jobs sched (fun joanother_task_hep_job jo j) jobs t1 (t1 + Δ).
  Proof.
    move: (H_busy_interval) ⇒ [[/andP [JINBI JINBI2] [QT _]] _].
    rewrite cumulative_i_thep_eq_service_of_othep ⇒ //.
    have /eqP TSK := H_job_of_tsk.
    by rewrite instantiated_quiet_time_equivalent_quiet_time.
  Qed.

End BusyIntervalInequalities.