Library prosa.analysis.facts.model.exceedance.SBF

Require Export prosa.analysis.facts.model.ideal_uni_exceed.
Require Export prosa.analysis.definitions.sbf.sbf.
Require Export prosa.analysis.definitions.sbf.busy.
Require Export prosa.model.processor.ideal_uni_exceed.

In this file, we instantiate the supply-bound function for ideal uniprocessors with exceedance.
Let us state the definition first.
Section SBFDefinition.

Let e be the bound on exceedance in any busy window.
  Variable e : work.
Then, the SBF is defined as follows.
  Definition eps_sbf (Δ : nat) : work := Δ - e.

End SBFDefinition.

Next, we establish some facts about the above-defined SBF.
Section SBFFacts.

Consider tasks characterized by nominal execution times ...
  Context {Task : TaskType} `{TaskCost Task}.

... and their associated jobs with costs and arrival times.
  Context {Job : JobType} `{JobTask Job Task}
          `{JobCost Job} `{JobArrival Job}.

Consider any JLFP policy.
  Context `{JLFP_policy Job}.

Assume an arrival sequence ...
  Variable arr_seq : arrival_sequence Job.

... and a corresponding ideal uniprocessor schedule subject to exceedance.
  Variable sched : schedule (exceedance_proc_state Job).

Assume e is the bound on exceedance in a busy interval ...
  Variable e : work.

... of a given task tsk.
  Variable tsk : Task.

Let us state the exceedance using Instance to make it locally available to the typeclasses database.
  #[local] Instance EPS_SBF_inst : SupplyBoundFunction := eps_sbf e.

Let us formally state the assumption that the total exceedance inside the busy interval of tsk is bounded by e.
  Hypothesis H_exceedance_in_busy_interval_bounded :
    ∀ j t1 t2,
      arrives_in arr_seq j →
      job_of_task tsk j →
        busy_interval_prefix arr_seq sched j t1 t2 →
        \sum_(t1 ≤ t < t2) is_exceedance_exec (sched t) ≤ e.

Since we model exceedance as blackouts, we trivially have that the blackouts are bounded by e.
  Lemma blackout_during_bounded j t1 t2 t :
    arrives_in arr_seq j →
    job_of_task tsk j →
    busy_interval_prefix arr_seq sched j t1 t2 →
    t1 ≤ t ≤ t2 →
    blackout_during sched t1 t ≤ e.
  Proof.
    move ⇒ ARRIN TSK PRE /andP[INEQ1 INEQ2].
    rewrite /blackout_during.
    rewrite (eq_sum_seq _ _ _ _ (fun t ⇒ is_exceedance_exec (sched t))).
    - specialize ( H_exceedance_in_busy_interval_bounded j t1 t2 ).
      feed_n 3 H_exceedance_in_busy_interval_bounded ⇒ //=.
      apply: leq_trans; last by apply H_exceedance_in_busy_interval_bounded.
      rewrite (big_cat_nat _ INEQ2) //=.
      by lia.
    - move ⇒ t' /[!mem_index_iota]IN _.
       rewrite blackout_implies_exceedance_execution.
       by apply /eqP.
  Qed.

Using the above, we can prove that our definition of SBF is valid.
  Lemma eps_sbf_is_valid : valid_busy_sbf arr_seq sched tsk EPS_SBF_inst.
  Proof.
    rewrite /valid_busy_sbf /valid_pred_sbf /EPS_SBF_inst /eps_sbf //=.
    split; first lia.
    rewrite /pred_sbf_respected ⇒ j t1 t2 ARRIN [TSK BUSYPREFIX] t LEQ.
    have Hsplit : t = t1 + (t - t1) by lia.
    rewrite Hsplit.
    have → : t1 + (t - t1) - t1 - e = (t - t1) - e by lia.
    set (Δ := (t - t1)) in ×.
    have ? : Δ - supply_during sched t1 (t1 + Δ) ≤ e; try lia.
    rewrite -blackout_during_complement //=.
    apply: blackout_during_bounded ⇒ //=.
    by lia.
  Qed.

Finally, we prove that our SBF only takes steps of one unit.
  Lemma eps_sbf_is_unit : unit_supply_bound_function EPS_SBF_inst.
  Proof.
    rewrite /unit_supply_bound_function ⇒ Δ.
    rewrite /EPS_SBF_inst /eps_sbf //=.
    by lia.
  Qed.

End SBFFacts.