Library prosa.analysis.facts.model.overheads.sbf.fp

Require Export prosa.analysis.facts.readiness.basic.
Require Export prosa.analysis.facts.model.overheads.blackout_bound.
Require Export prosa.analysis.facts.model.overheads.schedule_change_bound.
Require Export prosa.analysis.definitions.sbf.busy.

In this section, we define an SBF for the FP scheduling policy in the presence of overheads.
Section OverheadResourceModelValidSBF.

Consider any type of tasks...
  Context {Task : TaskType}.
  Context {FP : FP_policy Task}.
  Context `{MaxArrivals Task}.

... an arbitrary task set ts, ...
  Variable ts : seq Task.

... and bounds DB, CSB, and CRPDB on dispatch overhead, context-switch overhead, and preemption-related overhead, respectively.
  Variable DB CSB CRPDB : duration.

Consider a task tsk.
  Variable tsk : Task.

We define the blackout bound for FP in an interval of length Δ as the number of jobs with higher-or-equal priority (w.r.t. a given task tsk) that can arrive in Δ times two, plus one, multiplied by the sum of all overhead bounds.
The "+1" accounts for the fact that n arrivals can result in up to 1 + 2n segments without a schedule change, and thus up to 1 + 2n intervals wherein overhead duration is bounded by DB + CSB + CRPDB.
Under FP scheduling the set of tasks that needs to be considered is restricted: only jobs of tasks with higher-or-equal priority relative to tsk can cause schedule changes, which allows the blackout bound to be stated in terms of this subset of tasks.
  Definition fp_blackout_bound (Δ : duration) :=
    (DB + CSB + CRPDB) × (1 + 2 × \sum_(tsko <- ts | hep_task tsko tsk) max_arrivals tsko Δ).

We define FP's SBF as the interval length minus the (slowed-down) blackout bound in the same interval.
The slowdown ensures that the resulting SBF is monotonic and unit-growth, which is necessary to obtain response-time bounds using aRTA.
  #[local] Instance fp_ovh_sbf : SupplyBoundFunction :=
    fun Δ ⇒ Δ - slowed fp_blackout_bound Δ.

End OverheadResourceModelValidSBF.

In the following section, we show that the SBF defined above is indeed a valid SBF.
Section OverheadResourceModelValidSBF.

We assume the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready.
  #[local] Existing Instance basic_ready_instance.

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

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

Consider an FP-policy that indicates a higher-or-equal priority relation, and assume that this relation is reflexive and transitive.
  Context {FP : FP_policy Task}.
  Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
  Hypothesis H_priority_is_transitive : transitive_task_priorities FP.

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

... and any explicit-overhead uni-processor schedule without superfluous preemptions of this arrival sequence.
  Variable sched : schedule (overheads.processor_state Job).
  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
  Hypothesis H_work_conserving : work_conserving arr_seq sched.
  Hypothesis H_no_superfluous_preemptions : no_superfluous_preemptions sched.

Assume that the schedule respects the FP policy.
  Hypothesis H_respects_policy :
    respects_FP_policy_at_preemption_point arr_seq sched FP.

Assume that the preemption model is valid.
  Hypothesis H_valid_preemption_model :
    valid_preemption_model arr_seq sched.

We consider an arbitrary task set ts ...
  Variable ts : seq Task.

... and assume that all jobs stem from tasks in this task set.
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

We assume that max_arrivals is a family of valid arrival curves that constrains the arrival sequence arr_seq, i.e., for any task tsk in ts, max_arrival tsk is (1) an arrival bound of tsk, and ...
  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.

... (2) a monotonic function that equals 0 for the empty interval delta = 0.
  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.

We assume that all jobs have positive cost. This restriction is not fundamental to the analysis, but rather an artifact of the current proof structure in the library.
  Hypothesis H_all_jobs_have_positive_cost :
    ∀ j,
      arrives_in arr_seq j →
      job_cost_positive j.

Finally, we assume that the schedule respects a valid overhead resource model with dispatch overhead DB, context-switch overhead CSB, and preemption-related overhead CRPDB.
  Variable DB CSB CRPDB : duration.
  Hypothesis H_valid_overheads_model :
    overhead_resource_model sched DB CSB CRPDB.

We show that the SBF is monotone.
  Lemma overheads_sbf_monotone :
    ∀ tsk,
      sbf_is_monotone (fp_ovh_sbf ts DB CSB CRPDB tsk).
  Proof.
    move⇒ tsk x y NEQ.
    interval_to_duration x y k.
    have EQ: ∀ a b c d, (a + d ≤ b + c) → (a - b ≤ c - d). { clear. intros. lia. }
    apply: EQ.
    rewrite [in leqRHS]addnC -addnA leq_add2l.
    apply unit_growth_function_k_steps_bounded.
    by apply slowed_is_unit_step.
  Qed.

The introduced SBF is also a unit-supply SBF.
  Lemma overheads_sbf_unit :
    ∀ tsk,
      unit_supply_bound_function (fp_ovh_sbf ts DB CSB CRPDB tsk).
  Proof.
    move⇒ tsk δ; rewrite/fp_ovh_sbf.
    have LE:
      slowed (fp_blackout_bound ts DB CSB CRPDB tsk) δ
      ≤ slowed (fp_blackout_bound ts DB CSB CRPDB tsk) δ.+1.
    { apply slowed_respects_monotone; last by lia.
      move⇒ x y LE; rewrite /fp_ovh_sbf.
      rewrite leq_mul2l; apply/orP; right.
      rewrite leq_add2l leq_mul2l; apply/orP; right.
      rewrite big_seq_cond [leqRHS]big_seq_cond.
      apply leq_sum ⇒ tsko /andP [INo _].
      by apply H_valid_arrival_curve.
    }
    lia.
  Qed.

Lastly, we prove that the SBF is valid.
  Lemma overheads_sbf_busy_valid :
    ∀ tsk,
      valid_busy_sbf arr_seq sched tsk (fp_ovh_sbf ts DB CSB CRPDB tsk).
  Proof.
    move ⇒ tsk; split; first by unfold fp_ovh_sbf.
    move ⇒ j t1 t2 ARR [TSK PREF] t /andP [NEQ1 NEQ2].
    interval_to_duration t1 t δ.
    rewrite supply_during_complement; last first.
    { by apply: overheads_proc_model_provides_unit_supply; eauto 1. }
    rewrite addKn; apply leq_sub2l.
    apply slowed_respects_pointwise_leq with (f := fun δ ⇒ blackout_during sched t1 (t1 + δ)).
    { by move⇒ ?; rewrite addnA; apply blackout_during_unit_growth. }
    move⇒ Δ LE; rewrite /fp_blackout_bound.
    have F:
      blackout_during sched t1 (t1 + Δ)
      ≤ (DB + CSB + CRPDB) × (1 + 2 × (\sum_(tsko <- ts | hep_task tsko (job_task j)) max_arrivals tsko Δ)).
    { apply: leq_trans; first by apply: finite_sched_changes_bounded_overheads_blackout ⇒ //.
      rewrite /blackout_during leq_mul2l; apply/orP; right.
      have [Z|POSΔ] := posnP Δ.
      { by subst; rewrite addn0 /number_schedule_changes /index_iota subnS subnn //=. }
      rewrite [_ + 1]addnC leq_add2l; eapply schedule_changes_bounded_by_total_arrivals_FP ⇒ //.
      lia.
    }
    by apply: leq_trans; [apply: F | move: TSK ⇒ /eqP TSK; rewrite -TSK; lia].
  Qed.

End OverheadResourceModelValidSBF.