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

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 an arbitrary JLFP scheduling policy in the presence of overheads.
Section OverheadResourceModelValidSBF.

Consider any type of tasks,...
  Context {Task : TaskType}.
  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.

We define the blackout bound for JLFP in an interval of length Δ as the number of jobs 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.
Compared to FP and FIFO, the bound for JLFP is less tight because the policy leaves more freedom in how jobs may be scheduled, and our current analysis does not restrict this behavior further.
  Definition jlfp_blackout_bound (Δ : duration) :=
    (DB + CSB + CRPDB) × (1 + 2 × \sum_(tsk <- ts) max_arrivals tsk Δ).

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

Next, we define the "slowed-down" version of the JLFP 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 JLFP SBF is used internally in the analysis, while the unmodified JLFP SBF is used to state the top-level analysis result.
  Definition jlfp_ovh_sbf_slow : SupplyBoundFunction :=
    fun Δ ⇒ Δ - slowed jlfp_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 a JLFP-policy that indicates a higher-or-equal priority relation, and assume that this relation is reflexive and transitive.
  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
  Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.

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 JLFP policy.
  Hypothesis H_respects_policy :
    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.

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 :
    sbf_is_monotone (jlfp_ovh_sbf_slow ts DB CSB CRPDB).

In addition, we note that jlfp_blackout_bound is monotone as well.
  Remark jlfp_blackout_bound_monotone :
    monotone leq (jlfp_blackout_bound ts DB CSB CRPDB).

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

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

End OverheadResourceModelValidSBF.