# 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 :=
{
supply_bound_function Δ := Δ - 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 :=
{|
supply_bound_function Δ := Δ - slowed fp_blackout_bound Δ
|}.
End OverheadResourceModelValidSBF.
In the following section, we show that the SBF defined above is indeed a valid SBF.
Section OverheadResourceModelValidSBF.
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}.
We assume the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready.
Context {RM : JobReady Job (overheads.processor_state Job)}.
Hypothesis H_basic_readiness : basic_readiness RM.
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.