Newer
Older
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. *)
(** 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}.
(** 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...*)
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any ideal schedule of this arrival sequence. *)
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. *)
(** 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]. *)
(** 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. *)
(** 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 :
forall (A : duration),
is_in_search_space_seq A ->
exists (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:
(task_rbf (A + ε) - task_cost tsk + task_IBF A (A + F))
/\ R >= F + (task_cost tsk - task_rtct tsk).
move: H_valid_run_to_completion_threshold => [PRT1 PRT2]; move => A INSP.
clear H_sequential_tasks H_interference_and_workload_consistent_with_sequential_tasks.
move: (H_R_is_maximum_seq _ INSP) => [F [FIX LE]].
exists 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.
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 => //. }
