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

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

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

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.

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.

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 that the job costs are no larger than the task costs.

Consider an arbitrary task set.

Let tsk be any task in ts that is to be analyzed.

Consider a valid preemption model ...

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

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.

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.

We assume that the schedule is work-conserving.

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.

Hypothesis H_interference_and_workload_consistent_with_sequential_tasks :

interference_and_workload_consistent_with_sequential_tasks arr_seq sched tsk.

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.

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.

Hypothesis H_task_interference_is_bounded :

task_interference_is_bounded_by arr_seq sched tsk task_IBF.

Let's define some local names 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, Δ).

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 + ε, Δ).

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

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.

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.

For simplicity, let's define a local name for the search space.

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]; 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]].

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

∀ (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]; 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]].

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

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.