# 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.

# 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.
We prove that the maximum (with respect to the set of offsets) among the solutions of the response-time bound recurrence is a response-time bound for tsk. Note that in this section we add additional restrictions on the processor state. These assumptions allow us to eliminate the second equation from aRTA+'s recurrence since jobs experience delays only due to the lack of supply while executing non-preemptively.
Section AbstractRTARestrictedSupply.
Consider any type of tasks with a run-to-completion threshold ...
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskRunToCompletionThreshold 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 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.
Consider any valid arrival sequence.
Variable arr_seq : arrival_sequence Job.
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.
... 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.
Assume we are given valid WCETs for all tasks.
Hypothesis H_valid_job_cost :
arrivals_have_valid_job_costs arr_seq.
Consider a task set ts...
Variable ts : list Task.
... and a task tsk of ts that is to be analyzed.
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
Consider a valid preemption model ...
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
...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.
Assume we are provided with abstract functions for Interference and Interfering Workload.
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
We assume that the scheduler is work-conserving.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
Let L be a constant that bounds any busy interval of task tsk.
Variable L : duration.
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.
Next, we assume that intra_IBF is a bound on the intra-supply interference incurred by task tsk.
Variable intra_IBF : duration → duration → duration.
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 Δ.
Let IBF_P (A Δ : duration) :=
(Δ - 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).
Let IBF_NP (F Δ : duration) :=
(F - task_rtct tsk) + (Δ - SBF Δ - (F - SBF F)).
In the next section, we prove a few helper lemmas.
Section AuxiliaryLemmas.
Consider any job j of tsk.
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.
Consider the busy interval `[t1, t2)` of job j.
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval_prefix sched j t1 t2.
Let's define A as a relative arrival time of job j (with respect to time t1).
Let A : duration := job_arrival j - t1.
Consider an arbitrary time Δ ...
Variable Δ : duration.
... such that t1 + Δ is inside the busy interval...
Hypothesis H_inside_busy_interval : t1 + Δ < t2.
... the job j is not completed by time (t1 + Δ).
Hypothesis H_job_j_is_not_completed : ~~ completed_by sched j (t1 + Δ).
First, we show that blackout is counted as interference.
Lemma blackout_impl_interference :
∀ t,
t1 ≤ t < t2 →
is_blackout sched t →
interference j t.
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.
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 + Δ).
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 + Δ).
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).
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.
For clarity, let's define a local name for the search space.
Let is_in_search_space_rs := is_in_search_space L IBF_P.
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).
In the following, we prove that all 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).
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).
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.
Lemma IBF_P_sol_le_IBF_NP :
∀ (F Δ : duration),
F ≤ task_cost tsk + IBF_NP F Δ.
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.
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.
Theorem uniprocessor_response_time_bound_restricted_supply :
task_response_time_bound arr_seq sched tsk R.
End AbstractRTARestrictedSupply.