Library prosa.analysis.abstract.restricted_supply.abstract_rta
Require Export prosa.analysis.facts.behavior.supply.
Require Export prosa.analysis.facts.SBF.
Require Export prosa.analysis.abstract.abstract_rta.
Require Export prosa.analysis.abstract.iw_auxiliary.
Require Export prosa.analysis.abstract.IBF.supply.
Require Export prosa.analysis.abstract.restricted_supply.busy_sbf.
Require Export prosa.analysis.facts.SBF.
Require Export prosa.analysis.abstract.abstract_rta.
Require Export prosa.analysis.abstract.iw_auxiliary.
Require Export prosa.analysis.abstract.IBF.supply.
Require Export prosa.analysis.abstract.restricted_supply.busy_sbf.
Abstract Response-Time Analysis for Restricted-Supply Processors (aRSA)
In this section we propose a general framework for response-time analysis (RTA) for real-time tasks with arbitrary arrival models under uni-processor scheduling subject to supply restrictions, characterized by a given SBF.
Consider any type of tasks with a run-to-completion threshold ...
... 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}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
Consider any kind of fully supply-consuming unit-supply
processor state model.
Context `{PState : ProcessorState Job}.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_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 any valid arrival sequence.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Consider any restricted supply uniprocessor schedule of this
arrival sequence ...
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
... where jobs do not execute before their arrival nor after completion.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Assume we are given valid WCETs for all tasks.
Consider a task set ts...
Consider a valid preemption model ...
...and a valid task run-to-completion threshold function. That
is, task_rtc tsk is (1) no bigger than tsk's cost and (2)
for any job j of task tsk job_rtct j is bounded by
task_rtct tsk.
Hypothesis H_valid_run_to_completion_threshold :
valid_task_run_to_completion_threshold arr_seq tsk.
valid_task_run_to_completion_threshold arr_seq tsk.
Assume we are provided with abstract functions for Interference
and Interfering Workload.
We assume that the scheduler is work-conserving.
Variable L : duration.
Hypothesis H_busy_interval_exists :
busy_intervals_are_bounded_by arr_seq sched tsk L.
Hypothesis H_busy_interval_exists :
busy_intervals_are_bounded_by arr_seq sched tsk L.
Consider a unit SBF valid in busy intervals (w.r.t. task
tsk). 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 tsk SBF.
Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
Variable intra_IBF : duration → duration → duration.
Hypothesis H_intra_supply_interference_is_bounded :
intra_interference_is_bounded_by arr_seq sched tsk intra_IBF.
Hypothesis H_intra_supply_interference_is_bounded :
intra_interference_is_bounded_by arr_seq sched tsk intra_IBF.
Given any job j of task tsk that arrives exactly A units
after the beginning of the busy interval, the bound on the
interference incurred by j within an interval of length Δ is
no greater than (Δ - SBF Δ) + intra_IBF A Δ.
Next, we instantiate function IBF_NP, which is a function that
bounds interference in a non-preemptive stage of execution. We
prove that this function can be instantiated as λ tsk F Δ ⟹ (F
- task_rtct tsk) + (Δ - SBF Δ - (F - SBF F)).
Let us reiterate on the intuitive interpretation of this
function. Since F is a solution to the first equation
task_rtct tsk + IBF_P A F ≤ F, we know that by time
instant t1 + F a job receives task_rtct tsk units of service
and, hence, it becomes non-preemptive. Knowing this information,
how can we bound the job's interference in an interval
[t1, t1
+ Δ)>>? Note that this interval starts with the beginning of
the busy interval. We know that the job receives F - task_rtct
tsk units of interference. In the non-preemptive mode, a job
under analysis can still experience some interference due to a
lack of supply. This interference is bounded by (Δ - SBF Δ) -
(F - SBF F) since part of this interference has already been
accounted for in the preemptive part of the execution (F - SBF
F).
In the next section, we prove a few helper lemmas.
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.
Consider the busy interval
[t1, t2)
of job j.
Consider an arbitrary time Δ ...
First, we show that blackout is counted as interference.
Next, we show that interference is equal to a sum of two
functions: is_blackout and intra_interference.
Lemma blackout_plus_local_is_interference :
∀ t,
t1 ≤ t < t2 →
is_blackout sched t + intra_interference sched j t
= interference j t.
∀ t,
t1 ≤ t < t2 →
is_blackout sched t + intra_interference sched j t
= interference j t.
As a corollary, cumulative interference during a time
interval
[t1, t1 + Δ)
can be split into a sum of total
blackouts in [t1, t1 + Δ)
and cumulative intra-supply
interference during [t1, t1 + Δ)
.
Corollary blackout_plus_local_is_interference_cumul :
blackout_during sched t1 (t1 + Δ) + cumul_intra_interference sched j t1 (t1 + Δ)
= cumulative_interference j t1 (t1 + Δ).
blackout_during sched t1 (t1 + Δ) + cumul_intra_interference sched j t1 (t1 + Δ)
= cumulative_interference j t1 (t1 + Δ).
Moreover, since the total blackout duration in an interval
of length Δ is bounded by Δ - SBF Δ, the cumulative
interference during the time interval
[t1, t1 + Δ)
is
bounded by the sum of Δ - SBF Δ and cumulative
intra-supply interference during [t1, t1 + Δ)
.
Corollary cumulative_job_interference_bound :
cumulative_interference j t1 (t1 + Δ)
≤ (Δ - SBF Δ) + cumul_intra_interference sched j t1 (t1 + Δ).
cumulative_interference j t1 (t1 + Δ)
≤ (Δ - SBF Δ) + cumul_intra_interference sched j t1 (t1 + Δ).
Next, consider a duration F such that F ≤ Δ and job j
has enough service to become non-preemptive by time instant
t1 + F.
Variable F : duration.
Hypothesis H_F_le_Δ : F ≤ Δ.
Hypothesis H_enough_service : task_rtct tsk ≤ service sched j (t1 + F).
Hypothesis H_F_le_Δ : F ≤ Δ.
Hypothesis H_enough_service : task_rtct tsk ≤ service sched j (t1 + F).
Then, we show that job j does not experience any
intra-supply interference in the time interval
[t1 + F, t1 +
Δ)>>.
Lemma no_intra_interference_after_F :
cumul_intra_interference sched j (t1 + F) (t1 + Δ) = 0.
End AuxiliaryLemmas.
cumul_intra_interference sched j (t1 + F) (t1 + Δ) = 0.
End AuxiliaryLemmas.
For clarity, let's define a local name for the search space.
We use the following equation to bound the response-time of a
job of task tsk. Consider any value R that upper-bounds the
solution of each response-time recurrence, i.e., for any
relative arrival time A in the search space, there exists a
corresponding solution F such that (1) F ≤ A + R,
(2) task_rtct tsk + intra_IBF tsk A F ≤ SBF F and SBF F +
(task_cost tsk - task_rtct tsk) ≤ SBF (A + R).
Note that, compared to "ideal RTA," there is an additional requirement
F ≤ A + R. Intuitively, it is needed to rule out a nonsensical
situation when the non-preemptive stage completes earlier than
the preemptive stage.
Variable R : duration.
Hypothesis H_R_is_maximum_rs :
∀ (A : duration),
is_in_search_space_rs A →
∃ (F : duration),
F ≤ A + R
∧ task_rtct tsk + intra_IBF A F ≤ SBF F
∧ SBF F + (task_cost tsk - task_rtct tsk) ≤ SBF (A + R).
Hypothesis H_R_is_maximum_rs :
∀ (A : duration),
is_in_search_space_rs A →
∃ (F : duration),
F ≤ A + R
∧ task_rtct tsk + intra_IBF A F ≤ SBF F
∧ SBF F + (task_cost tsk - task_rtct tsk) ≤ SBF (A + R).
In the following section we prove that all the premises of
abstract RTA are satisfied.
First, we show that IBF_P correctly upper-bounds
interference in the preemptive stage of execution.
Lemma IBF_P_bounds_interference :
job_interference_is_bounded_by
arr_seq sched tsk IBF_P (relative_arrival_time_of_job_is_A sched).
job_interference_is_bounded_by
arr_seq sched tsk IBF_P (relative_arrival_time_of_job_is_A sched).
Next, we prove that IBF_NP correctly bounds interference in
the non-preemptive stage given a solution to the preemptive
stage F.
Lemma IBF_NP_bounds_interference :
job_interference_is_bounded_by
arr_seq sched tsk IBF_NP (relative_time_to_reach_rtct sched tsk IBF_P).
job_interference_is_bounded_by
arr_seq sched tsk IBF_NP (relative_time_to_reach_rtct sched tsk IBF_P).
Next, we prove that F is bounded by task_cost tsk + IBF_NP
F Δ for any F and Δ. As explained in file
analysis/abstract/abstract_rta, this shows that the second
stage indeed takes into account service received in the first
stage.
Next we prove that H_R_is_maximum_rs implies H_R_is_maximum.
Lemma max_in_rs_hypothesis_impl_max_in_arta_hypothesis :
∀ (A : duration),
is_in_search_space L IBF_P A →
∃ (F : duration),
task_rtct tsk + (F - SBF F + intra_IBF A F) ≤ F
∧ task_cost tsk + (F - task_rtct tsk + (A + R - SBF (A + R) - (F - SBF F))) ≤ A + R.
End RSaRTAPremises.
∀ (A : duration),
is_in_search_space L IBF_P A →
∃ (F : duration),
task_rtct tsk + (F - SBF F + intra_IBF A F) ≤ F
∧ task_cost tsk + (F - task_rtct tsk + (A + R - SBF (A + R) - (F - SBF F))) ≤ A + R.
End RSaRTAPremises.
Finally, we apply the uniprocessor_response_time_bound
theorem, and using the lemmas above, we prove that all the
requirements are satisfied. So, R is a response time bound.