Library prosa.analysis.abstract.restricted_supply.task_ibf_readiness

Require Export prosa.analysis.abstract.restricted_supply.abstract_seq_rta.
Require Export prosa.analysis.abstract.restricted_supply.iw_readiness.
Require Export prosa.analysis.definitions.sbf.busy.
Require Export prosa.analysis.definitions.workload.bounded.

Task Intra-Supply Interference is Bounded

In this file, we define the task intra-supply IBF task_intra_IBF for readiness-aware instantiation of Interference and Interfering Workload.
Section TaskIntraInterferenceIsBounded.

Consider any type of tasks ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context {Cost : JobCost Job}.
  Context `{JobArrival Job}.
  Context `{JobTask Job Task}.

Consider any kind of fully supply-consuming unit-supply uniprocessor model.
  Context `{PState : ProcessorState Job}.
  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.

Consider any definition of job readiness.
  Context `{!JobReady Job PState}.

Consider any JLFP policy that is reflexive.
  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.

We also assume that the policy respects sequential tasks.
  Hypothesis H_respects_sequential_tasks : policy_respects_sequential_tasks JLFP.

Consider any valid arrival sequence ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and a schedule of this arrival sequence.
  Variable sched : schedule PState.
  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.

Consider a readiness-aware definition of interference.
  #[local] Instance rs_jlfp_interference : Interference Job :=
    rs_readiness_jlfp_interference arr_seq sched.

Consider a readiness-aware definition of interfering workload.
  #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
    rs_readiness_jlfp_interfering_workload arr_seq sched.

Let tsk be any task to be analyzed.
  Variable tsk : Task.

Assume that there exists a bound on the service inversion experienced by any job of task tsk.
  Variable service_inversion_bound : duration → duration.
  Hypothesis H_service_inversion_is_bounded :
    service_inversion_is_bounded arr_seq sched service_inversion_bound.

Assume that there exists a bound on the higher-or-equal-priority workload from tasks different from tsk.
  Variable athep_workload_bound : duration → duration → duration.
  Hypothesis H_workload_is_bounded :
    athep_workload_is_bounded arr_seq sched tsk athep_workload_bound.

Assume that we have a bound on readiness interference.
  Variable readiness_interference_bound : duration → duration → duration.
  Hypothesis H_readiness_interference_bounded :
    readiness_interference_is_bounded arr_seq sched readiness_interference_bound.

Finally, we define the interference-bound function (task_intra_IBF).
  Definition task_intra_IBF (A R : duration) :=
    athep_workload_bound A R + service_inversion_bound A + readiness_interference_bound A R.

Next, we prove that task_intra_IBF is indeed an interference bound.
  Lemma instantiated_task_intra_interference_is_bounded :
    task_intra_interference_is_bounded_by arr_seq sched tsk task_intra_IBF.
  Proof.
    move ⇒ t1 t2 Δ j ARR TSK BUSY LT NCOMPL A OFF.
    move: (OFF _ _ BUSY) ⇒ EQA; subst A.
    have [ZERO|POS] := posnP (@job_cost _ Cost j).
    { by exfalso; rewrite /completed_by ZERO in NCOMPL. }
    eapply leq_trans; first eapply cumulative_task_interference_split ⇒ //.
    rewrite /task_intra_IBF leq_add //; last first.
    { apply leq_trans with (cumulative_readiness_interference arr_seq sched j t1 (t1 + Δ));
        first by apply leq_sum_seq ⇒ ? ? ?; lia.
      apply H_readiness_interference_bounded with (t2 := t2) ⇒ //=.
      by move: BUSY ⇒ [? ?]. }
    { rewrite leq_add //=.
      { erewrite cumulative_i_thep_eq_service_of_othep; eauto 2 ⇒ //; last first.
        { rewrite instantiated_quiet_time_equivalent_quiet_time ⇒ //; apply BUSY. }
        apply: leq_trans.
        { by apply service_of_jobs_le_workload ⇒ //; apply unit_supply_is_unit_service. }
        { by apply H_workload_is_bounded ⇒ //; apply: abstract_busy_interval_classic_quiet_time ⇒ //. } }
      { apply leq_trans with (cumulative_service_inversion arr_seq sched j t1 t2); last first.
        { apply H_service_inversion_is_bounded ⇒ //=.
          by move: BUSY ⇒ [? ?]. }
        by rewrite [X in _ ≤ X](@big_cat_nat _ _ _ (t1 + Δ)) //= leq_addr. } }
  Qed.

End TaskIntraInterferenceIsBounded.