Library prosa.analysis.abstract.restricted_supply.fp_bounded_bi
Require Export prosa.analysis.facts.blocking_bound_fp.
Require Export prosa.analysis.abstract.restricted_supply.abstract_rta.
Require Export prosa.analysis.abstract.restricted_supply.iw_instantiation.
Require Export prosa.analysis.definitions.sbf.busy.
Require Export prosa.analysis.abstract.restricted_supply.abstract_rta.
Require Export prosa.analysis.abstract.restricted_supply.iw_instantiation.
Require Export prosa.analysis.definitions.sbf.busy.
Sufficient Condition for Bounded Busy Intervals for RS FP
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any kind of fully supply-consuming unit-supply
uniprocessor model.
Context `{PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
Consider an FP policy that indicates a higher-or-equal priority
relation, and assume that the 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.
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.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Next, consider a schedule of this arrival sequence, ...
... allow for any work-bearing notion of job readiness, ...
... and assume that the schedule is valid.
In addition, we assume the existence of a function mapping jobs
to their preemption points ...
... and assume that it defines a valid preemption model with
bounded non-preemptive segments.
Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
Furthermore, we assume that the schedule is work-conserving ...
... and that it respects the scheduling policy.
Recall that busy_intervals_are_bounded_by is an abstract
notion. Hence, we need to introduce interference and interfering
workload. We will use the restricted-supply instantiations.
We say that job j incurs interference at time t iff it
cannot execute due to (1) the lack of supply at time t, (2)
service inversion (i.e., a lower-priority job receiving service
at t), or a higher-or-equal-priority job receiving service.
The interfering workload, in turn, is defined as the sum of the
blackout predicate, service inversion predicate, and the
interfering workload of jobs with higher or equal priority.
#[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
rs_jlfp_interfering_workload arr_seq sched.
rs_jlfp_interfering_workload arr_seq sched.
Consider an arbitrary task set ts, ...
... assume that all jobs come from the task set, ...
... and that the cost of a job does not exceed its task's WCET.
Consider a valid, unit supply-bound function "busy" SBF. That
is, (1) SBF 0 = 0, (2) for any duration Δ, the supply
produced during a busy-interval prefix of length Δ is at least
SBF Δ, and (3) SBF makes steps of at most one.
Context {SBF : SupplyBoundFunction}.
Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
Let max_arrivals be a family of valid arrival curves, i.e.,
for any task tsk in ts, max_arrival tsk is (1) an arrival
bound of tsk, and (2) it is a monotonic function that equals
0 for the empty interval delta = 0.
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
Consider a valid preemption model.
Let L be any positive fixed point of the busy-interval recurrence.
Variable L : duration.
Hypothesis H_L_positive : 0 < L.
Hypothesis H_fixed_point :
blocking_bound ts tsk + total_hep_request_bound_function_FP ts tsk L ≤ SBF L.
Hypothesis H_L_positive : 0 < L.
Hypothesis H_fixed_point :
blocking_bound ts tsk + total_hep_request_bound_function_FP ts tsk L ≤ SBF L.
Next, we provide a step-by-step proof of busy-interval boundedness.
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive : job_cost_positive j.
First, we note that since job j is pending at time
job_arrival j, there is a (potentially unbounded) busy
interval that starts no later than with the arrival of j.
Local Lemma busy_interval_prefix_exists :
∃ t1,
t1 ≤ job_arrival j
∧ busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
∃ t1,
t1 ≤ job_arrival j
∧ busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
Next, consider two cases: (1) when the busy-interval prefix
continues until time instant t1 + L and (2) when the busy
interval prefix terminates earlier. In either case, we can
show that the busy-interval prefix is bounded.
We start with the first case, where the busy-interval prefix
continues until time instant t1 + L.
Consider a time instant t1 such that
Note that at this point we do not necessarily know that
job_arrival j ≤ L; hence, we assume the existence of both
prefixes.
[t1, job_arrival
j]>> and [t1, t1 + L)
are both busy-interval prefixes of
job j.
Variable t1 : instant.
Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
Hypothesis H_busy_prefix_L : busy_interval_prefix arr_seq sched j t1 (t1 + L).
Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
Hypothesis H_busy_prefix_L : busy_interval_prefix arr_seq sched j t1 (t1 + L).
The crucial point to note is that the sum of the job's cost
(represented as workload_of_job) and the interfering
workload in the interval
[t1, t1 + L)
is bounded by L
due to the fixed point H_fixed_point.
Local Lemma workload_is_bounded :
workload_of_job arr_seq j t1 (t1 + L) + cumulative_interfering_workload j t1 (t1 + L) ≤ L.
workload_of_job arr_seq j t1 (t1 + L) + cumulative_interfering_workload j t1 (t1 + L) ≤ L.
It follows that t1 + L is a quiet time, which means that
the busy prefix ends (i.e., it is bounded).
Local Lemma busy_prefix_is_bounded_case1 :
∃ t2,
job_arrival j < t2
∧ t2 ≤ t1 + L
∧ busy_interval arr_seq sched j t1 t2.
End Case1.
∃ t2,
job_arrival j < t2
∧ t2 ≤ t1 + L
∧ busy_interval arr_seq sched j t1 t2.
End Case1.
Next, we consider the case when the interval
[t1, t1 + L)
is not a busy-interval prefix.
First, we prove a few helper lemmas.
Then, the service of higher-or-equal-priority jobs is less
than the workload of higher-or-equal-priority jobs in any
subinterval
[t1, t)
of the interval [t1, t2)
.
Local Lemma service_lt_workload_in_busy :
∀ t,
t1 < t < t2 →
service_of_hep_jobs arr_seq sched j t1 t < workload_of_hep_jobs arr_seq j t1 t.
∀ t,
t1 < t < t2 →
service_of_hep_jobs arr_seq sched j t1 t < workload_of_hep_jobs arr_seq j t1 t.
Consider a subinterval
[t1, t1 + Δ)
of the interval
[t1, t2)
. We show that the sum of j's workload and
the cumulative workload in [t1, t1 + Δ)
is strictly
larger than Δ.
Local Lemma workload_exceeds_interval :
∀ Δ,
0 < Δ →
t1 + Δ < t2 →
Δ < workload_of_job arr_seq j t1 (t1 + Δ) + cumulative_interfering_workload j t1 (t1 + Δ).
End HelperLemmas.
∀ Δ,
0 < Δ →
t1 + Δ < t2 →
Δ < workload_of_job arr_seq j t1 (t1 + Δ) + cumulative_interfering_workload j t1 (t1 + Δ).
End HelperLemmas.
Consider a time instant t1 such that
[t1, job_arrival
j]>> is a busy-interval prefix of j and [t1, t1 + L)
is not.
Variable t1 : instant.
Hypothesis H_arrives : t1 ≤ job_arrival j.
Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
Hypothesis H_no_busy_prefix_L : ¬ busy_interval_prefix arr_seq sched j t1 (t1 + L).
Hypothesis H_arrives : t1 ≤ job_arrival j.
Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
Hypothesis H_no_busy_prefix_L : ¬ busy_interval_prefix arr_seq sched j t1 (t1 + L).
Lemma job_arrival_is_bounded implies that the
busy-interval prefix starts at time t1, continues until
job_arrival j + 1, and then terminates before t1 + L.
Or, in other words, there is point in time t2 such that
(1) j's arrival is bounded by t2, (2) t2 is bounded by
t1 + L, and (3)
[t1, t2)
is busy interval of job
j.
Lemma busy_prefix_is_bounded_case2:
∃ t2, job_arrival j < t2 ∧ t2 ≤ t1 + L ∧ busy_interval arr_seq sched j t1 t2.
End Case2.
End StepByStepProof.
∃ t2, job_arrival j < t2 ∧ t2 ≤ t1 + L ∧ busy_interval arr_seq sched j t1 t2.
End Case2.
End StepByStepProof.