Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
P
PROSA  Formally Proven Schedulability Analysis
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
2
Issues
2
List
Boards
Labels
Milestones
Merge Requests
1
Merge Requests
1
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Vedant Chavda
PROSA  Formally Proven Schedulability Analysis
Commits
54220d8c
Commit
54220d8c
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 results
parent
6cb786f2
Changes
12
Hide whitespace changes
Inline
Sidebyside
Showing
12 changed files
with
160 additions
and
160 deletions
+160
160
restructuring/results/edf/rta/bounded_nps.v
restructuring/results/edf/rta/bounded_nps.v
+20
20
restructuring/results/edf/rta/bounded_pi.v
restructuring/results/edf/rta/bounded_pi.v
+25
25
restructuring/results/edf/rta/floating_nonpreemptive.v
restructuring/results/edf/rta/floating_nonpreemptive.v
+12
12
restructuring/results/edf/rta/fully_nonpreemptive.v
restructuring/results/edf/rta/fully_nonpreemptive.v
+7
7
restructuring/results/edf/rta/fully_preemptive.v
restructuring/results/edf/rta/fully_preemptive.v
+9
9
restructuring/results/edf/rta/limited_preemptive.v
restructuring/results/edf/rta/limited_preemptive.v
+14
14
restructuring/results/fixed_priority/rta/bounded_nps.v
restructuring/results/fixed_priority/rta/bounded_nps.v
+17
17
restructuring/results/fixed_priority/rta/bounded_pi.v
restructuring/results/fixed_priority/rta/bounded_pi.v
+20
20
restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
...uring/results/fixed_priority/rta/floating_nonpreemptive.v
+11
11
restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
...ucturing/results/fixed_priority/rta/fully_nonpreemptive.v
+5
5
restructuring/results/fixed_priority/rta/fully_preemptive.v
restructuring/results/fixed_priority/rta/fully_preemptive.v
+8
8
restructuring/results/fixed_priority/rta/limited_preemptive.v
...ructuring/results/fixed_priority/rta/limited_preemptive.v
+12
12
No files found.
restructuring/results/edf/rta/bounded_nps.v
View file @
54220d8c
...
...
@@ 4,18 +4,18 @@ Require Export rt.restructuring.analysis.facts.rbf.
Require
Import
rt
.
restructuring
.
model
.
priority
.
edf
.
From
mathcomp
Require
Import
ssreflect
ssrbool
eqtype
ssrnat
seq
path
fintype
bigop
.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
(** Throughout this file, we assume ideal uni

processor schedules. *)
Require
Import
rt
.
restructuring
.
model
.
processor
.
ideal
.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require
Import
rt
.
restructuring
.
model
.
readiness
.
basic
.
(** * RTA for EDFschedulers with Bounded NonPreemp
r
ive Segments *)
(** * RTA for EDFschedulers with Bounded NonPreemp
t
ive Segments *)
(** In this section we instantiate the Abstract RTA for EDFschedulers
with Bounded Priority Inversion to EDFschedulers for ideal
uniprocessor model of realtime tasks with arbitrary
arrival models _and_ bounded nonpreemp
r
ive segments. *)
arrival models _and_ bounded nonpreemp
t
ive segments. *)
(** Recall that Abstract RTA for EDFschedulers with Bounded Priority
Inversion does not specify the cause of priority inversion. In
...
...
@@ 51,7 +51,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
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 ideal uniprocessor schedule of this arrival sequence ... *)
(** Next, consider any ideal 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
.
...
...
@@ 60,12 +60,12 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Hypothesis
H_jobs_must_arrive_to_execute
:
jobs_must_arrive_to_execute
sched
.
Hypothesis
H_completed_jobs_dont_execute
:
completed_jobs_dont_execute
sched
.
(** In addition, we assume the existence of a function maping jobs
(** In addition, we assume the existence of a function map
p
ing jobs
to theirs preemption points ... *)
Context
`
{
JobPreemptable
Job
}.
(** ... and assume that it defines a valid preemption
model with bounded nonpreemptive segments. *)
model with bounded non

preemptive segments. *)
Hypothesis
H_valid_model_with_bounded_nonpreemptive_segments
:
valid_model_with_bounded_nonpreemptive_segments
arr_seq
sched
.
...
...
@@ 77,8 +77,8 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** Next, we assume that the schedule is a workconserving schedule... *)
Hypothesis
H_work_conserving
:
work_conserving
arr_seq
sched
.
(** ... and the schedule respects the policy defined by the
job_preemptable
function (i.e., jobs have bounded nonpreemptive segments). *)
(** ... and the schedule respects the policy defined by the
[job_preemptable]
function (i.e., jobs have bounded non

preemptive segments). *)
Hypothesis
H_respects_policy
:
respects_policy_at_preemption_point
arr_seq
sched
.
(** Consider an arbitrary task set ts, ... *)
...
...
@@ 92,14 +92,14 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
.
(** 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
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
.
(** 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
.
...
...
@@ 108,18 +108,18 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
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
.
(** We introduce as an abbreviation
"rbf"
for the task request bound function,
(** We introduce as an abbreviation
[rbf]
for the task request bound function,
which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
Let
rbf
:
=
task_request_bound_function
.
(** Next, we introduce
task_rbf
as an abbreviation for the task
request bound function of task
tsk
. *)
(** Next, we introduce
[task_rbf]
as an abbreviation for the task
request bound function of task
[tsk]
. *)
Let
task_rbf
:
=
rbf
tsk
.
(** Using the sum of individual request bound functions, we define the request bound
...
...
@@ 146,13 +146,13 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(
task_max_nonpreemptive_segment
tsk_o

ε
).
(** ** Priority inversion is bounded *)
(** In this section, we prove that a priority inversion for task
tsk
is bounded by
the maximum length of non
preem
tive segments among the tasks with lower priority. *)
(** In this section, we prove that a priority inversion for task
[tsk]
is bounded by
the maximum length of non
preemp
tive segments among the tasks with lower priority. *)
Section
PriorityInversionIsBounded
.
(** First, we prove that the maximum length of a priority
inversion of job j is bounded by the maximum length of a
nonpreemptive section of a task with lowerpriority task
non

preemptive section of a task with lowerpriority task
(i.e., the blocking term). *)
Lemma
priority_inversion_is_bounded_by_blocking
:
forall
j
t
,
...
...
@@ 249,7 +249,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** ** ResponseTime Bound *)
(** In this section, we prove that the maximum among the solutions of the responsetime
bound recurrence is a responsetime bound for
tsk
. *)
bound recurrence is a responsetime bound for
[tsk]
. *)
Section
ResponseTimeBound
.
(** Let L be any positive fixed point of the busy interval recurrence. *)
...
...
restructuring/results/edf/rta/bounded_pi.v
View file @
54220d8c
...
...
@@ 8,7 +8,7 @@ Require Import rt.restructuring.model.task.absolute_deadline.
Require
Import
rt
.
restructuring
.
analysis
.
abstract
.
ideal_jlfp_rta
.
From
mathcomp
Require
Import
ssreflect
ssrbool
eqtype
ssrnat
seq
path
fintype
bigop
.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
(** Throughout this file, we assume ideal uni

processor schedules. *)
Require
Import
rt
.
restructuring
.
model
.
processor
.
ideal
.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
...
...
@@ 94,14 +94,14 @@ Section AbstractRTAforEDFwithArrivalCurves.
(** Next, we assume that all jobs come from the task set. *)
Hypothesis
H_all_jobs_from_taskset
:
all_jobs_from_taskset
arr_seq
ts
.
(** 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
(** 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
.
(** 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
.
...
...
@@ 110,18 +110,18 @@ Section AbstractRTAforEDFwithArrivalCurves.
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
.
(** We introduce
"rbf"
as an abbreviation of the task request bound function,
(** We introduce
[rbf]
as an abbreviation of the task request bound function,
which is defined as [task_cost(T) × max_arrivals(T,Δ)] for some task T. *)
Let
rbf
:
=
task_request_bound_function
.
(** Next, we introduce
task_rbf
as an abbreviation
of the task request bound function of task
tsk
. *)
(** Next, we introduce
[task_rbf]
as an abbreviation
of the task request bound function of task
[tsk]
. *)
Let
task_rbf
:
=
rbf
tsk
.
(** Using the sum of individual request bound functions, we define the request bound
...
...
@@ 133,8 +133,8 @@ Section AbstractRTAforEDFwithArrivalCurves.
Let
number_of_task_arrivals
:
=
number_of_task_arrivals
arr_seq
.
(** Assume that there exists a constant priority_inversion_bound that bounds
the length of any priority inversion experienced by any job of
tsk
.
Since we analyze only task
tsk
, we ignore the lengths of priority
the length of any priority inversion experienced by any job of
[tsk]
.
Since we analyze only task
[tsk]
, we ignore the lengths of priority
inversions incurred by any other tasks. *)
Variable
priority_inversion_bound
:
duration
.
Hypothesis
H_priority_inversion_is_bounded
:
...
...
@@ 159,19 +159,19 @@ Section AbstractRTAforEDFwithArrivalCurves.
(** In case of search space for EDF we ask whether [task_rbf A ≠ task_rbf (A + ε)]... *)
Definition
task_rbf_changes_at
(
A
:
duration
)
:
=
task_rbf
A
!=
task_rbf
(
A
+
ε
).
(** ...or there exists a task
tsko
from ts such that [tsko ≠ tsk] and
(** ...or there exists a task
[tsko]
from ts such that [tsko ≠ tsk] and
[rbf(tsko, A + D tsk  D tsko) ≠ rbf(tsko, A + ε + D tsk  D tsko)].
Note that we use a slightly uncommon notation [has (λ tsko ⇒ P tskₒ) ts]
which can be interpreted as follows: taskset ts contains a task
tsko
such
that a predicate
P holds for tsko
. *)
which can be interpreted as follows: taskset ts contains a task
[tsko]
such
that a predicate
[P] holds for [tsko]
. *)
Definition
bound_on_total_hep_workload_changes_at
A
:
=
has
(
fun
tsko
=>
(
tsk
!=
tsko
)
&&
(
rbf
tsko
(
A
+
D
tsk

D
tsko
)
!=
rbf
tsko
((
A
+
ε
)
+
D
tsk

D
tsko
)))
ts
.
(** The final search space for EDF is a set of offsets that are less than
L
and where
task_rbf or bound_on_total_hep_workload
changes. *)
(** The final search space for EDF is a set of offsets that are less than
[L]
and where
[task_rbf] or [bound_on_total_hep_workload]
changes. *)
Let
is_in_search_space
(
A
:
duration
)
:
=
(
A
<
L
)
&&
(
task_rbf_changes_at
A

bound_on_total_hep_workload_changes_at
A
).
...
...
@@ 214,7 +214,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
Section
FillingOutHypothesesOfAbstractRTATheorem
.
(** First, we prove that in the instantiation of interference and interfering workload,
we really take into account everything that can interfere with
tsk
's jobs, and thus,
we really take into account everything that can interfere with
[tsk]
's jobs, and thus,
the scheduler satisfies the abstract notion of work conserving schedule. *)
Lemma
instantiated_i_and_w_are_coherent_with_schedule
:
work_conserving_ab
tsk
interference
interfering_workload
.
...
...
@@ 300,7 +300,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
constructing a sequence of inequalities. *)
Section
Inequalities
.
(* Consider an arbitrary job j of
tsk
. *)
(* Consider an arbitrary 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
.
...
...
@@ 408,7 +408,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
(** Next we focus on one task [tsk_o ≠ tsk] and consider two cases. *)
(** Case 1:
Δ ≤ A + ε + D tsk  D tsk_o
. *)
(** Case 1:
[Δ ≤ A + ε + D tsk  D tsk_o]
. *)
Section
Case1
.
(** Consider an arbitrary task [tsk_o ≠ tsk] from [ts]. *)
...
...
@@ 445,7 +445,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
End
Case1
.
(** Case 2:
A + ε + D tsk  D tsk_o ≤ Δ
. *)
(** Case 2:
[A + ε + D tsk  D tsk_o ≤ Δ]
. *)
Section
Case2
.
(** Consider an arbitrary task [tsk_o ≠ tsk] from [ts]. *)
...
...
@@ 561,8 +561,8 @@ Section AbstractRTAforEDFwithArrivalCurves.
task t, and the length of the interval to the maximum amount
of interference.
However, in this module we analyze only one task 
tsk
,
therefore it is “hardcoded” inside the interference bound
However, in this module we analyze only one task 
[tsk]
,
therefore it is “hard

coded” inside the interference bound
function IBF. Therefore, in order for the IBF signature to
match the required signature in module abstract_seq_RTA, we
wrap the IBF function in a function that accepts, but simply
...
...
@@ 594,13 +594,13 @@ Section AbstractRTAforEDFwithArrivalCurves.
(** Finally, we show that there exists a solution for the responsetime recurrence. *)
Section
SolutionOfResponseTimeReccurenceExists
.
(** 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_of_task
tsk
j
.
Hypothesis
H_job_cost_positive
:
job_cost_positive
j
.
(** Given any job j of task
tsk
that arrives exactly A units after the beginning of
(** Given any job j of task
[tsk]
that arrives exactly A units after the beginning of
the busy interval, the bound of the total interference incurred by j within an
interval of length Δ is equal to [task_rbf (A + ε)  task_cost tsk + IBF(A, Δ)]. *)
Let
total_interference_bound
tsk
(
A
Δ
:
duration
)
:
=
...
...
@@ 675,7 +675,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
(** ** Final Theorem *)
(** Based on the properties established above, we apply the abstract analysis
framework to infer that R is a responsetime bound for
tsk
. *)
framework to infer that R is a responsetime bound for
[tsk]
. *)
Theorem
uniprocessor_response_time_bound_edf
:
response_time_bounded_by
tsk
R
.
Proof
.
...
...
restructuring/results/edf/rta/floating_nonpreemptive.v
View file @
54220d8c
...
...
@@ 3,7 +3,7 @@ Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.floating
Require
Import
rt
.
restructuring
.
model
.
priority
.
edf
.
From
mathcomp
Require
Import
ssreflect
ssrbool
eqtype
ssrnat
seq
path
fintype
bigop
.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
(** Throughout this file, we assume ideal uni

processor schedules. *)
Require
Import
rt
.
restructuring
.
model
.
processor
.
ideal
.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
...
...
@@ 39,10 +39,10 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
Hypothesis
H_arrival_times_are_consistent
:
consistent_arrival_times
arr_seq
.
Hypothesis
H_arr_seq_is_a_set
:
arrival_sequence_uniq
arr_seq
.
(** Assume we have the model with floating nonpreemptive regions.
I.e., for each task only the length of the maximal nonpreemptive
(** Assume we have the model with floating non

preemptive regions.
I.e., for each task only the length of the maximal non

preemptive
segment is known _and_ each job level is divided into a number
of nonpreemptive segments by inserting preemption points. *)
of non

preemptive segments by inserting preemption points. *)
Context
`
{
JobPreemptionPoints
Job
}
`
{
TaskMaxNonpreemptiveSegment
Task
}.
Hypothesis
H_valid_task_model_with_floating_nonpreemptive_regions
:
...
...
@@ 59,18 +59,18 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
.
(** 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
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
.
(** 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
.
(** Next, consider any ideal uniprocessor schedule with limited
(** Next, consider any ideal uni

processor schedule with limited
preemptions of this arrival sequence ... *)
Variable
sched
:
schedule
(
ideal
.
processor_state
Job
).
Hypothesis
H_jobs_come_from_arrival_sequence
:
...
...
@@ 90,7 +90,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
Hypothesis
H_work_conserving
:
work_conserving
arr_seq
sched
.
(** ... and the schedule respects the policy defined by the
job_preemptable function (i.e., jobs have bounded nonpreemptive
job_preemptable function (i.e., jobs have bounded non

preemptive
segments). *)
Hypothesis
H_respects_policy
:
respects_policy_at_preemption_point
arr_seq
sched
.
...
...
@@ 101,12 +101,12 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
Let
bound_on_total_hep_workload_changes_at
:
=
bound_on_total_hep_workload_changes_at
ts
tsk
.
(** We introduce the abbreviation
"rbf"
for the task request bound function,
(** We introduce the abbreviation
[rbf]
for the task request bound function,
which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
Let
rbf
:
=
task_request_bound_function
.
(** Next, we introduce
task_rbf
as an abbreviation
for the task request bound function of task
tsk
. *)
(** Next, we introduce
[task_rbf]
as an abbreviation
for the task request bound function of task
[tsk]
. *)
Let
task_rbf
:
=
rbf
tsk
.
(** Using the sum of individual request bound functions, we define the request bound
...
...
restructuring/results/edf/rta/fully_nonpreemptive.v
View file @
54220d8c
...
...
@@ 4,7 +4,7 @@ Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.nonpreem
Require
Import
rt
.
restructuring
.
model
.
priority
.
edf
.
From
mathcomp
Require
Import
ssreflect
ssrbool
eqtype
ssrnat
seq
path
fintype
bigop
.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
(** Throughout this file, we assume ideal uni

processor schedules. *)
Require
Import
rt
.
restructuring
.
model
.
processor
.
ideal
.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
...
...
@@ 50,14 +50,14 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
.
(** 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
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
.
(** 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
.
...
...
@@ 90,12 +90,12 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
Let
bound_on_total_hep_workload_changes_at
:
=
bound_on_total_hep_workload_changes_at
ts
tsk
.
(** We introduce the abbreviation
"rbf"
for the task request bound function,
(** We introduce the abbreviation
[rbf]
for the task request bound function,
which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
Let
rbf
:
=
task_request_bound_function
.
(** Next, we introduce
task_rbf
as an abbreviation
for the task request bound function of task
tsk
. *)
(** Next, we introduce
[task_rbf]
as an abbreviation
for the task request bound function of task
[tsk]
. *)
Let
task_rbf
:
=
rbf
tsk
.
(** Using the sum of individual request bound functions, we define the request bound
...
...
restructuring/results/edf/rta/fully_preemptive.v
View file @
54220d8c
...
...
@@ 4,7 +4,7 @@ Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.preempti
Require
Import
rt
.
restructuring
.
model
.
priority
.
edf
.
From
mathcomp
Require
Import
ssreflect
ssrbool
eqtype
ssrnat
seq
path
fintype
bigop
.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
(** Throughout this file, we assume ideal uni

processor schedules. *)
Require
Import
rt
.
restructuring
.
model
.
processor
.
ideal
.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
...
...
@@ 50,14 +50,14 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
.
(** 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
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
.
(** 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
.
...
...
@@ 78,7 +78,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
Hypothesis
H_work_conserving
:
work_conserving
arr_seq
sched
.
(** ... and the schedule respects the policy defined by the
job_preemptable function (i.e., jobs have bounded non
preemptive
[job_preemptable] function (i.e., jobs have bounded non
preemptive
segments). *)
Hypothesis
H_respects_policy
:
respects_policy_at_preemption_point
arr_seq
sched
.
...
...
@@ 89,12 +89,12 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
Let
bound_on_total_hep_workload_changes_at
:
=
bound_on_total_hep_workload_changes_at
ts
tsk
.
(** We introduce the abbreviation
"rbf"
for the task request bound function,
(** We introduce the abbreviation
[rbf]
for the task request bound function,
which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
Let
rbf
:
=
task_request_bound_function
.
(** Next, we introduce
task_rbf
as an abbreviation
for the task request bound function of task
tsk
. *)
(** Next, we introduce
[task_rbf]
as an abbreviation
for the task request bound function of task
[tsk]
. *)
Let
task_rbf
:
=
rbf
tsk
.
(** Using the sum of individual request bound functions, we define the request bound
...
...
@@ 126,7 +126,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
A
+
F
=
task_rbf
(
A
+
ε
)
+
bound_on_total_hep_workload
A
(
A
+
F
)
/\
F
<=
R
.
(** Now, we can leverage the results for the abstract model with bounded nonpreemptive segments
(** Now, we can leverage the results for the abstract model with bounded non

preemptive segments
to establish a responsetime bound for the more concrete model of fully preemptive scheduling. *)
Theorem
uniprocessor_response_time_bound_fully_preemptive_edf
:
response_time_bounded_by
tsk
R
.
...
...
restructuring/results/edf/rta/limited_preemptive.v
View file @
54220d8c
...
...
@@ 3,7 +3,7 @@ Require Export rt.restructuring.analysis.facts.preemption.rtc_threshold.limited.
Require
Import
rt
.
restructuring
.
model
.
priority
.
edf
.
From
mathcomp
Require
Import
ssreflect
ssrbool
eqtype
ssrnat
seq
path
fintype
bigop
.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
(** Throughout this file, we assume ideal uni

processor schedules. *)
Require
Import
rt
.
restructuring
.
model
.
processor
.
ideal
.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
...
...
@@ 13,7 +13,7 @@ Require Import rt.restructuring.model.readiness.basic.
Require
Import
rt
.
restructuring
.
model
.
preemption
.
limited_preemptive
.
Require
Import
rt
.
restructuring
.
model
.
task
.
preemption
.
limited_preemptive
.
(** * RTA for EDFschedulers with Fixed Premption Points *)
(** * RTA for EDFschedulers with Fixed Pre
e
mption Points *)
(** In this module we prove the RTA theorem for EDFschedulers with fixed preemption points. *)
Section
RTAforFixedPreemptionPointsModelwithArrivalCurves
.
...
...
@@ 50,27 +50,27 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
.
(** Next, we assume we have the model with fixed preemption points.
I.e., each task is divided into a number of nonpreemptive segments
by inserting staticaly predefined preemption points. *)
I.e., each task is divided into a number of non

preemptive segments
by inserting statical
l
y predefined preemption points. *)
Context
`
{
JobPreemptionPoints
Job
}.
Context
`
{
TaskPreemptionPoints
Task
}.
Hypothesis
H_valid_model_with_fixed_preemption_points
:
valid_fixed_preemption_points_model
arr_seq
ts
.
(** 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
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
.
(** 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
.
(** Next, consider any ideal uniprocessor schedule with limited
preemptionsof this arrival sequence ... *)
(** Next, consider any ideal uni

processor schedule with limited
preemptions
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
.
...
...
@@ 89,7 +89,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
Hypothesis
H_work_conserving
:
work_conserving
arr_seq
sched
.
(** ... and the schedule respects the policy defined by the
job_preemptable function (i.e., jobs have bounded non
preemptive
[job_preemptable] function (i.e., jobs have bounded non
preemptive
segments). *)
Hypothesis
H_respects_policy
:
respects_policy_at_preemption_point
arr_seq
sched
.
...
...
@@ 99,12 +99,12 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
Let
bound_on_total_hep_workload_changes_at
:
=
bound_on_total_hep_workload_changes_at
ts
tsk
.
(** We introduce the abbreviation
"rbf"
for the task request bound function,
(** We introduce the abbreviation
[rbf]
for the task request bound function,
which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
Let
rbf
:
=
task_request_bound_function
.
(** Next, we introduce
task_rbf
as an abbreviation
for the task request bound function of task
tsk
. *)
(** Next, we introduce
[task_rbf]
as an abbreviation
for the task request bound function of task
[tsk]
. *)
Let
task_rbf
:
=
rbf
tsk
.
(** Using the sum of individual request bound functions, we define the request bound
...
...
@@ 143,7 +143,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
+
bound_on_total_hep_workload
A
(
A
+
F
)
/\
F
+
(
task_last_nonpr_segment
tsk

ε
)
<=
R
.
(** Now, we can leverage the results for the abstract model with bounded nonpreemptive segments
(** Now, we can leverage the results for the abstract model with bounded non

preemptive segments
to establish a responsetime bound for the more concrete model of fixed preemption points. *)
Theorem
uniprocessor_response_time_bound_edf_with_fixed_preemption_points
:
response_time_bounded_by
tsk
R
.
...
...
restructuring/results/fixed_priority/rta/bounded_nps.v
View file @
54220d8c
...
...
@@ 4,18 +4,18 @@ Require Export rt.restructuring.results.fixed_priority.rta.bounded_pi.
Require
Export
rt
.
restructuring
.
analysis
.
facts
.
priority_inversion
.
From
mathcomp
Require
Import
ssreflect
ssrbool
eqtype
ssrnat
seq
path
fintype
bigop
.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
(** Throughout this file, we assume ideal uni

processor schedules. *)
Require
Import
rt
.
restructuring
.
model
.
processor
.
ideal
.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require
Import
rt
.
restructuring
.
model
.
readiness
.
basic
.
(** * RTA for FPschedulers with Bounded NonPreemp
r
ive Segments *)
(** * RTA for FPschedulers with Bounded NonPreemp
t
ive Segments *)
(** In this section we instantiate the Abstract RTA for FPschedulers
with Bounded Priority Inversion to FPschedulers for ideal
uniprocessor model of realtime tasks with arbitrary
arrival models _and_ bounded nonpreemp
r
ive segments. *)
arrival models _and_ bounded nonpreemp
t
ive segments. *)
(** Recall that Abstract RTA for FPschedulers with Bounded Priority
Inversion does not specify the cause of priority inversion. In
...
...
@@ 41,7 +41,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
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 ideal uniprocessor schedule of this arrival sequence ... *)
(** Next, consider any ideal 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
.
...
...
@@ 50,12 +50,12 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Hypothesis
H_jobs_must_arrive_to_execute
:
jobs_must_arrive_to_execute
sched
.
Hypothesis
H_completed_jobs_dont_execute
:
completed_jobs_dont_execute
sched
.
(** In addition, we assume the existence of a function maping jobs
(** In addition, we assume the existence of a function map
p
ing jobs
to theirs preemption points ... *)
Context
`
{
JobPreemptable
Job
}.
(** ... and assume that it defines a valid preemption
model with bounded nonpreemptive segments. *)
model with bounded non

preemptive segments. *)
Hypothesis
H_valid_model_with_bounded_nonpreemptive_segments
:
valid_model_with_bounded_nonpreemptive_segments
arr_seq
sched
.
...
...
@@ 73,8 +73,8 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** Next, we assume that the schedule is a workconserving schedule... *)
Hypothesis
H_work_conserving
:
work_conserving
arr_seq
sched
.
(** ... and the schedule respects the policy defined by the
job_preemptable
function (i.e., jobs have bounded nonpreemptive segments). *)
(** ... and the schedule respects the policy defined by the
[job_preemptable]
function (i.e., jobs have bounded non

preemptive segments). *)
Hypothesis
H_respects_policy
:
respects_policy_at_preemption_point
arr_seq
sched
.
(** Consider an arbitrary task set ts, ... *)
...
...
@@ 88,14 +88,14 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
.
(** 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
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
.
(** 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
.
...
...
@@ 104,8 +104,8 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
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
.
...
...
@@ 124,12 +124,12 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(
task_max_nonpreemptive_segment
tsk_other

ε
).
(** ** Priority inversion is bounded *)
(** In this section, we prove that a priority inversion for task
tsk
is bounded by
the maximum length of non
preem
tive segments among the tasks with lower priority. *)
(** In this section, we prove that a priority inversion for task
[tsk]
is bounded by
the maximum length of non
preemp
tive segments among the tasks with lower priority. *)
Section
PriorityInversionIsBounded
.
(** First, we prove that the maximum length of a priority inversion of a job j is
bounded by the maximum length of a nonpreemptive section of a task with
bounded by the maximum length of a non

preemptive section of a task with
lowerpriority task (i.e., the blocking term). *)
Lemma
priority_inversion_is_bounded_by_blocking
:
forall
j
t
,
...
...
@@ 209,7 +209,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** ** ResponseTime Bound *)
(** In this section, we prove that the maximum among the solutions of the responsetime
bound recurrence is a responsetime bound for
tsk
. *)
bound recurrence is a responsetime bound for
[tsk]
. *)
Section
ResponseTimeBound
.
(** Let L be any positive fixed point of the busy interval recurrence. *)
...
...
restructuring/results/fixed_priority/rta/bounded_pi.v
View file @
54220d8c
...
...
@@ 3,7 +3,7 @@ Require Export rt.restructuring.analysis.facts.busy_interval.
Require
Import
rt
.
restructuring
.
analysis
.
abstract
.
ideal_jlfp_rta
.
From
mathcomp
Require
Import
ssreflect
ssrbool
eqtype
ssrnat
seq
path
fintype
bigop
.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
(** Throughout this file, we assume ideal uni

processor schedules. *)
Require
Import
rt
.
restructuring
.
model
.
processor
.
ideal
.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
...
...
@@ 77,14 +77,14 @@ Section AbstractRTAforFPwithArrivalCurves.
(** Next, we assume that all jobs come from the task set. *)
Hypothesis
H_all_jobs_from_taskset
:
all_jobs_from_taskset
arr_seq
ts
.
(** 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
(** 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
.
(** 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
.