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 Δ).

First, we define the FP SBF as the interval length minus the FP blackout bound.
  #[local] Instance fp_ovh_sbf : SupplyBoundFunction :=
    fun Δ ⇒ Δ - fp_blackout_bound Δ.

Next, we define the "slowed-down" version of the FP SBF as the interval length minus the slowed-down blackout bound. The slowdown ensures that the resulting SBF is monotone and unit-growth, which is necessary to obtain response-time bounds using aRSA. This slowed-down FP SBF is used internally in the analysis, while the unmodified FP SBF is used to state the top-level analysis result.
  Definition fp_ovh_sbf_slow : 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 monotone 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 slowed SBF is monotone.
  Lemma overheads_sbf_monotone :
    ∀ tsk,
      sbf_is_monotone (fp_ovh_sbf_slow ts DB CSB CRPDB tsk).

In addition, we note that fp_blackout_bound is monotone as well.
  Remark fp_blackout_bound_monotone :
    ∀ tsk,
      monotone leq (fp_blackout_bound ts DB CSB CRPDB tsk).

The slowed SBF is also a unit-supply SBF.
  Lemma overheads_sbf_unit :
    ∀ tsk,
      unit_supply_bound_function (fp_ovh_sbf_slow ts DB CSB CRPDB tsk).

Lastly, we prove that the slowed SBF is valid.
  Lemma overheads_sbf_busy_valid :
    ∀ tsk,
      valid_busy_sbf arr_seq sched tsk (fp_ovh_sbf_slow ts DB CSB CRPDB tsk).

End OverheadResourceModelValidSBF.