Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Marco Maida
PROSA  Formally Proven Schedulability Analysis
Commits
0b7ad51c
Commit
0b7ad51c
authored
Feb 04, 2016
by
Felipe Cerqueira
Browse files
Add proof of least fixed point to EDF RTA
parent
3ea56324
Changes
2
Hide whitespace changes
Inline
Sidebyside
analysis/basic/bertogna_edf_comp.v
View file @
0b7ad51c
...
...
@@ 320,6 +320,15 @@ Module ResponseTimeIterationEDF.
by
simpl
in
EQtsk
;
rewrite

EQtsk
;
subst
;
apply
leq_addr
.
Qed
.
(* The application of the function is inductive. *)
Lemma
bertogna_edf_comp_iteration_inductive
(
P
:
seq
task_with_response_time
>
Type
)
:
P
(
initial_state
ts
)
>
(
forall
k
,
P
(
f
k
)
>
P
(
f
(
k
.+
1
)))
>
P
(
f
(
max_steps
ts
)).
Proof
.
by
intros
P0
Pn
;
induction
(
max_steps
ts
)
;
last
by
apply
Pn
.
Qed
.
(* As a last step, we show that edf_rta_iteration preserves order, i.e., for any
list l1 no smaller than the initial state, and list l2 such that
l1 <= l2, we have (edf_rta_iteration l1) <= (edf_rta_iteration l2). *)
...
...
@@ 708,13 +717,13 @@ Module ResponseTimeIterationEDF.
End
DerivingContradiction
.
(* Using the lemmas above, we prove that edf_rta_iteration reaches
a fixed point
after (max_steps ts)
i
te
rations
, ... *)
Lemma
edf_claimed_bounds_
converges_helper
:
(* Using the lemmas above, we prove that edf_rta_iteration reaches
a fixed point
after (max_steps ts)
s
te
p
, ... *)
Lemma
edf_claimed_bounds_
finds_fixed_point_of_list
:
forall
rt_bounds
,
edf_claimed_bounds
ts
=
Some
rt_bounds
>
valid_sporadic_taskset
task_cost
task_period
task_deadline
ts
>
f
(
max_steps
ts
)
=
f
(
max_steps
ts
)
.+
1
.
f
(
max_steps
ts
)
=
edf_rta_iteration
(
f
(
max_steps
ts
)
)
.
Proof
.
intros
rt_bounds
SOME
VALID
.
unfold
valid_sporadic_taskset
,
is_valid_sporadic_task
in
*.
...
...
@@ 794,16 +803,37 @@ Module ResponseTimeIterationEDF.
by
apply
(
leq_ltn_trans
SUM
)
in
BUG
;
rewrite
ltnn
in
BUG
.
Qed
.
(* ..., which in turn implies that the responsetime bound is the fixed
point from Bertogna and Cirinei's equation. *)
Lemma
edf_claimed_bounds_converges
:
(* ...and since there cannot be a vector of responsetime bounds with values less than
the task costs, this solution is also the least fixed point. *)
Lemma
edf_claimed_bounds_finds_least_fixed_point
:
forall
v
,
all_le
(
initial_state
ts
)
v
>
v
=
edf_rta_iteration
v
>
all_le
(
f
(
max_steps
ts
))
v
.
Proof
.
intros
v
GE0
EQ
.
apply
bertogna_edf_comp_iteration_inductive
;
first
by
done
.
intros
k
GEk
.
rewrite
EQ
.
apply
bertogna_edf_comp_iteration_preserves_order
;
last
by
done
.
by
apply
bertogna_edf_comp_iteration_preserves_minimum
.
Qed
.
(* Therefore, with regard to the responsetime bound recurrence, ...*)
Let
rt_recurrence
(
tsk
:
sporadic_task
)
(
rt_bounds
:
seq
task_with_response_time
)
(
R
:
time
)
:
=
task_cost
tsk
+
div_floor
(
I
rt_bounds
tsk
R
)
num_cpus
.
(* ..., the individual responsetime bounds (elements of the list) are also fixed points. *)
Theorem
edf_claimed_bounds_finds_fixed_point_for_each_bound
:
forall
tsk
R
rt_bounds
,
edf_claimed_bounds
ts
=
Some
rt_bounds
>
(
tsk
,
R
)
\
in
rt_bounds
>
R
=
task_cost
tsk
+
div_floor
(
I
rt_bounds
tsk
R
)
num_cpus
.
R
=
rt_recurrence
tsk
rt_bounds
R
.
Proof
.
unfold
least_fixed_point
.
intros
tsk
R
rt_bounds
SOME
IN
.
have
CONV
:
=
edf_claimed_bounds_converges_helper
rt_bounds
.
have
CONV
:
=
edf_claimed_bounds_finds_fixed_point_of_list
rt_bounds
.
rewrite

iterS
in
CONV
;
fold
(
f
(
max_steps
ts
).+
1
)
in
CONV
.
unfold
edf_claimed_bounds
in
*
;
desf
.
exploit
(
CONV
)
;
[
by
done

by
done

intro
ITER
;
clear
CONV
].
unfold
f
in
ITER
.
...
...
@@ 824,7 +854,7 @@ Module ResponseTimeIterationEDF.
have
MAP
:
=
@
nth_map
_
(
tsk
,
0
)
_
_
(
update_bound
s
).
by
rewrite
MAP
//
EQ'
in
EQ
;
rewrite
EQ
.
Qed
.
End
Convergence
.
Section
MainProof
.
...
...
@@ 903,7 +933,7 @@ Module ResponseTimeIterationEDF.
(
task_deadline
:
=
task_deadline
)
(
job_deadline
:
=
job_deadline
)
(
job_task
:
=
job_task
)
(
ts
:
=
ts
)
(
tsk
:
=
tsk
)
(
rt_bounds
:
=
rt_bounds
)
;
try
(
by
ins
).
by
unfold
edf_claimed_bounds
in
SOME
;
desf
;
rewrite
edf_claimed_bounds_unzip1_iteration
.
by
ins
;
apply
edf_claimed_bounds_
converges
with
(
ts
:
=
ts
).
by
ins
;
apply
edf_claimed_bounds_
finds_fixed_point_for_each_bound
with
(
ts
:
=
ts
).
by
ins
;
rewrite
(
edf_claimed_bounds_le_deadline
ts
rt_bounds
).
Qed
.
...
...
analysis/jitter/bertogna_edf_comp.v
View file @
0b7ad51c
...
...
@@ 373,6 +373,15 @@ Module ResponseTimeIterationEDF.
by
simpl
in
EQtsk
;
rewrite

EQtsk
;
subst
;
apply
leq_addr
.
Qed
.
(* The application of the function is inductive. *)
Lemma
bertogna_edf_comp_iteration_inductive
(
P
:
seq
task_with_response_time
>
Type
)
:
P
(
initial_state
ts
)
>
(
forall
k
,
P
(
f
k
)
>
P
(
f
(
k
.+
1
)))
>
P
(
f
(
max_steps
ts
)).
Proof
.
by
intros
P0
Pn
;
induction
(
max_steps
ts
)
;
last
by
apply
Pn
.
Qed
.
(* As a last step, we show that edf_rta_iteration preserves order, i.e., for any
list l1 no smaller than the initial state, and list l2 such that
l1 <= l2, we have (edf_rta_iteration l1) <= (edf_rta_iteration l2). *)
...
...
@@ 492,7 +501,8 @@ Module ResponseTimeIterationEDF.
move
:
GE_COST
=>
/
allP
GE_COST
.
assert
(
LESUM
:
\
sum_
(
j
<
x1'

jldp_can_interfere_with
tsk_i
(
fst
j
))
interference_bound_edf
task_cost
task_period
task_deadline
task_jitter
tsk_i
delta
j
<=
\
sum_
(
j
<
x2'

jldp_can_interfere_with
tsk_i
(
fst
j
))
interference_bound_edf
task_cost
task_period
task_deadline
task_jitter
tsk_i
delta
j
<=
\
sum_
(
j
<
x2'

jldp_can_interfere_with
tsk_i
(
fst
j
))
interference_bound_edf
task_cost
task_period
task_deadline
task_jitter
tsk_i
delta'
j
).
{
set
elem
:
=
(
tsk0
,
R0
)
;
rewrite
2
!(
big_nth
elem
).
...
...
@@ 761,13 +771,13 @@ Module ResponseTimeIterationEDF.
End
DerivingContradiction
.
(* Using the lemmas above, we prove that edf_rta_iteration reaches
a fixed point
after (max_steps ts)
i
te
rations
, ... *)
Lemma
edf_claimed_bounds_
converges_helper
:
(* Using the lemmas above, we prove that edf_rta_iteration reaches
a fixed point
after (max_steps ts)
s
te
p
, ... *)
Lemma
edf_claimed_bounds_
finds_fixed_point_of_list
:
forall
rt_bounds
,
edf_claimed_bounds
ts
=
Some
rt_bounds
>
valid_sporadic_taskset
task_cost
task_period
task_deadline
ts
>
f
(
max_steps
ts
)
=
f
(
max_steps
ts
)
.+
1
.
f
(
max_steps
ts
)
=
edf_rta_iteration
(
f
(
max_steps
ts
)
)
.
Proof
.
intros
rt_bounds
SOME
VALID
.
unfold
valid_sporadic_taskset
,
is_valid_sporadic_task
in
*.
...
...
@@ 848,6 +858,58 @@ Module ResponseTimeIterationEDF.
by
apply
(
leq_ltn_trans
SUM
)
in
BUG
;
rewrite
ltnn
in
BUG
.
Qed
.
(* ...and since there cannot be a vector of responsetime bounds with values less than
the task costs, this solution is also the least fixed point. *)
Lemma
edf_claimed_bounds_finds_least_fixed_point
:
forall
v
,
all_le
(
initial_state
ts
)
v
>
v
=
edf_rta_iteration
v
>
all_le
(
f
(
max_steps
ts
))
v
.
Proof
.
intros
v
GE0
EQ
.
apply
bertogna_edf_comp_iteration_inductive
;
first
by
done
.
intros
k
GEk
.
rewrite
EQ
.
apply
bertogna_edf_comp_iteration_preserves_order
;
last
by
done
.
by
apply
bertogna_edf_comp_iteration_preserves_minimum
.
Qed
.
(* Therefore, with regard to the responsetime bound recurrence, ...*)
Let
rt_recurrence
(
tsk
:
sporadic_task
)
(
rt_bounds
:
seq
task_with_response_time
)
(
R
:
time
)
:
=
task_cost
tsk
+
div_floor
(
I
rt_bounds
tsk
R
)
num_cpus
.
(* ..., the individual responsetime bounds (elements of the list) are also fixed points. *)
Theorem
edf_claimed_bounds_finds_fixed_point_for_each_bound
:
forall
tsk
R
rt_bounds
,
edf_claimed_bounds
ts
=
Some
rt_bounds
>
(
tsk
,
R
)
\
in
rt_bounds
>
R
=
rt_recurrence
tsk
rt_bounds
R
.
Proof
.
unfold
least_fixed_point
.
intros
tsk
R
rt_bounds
SOME
IN
.
have
CONV
:
=
edf_claimed_bounds_finds_fixed_point_of_list
rt_bounds
.
rewrite

iterS
in
CONV
;
fold
(
f
(
max_steps
ts
).+
1
)
in
CONV
.
unfold
edf_claimed_bounds
in
*
;
desf
.
exploit
(
CONV
)
;
[
by
done

by
done

intro
ITER
;
clear
CONV
].
unfold
f
in
ITER
.
cut
(
update_bound
(
iter
(
max_steps
ts
)
edf_rta_iteration
(
initial_state
ts
))
(
tsk
,
R
)
=
(
tsk
,
R
)).
{
intros
EQ
.
have
F
:
=
@
f_equal
_
_
(
fun
x
=>
snd
x
)
_
(
tsk
,
R
).
by
apply
F
in
EQ
;
simpl
in
EQ
.
}
set
s
:
=
iter
(
max_steps
ts
)
edf_rta_iteration
(
initial_state
ts
).
fold
s
in
ITER
,
IN
.
move
:
IN
=>
/(
nthP
(
tsk
,
0
))
IN
;
destruct
IN
as
[
i
LT
EQ
].
generalize
EQ
;
rewrite
ITER
iterS
in
EQ
;
intro
EQ'
.
fold
s
in
EQ
.
unfold
edf_rta_iteration
in
EQ
.
have
MAP
:
=
@
nth_map
_
(
tsk
,
0
)
_
_
(
update_bound
s
).
by
rewrite
MAP
//
EQ'
in
EQ
;
rewrite
EQ
.
Qed
.
(* ..., which in turn implies that the responsetime bound is the fixed
point from Bertogna and Cirinei's equation. *)
Lemma
edf_claimed_bounds_converges
:
...
...
@@ 857,7 +919,8 @@ Module ResponseTimeIterationEDF.
R
=
task_cost
tsk
+
div_floor
(
I
rt_bounds
tsk
R
)
num_cpus
.
Proof
.
intros
tsk
R
rt_bounds
SOME
IN
.
have
CONV
:
=
edf_claimed_bounds_converges_helper
rt_bounds
.
have
CONV
:
=
edf_claimed_bounds_finds_fixed_point_of_list
rt_bounds
.
rewrite

iterS
in
CONV
;
fold
(
f
(
max_steps
ts
).+
1
)
in
CONV
.
unfold
edf_claimed_bounds
in
*
;
desf
.
exploit
(
CONV
)
;
[
by
done

by
done

intro
ITER
;
clear
CONV
].
unfold
f
in
ITER
.
...
...
@@ 962,7 +1025,7 @@ Module ResponseTimeIterationEDF.
(
task_deadline
:
=
task_deadline
)
(
job_deadline
:
=
job_deadline
)
(
job_jitter
:
=
job_jitter
)
(
job_task
:
=
job_task
)
(
ts
:
=
ts
)
(
tsk
:
=
tsk
)
(
rt_bounds
:
=
rt_bounds
)
;
try
(
by
ins
).
by
unfold
edf_claimed_bounds
in
SOME
;
desf
;
rewrite
edf_claimed_bounds_unzip1_iteration
.
by
ins
;
apply
edf_claimed_bounds_
converges
with
(
ts
:
=
ts
).
by
ins
;
apply
edf_claimed_bounds_
finds_fixed_point_for_each_bound
with
(
ts
:
=
ts
).
by
ins
;
rewrite
(
edf_claimed_bounds_le_deadline
ts
rt_bounds
).
Qed
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment