Library prosa.results.rs.exceedance.fully_nonpreemptive_rta
Require Export prosa.analysis.facts.readiness.sequential.
Require Export prosa.analysis.abstract.restricted_supply.task_intra_interference_bound.
Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.fp.
Require Export prosa.analysis.abstract.restricted_supply.search_space.fp.
Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
Require Export prosa.analysis.facts.model.exceedance.SBF.
Require Export prosa.model.composite.valid_task_arrival_sequence.
Require Export prosa.analysis.abstract.restricted_supply.task_intra_interference_bound.
Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.fp.
Require Export prosa.analysis.abstract.restricted_supply.search_space.fp.
Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
Require Export prosa.analysis.facts.model.exceedance.SBF.
Require Export prosa.model.composite.valid_task_arrival_sequence.
Exceedance-Aware RTA for Fully Non-Preemptive Fixed-Priority Uniprocessor Scheduling
Consider tasks characterized by nominal execution times and arbitrary arrival curves, ...
... and their corresponding jobs.
Consider any arrival sequence.
We assume sequential readiness.
We assume that all tasks are fully non-preemptive.
#[local] Existing Instance fully_nonpreemptive_job_model.
#[local] Existing Instance fully_nonpreemptive_task_model.
#[local] Existing Instance fully_nonpreemptive_rtc_threshold.
#[local] Existing Instance fully_nonpreemptive_task_model.
#[local] Existing Instance fully_nonpreemptive_rtc_threshold.
We assume we are given a task set, with valid arrival curves for each task
in the task set, and that all jobs in the arrival sequence stem from tasks
in the given task set.
Variable ts : seq Task.
Hypothesis H_valid_task_arrival_sequence : valid_task_arrival_sequence ts arr_seq.
Hypothesis H_valid_task_arrival_sequence : valid_task_arrival_sequence ts arr_seq.
Assume we have a valid, nonpreemptive, and work-conserving schedule.
Variable sched : schedule (exceedance_proc_state Job).
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
Assume that the FP policy under consideration 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.
We assume that the schedule respects the FP scheduling policy.
Hypothesis H_respects_policy_at_preemption_point :
respects_FP_policy_at_preemption_point arr_seq sched FP.
respects_FP_policy_at_preemption_point arr_seq sched FP.
Let us say that e is the bound on the total exceedance ...
... inside any busy interval of a task tsk from the given task set.
Let us locally recall the exceedance SBF using Instance to make
it available to the typeclasses hints database.
Let us formally state that the total exceedance inside the busy
window is bounded.
Hypothesis H_exceedance_in_busy_interval_bounded :
∀ j t1 t2,
arrives_in arr_seq j →
job_of_task tsk j →
busy_interval_prefix arr_seq sched j t1 t2 →
\sum_(t1 ≤ t < t2) is_exceedance_exec (sched t) ≤ e.
∀ j t1 t2,
arrives_in arr_seq j →
job_of_task tsk j →
busy_interval_prefix arr_seq sched j t1 t2 →
\sum_(t1 ≤ t < t2) is_exceedance_exec (sched t) ≤ e.
Let us locally define some abbreviations for clarity.
Let rbf := task_request_bound_function.
Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
First, we define the bound on the maximum length of a busy window.
Definition busy_window_recurrence_solution L :=
L > e
∧ L ≥ blocking_bound ts tsk + total_hep_rbf L + e.
L > e
∧ L ≥ blocking_bound ts tsk + total_hep_rbf L + e.
Then we define the response-time "recurrence" (i.e., set of inequalities) ...
Definition rta_recurrence_solution L R :=
∀ (A : duration),
is_in_search_space tsk L A →
∃ (F : duration),
A ≤ F ≤ A + R
∧ F ≥ blocking_bound ts tsk
+ (rbf tsk (A + ε) - (task_cost tsk - ε))
+ total_ohep_rbf F + e
∧ A + R ≥ F + (task_cost tsk - ε) + e.
∀ (A : duration),
is_in_search_space tsk L A →
∃ (F : duration),
A ≤ F ≤ A + R
∧ F ≥ blocking_bound ts tsk
+ (rbf tsk (A + ε) - (task_cost tsk - ε))
+ total_ohep_rbf F + e
∧ A + R ≥ F + (task_cost tsk - ε) + e.
... and prove that any solution R satisfying this predicate is a bound on the
maximum response time of task tsk in sched.
Theorem uniprocessor_response_time_bound_fully_nonpreemptive_fp :
∀ (L : duration),
busy_window_recurrence_solution L →
∀ (R : duration),
rta_recurrence_solution L R →
task_response_time_bound arr_seq sched tsk R.
End RTA.
∀ (L : duration),
busy_window_recurrence_solution L →
∀ (R : duration),
rta_recurrence_solution L R →
task_response_time_bound arr_seq sched tsk R.
End RTA.