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.sequential.
Require Export prosa.analysis.abstract.ideal.abstract_rta.
Require Export prosa.analysis.facts.model.rbf.
Require Export prosa.analysis.facts.model.task_arrivals.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.analysis.abstract.ideal.abstract_rta.
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.
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 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 (ideal.processor_state Job).
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.
Let's define some local names for clarity.
Let task_rbf := task_request_bound_function tsk.
Let arrivals_between := arrivals_between arr_seq.
Let service_of_jobs_at := service_of_jobs_at sched.
Let arrivals_between := arrivals_between arr_seq.
Let service_of_jobs_at := service_of_jobs_at sched.
In this section, we introduce a few new definitions to make it
easier to express the new bound on the worst-case interference.
When assuming sequential tasks, we can introduce an additional
hypothesis that ensures that the values of interference and
workload remain consistent. It is important to note that
before a busy interval of a job j of task tsk begins, both
the cumulative task workload and task service must be equal
within the interval
[0, t1)
. This has an implication that
a busy interval for job j cannot begin if there is another
pending job of the same task tsk. This requirement makes
sense only in the context of sequential tasks.
Definition interference_and_workload_consistent_with_sequential_tasks :=
∀ (j : Job) (t1 t2 : instant),
arrives_in arr_seq j →
job_of_task tsk j →
job_cost j > 0 →
busy_interval sched j t1 t2 →
task_workload_between arr_seq tsk 0 t1 = task_service_of_jobs_in sched tsk (arrivals_between 0 t1) 0 t1.
∀ (j : Job) (t1 t2 : instant),
arrives_in arr_seq j →
job_of_task tsk j →
job_cost j > 0 →
busy_interval sched j t1 t2 →
task_workload_between arr_seq tsk 0 t1 = task_service_of_jobs_in sched tsk (arrivals_between 0 t1) 0 t1.
Next we introduce the notion of task interference.
Intuitively, task tsk incurs interference when some of the
jobs of task tsk incur interference. As a result, tsk
cannot make any progress. More formally, task tsk
experiences interference at a time instant time t, if at
time t task tsk is not scheduled and there exists a job of
tsk that (1) experiences interference and (2) has arrived
before some time instant upper_bound.
It is important to note two subtle points: according to our
semantics of the interference function, jobs from the same
task can cause interference to each other. In the definition
of interference of a task we want to avoid such
situations. That is why we use the term ~~ task_scheduled_at
tsk t.
Moreover, in order to make the definition constructive, we
introduce an upper bound on the arrival time of jobs from task
tsk. As a result, we need to consider only a finite number
of jobs. For the function to produce the correct values it is
enough to specify a sufficiently large upper_bound. Usually
as upper_bound one can use the end of the corresponding busy
interval.
Definition task_interference_received_before (tsk : Task) (t__up : instant) (t : instant) :=
¬ task_scheduled_at sched tsk t ∧
∃ j, interference j t ∧ j \in task_arrivals_before arr_seq tsk t__up.
¬ task_scheduled_at sched tsk t ∧
∃ j, interference j t ∧ j \in task_arrivals_before arr_seq tsk t__up.
We also define a decidable counterpart of this definition...
Definition task_interference_received_before_dec (tsk : Task) (t__up : instant) (t : instant) :=
(~~ task_scheduled_at sched tsk t)
&& has (fun j ⇒ interference j t) (task_arrivals_before arr_seq tsk t__up).
(~~ task_scheduled_at sched tsk t)
&& has (fun j ⇒ interference j t) (task_arrivals_before arr_seq tsk t__up).
... and prove that the propositional and decidable definitions
are equivalent.
Lemma task_interference_received_before_P :
∀ tsk t__up t, reflect (task_interference_received_before tsk t__up t)
(task_interference_received_before_dec tsk t__up t).
∀ tsk t__up t, reflect (task_interference_received_before tsk t__up t)
(task_interference_received_before_dec tsk t__up t).
Next we define the cumulative task interference.
Definition cumul_task_interference tsk upper_bound t1 t2 :=
\sum_(t1 ≤ t < t2) task_interference_received_before_dec tsk upper_bound t.
\sum_(t1 ≤ t < t2) task_interference_received_before_dec tsk upper_bound t.
We say that task interference is bounded by
task_interference_bound_function (task_IBF) iff for any
job j of task tsk cumulative task interference within
the interval t1, t1 + R) is bounded by function
[task_IBF(tsk, A, R)]. Note that this definition is almost
the same as the definition of [job_interference_is_bounded_by]
from the non-necessarily-sequential case. However, in this case
we ignore the interference that comes from jobs from the same
task.
Definition task_interference_is_bounded_by
(task_interference_bound_function : Task → duration → duration → duration) :=
∀ j R t1 t2,
arrives_in arr_seq j →
job_of_task tsk j →
t1 + R < t2 →
~~ completed_by sched j (t1 + R) →
busy_interval sched j t1 t2 →
let offset := job_arrival j - t1 in
cumul_task_interference tsk t2 t1 (t1 + R) ≤ task_interference_bound_function tsk offset R.
End Definitions.
(task_interference_bound_function : Task → duration → duration → duration) :=
∀ j R t1 t2,
arrives_in arr_seq j →
job_of_task tsk j →
t1 + R < t2 →
~~ completed_by sched j (t1 + R) →
busy_interval sched j t1 t2 →
let offset := job_arrival j - t1 in
cumul_task_interference tsk t2 t1 (t1 + R) ≤ task_interference_bound_function tsk offset R.
End Definitions.
In this section, we prove that the maximum among the solutions
of the response-time bound recurrence is a response-time bound
for tsk.
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.
Hypothesis H_interference_and_workload_consistent_with_sequential_tasks :
interference_and_workload_consistent_with_sequential_tasks.
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_interference_bound_function is a
bound on interference incurred by the task.
Variable task_interference_bound_function : Task → duration → duration → duration.
Hypothesis H_task_interference_is_bounded :
task_interference_is_bounded_by task_interference_bound_function.
Hypothesis H_task_interference_is_bounded :
task_interference_is_bounded_by task_interference_bound_function.
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 (tsk : Task) (A Δ : duration) :=
task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A Δ.
task_rbf (A + ε) - task_cost tsk + task_interference_bound_function 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 (tsk, A, Δ) ≠
total_interference_bound (tsk, 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_interference_bound_function tsk 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_interference_bound_function tsk A (A + F) ∧
R ≥ F + (task_cost tsk - task_rtct tsk).
In this section we prove a few simple lemmas about the
completion of jobs from the task considering the busy interval
of the job under consideration.
Variable j1 j2 : Job.
Hypothesis H_j1_arrives : arrives_in arr_seq j1.
Hypothesis H_j2_arrives : arrives_in arr_seq j2.
Hypothesis H_j1_from_tsk : job_of_task tsk j1.
Hypothesis H_j2_from_tsk : job_of_task tsk j2.
Hypothesis H_j1_cost_positive : job_cost_positive j1.
Hypothesis H_j1_arrives : arrives_in arr_seq j1.
Hypothesis H_j2_arrives : arrives_in arr_seq j2.
Hypothesis H_j1_from_tsk : job_of_task tsk j1.
Hypothesis H_j2_from_tsk : job_of_task tsk j2.
Hypothesis H_j1_cost_positive : job_cost_positive j1.
Consider the busy interval
[t1, t2)
of job j1.
We prove that if a job from task tsk arrived before the beginning of the busy
interval, then it must be completed before the beginning of the busy interval
Next we prove that if a job is pending after the beginning
of the busy interval
[t1, t2)
then it arrives after
t1.
Lemma arrives_after_beginning_of_busy_interval:
∀ t,
t1 ≤ t →
pending sched j2 t →
arrived_between j2 t1 t.+1.
End CompletionOfJobsFromSameTask.
∀ t,
t1 ≤ t →
pending sched j2 t →
arrived_between j2 t1 t.+1.
End CompletionOfJobsFromSameTask.
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
hypotheses H_sequential_tasks, H_i_w_are_task_consistent and
H_task_interference_is_bounded_by imply
H_job_interference_is_bounded, and the fact that
H_R_is_maximum_seq implies H_R_is_maximum.
In this section we show that there exists a bound for
cumulative interference for any job of task tsk, i.e., the
hypothesis H_job_interference_is_bounded holds.
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.
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.
Consider an arbitrary time x ...
In this section, we show that the cumulative interference of
job j in the interval
[t1, t1 + x)
is bounded by the sum
of the task workload in the interval t1, t1 + A + ε) and
the cumulative interference of [j]'s task in the interval
[t1, t1 + x). Note that the task workload is computed only
on the interval [t1, t1 + A + ε). Thanks to the hypothesis
about sequential tasks, jobs of task [tsk] that arrive after
[t1 + A + ε] cannot interfere with [j].
We start by proving a simpler analog of the lemma that
states that at any time instant
Next we consider 4 cases.
t ∈ [t1, t1 + x)
the
sum of interference j t and scheduled_at j t is no
larger than the sum of the service received by jobs of
task tsk at time t and task_iterference tsk t.
Consider an arbitrary time instant t ∈
[t1, t1 + x)
.
Assume the processor is idle at time t.
In case when the processor is idle, one can show that
interference j t = 1, scheduled_at j t = 0. But
since interference doesn't come from a job of task
tsk task_interference tsk = 1. Which reduces to 1
≤ 1.
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_idle:
interference j t + scheduled_at sched j t
≤ service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+ task_interference_received_before_dec tsk t2 t.
End Case1.
Section Case2.
interference j t + scheduled_at sched j t
≤ service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+ task_interference_received_before_dec tsk t2 t.
End Case1.
Section Case2.
Variable j' : Job.
Hypothesis H_sched : sched t = Some j'.
Hypothesis H_not_job_of_tsk : ~~ job_of_task tsk j'.
Hypothesis H_sched : sched t = Some j'.
Hypothesis H_not_job_of_tsk : ~~ job_of_task tsk j'.
If a job j' from another task is scheduled at time
t, then interference j t = 1, scheduled_at j t =
0. But since interference doesn't come from a job of
task tsk task_interference tsk = 1. Which reduces
to 1 ≤ 1.
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_task:
interference j t + scheduled_at sched j t ≤
service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t +
task_interference_received_before_dec tsk t2 t.
End Case2.
Section Case3.
interference j t + scheduled_at sched j t ≤
service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t +
task_interference_received_before_dec tsk t2 t.
End Case2.
Section Case3.
Variable j' : Job.
Hypothesis H_sched : scheduled_at sched j' t.
Hypothesis H_not_job_of_tsk : job_of_task tsk j'.
Hypothesis H_j_neq_j' : j != j'.
Hypothesis H_sched : scheduled_at sched j' t.
Hypothesis H_not_job_of_tsk : job_of_task tsk j'.
Hypothesis H_j_neq_j' : j != j'.
If a job j' (different from j) of task tsk is
scheduled at time t, then interference j t = 1,
scheduled_at j t = 0. Moreover, since interference
comes from a job of the same task task_interference
tsk = 0. However, in this case service_of_jobs of
tsk = 1. Which reduces to 1 ≤ 1.
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_job:
interference j t + scheduled_at sched j t
≤ service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+ task_interference_received_before_dec tsk t2 t.
End Case3.
Section Case4.
interference j t + scheduled_at sched j t
≤ service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+ task_interference_received_before_dec tsk t2 t.
End Case3.
Section Case4.
If job j is scheduled at time t, then
interference = 0, scheduled_at = 1, but note that
service_of_jobs of tsk = 1, therefore inequality
reduces to 1 ≤ 1.
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_j:
interference j t + scheduled_at sched j t
≤ service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+ task_interference_received_before_dec tsk t2 t.
End Case4.
interference j t + scheduled_at sched j t
≤ service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+ task_interference_received_before_dec tsk t2 t.
End Case4.
We use the above case analysis to prove that any time
instant
t ∈ [t1, t1 + x)
the sum of interference j
t and scheduled_at j t is no larger than the sum of
the service received by jobs of task tsk at time t and
task_iterference tsk t.
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference:
interference j t + scheduled_at sched j t
≤ service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+ task_interference_received_before_dec tsk t2 t.
End CaseAnalysis.
interference j t + scheduled_at sched j t
≤ service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t
+ task_interference_received_before_dec tsk t2 t.
End CaseAnalysis.
Next we prove cumulative version of the lemma above.
Lemma cumul_interference_plus_sched_le_serv_of_task_plus_cumul_task_interference:
cumulative_interference j t1 (t1 + x)
≤ (task_service_of_jobs_in sched tsk (arrivals_between t1 (t1 + A + ε)) t1 (t1 + x)
- service_during sched j t1 (t1 + x)) + cumul_task_interference tsk t2 t1 (t1 + x).
cumulative_interference j t1 (t1 + x)
≤ (task_service_of_jobs_in sched tsk (arrivals_between t1 (t1 + A + ε)) t1 (t1 + x)
- service_during sched j t1 (t1 + x)) + cumul_task_interference tsk t2 t1 (t1 + x).
On the other hand, the service terms in the inequality
above can be upper-bound by the workload terms.
Lemma serv_of_task_le_workload_of_task_plus:
task_service_of_jobs_in sched tsk (arrivals_between t1 (t1 + A + ε)) t1 (t1 + x)
- service_during sched j t1 (t1 + x) + cumul_task_interference tsk t2 t1 (t1 + x)
≤ (task_workload_between arr_seq tsk t1 (t1 + A + ε) - job_cost j)
+ cumul_task_interference tsk t2 t1 (t1 + x).
task_service_of_jobs_in sched tsk (arrivals_between t1 (t1 + A + ε)) t1 (t1 + x)
- service_during sched j t1 (t1 + x) + cumul_task_interference tsk t2 t1 (t1 + x)
≤ (task_workload_between arr_seq tsk t1 (t1 + A + ε) - job_cost j)
+ cumul_task_interference tsk t2 t1 (t1 + x).
Finally, we show that the cumulative interference of job
j in the interval
[t1, t1 + x)
is bounded by the sum
of the task workload in the interval t1, t1 + A + ε) and
the cumulative interference of [j]'s task in the interval
<<[t1, t1 + x)>>.
Lemma cumulative_job_interference_le_task_interference_bound:
cumulative_interference j t1 (t1 + x)
≤ (task_workload_between arr_seq tsk t1 (t1 + A + ε) - job_cost j)
+ cumul_task_interference tsk t2 t1 (t1 + x).
End TaskInterferenceBoundsInterference.
cumulative_interference j t1 (t1 + x)
≤ (task_workload_between arr_seq tsk t1 (t1 + A + ε) - job_cost j)
+ cumul_task_interference tsk t2 t1 (t1 + x).
End TaskInterferenceBoundsInterference.
In order to obtain a more convenient bound on the cumulative
interference, we need to abandon the actual workload in
favor of a bound that depends on task parameters only. So,
we show that the actual workload of the task excluding workload
of any job j is no greater than the bound on the workload
excluding the cost of job j's task.
Lemma task_rbf_excl_tsk_bounds_task_workload_excl_j:
task_workload_between arr_seq tsk t1 (t1 + A + ε) - job_cost j ≤ task_rbf (A + ε) - task_cost tsk.
task_workload_between arr_seq tsk t1 (t1 + A + ε) - job_cost j ≤ task_rbf (A + ε) - task_cost tsk.
Finally, we use the lemmas above to obtain the bound on
interference in terms of task_rbf and
task_interference.
Lemma cumulative_job_interference_bound:
cumulative_interference j t1 (t1 + x)
≤ (task_rbf (A + ε) - task_cost tsk) + cumul_task_interference tsk t2 t1 (t1 + x).
End BoundOfCumulativeJobInterference.
cumulative_interference j t1 (t1 + x)
≤ (task_rbf (A + ε) - task_cost tsk) + cumul_task_interference tsk t2 t1 (t1 + x).
End BoundOfCumulativeJobInterference.
In this section, we prove that H_R_is_maximum_seq implies H_R_is_maximum.
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
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_interference_bound_function tsk A (A + F)) ∧
R ≥ F + (task_cost tsk - task_rtct tsk).
End MaxInSeqHypothesisImpMaxInNonseqHypothesis.
∀ (A : duration),
is_in_search_space A →
∃ (F : duration),
A + F ≥ task_rtct tsk +
(task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A (A + F)) ∧
R ≥ F + (task_cost tsk - task_rtct tsk).
End MaxInSeqHypothesisImpMaxInNonseqHypothesis.
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.