Skip to content
GitLab
Menu
Projects
Groups
Snippets
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
6c16aec6
Commit
6c16aec6
authored
Jan 10, 2016
by
Felipe Cerqueira
Browse files
Cleanup EDF theory file
parent
8e6384a4
Changes
3
Hide whitespace changes
Inline
Sidebyside
Makefile
View file @
6c16aec6
...
...
@@ 14,7 +14,7 @@
#
# This Makefile was generated by the command line :
# coq_makefile arrival_sequence.v bertogna_edf_comp.v bertogna_edf_theory.v bertogna_fp_comp.v bertogna_fp_jitter_comp.v bertogna_fp_jitter_theory.v bertogna_fp_theory.v extralib.v ExtraRelations.v guan_fp_comp.v guan_fp_theory.v interference.v job.v platform.v priority.v response_time.v schedulability.v schedule.v ssromega.v task_arrival.v task.v util_divround.v util_lemmas.v Vbase.v workload_bound.v workload_guan.v workload_jitter.v workload.v
# coq_makefile arrival_sequence.v bertogna_edf_comp.v bertogna_edf_theory.v bertogna_fp_comp.v bertogna_fp_jitter_comp.v bertogna_fp_jitter_theory.v bertogna_fp_theory.v extralib.v ExtraRelations.v guan_fp_comp.v guan_fp_theory.v
interference_bound_edf.v
interference.v job.v platform.v priority.v response_time.v schedulability.v schedule.v ssromega.v task_arrival.v task.v util_divround.v util_lemmas.v Vbase.v workload_bound.v workload_guan.v workload_jitter.v workload.v
#
.DEFAULT_GOAL
:=
all
...
...
@@ 91,6 +91,7 @@ VFILES:=arrival_sequence.v\
ExtraRelations.v
\
guan_fp_comp.v
\
guan_fp_theory.v
\
interference_bound_edf.v
\
interference.v
\
job.v
\
platform.v
\
...
...
bertogna_edf_theory.v
View file @
6c16aec6
...
...
@@ 264,7 +264,12 @@ Module ResponseTimeAnalysisEDF.
Lemma
bertogna_edf_specific_bound_holds
:
x
tsk_other
<=
edf_specific_bound
tsk_other
R_other
.
Proof
.
apply
interference_bound_edf_bounds_interference
.
apply
interference_bound_edf_bounds_interference
with
(
job_deadline0
:
=
job_deadline
)
(
ts0
:
=
ts
)
;
try
(
by
done
)
;
[
by
apply
bertogna_edf_tsk_other_in_ts

by
apply
H_tasks_miss_no_deadlines

by
apply
H_tasks_miss_no_deadlines

].
by
ins
;
apply
H_all_previous_jobs_completed_on_time
with
(
tsk_other
:
=
tsk_other
).
Qed
.
End
LemmasAboutInterferingTasks
.
...
...
@@ 647,14 +652,13 @@ Module ResponseTimeAnalysisEDF.
intro
EX
;
destruct
EX
as
[
tsk_other
[
R_other
[
HP
LTmin
]]].
unfold
interference_bound_edf
,
interference_bound_fp
in
LTmin
.
rewrite
minnAC
in
LTmin
;
apply
min_lt_same
in
LTmin
.
unfold
minn
in
LTmin
;
clear

LTmin
HP
BEFOREok
tsk
;
desf
.
have
BASICBOUND
:
=
bertogna_edf_workload_bounds_interference
R'
j
BEFOREok
tsk_other
R_other
HP
.
have
EDFBOUND
:
=
(
bertogna_edf_specific_bound_holds
tsk'
R'
INbounds
j
JOBtsk
BEFOREok
tsk_other
R_other
HP
).
unfold
minn
in
LTmin
;
clear

LTmin
HP
BASICBOUND
EDFBOUND
tsk
;
desf
.
{
exploit
(
bertogna_edf_workload_bounds_interference
R'
j
)
;
try
(
by
done
)
;
[
by
apply
HP

intro
BASICBOUND
].
by
apply
(
leq_ltn_trans
BASICBOUND
)
in
LTmin
;
rewrite
ltnn
in
LTmin
.
}
{
have
EDFBOUND
:
=
(
bertogna_edf_specific_bound_holds
tsk'
R'
j
tsk_other
R_other
).
by
apply
(
leq_ltn_trans
EDFBOUND
)
in
LTmin
;
rewrite
ltnn
in
LTmin
.
}
Qed
.
...
...
interference_bound_edf.v
View file @
6c16aec6
...
...
@@ 124,13 +124,17 @@ Module EDFSpecificBound.
Variable
j_i
:
JobIn
arr_seq
.
Hypothesis
H_job_of_tsk_i
:
job_task
j_i
=
tsk_i
.
(* Let tsk_k denote any interfering task,
and R_k its responsetime bound
. *)
(* Let tsk_k denote any interfering task,
..
. *)
Variable
tsk_k
:
sporadic_task
.
Hypothesis
H_tsk_k_in_task_set
:
tsk_k
\
in
ts
.
(* ...and R_k its responsetime bound. *)
Variable
R_k
:
time
.
Hypothesis
H_R_k_le_deadline
:
R_k
<=
task_deadline
tsk_k
.
(* Consider a time window of length delta, starting with j_i's arrival time. *)
(* Consider a time window of length delta
<= D_i
, starting with j_i's arrival time. *)
Variable
delta
:
time
.
Hypothesis
H_delta_le_deadline
:
delta
<=
task_deadline
tsk_i
.
(* Assume that the jobs of tsk_k satisfy the responsetime bound before the end of the interval *)
Hypothesis
H_all_previous_jobs_completed_on_time
:
...
...
@@ 159,7 +163,6 @@ Module EDFSpecificBound.
Let
D_k
:
=
task_deadline
tsk_k
.
Let
p_k
:
=
task_period
tsk_k
.
Print
edf_specific_interference_bound
.
Let
n_k
:
=
div_floor
D_i
p_k
.
(* Identify the subset of jobs that actually cause interference *)
...
...
@@ 262,12 +265,13 @@ Module EDFSpecificBound.
End
SimplifyJobSequence
.
(* Next, we prove some facts relating job deadlines and interference under EDF.*)
Section
FactsAboutEDF
.
(* Under EDF scheduling, a job only causes interference if its deadline
is not larger than the deadline of the analyzed job.
TODO:
this should
be in the interference.v file
.
*)
Lemma
interference_under_edf_implies_shorter_deadline
:
TODO:
Should this
be in the interference.v file
?
*)
Lemma
interference_under_edf_implies_shorter_deadline
s
:
forall
(
j
j'
:
JobIn
arr_seq
)
t1
t2
,
job_interference
job_cost
rate
sched
j'
j
t1
t2
!=
0
>
job_arrival
j
+
job_deadline
j
<=
job_arrival
j'
+
job_deadline
j'
.
...
...
@@ 337,42 +341,66 @@ Module EDFSpecificBound.
Variable
elem
:
JobIn
arr_seq
.
Let
j_fst
:
=
nth
elem
sorted_jobs
0
.
Let
a_fst
:
=
job_arrival
j_fst
.
(* The first job is an interfering job of task tsk_k. *)
Lemma
interference_bound_edf_j_fst_is_job_of_tsk_k
:
job_task
j_fst
=
tsk_k
/\
interference_caused_by
j_fst
t1
t2
!=
0
/\
j_fst
\
in
jobs_scheduled_between
sched
t1
t2
.
Proof
.
by
apply
interference_bound_edf_all_jobs_from_tsk_k
,
mem_nth
,
interference_bound_edf_at_least_one_job
.
Qed
.
(* The deadline of j_fst is the deadline of tsk_k. *)
Lemma
interference_bound_edf_j_fst_deadline
:
job_deadline
j_fst
=
task_deadline
tsk_k
.
Proof
.
unfold
valid_sporadic_job
in
*.
rename
H_valid_job_parameters
into
PARAMS
.
have
FST
:
=
interference_bound_edf_j_fst_is_job_of_tsk_k
.
destruct
FST
as
[
FSTtask
_
].
by
specialize
(
PARAMS
j_fst
)
;
des
;
rewrite
PARAMS1
FSTtask
.
Qed
.
(* In this section, we prove some basic lemmas about j_fst. *)
Section
FactsAboutFirstJob
.
(* The first job is an interfering job of task tsk_k. *)
Lemma
interference_bound_edf_j_fst_is_job_of_tsk_k
:
job_task
j_fst
=
tsk_k
/\
interference_caused_by
j_fst
t1
t2
!=
0
/\
j_fst
\
in
jobs_scheduled_between
sched
t1
t2
.
Proof
.
by
apply
interference_bound_edf_all_jobs_from_tsk_k
,
mem_nth
,
interference_bound_edf_at_least_one_job
.
Qed
.
(* The deadline of j_i is the deadline of tsk_i. *)
Lemma
interference_bound_edf_j_i_deadline
:
job_deadline
j_i
=
task_deadline
tsk_i
.
Proof
.
unfold
valid_sporadic_job
in
*.
rename
H_valid_job_parameters
into
PARAMS
,
H_job_of_tsk_i
into
JOBtsk
.
by
specialize
(
PARAMS
j_i
)
;
des
;
rewrite
PARAMS1
JOBtsk
.
Qed
.
(* The deadline of j_fst is the deadline of tsk_k. *)
Lemma
interference_bound_edf_j_fst_deadline
:
job_deadline
j_fst
=
task_deadline
tsk_k
.
Proof
.
unfold
valid_sporadic_job
in
*.
rename
H_valid_job_parameters
into
PARAMS
.
have
FST
:
=
interference_bound_edf_j_fst_is_job_of_tsk_k
.
destruct
FST
as
[
FSTtask
_
].
by
specialize
(
PARAMS
j_fst
)
;
des
;
rewrite
PARAMS1
FSTtask
.
Qed
.
(* The deadline of j_i is the deadline of tsk_i. *)
Lemma
interference_bound_edf_j_i_deadline
:
job_deadline
j_i
=
task_deadline
tsk_i
.
Proof
.
unfold
valid_sporadic_job
in
*.
rename
H_valid_job_parameters
into
PARAMS
,
H_job_of_tsk_i
into
JOBtsk
.
by
specialize
(
PARAMS
j_i
)
;
des
;
rewrite
PARAMS1
JOBtsk
.
Qed
.
(* If j_fst completes by its responsetime bound, then t1 <= a_fst + R_k,
where t1 is the beginning of the time window (arrival of j_i). *)
Lemma
interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
:
completed
job_cost
rate
sched
j_fst
(
a_fst
+
R_k
)
>
t1
<=
a_fst
+
R_k
.
Proof
.
rename
H_rate_equals_one
into
RATE
.
intros
RBOUND
.
rewrite
leqNgt
;
apply
/
negP
;
unfold
not
;
intro
BUG
.
have
FST
:
=
interference_bound_edf_j_fst_is_job_of_tsk_k
.
destruct
FST
as
[
_
[
FSTserv
_
]].
move
:
FSTserv
=>
/
negP
FSTserv
;
apply
FSTserv
.
rewrite

leqn0
;
apply
leq_trans
with
(
n
:
=
service_during
rate
sched
j_fst
t1
t2
)
;
first
by
apply
job_interference_le_service
;
ins
;
rewrite
RATE
.
rewrite
leqn0
;
apply
/
eqP
.
by
apply
cumulative_service_after_job_rt_zero
with
(
job_cost0
:
=
job_cost
)
(
R
:
=
R_k
)
;
try
(
by
done
)
;
apply
ltnW
.
Qed
.
End
FactsAboutFirstJob
.
(* Now, let's prove the interference bound for the particular case with a single job.
This case must be dealt with separately because the single job can be both
carryin and carryout at the same time, so its response time
may
not
be
bounded by R_k (from the hypothesis H_all_previous_jobs_completed_on_time). *)
carryin and carryout at the same time, so its response time
is
not
necessarily
bounded by R_k (from the hypothesis H_all_previous_jobs_completed_on_time). *)
Section
InterferenceSingleJob
.
(* Assume that there's at least one job in the sorted list. *)
...
...
@@ 395,126 +423,218 @@ Module EDFSpecificBound.
by
rewrite

ltnNge
in
EQnk
;
rewrite
modn_small
//.
Qed
.
(*rewrite mul0n add0n big_nat_recl // big_geq // addn0; fold j_fst.
rewrite leq_min; apply/andP; split;
first by apply LTserv; rewrite INboth; apply/(nthP elem); exists 0; rewrite ?SIZE.*)
(* If j_fst completes by its responsetime bound, then t1 <= a_fst + R_k,
where t1 is the beginning of the time window (arrival of j_i). *)
Lemma
interference_bound_edf_j_fst_completes_on_time_implies_response_time_inside_interval
:
completed
job_cost
rate
sched
j_fst
(
a_fst
+
R_k
)
>
t1
<=
a_fst
+
R_k
.
Proof
.
rename
H_rate_equals_one
into
RATE
.
intros
RBOUND
.
rewrite
leqNgt
;
apply
/
negP
;
unfold
not
;
intro
BUG
.
have
FST
:
=
interference_bound_edf_j_fst_is_job_of_tsk_k
.
destruct
FST
as
[
_
[
FSTserv
_
]].
move
:
FSTserv
=>
/
negP
FSTserv
;
apply
FSTserv
.
rewrite

leqn0
;
apply
leq_trans
with
(
n
:
=
service_during
rate
sched
j_fst
t1
t2
)
;
first
by
apply
job_interference_le_service
;
ins
;
rewrite
RATE
.
rewrite
leqn0
;
apply
/
eqP
.
by
apply
cumulative_service_after_job_rt_zero
with
(
job_cost0
:
=
job_cost
)
(
R
:
=
R_k
)
;
try
(
by
done
)
;
apply
ltnW
.
Qed
.
Lemma
interference_bound_edf_holds_for_a_single_job
:
interference_caused_by
j_fst
t1
t2
<=
interference_bound
.
Proof
.
unfold
interference_caused_by
.
admit
.
Qed
.
(*assert (COMPok: completed job_cost rate sched j_fst (a_fst + R_k) > job_interference job_cost rate sched j_i j_fst t1 t2 <= D_i  (D_k  R_k)).
{
intros RBOUND.
apply PRIOinterf in FSTserv; rename FSTserv into LEdl.
(* Next, we show that if j_fst completes by its responsetime bound R_k,
then then interference bound holds. *)
Section
ResponseTimeOfSingleJobBounded
.
destruct (D_k  R_k <= D_i) eqn:LEdk; last first.
{
apply negbT in LEdk; rewrite ltnNge in LEdk.
apply leq_trans with (n := 0); last by done.
apply leq_trans with (n := job_interference job_cost rate sched j_i j_fst
(a_fst + R_k) t2).
{
apply extend_sum; last by apply leqnn.
rewrite (leq_add2r D_i).
rewrite DLi DLfst in LEdl.
apply leq_trans with (n := a_fst + D_k); last by done.
rewrite addnA leq_add2l.
by apply ltnW; rewrite ltn_subRL.
}
apply leq_trans with (n := service_during rate sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service; ins; rewrite RATE.
unfold service_during.
by rewrite > cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
try (by done); apply leqnn.
}
{
rewrite (leq_add2r (D_k  R_k)) subh1 // addnBA // subnn addn0.
assert (SUBST: D_k  R_k = \sum_(a_fst + R_k <= i < a_fst + D_k) 1).
{
rewrite big_const_nat iter_addn mul1n addn0.
rewrite addnC subnBA; last by apply leq_addr.
by rewrite addnC addnBA // subnn addn0.
}
apply leq_trans with (n := job_interference job_cost rate sched j_i j_fst t1
(a_fst + D_k) + (D_k  R_k)).
{
rewrite leq_add2r.
destruct (t2 <= a_fst + R_k) eqn:LEt2.
Hypothesis
H_j_fst_completed_by_rt_bound
:
completed
job_cost
rate
sched
j_fst
(
a_fst
+
R_k
).
Lemma
interference_bound_edf_holds_for_single_job_that_completes_on_time
:
job_interference
job_cost
rate
sched
j_i
j_fst
t1
t2
<=
D_i

(
D_k

R_k
).
Proof
.
rename
H_j_fst_completed_by_rt_bound
into
RBOUND
.
have
AFTERt1
:
=
interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
RBOUND
.
have
FST
:
=
interference_bound_edf_j_fst_is_job_of_tsk_k
.
destruct
FST
as
[
_
[
LEdl
_
]].
apply
interference_under_edf_implies_shorter_deadlines
in
LEdl
.
destruct
(
D_k

R_k
<=
D_i
)
eqn
:
LEdk
;
last
first
.
{
apply extend_sum; first by apply leqnn.
apply leq_trans with (n := a_fst + R_k); first by done.
by rewrite leq_add2l; apply NOMISS.
apply
negbT
in
LEdk
;
rewrite

ltnNge
in
LEdk
.
apply
leq_trans
with
(
n
:
=
0
)
;
last
by
done
.
apply
leq_trans
with
(
n
:
=
job_interference
job_cost
rate
sched
j_i
j_fst
(
a_fst
+
R_k
)
t2
).
{
apply
extend_sum
;
last
by
apply
leqnn
.
rewrite
(
leq_add2r
D_i
).
rewrite
interference_bound_edf_j_fst_deadline
interference_bound_edf_j_i_deadline
in
LEdl
.
apply
leq_trans
with
(
n
:
=
a_fst
+
D_k
)
;
last
by
done
.
rewrite

addnA
leq_add2l
.
by
apply
ltnW
;
rewrite

ltn_subRL
.
}
apply
leq_trans
with
(
n
:
=
service_during
rate
sched
j_fst
(
a_fst
+
R_k
)
t2
)
;
first
by
apply
job_interference_le_service
;
ins
;
rewrite
H_rate_equals_one
.
unfold
service_during
;
rewrite
leqn0
;
apply
/
eqP
.
by
apply
cumulative_service_after_job_rt_zero
with
(
job_cost0
:
=
job_cost
)
(
R
:
=
R_k
)
;
try
(
by
done
)
;
apply
leqnn
.
}
{
rewrite
(
leq_add2r
(
D_k

R_k
))
subh1
//

addnBA
//
subnn
addn0
.
assert
(
SUBST
:
D_k

R_k
=
\
sum_
(
a_fst
+
R_k
<=
i
<
a_fst
+
D_k
)
1
).
{
rewrite
big_const_nat
iter_addn
mul1n
addn0
.
rewrite
addnC

subnBA
;
last
by
apply
leq_addr
.
by
rewrite
addnC

addnBA
//
subnn
addn0
.
}
apply
leq_trans
with
(
n
:
=
job_interference
job_cost
rate
sched
j_i
j_fst
t1
(
a_fst
+
D_k
)
+
(
D_k

R_k
)).
{
rewrite
leq_add2r
.
destruct
(
t2
<=
a_fst
+
R_k
)
eqn
:
LEt2
.
{
apply
extend_sum
;
first
by
apply
leqnn
.
apply
leq_trans
with
(
n
:
=
a_fst
+
R_k
)
;
first
by
done
.
by
rewrite
leq_add2l
;
apply
H_R_k_le_deadline
.
}
{
unfold
job_interference
.
apply
negbT
in
LEt2
;
rewrite

ltnNge
in
LEt2
.
rewrite
>
big_cat_nat
with
(
n
:
=
a_fst
+
R_k
)
;
[
simpl

by
apply
AFTERt1

by
apply
ltnW
].
apply
leq_trans
with
(
n
:
=
job_interference
job_cost
rate
sched
j_i
j_fst
t1
(
a_fst
+
R_k
)
+
service_during
rate
sched
j_fst
(
a_fst
+
R_k
)
t2
).
{
rewrite
leq_add2l
.
by
apply
job_interference_le_service
;
ins
;
rewrite
H_rate_equals_one
.
}
unfold
service_during
.
rewrite
>
cumulative_service_after_job_rt_zero
with
(
job_cost0
:
=
job_cost
)
(
R
:
=
R_k
)
;
try
(
by
done
)
;
last
by
apply
leqnn
.
rewrite
addn0
;
apply
extend_sum
;
first
by
apply
leqnn
.
by
rewrite
leq_add2l
;
apply
H_R_k_le_deadline
.
}
}
unfold
job_interference
.
apply negbT in LEt2; rewrite ltnNge in LEt2.
rewrite
>
big_cat_nat
with
(
n
:
=
a_fst
+
R_k
)
;
[simpl
 by apply AFTERt1  by
apply ltnW
].
[
simpl

by
apply
AFTERt1

by
rewrite
leq_add2l
;
apply
H_R_k_le_deadline
].
apply
leq_trans
with
(
n
:
=
job_interference
job_cost
rate
sched
j_i
j_fst
t1
(a_fst + R_k)
+ service_during rate sched j_fst (a_fst + R_k) t2).
(
a_fst
+
R_k
)
+
service_during
rate
sched
j_fst
(
a_fst
+
R_k
)
(
a_fst
+
D_k
)
+
(
D_k

R_k
)).
{
rewrite leq_add2l.
by apply job_interference_le_service; ins; rewrite
RATE
.
rewrite
leq_add2r
leq_add2l
.
by
apply
job_interference_le_service
;
ins
;
rewrite
H_rate_equals_one
.
}
unfold
service_during
.
rewrite > cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R
:=
R_k);
rewrite
>
cumulative_service_after_job_rt_zero
with
(
job_cost0
:
=
job_cost
)
(
R
:
=
R_k
)
;
try
(
by
done
)
;
last
by
apply
leqnn
.
rewrite addn0; apply extend_sum; first by apply leqnn.
by rewrite leq_add2l; apply NOMISS.
rewrite
addn0
.
apply
leq_trans
with
(
n
:
=
(
\
sum_
(
t1
<=
t
<
a_fst
+
R_k
)
1
)
+
\
sum_
(
a_fst
+
R_k
<=
t
<
a_fst
+
D_k
)
1
).
{
apply
leq_add
;
last
by
rewrite
SUBST
.
by
unfold
job_interference
;
apply
leq_sum
;
ins
;
apply
leq_b1
.
}
rewrite

big_cat_nat
;
[
simpl

by
apply
AFTERt1

by
rewrite
leq_add2l
;
apply
H_R_k_le_deadline
].
rewrite
big_const_nat
iter_addn
mul1n
addn0
leq_subLR
.
by
unfold
D_i
,
D_k
,
t1
,
a_fst
;
rewrite

interference_bound_edf_j_fst_deadline

interference_bound_edf_j_i_deadline
.
}
Qed
.
End
ResponseTimeOfSingleJobBounded
.
(* Else, if j_fst did not complete by its responsetime bound, then
we need a separate proof. *)
Section
ResponseTimeOfSingleJobNotBounded
.
Hypothesis
H_j_fst_not_complete_by_rt_bound
:
~~
completed
job_cost
rate
sched
j_fst
(
a_fst
+
R_k
).
(* This of course implies that a_fst + R_k lies after the end of the interval,
otherwise j_fst would have completed by its responsetime bound. *)
Lemma
interference_bound_edf_response_time_bound_of_j_fst_after_interval
:
job_arrival
j_fst
+
R_k
>=
job_arrival
j_i
+
delta
.
Proof
.
have
FST
:
=
interference_bound_edf_j_fst_is_job_of_tsk_k
.
destruct
FST
as
[
FSTtask
_
].
rewrite
leqNgt
;
apply
/
negP
;
intro
LT
.
move
:
H_j_fst_not_complete_by_rt_bound
=>
/
negP
BUG
;
apply
BUG
.
by
apply
H_all_previous_jobs_completed_on_time
.
Qed
.
(* If the slack is too big (D_i < D_k  R_k), j_fst causes no interference. *)
Lemma
interference_bound_edf_holds_for_single_job_with_big_slack
:
D_i
<
D_k

R_k
>
interference_caused_by
j_fst
t1
t2
=
0
.
Proof
.
intro
LTdk
.
rewrite
ltn_subRL
in
LTdk
.
rewrite
(
ltn_add2l
a_fst
)
addnA
in
LTdk
.
apply
leq_ltn_trans
with
(
m
:
=
t1
+
D_i
)
in
LTdk
;
last
first
.
{
rewrite
leq_add2r
.
apply
leq_trans
with
(
n
:
=
t1
+
delta
)
;
first
by
apply
leq_addr
.
by
apply
interference_bound_edf_response_time_bound_of_j_fst_after_interval
.
}
}
apply
/
eqP
;
rewrite
[
_
_
_
_
==
0
]
negbK
;
apply
/
negP
;
red
;
intro
BUG
.
apply
interference_under_edf_implies_shorter_deadlines
in
BUG
.
rewrite
interference_bound_edf_j_fst_deadline
interference_bound_edf_j_i_deadline
in
BUG
.
by
apply
(
leq_trans
LTdk
)
in
BUG
;
rewrite
ltnn
in
BUG
.
Qed
.
(* Else, if the slack is small, j_fst causes interference no longer than
D_i  (D_k  R_k). *)
Lemma
interference_bound_edf_holds_for_single_job_with_small_slack
:
D_i
>=
D_k

R_k
>
interference_caused_by
j_fst
t1
t2
<=
D_i

(
D_k

R_k
).
Proof
.
intro
LEdk
.
have
FST
:
=
interference_bound_edf_j_fst_is_job_of_tsk_k
.
destruct
FST
as
[
FSTtask
[
LEdl
_
]].
have
LTr
:
=
interference_bound_edf_response_time_bound_of_j_fst_after_interval
.
apply
subh3
;
last
by
apply
LEdk
.
apply
leq_trans
with
(
n
:
=
job_interference
job_cost
rate
sched
j_i
j_fst
t1
(
job_arrival
j_fst
+
R_k
)
+
(
D_k

R_k
))
;
first
by
rewrite
leq_add2r
;
apply
extend_sum
;
[
by
apply
leqnn
].
apply
leq_trans
with
(
n
:
=
\
sum_
(
t1
<=
t
<
a_fst
+
R_k
)
1
+
\
sum_
(
a_fst
+
R_k
<=
t
<
a_fst
+
D_k
)
1
).
{
apply
leq_add
;
unfold
job_interference
;
first
by
apply
leq_sum
;
ins
;
apply
leq_b1
.
rewrite
big_const_nat
iter_addn
mul1n
addn0
addnC
.
rewrite

subnBA
;
last
by
apply
leq_addr
.
by
rewrite
addnC

addnBA
//
subnn
addn0
.
}
rewrite

big_cat_nat
;
simpl
;
last
2
first
.
{
apply
leq_trans
with
(
n
:
=
t1
+
delta
)
;
first
by
apply
leq_addr
.
by
apply
interference_bound_edf_response_time_bound_of_j_fst_after_interval
.
}
by
rewrite
leq_add2l
;
apply
H_R_k_le_deadline
.
rewrite
big_const_nat
iter_addn
mul1n
addn0
leq_subLR
.
unfold
D_i
,
D_k
,
t1
,
a_fst
;
rewrite

interference_bound_edf_j_fst_deadline

interference_bound_edf_j_i_deadline
.
by
apply
interference_under_edf_implies_shorter_deadlines
in
LEdl
.
Qed
.
End
ResponseTimeOfSingleJobNotBounded
.
(* Finally, we prove that the interference caused by the single job
is bounded by D_i  (D_k  R_k). *)
Lemma
interference_bound_edf_interference_of_j_fst_limited_by_slack
:
interference_caused_by
j_fst
t1
t2
<=
D_i

(
D_k

R_k
).
Proof
.
destruct
(
completed
job_cost
rate
sched
j_fst
(
a_fst
+
R_k
))
eqn
:
COMP
;
first
by
apply
interference_bound_edf_holds_for_single_job_that_completes_on_time
.
apply
negbT
in
COMP
.
destruct
(
ltnP
D_i
(
D_k

R_k
))
as
[
LEdk

LTdk
].
by
rewrite
interference_bound_edf_holds_for_single_job_with_big_slack
.
by
apply
interference_bound_edf_holds_for_single_job_with_small_slack
.
Qed
.
unfold job_interference.
rewrite > big_cat_nat with (n := a_fst + R_k);
[simplby apply AFTERt1  by rewrite leq_add2l; apply NOMISS].
apply leq_trans with (n := job_interference job_cost rate sched j_i j_fst t1 (a_fst + R_k)
+ service_during rate sched j_fst (a_fst + R_k) (a_fst + D_k)
+ (D_k  R_k)).
{
rewrite leq_add2r leq_add2l.
by apply job_interference_le_service; ins; rewrite RATE.
}
unfold service_during.
rewrite > cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
try (by done); last by apply leqnn.
rewrite addn0.
apply leq_trans with (n := (\sum_(t1 <= t < a_fst + R_k) 1) +
\sum_(a_fst + R_k <= t < a_fst + D_k) 1).
Lemma
interference_bound_edf_holds_for_a_single_job
:
interference_caused_by
j_fst
t1
t2
<=
interference_bound
.
Proof
.
rename
H_many_jobs
into
NUM
,
H_only_one_job
into
SIZE
.
unfold
interference_caused_by
,
interference_bound
,
edf_specific_interference_bound
.
fold
D_i
D_k
p_k
n_k
.
rewrite
SIZE
ltnS
leqn0
in
NUM
;
move
:
NUM
=>
/
eqP
EQnk
.
rewrite
EQnk
mul0n
add0n
.
rewrite
leq_min
;
apply
/
andP
;
split
.
{
apply leq_add; last by rewrite SUBST.
by unfold job_interference; apply leq_sum; ins; apply leq_b1.
apply
interference_bound_edf_interference_le_task_cost
.
rewrite
interference_bound_edf_job_in_same_sequence
.
by
apply
mem_nth
;
rewrite
SIZE
.
}
rewrite big_cat_nat;
[simpl  by apply AFTERt1  by rewrite leq_add2l; apply NOMISS ].
rewrite big_const_nat iter_addn mul1n addn0 leq_subLR.
by unfold D_k, D_i, t2; rewrite DLfst DLi; apply LEdl.
}
}*)
rewrite
interference_bound_edf_simpl_when_there's_one_job
.
by
apply
interference_bound_edf_interference_of_j_fst_limited_by_slack
.
Qed
.
End
InterferenceSingleJob
.
(* Next, consider the last case where there are at least two jobs:
...
...
@@ 524,60 +644,159 @@ Module EDFSpecificBound.
(* Assume there are at least two jobs. *)
Variable
num_mid_jobs
:
nat
.
Hypothesis
H_at_least_two_jobs
:
size
sorted_jobs
=
num_mid_jobs
.+
2
.
Let
j_lst
:
=
nth
elem
sorted_jobs
num_mid_jobs
.+
1
.
(* The last job is an interfering job of task tsk_k. *)
Lemma
interference_bound_edf_j_lst_is_job_of_tsk_k
:
job_task
j_lst
=
tsk_k
/\
interference_caused_by
j_lst
t1
t2
!=
0
/\
j_lst
\
in
jobs_scheduled_between
sched
t1
t2
.
(* Let j_lst be the last job of the sequence and a_lst its arrival time. *)
Let
j_lst
:
=
nth
elem
sorted_jobs
num_mid_jobs
.+
1
.
Let
a_lst
:
=
job_arrival
j_lst
.
(* In this section, we prove some basic lemmas about the first and last jobs. *)
Section
FactsAboutFirstAndLastJobs
.
(* The last job is an interfering job of task tsk_k. *)
Lemma
interference_bound_edf_j_lst_is_job_of_tsk_k
:
job_task
j_lst
=
tsk_k
/\
interference_caused_by
j_lst
t1
t2
!=
0
/\
j_lst
\
in
jobs_scheduled_between
sched
t1
t2
.
Proof
.
apply
interference_bound_edf_all_jobs_from_tsk_k
,
mem_nth
.
by
rewrite
H_at_least_two_jobs
.
Qed
.
(* The deadline of j_lst is the deadline of tsk_k. *)
Lemma
interference_bound_edf_j_lst_deadline
:
job_deadline
j_lst
=
task_deadline
tsk_k
.
Proof
.
unfold
valid_sporadic_job
in
*.
rename
H_valid_job_parameters
into
PARAMS
.
have
LST
:
=
interference_bound_edf_j_lst_is_job_of_tsk_k
.
destruct
LST
as
[
LSTtask
_
].
by
specialize
(
PARAMS
j_lst
)
;
des
;
rewrite
PARAMS1
LSTtask
.
Qed
.
(* The first job arrives before the last job. *)
Lemma
interference_bound_edf_j_fst_before_j_lst
:
job_arrival
j_fst
<=
job_arrival
j_lst
.
Proof
.
rename
H_at_least_two_jobs
into
SIZE
.
unfold
j_fst
,
j_lst
;
rewrite
[
num_mid_jobs
.+
1
]
add0n
.
apply
prev_le_next
;
last
by
rewrite
SIZE
leqnn
.
by
intros
i
LT
;
apply
interference_bound_edf_jobs_ordered_by_arrival
.
Qed
.
(* The last job arrives before the end of the interval. *)
Lemma
interference_bound_edf_last_job_arrives_before_end_of_interval
:
job_arrival
j_lst
<
t2
.
Proof
.
rename
H_rate_equals_one
into
RATE
.
rewrite
leqNgt
;
apply
/
negP
;
unfold
not
;
intro
LT2
.
exploit
interference_bound_edf_all_jobs_from_tsk_k
.
{
apply
mem_nth
;
instantiate
(
1
:
=
num_mid_jobs
.+
1
).
by
rewrite
(
ltn_add2r
1
)
addn1
H_at_least_two_jobs
addn1
.
}
instantiate
(
1
:
=
elem
)
;
move
=>
[
LSTtsk
[/
eqP
LSTserv
LSTin
]].
apply
LSTserv
;
apply
/
eqP
;
rewrite

leqn0
.