Project Page Index Table of Contents

# Library prosa.analysis.abstract.ideal.abstract_seq_rta

Require Export prosa.analysis.definitions.task_schedule.
Require Export prosa.analysis.facts.model.rbf.
Require Export prosa.analysis.facts.model.task_arrivals.
Require Export prosa.analysis.facts.model.task_schedule.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.analysis.abstract.ideal.abstract_rta.
Require Export prosa.analysis.abstract.IBF.task.

# Abstract Response-Time Analysis with sequential tasks

In this section we propose the general framework for response-time analysis (RTA) of uni-processor scheduling of real-time tasks with arbitrary arrival models and sequential tasks.
We prove that the maximum among the solutions of the response-time bound recurrence for some set of parameters is a response-time bound for tsk. Note that in this section we do rely on the hypothesis about task sequentiality. This allows us to provide a more precise response-time bound function, since jobs of the same task will be executed strictly in the order they arrive.
Section Sequential_Abstract_RTA.
Consider any type of tasks ...
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 ideal uni-processor state model.
Context `{PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
Consider any valid arrival sequence with consistent, non-duplicate arrivals...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
... and any ideal 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 that the job costs are no larger than the task costs.
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
Consider an arbitrary task set.
Variable ts : list Task.
Let tsk be any task in 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_rtct tsk is (1) no bigger than tsk's cost, (2) for any job of task tsk job_rtct is bounded by task_rtct.
Hypothesis H_valid_run_to_completion_threshold :
valid_task_run_to_completion_threshold arr_seq tsk.
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.
Assume we are provided with abstract functions for interference and interfering workload.
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
We assume that the schedule is work-conserving.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
Unlike the previous theorem uniprocessor_response_time_bound_ideal, we assume that (1) tasks are sequential, moreover (2) functions interference and interfering_workload are consistent with the hypothesis of sequential tasks.
Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
Hypothesis H_interference_and_workload_consistent_with_sequential_tasks :
interference_and_workload_consistent_with_sequential_tasks arr_seq sched tsk.
Assume we have a constant L that bounds the busy interval of any of tsk's jobs.
Variable L : duration.
Hypothesis H_busy_interval_exists :
busy_intervals_are_bounded_by arr_seq sched tsk L.
Next, we assume that task_IBF is a bound on interference incurred by the task.
Variable task_IBF : duration → duration → duration.
Hypothesis H_task_interference_is_bounded :
task_interference_is_bounded_by arr_seq sched tsk task_IBF.
Let us abbreviate task tsk's RBF for clarity.
Let task_rbf := task_request_bound_function tsk.
Given any job j of task tsk that arrives exactly A units after the beginning of the busy interval, the bound on the total interference incurred by j within an interval of length Δ is no greater than task_rbf (A + ε) - task_cost tsk + task's IBF Δ. Note that in case of sequential tasks the bound consists of two parts: (1) the part that bounds the interference received from other jobs of task tsk -- task_rbf (A + ε) - task_cost tsk and (2) any other interference that is bounded by task_IBF(tsk, A, Δ).
Let total_interference_bound (A Δ : duration) :=
task_rbf (A + ε) - task_cost tsk + task_IBF A Δ.
Note that since we consider the modified interference bound function, the search space has also changed. One can see that the new search space is guaranteed to include any A for which task_rbf (A) ≠ task_rbf (A + ε), since this implies the fact that total_interference_bound (A, Δ) ≠ total_interference_bound (A + ε, Δ).
Let is_in_search_space_seq := is_in_search_space L total_interference_bound.
Consider any value R, and assume that for any relative arrival time A from the search space there is a solution F of the response-time recurrence that is bounded by R. In contrast to the formula in "non-sequential" Abstract RTA, assuming that tasks are sequential leads to a more precise response-time bound. Now we can explicitly express the interference caused by other jobs of the task under consideration.
To understand the right part of the fix-point in the equation, it is helpful to note that the bound on the total interference (bound_of_total_interference) is equal to task_rbf (A + ε) - task_cost tsk + task_IBF tsk A Δ. Besides, a job must receive enough service to become non-preemptive task_lock_in_service tsk. The sum of these two quantities is exactly the right-hand side of the equation.
Variable R : duration.
Hypothesis H_R_is_maximum_seq :
∀ (A : duration),
is_in_search_space_seq A →
∃ (F : duration),
A + F ≥ (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + task_IBF A (A + F)
∧ R ≥ F + (task_cost tsk - task_rtct tsk).
Since we are going to use the uniprocessor_response_time_bound_ideal theorem to prove the theorem of this section, we have to show that all the hypotheses are satisfied. Namely, we need to show that H_R_is_maximum_seq implies H_R_is_maximum. Note that the fact that hypotheses H_sequential_tasks, H_i_w_are_task_consistent and H_task_interference_is_bounded_by imply H_job_interference_is_bounded is proven in the file analysis/abstract/IBF/task.
In this section, we prove that H_R_is_maximum_seq implies H_R_is_maximum.
Section MaxInSeqHypothesisImpMaxInNonseqHypothesis.
To rule out pathological cases with the H_R_is_maximum_seq equation (such as task_cost tsk being greater than task_rbf (A + ε)), we assume that the arrival curve is non-pathological.
Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
For simplicity, let's define a local name for the search space.
Let is_in_search_space A :=
is_in_search_space L total_interference_bound A.
We prove that H_R_is_maximum holds.
Lemma max_in_seq_hypothesis_implies_max_in_nonseq_hypothesis :
∀ (A : duration),
is_in_search_space A →
∃ (F : duration),
A + F ≥ task_rtct tsk
+ (task_rbf (A + ε) - task_cost tsk + task_IBF A (A + F))
∧ R ≥ F + (task_cost tsk - task_rtct tsk).
Proof.
move: H_valid_run_to_completion_threshold ⇒ [PRT1 PRT2] ⇒ A INSP.
clear H_sequential_tasks H_interference_and_workload_consistent_with_sequential_tasks.
move: (H_R_is_maximum_seq _ INSP) ⇒ [F [FIX LE]].
∃ F; split⇒ [|//].
rewrite -{2}(leqRW FIX).
rewrite addnA leq_add2r.
rewrite addnBA; last first.
{ apply leq_trans with (task_rbf 1).
- exact: task_rbf_1_ge_task_cost.
- by apply: task_rbf_monotone ⇒ //; rewrite addn1.
}
by rewrite subnBA; auto; rewrite addnC.
Qed.
End MaxInSeqHypothesisImpMaxInNonseqHypothesis.
We apply the uniprocessor_response_time_bound_ideal theorem, and using the lemmas proven earlier, we prove that all the requirements are satisfied. So, R is a response-time bound.
Theorem uniprocessor_response_time_bound_seq :
task_response_time_bound arr_seq sched tsk R.
Proof.
move ⇒ j ARR TSK.
eapply uniprocessor_response_time_bound_ideal ⇒ //.
{ exact: task_IBF_implies_job_IBF ⇒ //. }
{ exact: max_in_seq_hypothesis_implies_max_in_nonseq_hypothesis ⇒ //. }
Qed.
End Sequential_Abstract_RTA.