Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Vedant Chavda
PROSA  Formally Proven Schedulability Analysis
Commits
d1f8192c
Commit
d1f8192c
authored
Dec 02, 2019
by
Sergey Bozhko
Committed by
Björn Brandenburg
Dec 10, 2019
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
address spellchecking issues in analysis
parent
54220d8c
Changes
27
Hide whitespace changes
Inline
Sidebyside
Showing
27 changed files
with
320 additions
and
326 deletions
+320
326
restructuring/analysis/abstract/abstract_rta.v
restructuring/analysis/abstract/abstract_rta.v
+61
61
restructuring/analysis/abstract/abstract_seq_rta.v
restructuring/analysis/abstract/abstract_seq_rta.v
+53
53
restructuring/analysis/abstract/definitions.v
restructuring/analysis/abstract/definitions.v
+33
33
restructuring/analysis/abstract/ideal_jlfp_rta.v
restructuring/analysis/abstract/ideal_jlfp_rta.v
+15
15
restructuring/analysis/abstract/run_to_completion.v
restructuring/analysis/abstract/run_to_completion.v
+12
12
restructuring/analysis/abstract/search_space.v
restructuring/analysis/abstract/search_space.v
+37
38
restructuring/analysis/concepts/priority_inversion.v
restructuring/analysis/concepts/priority_inversion.v
+6
6
restructuring/analysis/concepts/request_bound_function.v
restructuring/analysis/concepts/request_bound_function.v
+8
8
restructuring/analysis/concepts/schedulability.v
restructuring/analysis/concepts/schedulability.v
+7
7
restructuring/analysis/definitions/carry_in.v
restructuring/analysis/definitions/carry_in.v
+2
2
restructuring/analysis/definitions/task_schedule.v
restructuring/analysis/definitions/task_schedule.v
+6
6
restructuring/analysis/facts/behavior/ideal_schedule.v
restructuring/analysis/facts/behavior/ideal_schedule.v
+7
7
restructuring/analysis/facts/behavior/service.v
restructuring/analysis/facts/behavior/service.v
+4
4
restructuring/analysis/facts/behavior/service_of_jobs.v
restructuring/analysis/facts/behavior/service_of_jobs.v
+9
9
restructuring/analysis/facts/behavior/task_arrivals.v
restructuring/analysis/facts/behavior/task_arrivals.v
+1
1
restructuring/analysis/facts/busy_interval.v
restructuring/analysis/facts/busy_interval.v
+6
6
restructuring/analysis/facts/preemption/job/limited.v
restructuring/analysis/facts/preemption/job/limited.v
+6
6
restructuring/analysis/facts/preemption/job/preemptive.v
restructuring/analysis/facts/preemption/job/preemptive.v
+1
1
restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
...analysis/facts/preemption/rtc_threshold/job_preemptable.v
+3
3
restructuring/analysis/facts/preemption/task/floating.v
restructuring/analysis/facts/preemption/task/floating.v
+6
6
restructuring/analysis/facts/preemption/task/limited.v
restructuring/analysis/facts/preemption/task/limited.v
+2
2
restructuring/analysis/facts/preemption/task/nonpreemptive.v
restructuring/analysis/facts/preemption/task/nonpreemptive.v
+3
3
restructuring/analysis/facts/preemption/task/preemptive.v
restructuring/analysis/facts/preemption/task/preemptive.v
+2
2
restructuring/analysis/facts/priority_inversion.v
restructuring/analysis/facts/priority_inversion.v
+14
17
restructuring/analysis/facts/rbf.v
restructuring/analysis/facts/rbf.v
+14
16
restructuring/analysis/facts/readiness/basic.v
restructuring/analysis/facts/readiness/basic.v
+1
1
restructuring/analysis/transform/edf_trans.v
restructuring/analysis/transform/edf_trans.v
+1
1
No files found.
restructuring/analysis/abstract/abstract_rta.v
View file @
d1f8192c
...
...
@@ 6,9 +6,9 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** * Abstract ResponseTime Analysis *)
(** In this module, we propose the general framework for responsetime analysis (RTA)
of uniprocessor scheduling of realtime tasks with arbitrary arrival models. *)
of uni

processor scheduling of realtime tasks with arbitrary arrival models. *)
(** We prove that the maximum (with respect to the set of offsets) among the solutions
of the responsetime bound recurrence is a response time bound for tsk. Note that
of the responsetime bound recurrence is a response time bound for
[
tsk
]
. Note that
in this section we do not rely on any hypotheses about job sequentiality. *)
Section
Abstract_RTA
.
...
...
@@ 29,7 +29,7 @@ Section Abstract_RTA.
Hypothesis
H_arrival_times_are_consistent
:
consistent_arrival_times
arr_seq
.
Hypothesis
H_arr_seq_is_a_set
:
arrival_sequence_uniq
arr_seq
.
(** Next, consider any uniprocessor schedule of this arrival sequence...*)
(** Next, consider any uni

processor 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
.
...
...
@@ 44,7 +44,7 @@ Section Abstract_RTA.
(** Consider a task set ts... *)
Variable
ts
:
list
Task
.
(** ... and a task tsk of ts that is to be analyzed. *)
(** ... and a task
[
tsk
]
of ts that is to be analyzed. *)
Variable
tsk
:
Task
.
Hypothesis
H_tsk_in_ts
:
tsk
\
in
ts
.
...
...
@@ 53,8 +53,8 @@ Section Abstract_RTA.
valid_preemption_model
arr_seq
sched
.
(** ...and a valid task runtocompletion threshold function. That is,
[task_run_to_completion_threshold tsk] is (1) no bigger than tsk's
cost, (2) for any job of task tsk job_run_to_completion_threshold
[task_run_to_completion_threshold tsk] is (1) no bigger than
[
tsk
]
's
cost, (2) for any job of task
[
tsk
]
job_run_to_completion_threshold
is bounded by task_run_to_completion_threshold. *)
Hypothesis
H_valid_run_to_completion_threshold
:
valid_task_run_to_completion_threshold
arr_seq
tsk
.
...
...
@@ 77,13 +77,13 @@ Section Abstract_RTA.
Let
busy_interval
:
=
busy_interval
sched
interference
interfering_workload
.
Let
response_time_bounded_by
:
=
task_response_time_bound
arr_seq
sched
.
(** Let L be a constant which bounds any busy interval of task tsk. *)
(** Let L be a constant which bounds any busy interval of task
[
tsk
]
. *)
Variable
L
:
duration
.
Hypothesis
H_busy_interval_exists
:
busy_intervals_are_bounded_by
interference
interfering_workload
L
.
(** Next, assume that interference_bound_function is a bound on
the interference incurred by jobs of task tsk. *)
the interference incurred by jobs of task
[
tsk
]
. *)
Variable
interference_bound_function
:
Task
>
duration
>
duration
>
duration
.
Hypothesis
H_job_interference_is_bounded
:
job_interference_is_bounded_by
...
...
@@ 92,9 +92,9 @@ Section Abstract_RTA.
(** For simplicity, let's define a local name for the search space. *)
Let
is_in_search_space
A
:
=
is_in_search_space
tsk
L
interference_bound_function
A
.
(** Consider any value
R
that upperbounds the solution of each responsetime recurrence,
(** Consider any value
[R]
that upperbounds the solution of each responsetime recurrence,
i.e., for any relative arrival time A in the search space, there exists a corresponding
solution
F
such that F + (task_cost tsk  task_run_to_completion_threshold tsk) <= R. *)
solution
[F]
such that
[
F + (task_cost tsk  task_run_to_completion_threshold tsk) <= R
]
. *)
Variable
R
:
nat
.
Hypothesis
H_R_is_maximum
:
forall
A
,
...
...
@@ 105,10 +105,10 @@ Section Abstract_RTA.
F
+
(
task_cost
tsk

task_run_to_completion_threshold
tsk
)
<=
R
.
(** In this section we show a detailed proof of the main theorem
that establishes that R is a responsetime bound of task tsk. *)
that establishes that R is a responsetime bound of task
[
tsk
]
. *)
Section
ProofOfTheorem
.
(** Consider any job j of tsk with positive cost. *)
(** Consider any job j of
[
tsk
]
with positive cost. *)
Variable
j
:
Job
.
Hypothesis
H_j_arrives
:
arrives_in
arr_seq
j
.
Hypothesis
H_job_of_tsk
:
job_task
j
=
tsk
.
...
...
@@ 123,29 +123,29 @@ Section Abstract_RTA.
(** In order to prove that R is a responsetime bound of job j, we use hypothesis H_R_is_maximum.
Note that the relative arrival time (A) is not necessarily from the search space. However,
earlier we have proven that for any A there exists another A_sp from the search space that
shares the same IBF value. Moreover, we've also shown that there exists an F_sp such that
F_sp is a solution of the response time recurrence for parameter A_sp. Thus, despite the
earlier we have proven that for any A there exists another
[
A_sp
]
from the search space that
shares the same IBF value. Moreover, we've also shown that there exists an
[
F_sp
]
such that
[
F_sp
]
is a solution of the response time recurrence for parameter
[
A_sp
]
. Thus, despite the
fact that the relative arrival time may not lie in the search space, we can still use
the assumption H_R_is_maximum. *)
(** More formally, consider any A_sp and F_sp such that:.. *)
(** More formally, consider any
[
A_sp
]
and
[
F_sp
]
such that:.. *)
Variable
A_sp
F_sp
:
duration
.
(** (a) A_sp is less than or equal to
A
... *)
(** (a)
[
A_sp
]
is less than or equal to
[A]
... *)
Hypothesis
H_A_gt_Asp
:
A_sp
<=
A
.
(** (b) interference_bound_function(A, x) is equal to
interference_bound_function(A_sp, x) for all
x
less than
L
... *)
(** (b)
[
interference_bound_function(A, x)
]
is equal to
[
interference_bound_function(A_sp, x)
]
for all
[x]
less than
[L]
... *)
Hypothesis
H_equivalent
:
are_equivalent_at_values_less_than
(
interference_bound_function
tsk
A
)
(
interference_bound_function
tsk
A_sp
)
L
.
(** (c) A_sp is in the search space, ... *)
(** (c)
[
A_sp
]
is in the search space, ... *)
Hypothesis
H_Asp_is_in_search_space
:
is_in_search_space
A_sp
.
(** (d) [A_sp + F_sp] is a solution of the response time rec
c
urence... *)
(** (d) [A_sp + F_sp] is a solution of the response time recu
r
rence... *)
Hypothesis
H_Asp_Fsp_fixpoint
:
A_sp
+
F_sp
=
task_run_to_completion_threshold
tsk
+
interference_bound_function
tsk
A_sp
(
A_sp
+
F_sp
).
...
...
@@ 162,7 +162,7 @@ Section Abstract_RTA.
(** By assumption, suppose that t2 is less than or equal to [t1 + A_sp + F_sp]. *)
Hypothesis
H_big_fixpoint_solution
:
t2
<=
t1
+
(
A_sp
+
F_sp
).
(** Then we prove that [job_arrival j + R] is no less than t2. *)
(** Then we prove that [job_arrival j + R] is no less than
[
t2
]
. *)
Lemma
t2_le_arrival_plus_R
:
t2
<=
job_arrival
j
+
R
.
Proof
.
...
...
@@ 197,32 +197,32 @@ Section Abstract_RTA.
Hypothesis
H_small_fixpoint_solution
:
t1
+
(
A_sp
+
F_sp
)
<
t2
.
(** Next, let's consider two other cases: *)
(** CASE 1: the value of the fixpoint is no less than the relative arrival time of job
j
. *)
(** CASE 1: the value of the fix

point is no less than the relative arrival time of job
[j]
. *)
Section
FixpointIsNoLessThanArrival
.
(** Suppose that [A_sp + F_sp] is no less than relative arrival of job
j
. *)
(** Suppose that [A_sp + F_sp] is no less than relative arrival of job
[j]
. *)
Hypothesis
H_fixpoint_is_no_less_than_relative_arrival_of_j
:
A
<=
A_sp
+
F_sp
.
(** In this section, we prove that the fact that job
j
is not completed by
(** In this section, we prove that the fact that job
[j]
is not completed by
time [job_arrival j + R] leads to a contradiction. Which in turn implies
that the opposite is true  job
j
completes by time [job_arrival j + R]. *)
that the opposite is true  job
[j]
completes by time [job_arrival j + R]. *)
Section
ProofByContradiction
.
(** Recall that by lemma "solution_for_A_exists" there is a solution
F
of the responsetime recurrence for the given relative arrival time
A
(** Recall that by lemma "solution_for_A_exists" there is a solution
[F]
of the responsetime recurrence for the given relative arrival time
[A]
(which is not necessarily from the search space). *)
(** Thus, consider a constant
F
such that:.. *)
(** Thus, consider a constant
[F]
such that:.. *)
Variable
F
:
duration
.
(** (a) the sum of A_sp and F_sp is equal to the sum of
A
and
F
... *)
(** (a) the sum of
[
A_sp
]
and
[
F_sp
]
is equal to the sum of
[A]
and
[F]
... *)
Hypothesis
H_Asp_Fsp_eq_A_F
:
A_sp
+
F_sp
=
A
+
F
.
(** (b)
F
is at most F_sp... *)
(** (b)
[F]
is at mo
1
st
[
F_sp
]
... *)
Hypothesis
H_F_le_Fsp
:
F
<=
F_sp
.
(** (c) and [A + F] is a solution for the responsetime recurrence for
A
. *)
(** (c) and [A + F] is a solution for the responsetime recurrence for
[A]
. *)
Hypothesis
H_A_F_fixpoint
:
A
+
F
=
task_run_to_completion_threshold
tsk
+
interference_bound_function
tsk
A
(
A
+
F
).
(** Next, we assume that job
j
is not completed by time [job_arrival j + R]. *)
(** Next, we assume that job
[j]
is not completed by time [job_arrival j + R]. *)
Hypothesis
H_j_not_completed
:
~~
completed_by
sched
j
(
job_arrival
j
+
R
).
(** Some additional reasoning is required since the term [task_cost tsk  task_run_to_completion_threshold tsk]
...
...
@@ 233,25 +233,25 @@ Section Abstract_RTA.
in the case of floating nonpreemptive sections).
In this case we cannot directly apply lemma "j_receives_at_least_run_to_completion_threshold". Therefore
we introduce two temporal notions of the last nonpreemptive region of job j and an execution
we introduce two temporal notions of the last non

preemptive region of job j and an execution
optimism. We use these notions inside this proof, so we define them only locally. *)
(** Let the last nonpreemptive region of job
j
(last) be the difference between the cost of the job
and the
j
's runtocompletion threshold (i.e. [job_cost j  job_run_to_completion_threshold j]).
(** Let the last non

preemptive region of job
[j]
(last) be the difference between the cost of the job
and the
[j]
's runtocompletion threshold (i.e. [job_cost j  job_run_to_completion_threshold j]).
We know that after j has reached its runtocompletion threshold, it will additionally be executed
[job_last j] units of time. *)
Let
job_last
:
=
job_cost
j

job_run_to_completion_threshold
j
.
(** And let execution optimism (optimism) be the difference between the tsk's
runtocompletion threshold and the
j
's runtocompletion threshold (i.e.
(** And let execution optimism (optimism) be the difference between the
[
tsk
]
's
runtocompletion threshold and the
[j]
's runtocompletion threshold (i.e.
[task_run_to_completion_threshold  job_run_to_completion_threshold]).
Intuitively, optimism is how much earlier job j has received its
runtocompletion threshold than it could at worst. *)
Let
optimism
:
=
task_run_to_completion_threshold
tsk

job_run_to_completion_threshold
j
.
(** From lemma "j_receives_at_least_run_to_completion_threshold" with paramete
t
rs [progress_of_job :=
job_run_to_completion_threshold j] and [delta := (A + F)  optimism)] we know that service of
j
by time [t1 + (A + F)  optimism] is no less than [job_run_to_completion_threshold j]. Hence, job
j
(** From lemma "j_receives_at_least_run_to_completion_threshold" with parameters [progress_of_job :=
job_run_to_completion_threshold j] and [delta := (A + F)  optimism)] we know that service of
[j]
by time [t1 + (A + F)  optimism] is no less than [job_run_to_completion_threshold j]. Hence, job
[j]
is completed by time [t1 + (A + F)  optimism + last]. *)
Lemma
j_is_completed_by_t1_A_F_optimist_last
:
completed_by
sched
j
(
t1
+
(
A
+
F

optimism
)
+
job_last
).
...
...
@@ 295,10 +295,10 @@ Section Abstract_RTA.
So, for example [a + (b  c) = a + b  c] only if [b ≥ c]. *)
Section
AuxiliaryInequalities
.
(** Recall that we consider a busy interval of a job
j
, and
j
has arrived
A
time units
(** Recall that we consider a busy interval of a job
[j]
, and
[j]
has arrived
[A]
time units
after the beginning the busy interval. From basic properties of a busy interval it
follows that job
j
incur
r
s interference at any time instant t ∈ [t1, t1 + A).
Therefore interference_bound_function(tsk, A, A + F) is at least
A
. *)
follows that job
[j]
incurs interference at any time instant t ∈ [t1, t1 + A).
Therefore
[
interference_bound_function(tsk, A, A + F)
]
is at least
[A]
. *)
Lemma
relative_arrival_le_interference_bound
:
A
<=
interference_bound_function
tsk
A
(
A
+
F
).
Proof
.
...
...
@@ 342,7 +342,7 @@ Section Abstract_RTA.
Qed
.
(** As two trivial corollaries, we show that
tsk's runtocompletion threshold is at most F_sp... *)
[
tsk
]
's runtocompletion threshold is at most
[
F_sp
]
... *)
Corollary
tsk_run_to_completion_threshold_le_Fsp
:
task_run_to_completion_threshold
tsk
<=
F_sp
.
Proof
.
...
...
@@ 354,7 +354,7 @@ Section Abstract_RTA.
apply
leq_trans
with
F
;
auto
.
Qed
.
(** ... and optimism is at most
F
. *)
(** ... and optimism is at most
[F]
. *)
Corollary
optimism_le_F
:
optimism
<=
F
.
Proof
.
...
...
@@ 371,13 +371,13 @@ Section Abstract_RTA.
(** Next we show that [t1 + (A + F)  optimism + last] is at most [job_arrival j + R],
which is easy to see from the following sequence of inequalities:
t1 + (A + F)  optimism + last
≤ job_arrival j + (F  optimism) + job_last
≤ job_arrival j + (F_sp  optimism) + job_last
≤ job_arrival j + F_sp + (job_last  optimism)
≤ job_arrival j + F_sp + job_cost j  task_run_to_completion_threshold tsk
≤ job_arrival j + F_sp + task_cost tsk  task_run_to_completion_threshold tsk
≤ job_arrival j + R. *)
[
t1 + (A + F)  optimism + last
]
[
≤ job_arrival j + (F  optimism) + job_last
]
[
≤ job_arrival j + (F_sp  optimism) + job_last
]
[
≤ job_arrival j + F_sp + (job_last  optimism)
]
[
≤ job_arrival j + F_sp + job_cost j  task_run_to_completion_threshold tsk
]
[
≤ job_arrival j + F_sp + task_cost tsk  task_run_to_completion_threshold tsk
]
[
≤ job_arrival j + R
]
. *)
Lemma
t1_A_F_optimist_last_le_arrival_R
:
t1
+
(
A
+
F

optimism
)
+
job_last
<=
job_arrival
j
+
R
.
Proof
.
...
...
@@ 406,7 +406,7 @@ Section Abstract_RTA.
}
Qed
.
(** ... which contradicts the initial assumption about
j
is not
(** ... which contradicts the initial assumption about
[j]
is not
completed by time [job_arrival j + R]. *)
Lemma
j_is_completed_earlier_contradiction
:
False
.
Proof
.
...
...
@@ 417,7 +417,7 @@ Section Abstract_RTA.
End
ProofByContradiction
.
(** Putting everything together, we conclude that
j
is completed by [job_arrival j + R]. *)
(** Putting everything together, we conclude that
[j]
is completed by [job_arrival j + R]. *)
Lemma
job_completed_by_arrival_plus_R_2
:
completed_by
sched
j
(
job_arrival
j
+
R
).
Proof
.
...
...
@@ 445,9 +445,9 @@ Section Abstract_RTA.
End
FixpointIsNoLessThanArrival
.
(** CASE 2: the value of the fixpoint is less than the relative arrival time of
job j (which turns out to be impossible, i.e. the solution of the respon
c
etime
recurren
s
e is always equal to or greater than the relative arrival time). *)
(** CASE 2: the value of the fix

point is less than the relative arrival time of
job j (which turns out to be impossible, i.e. the solution of the respon
s
etime
recurren
c
e is always equal to or greater than the relative arrival time). *)
Section
FixpointCannotBeSmallerThanArrival
.
(** Assume that [A_sp + F_sp] is less than A. *)
...
...
@@ 497,8 +497,8 @@ Section Abstract_RTA.
by
rewrite
{
2
}
H_Asp_Fsp_fixpoint
leq_add
//
;
apply
H_valid_run_to_completion_threshold
.
Qed
.
(** However, this is a contradiction. Since job
j
has not yet arrived, its service
is equal to
0
. However, runtocompletion threshold is always positive. *)
(** However, this is a contradiction. Since job
[j]
has not yet arrived, its service
is equal to
[0]
. However, runtocompletion threshold is always positive. *)
Lemma
relative_arrival_time_is_no_less_than_fixpoint
:
False
.
Proof
.
...
...
@@ 518,7 +518,7 @@ Section Abstract_RTA.
End
ProofOfTheorem
.
(** Using the lemmas above, we prove that
R
is a responsetime bound. *)
(** Using the lemmas above, we prove that
[R]
is a responsetime bound. *)
Theorem
uniprocessor_response_time_bound
:
response_time_bounded_by
tsk
R
.
Proof
.
...
...
restructuring/analysis/abstract/abstract_seq_rta.v
View file @
d1f8192c
...
...
@@ 8,11 +8,11 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** * Abstract ResponseTime Analysis with sequential tasks *)
(** In this section we propose the general framework for responsetime analysis (RTA)
of uniprocessor scheduling of realtime tasks with arbitrary arrival models
of uni

processor scheduling of realtime tasks with arbitrary arrival models
and sequential tasks. *)
(** We prove that the maximum among the solutions of the responsetime bound
recurrence for some set of parameters is a responsetime bound for tsk.
recurrence for some set of parameters is a responsetime 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 responsetime
bound function, since jobs of the same task will be executed strictly
...
...
@@ 51,7 +51,7 @@ Section Sequential_Abstract_RTA.
(** Consider an arbitrary task set. *)
Variable
ts
:
list
Task
.
(** Let tsk be any task in ts that is to be analyzed. *)
(** Let
[
tsk
]
be any task in ts that is to be analyzed. *)
Variable
tsk
:
Task
.
Hypothesis
H_tsk_in_ts
:
tsk
\
in
ts
.
...
...
@@ 60,15 +60,15 @@ Section Sequential_Abstract_RTA.
valid_preemption_model
arr_seq
sched
.
(** ...and a valid task runtocompletion threshold function. That is,
[task_run_to_completion_threshold tsk] is (1) no bigger than tsk's
cost, (2) for any job of task tsk
job_run_to_completion_threshold
is bounded by task_run_to_completion_threshold. *)
[task_run_to_completion_threshold tsk] is (1) no bigger than
[
tsk
]
's
cost, (2) for any job of task
[
tsk
] [
job_run_to_completion_threshold
]
is bounded by
[
task_run_to_completion_threshold
]
. *)
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. *)
(** 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
.
...
...
@@ 92,7 +92,7 @@ Section Sequential_Abstract_RTA.
(** When assuming sequential tasks, we can introduce an additional hypothesis that
ensures that the values of interference and workload remain consistent. It states
that any of tsk's job, that arrived before the busy interval, should be
that any of
[
tsk
]
's job, that arrived before the busy interval, should be
completed by the beginning of the busy interval. *)
Definition
interference_and_workload_consistent_with_sequential_tasks
:
=
forall
(
j
:
Job
)
(
t1
t2
:
instant
),
...
...
@@ 102,11 +102,11 @@ Section Sequential_Abstract_RTA.
busy_interval
j
t1
t2
>
task_workload_between
0
t1
=
task_service_of_jobs_in
(
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
(** 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
...
...
@@ 115,7 +115,7 @@ Section Sequential_Abstract_RTA.
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
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. *)
...
...
@@ 127,11 +127,11 @@ Section Sequential_Abstract_RTA.
Definition
cumul_task_interference
tsk
upper_bound
t1
t2
:
=
\
sum_
(
t1
<=
t
<
t2
)
task_interference_received_before
tsk
upper_bound
t
.
(** We say that task interference is bounded by task_interference_bound_function (tIBF)
iff for any job
j
of task tsk cumulative _task_ interference within the interval
[t1, t1 + R) is bounded by function tIBF(tsk, A, R).
(** We say that task interference is bounded by task_interference_bound_function (
[
tIBF
]
)
iff for any job
[j]
of task
[
tsk
]
cumulative _task_ interference within the interval
[t1, t1 + R) is bounded by function
[
tIBF(tsk, A, R)
]
.
Note that this definition is almost the same as the definition of job_interference_is_bounded_by
from the nonne
s
essarysequential case. However, in this case we ignore the
from the nonne
c
essarysequential 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
)
:
=
...
...
@@ 147,7 +147,7 @@ Section Sequential_Abstract_RTA.
End
Definitions
.
(** In this section, we prove that the maximum among the solutions of the
responsetime bound recurrence is a responsetime bound for tsk. *)
responsetime bound recurrence is a responsetime bound for
[
tsk
]
. *)
Section
ResponseTimeBound
.
(** For simplicity, let's define some local names. *)
...
...
@@ 166,7 +166,7 @@ Section Sequential_Abstract_RTA.
Hypothesis
H_interference_and_workload_consistent_with_sequential_tasks
:
interference_and_workload_consistent_with_sequential_tasks
.
(** Assume we have a constant L which bounds the busy interval of any of tsk's jobs. *)
(** Assume we have a constant L which 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
interference
interfering_workload
L
.
...
...
@@ 176,12 +176,12 @@ Section Sequential_Abstract_RTA.
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
Δ
(** 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
interferece that is bounded by task_IBF(tsk, A, Δ). *)
received from other jobs of task
[
tsk
]
 [task_rbf (A + ε)  task_cost tsk] and (2) any other
interfere
n
ce 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
Δ
.
...
...
@@ 191,14 +191,14 @@ Section Sequential_Abstract_RTA.
[total_interference_bound (tsk, A, Δ) ≠ total_interference_bound (tsk, A + ε, Δ)]. *)
Let
is_in_search_space_seq
:
=
is_in_search_space
tsk
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 responsetime recurrence that is bounded by
R
. In
(** Consider any value
[R]
, and assume that for any relative arrival time
[A]
from the search
space there is a solution
[F]
of the responsetime recurrence that is bounded by
[R]
. In
contrast to the formula in "nonsequential" Abstract RTA, assuming that tasks are
sequential leads to a more precise responsetime bound. Now we can explicitly express
the interference caused by other jobs of the task under consideration.
To understand the right part of the fixpoint in the equation it is helpful to note
that the bound on the total interference (bound_of_total_interference) is equal to
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 + tIBF tsk A Δ]. Besides, a job must receive
enough service to become nonpreemptive [task_lock_in_service tsk]. The sum of
these two quantities is exactly the righthand side of the equation. *)
...
...
@@ 215,7 +215,7 @@ Section Sequential_Abstract_RTA.
considering the busy interval of the job under consideration. *)
Section
CompletionOfJobsFromSameTask
.
(** Consider any two jobs j1
j2 of tsk. *)
(** Consider any two jobs
[
j1
] [
j2
]
of
[
tsk
]
. *)
Variable
j1
j2
:
Job
.
Hypothesis
H_j1_arrives
:
arrives_in
arr_seq
j1
.
Hypothesis
H_j2_arrives
:
arrives_in
arr_seq
j2
.
...
...
@@ 227,7 +227,7 @@ Section Sequential_Abstract_RTA.
Variable
t1
t2
:
instant
.
Hypothesis
H_busy_interval
:
busy_interval
j1
t1
t2
.
(** We prove that if a job from task tsk arrived before the beginning of the busy
(** 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 *)
Lemma
completed_before_beginning_of_busy_interval
:
job_arrival
j2
<
t1
>
...
...
@@ 270,10 +270,10 @@ Section Sequential_Abstract_RTA.
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. *)
job of task
[
tsk
]
, i.e., the hypothesis
[
H_job_interference_is_bounded
]
holds. *)
Section
BoundOfCumulativeJobInterference
.
(** Consider any job
j
of tsk. *)
(** Consider any job
[j]
of
[
tsk
]
. *)
Variable
j
:
Job
.
Hypothesis
H_j_arrives
:
arrives_in
arr_seq
j
.
Hypothesis
H_job_of_tsk
:
job_task
j
=
tsk
.
...
...
@@ 295,9 +295,9 @@ Section Sequential_Abstract_RTA.
(** 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
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. *)
task
[
tsk
]
that arrive after [t1 + A + ε] cannot interfere with j. *)
Section
TaskInterferenceBoundsInterference
.
(** We start by proving a simpler analog of the lemma which states that at
...
...
@@ 314,13 +314,13 @@ Section Sequential_Abstract_RTA.
Section
Case1
.
(** Assume the processor is idle at time
t
. *)
(** Assume the processor is idle at time
[t]
. *)
Hypothesis
H_idle
:
sched
t
=
None
.
(** 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_interferece tsk = 1]. Which reduces to [1 ≤ 1]. *)
interference doesn't come from a job of task
[
tsk
]
[task_interfere
n
ce 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
+
...
...
@@ 344,15 +344,15 @@ Section Sequential_Abstract_RTA.
Section
Case2
.
(** Assume a job j' from another task is scheduled at time
t
. *)
(** Assume a job
[
j'
]
from another task is scheduled at time
[t]
. *)
Variable
j'
:
Job
.
Hypothesis
H_sched
:
sched
t
=
Some
j'
.
Hypothesis
H_not_job_of_tsk
:
job_task
j'
!=
tsk
.
(** If a job
j
' from another task is scheduled at time
t
,
(** 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_interferece tsk = 1]. Which reduces to [1 ≤ 1]. *)
since interference doesn't come from a job of task
[
tsk
]
[task_interfere
n
ce 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
+
...
...
@@ 384,15 +384,15 @@ Section Sequential_Abstract_RTA.
Section
Case3
.
(** Assume a job j' (different from j) of task tsk is scheduled at time
t
. *)
(** Assume a job
[
j'
]
(different from j) of task
[
tsk
]
is scheduled at time
[t]
. *)
Variable
j'
:
Job
.
Hypothesis
H_sched
:
sched
t
=
Some
j'
.
Hypothesis
H_not_job_of_tsk
:
job_task
j'
==
tsk
.
Hypothesis
H_j_neq_j'
:
j
!=
j'
.
(** If a job j' (different from
j
) of task tsk is scheduled at time
t
, then
(** 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_interferece tsk = 0]. However,
comes from a job of the same task [task_interfere
n
ce 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
<=
...
...
@@ 444,10 +444,10 @@ Section Sequential_Abstract_RTA.
Section
Case4
.
(** Assume that job
j
is scheduled at time
t
. *)
(** Assume that job
[j]
is scheduled at time
[t]
. *)
Hypothesis
H_sched
:
sched
t
=
Some
j
.
(** If job
j
is scheduled at time
t
, then [interference = 0, scheduled_at = 1], but
(** 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
<=
...
...
@@ 551,7 +551,7 @@ Section Sequential_Abstract_RTA.
(** 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). *)
the cumulative interference of
[j]
's task in the interval [t1, t1 + x). *)
Lemma
cumulative_job_interference_le_task_interference_bound
:
cumul_interference
j
t1
(
t1
+
x
)
<=
(
task_workload_between
t1
(
t1
+
A
+
ε
)

job_cost
j
)
...
...
@@ 569,8 +569,8 @@ Section Sequential_Abstract_RTA.
(** In order to obtain a more convenient bound of the cumulative interference, we need to
abandon the actual workload in favor of a bound which depends on task parameters only.
So, we show that actual workload of the task excluding workload of any job
j
is no
greater than bound of workload excluding the cost of job
j
's task. *)
So, we show that actual workload of the task excluding workload of any job
[j]
is no
greater than bound of workload excluding the cost of job
[j]
's task. *)
Lemma
task_rbf_excl_tsk_bounds_task_workload_excl_j
:
task_workload_between
t1
(
t1
+
A
+
ε
)

job_cost
j
<=
task_rbf
(
A
+
ε
)

task_cost
tsk
.
Proof
.
...
...
@@ 615,7 +615,7 @@ Section Sequential_Abstract_RTA.
Qed
.
(** Finally, we use the lemmas above to obtain the bound on
interference in terms of task_rbf and task_interfere. *)
[
interference
]
in terms of
[
task_rbf
]
and
[
task_interfere
nce]
. *)
Lemma
cumulative_job_interference_bound
:
cumul_interference
j
t1
(
t1
+
x
)
<=
(
task_rbf
(
A
+
ε
)

task_cost
tsk
)
+
cumul_task_interference
t2
t1
(
t1
+
x
).
...
...
@@ 637,7 +637,7 @@ Section Sequential_Abstract_RTA.
(** In this section, we prove that [H_R_is_maximum_seq] implies [H_R_is_maximum]. *)
Section
MaxInSeqHypothesisImpMaxInNonseqHypothesis
.
(** Consider any job
j
of tsk. *)
(** Consider any job
[j]
of
[
tsk
]
. *)
Variable
j
:
Job
.
Hypothesis
H_j_arrives
:
arrives_in
arr_seq
j
.
Hypothesis
H_job_of_tsk
:
job_task
j
=
tsk
.
...
...