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
Felipe Cerqueira
rtproofs
Commits
0582d634
Commit
0582d634
authored
Jan 13, 2016
by
Felipe Cerqueira
Browse files
Broken: still removing rate
parent
02b83aea
Changes
9
Hide whitespace changes
Inline
Sidebyside
Showing
9 changed files
with
220 additions
and
248 deletions
+220
248
bertogna_fp_theory.v
bertogna_fp_theory.v
+30
37
interference.v
interference.v
+24
38
interference_bound_edf.v
interference_bound_edf.v
+15
18
platform.v
platform.v
+5
6
response_time.v
response_time.v
+9
11
schedulability.v
schedulability.v
+11
14
schedule.v
schedule.v
+54
45
workload.v
workload.v
+34
33
workload_bound.v
workload_bound.v
+38
46
No files found.
bertogna_fp_theory.v
View file @
0582d634
...
...
@@ 80,7 +80,6 @@ Module ResponseTimeAnalysisFP.
(
*
Consider
any
schedule
such
that
...
*
)
Variable
num_cpus
:
nat
.
Variable
rate
:
Job
>
processor
num_cpus
>
nat
.
Variable
sched
:
schedule
num_cpus
arr_seq
.
(
*
...
jobs
do
not
execute
before
their
arrival
times
nor
longer
...
...
@@ 88,14 +87,12 @@ Module ResponseTimeAnalysisFP.
Hypothesis
H_jobs_must_arrive_to_execute
:
jobs_must_arrive_to_execute
sched
.
Hypothesis
H_completed_jobs_dont_execute
:
completed_jobs_dont_execute
job_cost
rate
sched
.
completed_jobs_dont_execute
job_cost
sched
.
(
*
Also
assume
that
jobs
do
not
execute
in
parallel
,
processors
have
unit
speed
,
and
that
there
exists
at
least
one
processor
.
*
)
(
*
Also
assume
that
jobs
do
not
execute
in
parallel
and
that
there
exists
at
least
one
processor
.
*
)
Hypothesis
H_no_parallelism
:
jobs_dont_execute_in_parallel
sched
.
Hypothesis
H_rate_equals_one
:
forall
j
cpu
,
rate
j
cpu
=
1.
Hypothesis
H_at_least_one_cpu
:
num_cpus
>
0.
...
...
@@ 112,9 +109,9 @@ Module ResponseTimeAnalysisFP.
Hypothesis
task_in_ts
:
tsk
\
in
ts
.
Let
no_deadline_is_missed_by_tsk
(
tsk
:
sporadic_task
)
:=
task_misses_no_deadline
job_cost
job_deadline
job_task
rate
sched
tsk
.
task_misses_no_deadline
job_cost
job_deadline
job_task
sched
tsk
.
Let
is_response_time_bound
(
tsk
:
sporadic_task
)
:=
is_response_time_bound_of_task
job_cost
job_task
tsk
rate
sched
.
is_response_time_bound_of_task
job_cost
job_task
tsk
sched
.
(
*
Assume
a
known
response

time
bound
for
any
interfering
task
*
)
Let
task_with_response_time
:=
(
sporadic_task
*
time
)
%
type
.
...
...
@@ 133,7 +130,7 @@ Module ResponseTimeAnalysisFP.
Hypothesis
H_response_time_of_interfering_tasks_is_known
:
forall
hp_tsk
R
,
(
hp_tsk
,
R
)
\
in
hp_bounds
>
is_response_time_bound_of_task
job_cost
job_task
hp_tsk
rate
sched
R
.
is_response_time_bound_of_task
job_cost
job_task
hp_tsk
sched
R
.
(
*
Assume
that
the
response

time
bounds
are
larger
than
task
costs
.
*
)
Hypothesis
H_response_time_bounds_ge_cost
:
...
...
@@ 151,7 +148,7 @@ Module ResponseTimeAnalysisFP.
the
processors
must
be
busy
with
jobs
of
equal
or
higher
priority
.
*
)
Hypothesis
H_global_scheduling_invariant
:
FP_scheduling_invariant_holds
job_cost
job_task
num_cpus
rate
sched
ts
higher_eq_priority
.
FP_scheduling_invariant_holds
job_cost
job_task
num_cpus
sched
ts
higher_eq_priority
.
(
*
Let
R
be
the
fixed
point
of
Bertogna
and
Cirinei
'
s
recurrence
,
...
*
)
Variable
R
:
time
.
...
...
@@ 173,15 +170,15 @@ Module ResponseTimeAnalysisFP.
Hypothesis
H_job_of_tsk
:
job_task
j
=
tsk
.
(
*
Assume
that
job
j
hasn
'
t
completed
by
the
response
time
bound
.
*
)
Hypothesis
H_j_not_completed
:
~~
completed
job_cost
rate
sched
j
(
job_arrival
j
+
R
).
Hypothesis
H_j_not_completed
:
~~
completed
job_cost
sched
j
(
job_arrival
j
+
R
).
(
*
Let
'
s
call
x
the
interference
incurred
by
job
j
due
to
tsk_other
,
...
*
)
Let
x
(
tsk_other
:
sporadic_task
)
:=
task_interference
job_cost
job_task
rate
sched
j
task_interference
job_cost
job_task
sched
j
tsk_other
(
job_arrival
j
)
(
job_arrival
j
+
R
).
(
*
and
X
the
total
interference
incurred
by
job
j
due
to
any
task
.
*
)
Let
X
:=
total_interference
job_cost
rate
sched
j
(
job_arrival
j
)
(
job_arrival
j
+
R
).
Let
X
:=
total_interference
job_cost
sched
j
(
job_arrival
j
)
(
job_arrival
j
+
R
).
(
*
Recall
Bertogna
and
Cirinei
'
s
workload
bound
.
*
)
Let
workload_bound
(
tsk_other
:
sporadic_task
)
(
R_other
:
time
)
:=
...
...
@@ 234,27 +231,24 @@ Module ResponseTimeAnalysisFP.
H_restricted_deadlines
into
RESTR
,
H_response_time_of_interfering_tasks_is_known
into
RESP
,
H_interfering_tasks_miss_no_deadlines
into
NOMISS
,
H_rate_equals_one
into
RATE
,
H_response_time_bounds_ge_cost
into
GE_COST
.
unfold
x
,
workload_bound
.
have
INts
:=
bertogna_fp_tsk_other_in_ts
.
apply
leq_trans
with
(
n
:=
workload
job_task
rate
sched
tsk_other
apply
leq_trans
with
(
n
:=
workload
job_task
sched
tsk_other
(
job_arrival
j
)
(
job_arrival
j
+
R
));
first
by
apply
task_interference_le_workload
;
ins
;
rewrite
RATE
.
{
apply
workload_bounded_by_W
with
(
task
_deadline0
:=
task
_deadline
)
(
job_cost0
:=
job_cost
)
(
job_deadline0
:=
job_deadline
);
try
(
by
ins
);
last
2
first
;
first
by
apply
task_interference_le_workload
.
apply
workload_bounded_by_W
with
(
task_deadline0
:=
task_deadline
)
(
job_cost0
:=
job_cost
)
(
job
_deadline0
:=
job
_deadline
)
;
try
(
by
ins
);
last
2
first
;
[
by
ins
;
apply
GE_COST

by
ins
;
apply
RESP
with
(
hp_tsk
:=
tsk_other
)

by
ins
;
rewrite
RATE

by
ins
;
apply
TASK_PARAMS

by
ins
;
apply
RESTR

].
red
;
red
;
move
=>
j
'
JOBtsk
'
_
;
unfold
job_misses_no_deadline
.
specialize
(
PARAMS
j
'
);
des
.
rewrite
PARAMS1
JOBtsk
'
.
apply
completion_monotonic
with
(
t
:=
job_arrival
j
'
+
R_other
);
ins
;
[
by
rewrite
leq_add2l
;
apply
NOMISS

by
apply
(
RESP
tsk_other
)].
}
red
;
red
;
move
=>
j
'
JOBtsk
'
_
;
unfold
job_misses_no_deadline
.
specialize
(
PARAMS
j
'
);
des
.
rewrite
PARAMS1
JOBtsk
'
.
by
apply
completion_monotonic
with
(
t
:=
job_arrival
j
'
+
R_other
);
ins
;
[
by
rewrite
leq_add2l
;
apply
NOMISS

by
apply
(
RESP
tsk_other
)].
Qed
.
End
LemmasAboutInterferingTasks
.
...
...
@@ 274,7 +268,7 @@ Module ResponseTimeAnalysisFP.
(
*
Since
j
has
not
completed
,
recall
the
time
when
it
is
not
executing
is
the
total
interference
.
*
)
exploit
(
complement_of_interf_equals_service
job_cost
rate
sched
j
(
job_arrival
j
)
exploit
(
complement_of_interf_equals_service
job_cost
sched
j
(
job_arrival
j
)
(
job_arrival
j
+
R
));
last
intro
EQinterf
;
ins
;
unfold
has_arrived
;
first
by
apply
leqnn
.
rewrite
{
2
}
[
_
+
R
]
addnC

addnBA
// subnn addn0 in EQinterf.
...
...
@@ 285,7 +279,7 @@ Module ResponseTimeAnalysisFP.
apply
(
leq_ltn_trans
(
COMP
j
(
job_arrival
j
+
R
)))
in
NOTCOMP
.
by
rewrite
ltnn
in
NOTCOMP
.
}
apply
leq_trans
with
(
n
:=
R

service
rate
sched
j
(
job_arrival
j
+
R
));
last
first
.
apply
leq_trans
with
(
n
:=
R

service
sched
j
(
job_arrival
j
+
R
));
last
first
.
{
unfold
service
;
rewrite
service_before_arrival_eq_service_during
;
ins
.
rewrite
EQinterf
subKn
;
first
by
done
.
...
...
@@ 319,9 +313,9 @@ Module ResponseTimeAnalysisFP.
unfold
FP_scheduling_invariant_holds
in
*
.
unfold
x
,
X
,
total_interference
,
task_interference
.
rewrite

big_mkcond

exchange_big
big_distrl
/=
.
rewrite
[
\
sum_
(
_
<=
_
<
_

backlogged
_
_
_
_
_
)
_
]
big_mkcond
.
rewrite
[
\
sum_
(
_
<=
_
<
_

backlogged
_
_
_
_
)
_
]
big_mkcond
.
apply
eq_big_nat
;
move
=>
t
LTt
.
destruct
(
backlogged
job_cost
rate
sched
j
t
)
eqn
:
BACK
;
destruct
(
backlogged
job_cost
sched
j
t
)
eqn
:
BACK
;
last
by
rewrite
(
eq_bigr
(
fun
i
=>
0
));
[
by
rewrite
big_const_seq
iter_addn
mul0n
addn0

by
done
].
rewrite
big_mkcond
mul1n
/=
.
...
...
@@ 348,11 +342,11 @@ Module ResponseTimeAnalysisFP.
rename
H_global_scheduling_invariant
into
INVARIANT
.
intros
delta
HAS
.
set
some_interference_A
:=
fun
t
=>
backlogged
job_cost
rate
sched
j
t
&&
backlogged
job_cost
sched
j
t
&&
has
(
fun
tsk_k
=>
((
x
tsk_k
>=
delta
)
&&
task_is_scheduled
job_task
sched
tsk_k
t
))
ts_interf
.
set
total_interference_B
:=
fun
t
=>
backlogged
job_cost
rate
sched
j
t
*
backlogged
job_cost
sched
j
t
*
count
(
fun
tsk_k
=>
(
x
tsk_k
<
delta
)
&&
task_is_scheduled
job_task
sched
tsk_k
t
)
ts_interf
.
...
...
@@ 365,7 +359,7 @@ Module ResponseTimeAnalysisFP.
apply
leq_trans
with
(
n
:=
x
tsk_a
);
first
by
apply
LEa
.
unfold
x
,
task_interference
,
some_interference_A
.
apply
leq_sum
;
ins
.
destruct
(
backlogged
job_cost
rate
sched
j
i
);
destruct
(
backlogged
job_cost
sched
j
i
);
[
rewrite
2
!
andTb

by
ins
].
destruct
(
task_is_scheduled
job_task
sched
tsk_a
i
)
eqn
:
SCHEDa
;
[
apply
eq_leq
;
symmetry

by
ins
].
...
...
@@ 378,7 +372,7 @@ Module ResponseTimeAnalysisFP.
rewrite
big_distrl
/=
.
apply
leq_sum
;
intros
t
_.
unfold
some_interference_A
,
total_interference_B
.
destruct
(
backlogged
job_cost
rate
sched
j
t
)
eqn
:
BACK
;
destruct
(
backlogged
job_cost
sched
j
t
)
eqn
:
BACK
;
[
rewrite
andTb
mul1n

by
done
].
destruct
(
has
(
fun
tsk_k
:
sporadic_task
=>
(
delta
<=
x
tsk_k
)
&&
task_is_scheduled
job_task
sched
tsk_k
t
)
ts_interf
)
eqn
:
HAS
'
;
...
...
@@ 438,7 +432,7 @@ Module ResponseTimeAnalysisFP.
unfold
x
at
2
,
task_interference
.
rewrite
exchange_big
/=
;
apply
leq_sum
;
intros
t
_.
unfold
total_interference_B
.
destruct
(
backlogged
job_cost
rate
sched
j
t
);
last
by
ins
.
destruct
(
backlogged
job_cost
sched
j
t
);
last
by
ins
.
rewrite
mul1n

sum1_count
.
rewrite
big_seq_cond
big_mkcond
[
\
sum_
(
i
<
ts_interf

_
<
_
)
_
]
big_mkcond
.
by
apply
leq_sum
;
ins
;
clear

i
;
desf
;
des
;
rewrite
?
Heq2
.
...
...
@@ 580,14 +574,13 @@ Module ResponseTimeAnalysisFP.
H_response_time_of_interfering_tasks_is_known
into
RESP
,
H_hp_bounds_has_interfering_tasks
into
UNZIP
,
H_interfering_tasks_miss_no_deadlines
into
NOMISS
,
H_rate_equals_one
into
RATE
,
H_global_scheduling_invariant
into
INVARIANT
,
H_response_time_bounds_ge_cost
into
GE_COST
.
intros
j
JOBtsk
.
(
*
Now
we
start
the
proof
.
Assume
by
contradiction
that
job
j
is
not
complete
at
time
(
job_arrival
j
+
R
).
*
)
destruct
(
completed
job_cost
rate
sched
j
(
job_arrival
j
+
R
))
eqn
:
NOTCOMP
;
destruct
(
completed
job_cost
sched
j
(
job_arrival
j
+
R
))
eqn
:
NOTCOMP
;
first
by
done
.
apply
negbT
in
NOTCOMP
;
exfalso
.
...
...
interference.v
View file @
0582d634
...
...
@@ 3,7 +3,7 @@ Require Import Vbase task job schedule priority workload util_divround
Module
Interference
.
Import
Schedule
Priority
Workload
.
Import
Schedule
OfSporadicTask
Priority
Workload
.
Section
InterferingTasks
.
...
...
@@ 45,9 +45,8 @@ Module Interference.
(
*
Assume
any
job
arrival
sequence
...
*
)
Context
{
arr_seq
:
arrival_sequence
Job
}
.
(
*
...
and
any
platform
.
*
)
(
*
...
and
any
schedule
.
*
)
Context
{
num_cpus
:
nat
}
.
Variable
rate
:
Job
>
processor
num_cpus
>
nat
.
Variable
sched
:
schedule
num_cpus
arr_seq
.
(
*
Consider
any
job
j
that
incurs
interference
.
*
)
...
...
@@ 55,7 +54,7 @@ Module Interference.
(
*
Recall
the
definition
of
backlogged
(
pending
and
not
scheduled
).
*
)
Let
job_is_backlogged
(
t
:
time
)
:=
backlogged
job_cost
rate
sched
j
t
.
backlogged
job_cost
sched
j
t
.
Section
TotalInterference
.
...
...
@@ 134,12 +133,10 @@ Module Interference.
first
by
apply
leq_sum
;
ins
;
apply
leq_b1
.
by
rewrite
big_const_nat
iter_addn
mul1n
addn0
addKn
leqnn
.
Qed
.
Hypothesis
rate_positive
:
forall
cpu
t
,
rate
cpu
t
>
0.
Lemma
job_interference_le_service
:
forall
j_other
t1
t2
,
job_interference
j_other
t1
t2
<=
service_during
rate
sched
j_other
t1
t2
.
job_interference
j_other
t1
t2
<=
service_during
sched
j_other
t1
t2
.
Proof
.
intros
j_other
t1
t2
;
unfold
job_interference
,
service_during
.
apply
leq_trans
with
(
n
:=
\
sum_
(
t1
<=
t
<
t2
)
scheduled
sched
j_other
t
);
...
...
@@ 148,13 +145,12 @@ Module Interference.
destruct
(
scheduled
sched
j_other
t
)
eqn
:
SCHED
;
last
by
done
.
move:
SCHED
=>
/
existsP
EX
;
destruct
EX
as
[
cpu
];
move
:
H
=>
/
andP
[
IN
SCHED
].
unfold
service_at
;
rewrite
(
bigD1
cpu
);
last
by
done
.
by
apply
leq_trans
with
(
n
:=
rate
j_other
cpu
);
[
by
apply
rate_positive

apply
leq_addr
].
by
apply
leq_trans
with
(
n
:=
1
).
Qed
.
Lemma
task_interference_le_workload
:
forall
tsk
t1
t2
,
task_interference
tsk
t1
t2
<=
workload
job_task
rate
sched
tsk
t1
t2
.
task_interference
tsk
t1
t2
<=
workload
job_task
sched
tsk
t1
t2
.
Proof
.
unfold
task_interference
,
workload
;
intros
tsk
t1
t2
.
apply
leq_sum
;
intros
t
_.
...
...
@@ 166,17 +162,15 @@ Module Interference.
destruct
SCHED
as
[
cpu
_
HAScpu
].
rewrite
>
bigD1
with
(
j
:=
cpu
);
simpl
;
last
by
ins
.
apply
ltn_addr
;
unfold
service_of_task
,
schedules_job_of_tsk
in
*
.
by
destruct
(
sched
cpu
t
);
[
rewrite
HAScpu
mul1n
rate_positive

by
ins
].
by
destruct
(
sched
cpu
t
);
[
rewrite
HAScpu

by
done
].
Qed
.
End
BasicLemmas
.
Section
EquivalenceTaskInterference
.
Hypothesis
H_no_intratask_parallelism
:
forall
(
j
j
'
:
JobIn
arr_seq
)
t
,
job_task
j
=
job_task
j
'
>
scheduled
sched
j
t
>
scheduled
sched
j
'
t
>
False
.
jobs_of_same_task_dont_execute_in_parallel
job_task
sched
.
Lemma
interference_eq_interference_joblist
:
forall
tsk
t1
t2
,
...
...
@@ 202,6 +196,7 @@ Module Interference.
first
by
rewrite
big_const_seq
iter_addn
mul0n
addn0
addn0
.
intros
j1
_
;
desf
;
[
rewrite
andTb

by
done
].
apply
/
eqP
;
rewrite
eqb0
;
apply
/
negP
;
unfold
not
;
intro
SCHEDULED
'
.
exploit
(
H_no_intratask_parallelism
j0
j1
t
).
apply
(
H_no_intratask_parallelism
j0
j1
t
);
try
(
by
done
).
by
move
:
Heq0
=>
/
eqP
Heq0
;
rewrite
Heq0
.
}
...
...
@@ 243,41 +238,33 @@ Module Interference.
Hypothesis
no_parallelism
:
jobs_dont_execute_in_parallel
sched
.
(
*
and
that
processors
have
unit
speed
.
*
)
Hypothesis
rate_equals_one
:
forall
j
cpu
,
rate
j
cpu
=
1.
(
*
Also
assume
that
jobs
only
execute
after
they
arrived
(
*
...,
and
that
jobs
only
execute
after
they
arrived
and
no
longer
than
their
execution
costs
.
*
)
Hypothesis
jobs_must_arrive_to_execute
:
jobs_must_arrive_to_execute
sched
.
Hypothesis
completed_jobs_dont_execute
:
completed_jobs_dont_execute
job_cost
rate
sched
.
completed_jobs_dont_execute
job_cost
sched
.
(
*
If
job
j
had
already
arrived
at
time
t1
and
did
not
yet
complete
by
time
t2
,
...
*
)
Hypothesis
job_has_arrived
:
has_arrived
j
t1
.
Hypothesis
job_is_not_complete
:
~~
completed
job_cost
rate
sched
j
t2
.
~~
completed
job_cost
sched
j
t2
.
(
*
then
the
service
received
by
j
during
[
t1
,
t2
)
equals
the
cumulative
time
in
which
it
did
not
incur
interference
.
*
)
Lemma
complement_of_interf_equals_service
:
\
sum_
(
t1
<=
t
<
t2
)
service_at
rate
sched
j
t
=
\
sum_
(
t1
<=
t
<
t2
)
service_at
sched
j
t
=
t2

t1

total_interference
t1
t2
.
Proof
.
unfold
completed
,
total_interference
,
job_is_backlogged
,
backlogged
,
service_during
,
pending
.
rename
no_parallelism
into
NOPAR
,
rate_equals_one
into
RATE
,
jobs_must_arrive_to_execute
into
MUSTARRIVE
,
completed_jobs_dont_execute
into
COMP
,
job_is_not_complete
into
NOTCOMP
.
assert
(
SERVICE_ONE
:
forall
j
t
,
service_at
rate
sched
j
t
<=
1
).
by
ins
;
apply
service_at_le_max_rate
;
ins
;
rewrite
RATE
.
(
*
Reorder
terms
...
*
)
apply
/
eqP
;
rewrite
subh4
;
first
last
.
{
...
...
@@ 286,23 +273,23 @@ Module Interference.
}
{
rewrite

[
t2

t1
]
mul1n

[
1
*
_
]
addn0

iter_addn

big_const_nat
.
by
apply
leq_sum
;
ins
;
apply
service_at_
le_max_rate
;
ins
;
rewrite
RATE
.
by
apply
leq_sum
;
ins
;
apply
service_at_
most_one
.
}
apply
/
eqP
.
apply
eq_trans
with
(
y
:=
\
sum_
(
t1
<=
t
<
t2
)
(
1

service_at
rate
sched
j
t
));
(
1

service_at
sched
j
t
));
last
first
.
{
apply
/
eqP
;
rewrite
<
eqn_add2r
with
(
p
:=
\
sum_
(
t1
<=
t
<
t2
)
service_at
rate
sched
j
t
).
service_at
sched
j
t
).
rewrite
subh1
;
last
first
.
rewrite

[
t2

t1
]
mul1n

[
1
*
_
]
addn0

iter_addn

big_const_nat
.
by
apply
leq_sum
;
ins
;
apply
SERVICE_ONE
.
by
apply
leq_sum
;
ins
;
apply
service_at_most_one
.
rewrite

addnBA
// subnn addn0 big_split /=.
rewrite

[
t2

t1
]
mul1n

[
1
*
_
]
addn0

iter_addn

big_const_nat
.
apply
/
eqP
;
apply
eq_bigr
;
ins
;
rewrite
subh1
;
[
by
rewrite

addnBA
// subnn addn0  by apply
SERVICE_ONE
].
[
by
rewrite

addnBA
// subnn addn0  by apply
service_at_most_one
].
}
rewrite
big_nat_cond
[
\
sum_
(
_
<=
_
<
_

true
)
_
]
big_nat_cond
.
apply
eq_bigr
;
intro
t
;
rewrite
andbT
;
move
=>
/
andP
[
GEt1
LTt2
].
...
...
@@ 311,15 +298,14 @@ Module Interference.
apply
negbFE
in
SCHED
;
unfold
scheduled
in
*
.
move:
SCHED
=>
/
exists_inP
SCHED
;
destruct
SCHED
as
[
cpu
INcpu
SCHEDcpu
].
rewrite
andbF
;
apply
/
eqP
.
rewrite

(
eqn_add2r
(
service_at
rate
sched
j
t
))
add0n
.
rewrite
subh1
;
last
by
apply
SERVICE_ONE
.
rewrite

(
eqn_add2r
(
service_at
sched
j
t
))
add0n
.
rewrite
subh1
;
last
by
apply
service_at_most_one
.
rewrite

addnBA
// subnn addn0.
rewrite
eqn_leq
;
apply
/
andP
;
split
;
first
by
apply
SERVICE_ONE
.
rewrite
eqn_leq
;
apply
/
andP
;
split
;
first
by
apply
service_at_most_one
.
unfold
service_at
;
rewrite
(
bigD1
cpu
)
/=
;
last
by
apply
SCHEDcpu
.
apply
leq_trans
with
(
n
:=
rate
j
cpu
);
[
by
rewrite
RATE

by
apply
leq_addr
].
by
apply
leq_trans
with
(
n
:=
1
).
}
apply
not_scheduled_no_service
with
(
rate0
:=
rate
)
in
SCHED
.
apply
not_scheduled_no_service
in
SCHED
.
rewrite
SCHED
subn0
andbT
;
apply
/
eqP
;
rewrite
eqb1
.
apply
/
andP
;
split
;
first
by
apply
leq_trans
with
(
n
:=
t1
).
apply
/
negP
;
unfold
not
;
intro
BUG
.
...
...
interference_bound_edf.v
View file @
0582d634
...
...
@@ 65,7 +65,6 @@ Module EDFSpecificBound.
(
*
Consider
any
schedule
such
that
...
*
)
Variable
num_cpus
:
nat
.
Variable
rate
:
Job
>
processor
num_cpus
>
nat
.
Variable
sched
:
schedule
num_cpus
arr_seq
.
(
*
...
jobs
do
not
execute
before
their
arrival
times
nor
longer
...
...
@@ 73,14 +72,12 @@ Module EDFSpecificBound.
Hypothesis
H_jobs_must_arrive_to_execute
:
jobs_must_arrive_to_execute
sched
.
Hypothesis
H_completed_jobs_dont_execute
:
completed_jobs_dont_execute
job_cost
rate
sched
.
completed_jobs_dont_execute
job_cost
sched
.
(
*
Also
assume
that
jobs
do
not
execute
in
parallel
,
processors
have
unit
speed
,
and
that
there
exists
at
least
one
processor
.
*
)
(
*
Also
assume
that
jobs
do
not
execute
in
parallel
and
that
there
exists
at
least
one
processor
.
*
)
Hypothesis
H_no_parallelism
:
jobs_dont_execute_in_parallel
sched
.
Hypothesis
H_rate_equals_one
:
forall
j
cpu
,
rate
j
cpu
=
1.
Hypothesis
H_at_least_one_cpu
:
num_cpus
>
0.
...
...
@@ 105,16 +102,16 @@ Module EDFSpecificBound.
forall
tsk
,
tsk
\
in
ts
>
task_deadline
tsk
<=
task_period
tsk
.
Let
no_deadline_is_missed_by_tsk
(
tsk
:
sporadic_task
)
:=
task_misses_no_deadline
job_cost
job_deadline
job_task
rate
sched
tsk
.
task_misses_no_deadline
job_cost
job_deadline
job_task
sched
tsk
.
Let
response_time_bounded_by
(
tsk
:
sporadic_task
)
:=
is_response_time_bound_of_task
job_cost
job_task
tsk
rate
sched
.
is_response_time_bound_of_task
job_cost
job_task
tsk
sched
.
(
*
Assume
that
the
schedule
satisfies
the
global
scheduling
invariant
for
EDF
,
i
.
e
.,
if
any
job
of
tsk
is
backlogged
,
every
processor
must
be
busy
with
jobs
with
no
larger
absolute
deadline
.
*
)
Let
higher_eq_priority
:=
@
EDF
Job
arr_seq
job_deadline
.
(
*
TODO
:
implicit
params
broken
*
)
Hypothesis
H_global_scheduling_invariant
:
JLFP_JLDP_scheduling_invariant_holds
job_cost
num_cpus
rate
sched
higher_eq_priority
.
JLFP_JLDP_scheduling_invariant_holds
job_cost
num_cpus
sched
higher_eq_priority
.
(
*
Let
tsk_i
be
the
task
to
be
analyzed
,
...
*
)
Variable
tsk_i
:
sporadic_task
.
...
...
@@ 141,7 +138,7 @@ Module EDFSpecificBound.
forall
(
j_k
:
JobIn
arr_seq
),
job_task
j_k
=
tsk_k
>
job_arrival
j_k
+
R_k
<
job_arrival
j_i
+
delta
>
completed
job_cost
rate
sched
j_k
(
job_arrival
j_k
+
R_k
).
completed
job_cost
sched
j_k
(
job_arrival
j_k
+
R_k
).
(
*
In
this
section
,
we
prove
that
Bertogna
and
Cirinei
'
s
EDF
interference
bound
indeed
bounds
the
interference
caused
by
task
tsk_k
in
the
interval
[
t1
,
t1
+
delta
).
*
)
...
...
@@ 149,7 +146,7 @@ Module EDFSpecificBound.
(
*
Let
'
s
call
x
the
task
interference
incurred
by
job
j
due
to
tsk_k
.
*
)
Let
x
:=
task_interference
job_cost
job_task
rate
sched
j_i
task_interference
job_cost
job_task
sched
j_i
tsk_k
(
job_arrival
j_i
)
(
job_arrival
j_i
+
delta
).
(
*
Also
,
recall
the
EDF

specific
interference
bound
for
EDF
.
*
)
...
...
@@ 168,11 +165,11 @@ Module EDFSpecificBound.
(
*
Identify
the
subset
of
jobs
that
actually
cause
interference
*
)
Let
interfering_jobs
:=
filter
(
fun
(
x
:
JobIn
arr_seq
)
=>
(
job_task
x
==
tsk_k
)
&&
(
job_interference
job_cost
rate
sched
j_i
x
t1
t2
!=
0
))
(
job_task
x
==
tsk_k
)
&&
(
job_interference
job_cost
sched
j_i
x
t1
t2
!=
0
))
(
jobs_scheduled_between
sched
t1
t2
).
(
*
Let
'
s
give
a
simpler
name
to
job
interference
.
*
)
Let
interference_caused_by
:=
job_interference
job_cost
rate
sched
j_i
.
Let
interference_caused_by
:=
job_interference
job_cost
sched
j_i
.
(
*
Now
,
consider
the
list
of
interfering
jobs
sorted
by
arrival
time
.
*
)
Let
order
:=
fun
(
x
y
:
JobIn
arr_seq
)
=>
job_arrival
x
<=
job_arrival
y
.
...
...
@@ 185,10 +182,11 @@ Module EDFSpecificBound.
(
*
Use
the
alternative
definition
of
task
interference
,
based
on
individual
job
interference
.
*
)
Lemma
interference_bound_edf_use_another_definition
:
x
=
\
sum_
(
j
<
jobs_scheduled_between
sched
t1
t2

job_task
j
==
tsk_k
)
x
<
=
\
sum_
(
j
<
jobs_scheduled_between
sched
t1
t2

job_task
j
==
tsk_k
)
interference_caused_by
j
t1
t2
.
Proof
.
by
apply
interference_eq_interference_joblist
.
apply
interference_eq_interference_joblist
.
Qed
.
(
*
Remove
the
elements
that
we
don
'
t
care
about
from
the
sum
*
)
...
...
@@ 201,7 +199,7 @@ Module EDFSpecificBound.
rewrite
big_mkcond
;
rewrite
[
\
sum_
(
_
<
_

_
)
_
]
big_mkcond
/=
.
apply
eq_bigr
;
intros
i
_
;
clear

i
.
destruct
(
job_task
i
==
tsk_k
);
rewrite
?
andTb
?
andFb
;
last
by
done
.
destruct
(
job_interference
job_cost
rate
sched
j_i
i
t1
t2
!=
0
)
eqn
:
DIFF
;
first
by
done
.
destruct
(
job_interference
job_cost
sched
j_i
i
t1
t2
!=
0
)
eqn
:
DIFF
;
first
by
done
.
by
apply
negbT
in
DIFF
;
rewrite
negbK
in
DIFF
;
apply
/
eqP
.
Qed
.
...
...
@@ 251,8 +249,7 @@ Module EDFSpecificBound.
forall
j
(
INi
:
j
\
in
interfering_jobs
),
interference_caused_by
j
t1
t2
<=
task_cost
tsk_k
.
Proof
.
rename
H_valid_job_parameters
into
PARAMS
,
H_rate_equals_one
into
RATE
.
rename
H_valid_job_parameters
into
PARAMS
.
intros
j
;
rewrite
mem_filter
;
move
=>
/
andP
[
/
andP
[
/
eqP
JOBj
_
]
_
].
specialize
(
PARAMS
j
);
des
.
apply
leq_trans
with
(
n
:=
service_during
rate
sched
j
t1
t2
);
...
...
platform.v
View file @
0582d634
...
...
@@ 20,9 +20,8 @@ Module Platform.
(
*
Assume
any
job
arrival
sequence
...
*
)
Context
{
arr_seq
:
arrival_sequence
Job
}
.
(
*
Consider
any
schedule
such
that
..
.
*
)
(
*
Consider
any
schedule
.
*
)
Variable
num_cpus
:
nat
.
Variable
rate
:
Job
>
processor
num_cpus
>
nat
.
Variable
sched
:
schedule
num_cpus
arr_seq
.
(
*
Assume
that
we
have
a
task
set
where
all
tasks
have
valid
...
...
@@ 41,7 +40,7 @@ Module Platform.
forall
(
tsk
:
sporadic_task
)
(
j
:
JobIn
arr_seq
)
(
t
:
time
),
tsk
\
in
ts
>
job_task
j
=
tsk
>
backlogged
job_cost
rate
sched
j
t
>
backlogged
job_cost
sched
j
t
>
count
(
fun
tsk_other
:
sporadic_task
=>
is_interfering_task_fp
higher_eq_priority
tsk
tsk_other
&&
...
...
@@ 59,7 +58,7 @@ Module Platform.
jobs
of
higher

priority
.
*
)
Definition
JLFP_JLDP_scheduling_invariant_holds
:=
forall
(
j
:
JobIn
arr_seq
)
(
t
:
time
),
backlogged
job_cost
rate
sched
j
t
>
backlogged
job_cost
sched
j
t
>
count
(
fun
j_other
=>
higher_eq_priority
t
j_other
j
)
(
jobs_scheduled_at
sched
t
)
...
...
@@ 73,7 +72,7 @@ Module Platform.
(
*
The
job
which
is
interfering
has
higher
or
equal
priority
to
the
interfered
one
.
*
)
Lemma
interfering_job_has_higher_eq_prio
:
forall
j
j_other
t
,
backlogged
job_cost
rate
sched
j
t
>
backlogged
job_cost
sched
j
t
>
scheduled
sched
j_other
t
>
higher_eq_priority
t
j_other
j
.
Proof
.
...
...
@@ 167,7 +166,7 @@ Module Platform.
Lemma
cpus_busy_with_interfering_tasks
:
forall
(
j
:
JobIn
arr_seq
)
tsk
t
,
job_task
j
=
tsk
>
backlogged
job_cost
rate
sched
j
t
>
backlogged
job_cost
sched
j
t
>
count
(
fun
j
:
sporadic_task
=>
is_interfering_task_jlfp
tsk
j
&&
...
...
response_time.v
View file @
0582d634
...
...
@@ 19,13 +19,12 @@ Module ResponseTime.
(
*
...
and
a
particular
schedule
,
...
*
)
Context
{
num_cpus
:
nat
}
.
Variable
rate
:
Job
>
processor
num_cpus
>
nat
.
Variable
sched
:
schedule
num_cpus
arr_seq
.
(
*
...
R
is
a
response

time
bound
of
tsk
in
this
schedule
...
*
)
Variable
R
:
time
.
Let
job_has_completed_by
:=
completed
job_cost
rate
sched
.
Let
job_has_completed_by
:=
completed
job_cost
sched
.
(
*
...
iff
any
job
j
of
tsk
in
this
arrival
sequence
has
completed
by
(
job_arrival
j
+
R
).
*
)
...
...
@@ 48,13 +47,12 @@ Module ResponseTime.
(
*
Consider
any
valid
schedule
...
*
)
Context
{
num_cpus
:
nat
}
.
Variable
sched
:
schedule
num_cpus
arr_seq
.
Variable
rate
:
Job
>
processor
num_cpus
>
nat
.
Let
job_has_completed_by
:=
completed
job_cost
rate
sched
.
Let
job_has_completed_by
:=
completed
job_cost
sched
.
(
*
...
where
jobs
dont
execute
after
completion
.
*
)
Hypothesis
H_completed_jobs_dont_execute
:
completed_jobs_dont_execute
job_cost
rate
sched
.
completed_jobs_dont_execute
job_cost
sched
.
Section
SpecificJob
.
...
...
@@ 70,7 +68,7 @@ Module ResponseTime.
Lemma
service_after_job_rt_zero
:
forall
t
'
,
t
'
>=
job_arrival
j
+
R
>
service_at
rate
sched
j
t
'
=
0.
service_at
sched
j
t
'
=
0.
Proof
.
rename
response_time_bound
into
RT
,
H_completed_jobs_dont_execute
into
EXEC
;
ins
.
...
...
@@ 79,7 +77,7 @@ Module ResponseTime.
apply
/
eqP
;
rewrite

leqn0
.
rewrite
<
leq_add2l
with
(
p
:=
job_cost
j
).
move:
RT
=>
/
eqP
RT
;
rewrite
{
1
}
RT
addn0
.
apply
leq_trans
with
(
n
:=
service
rate
sched
j
t
'
.
+
1
);
apply
leq_trans
with
(
n
:=
service
sched
j
t
'
.
+
1
);
last
by
apply
EXEC
.
unfold
service
;
rewrite
>
big_cat_nat
with
(
p
:=
t
'
.
+
1
)
(
n
:=
job_arrival
j
+
R
);
...
...
@@ 91,7 +89,7 @@ Module ResponseTime.
Lemma
cumulative_service_after_job_rt_zero
:
forall
t
'
t
''
,
t
'
>=
job_arrival
j
+
R
>
\
sum_
(
t
'
<=
t
<
t
''
)
service_at
rate
sched
j
t
=
0.
\
sum_
(
t
'
<=
t
<
t
''
)
service_at
sched
j
t
=
0.
Proof
.
ins
;
apply
/
eqP
;
rewrite

leqn0
.
rewrite
big_nat_cond
;
rewrite
>
eq_bigr
with
(
F2
:=
fun
i
=>
0
);
...
...
@@ 111,7 +109,7 @@ Module ResponseTime.
(
*
...
for
which
a
response

time
bound
R
is
known
.
*
)
Variable
R
:
time
.
Hypothesis
response_time_bound
:
is_response_time_bound_of_task
job_cost
job_task
tsk
rate
sched
R
.
is_response_time_bound_of_task
job_cost
job_task
tsk
sched
R
.