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
8e5fabfe
Commit
8e5fabfe
authored
Jan 19, 2016
by
Felipe Cerqueira
Browse files
Prove lemma relating joblevel invariant and tasklevel invariant
parent
7ef6c8c5
Changes
2
Hide whitespace changes
Inline
Sidebyside
Showing
2 changed files
with
273 additions
and
175 deletions
+273
175
bertogna_edf_theory.v
bertogna_edf_theory.v
+107
11
platform.v
platform.v
+166
164
No files found.
bertogna_edf_theory.v
View file @
8e5fabfe
...
...
@@ 117,7 +117,7 @@ Module ResponseTimeAnalysisEDF.
(
*
Assume
that
we
have
a
task
set
where
all
tasks
have
valid
parameters
and
restricted
deadlines
.
*
)
Variable
ts
:
taskset_of
sporadic_task
.
Hypothesis
all_jobs_from_taskset
:
Hypothesis
H_
all_jobs_from_taskset
:
forall
(
j
:
JobIn
arr_seq
),
job_task
j
\
in
ts
.
Hypothesis
H_valid_task_parameters
:
valid_sporadic_taskset
task_cost
task_period
task_deadline
ts
.
...
...
@@ 151,13 +151,42 @@ Module ResponseTimeAnalysisEDF.
Let
higher_eq_priority
:=
@
EDF
Job
arr_seq
job_deadline
.
(
*
TODO
:
implicit
params
broken
*
)
(
*
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
.
*
)
Hypothesis
H_global_scheduling_invariant
:
JLFP_JLDP_scheduling_invariant_holds
job_cost
num_cpus
sched
higher_eq_priority
.
(
*
The
EDF
scheduling
invariant
together
with
no
intra

task
parallelism
imply
task
precedence
constraints
.
*
)
Lemma
edf_no_intratask_parallelism_implies_task_precedence
:
task_precedence_constraints
job_cost
job_task
sched
.
Proof
.
rename
H_no_intra_task_parallelism
into
NOINTRA
,
H_valid_job_parameters
into
JOBPARAMS
.
unfold
task_precedence_constraints
,
valid_sporadic_job
,
jobs_of_same_task_dont_execute_in_parallel
in
*
.
intros
j
j
'
t
SAMEtsk
BEFORE
PENDING
.
apply
/
negP
;
unfold
not
;
intro
SCHED
'
.
destruct
(
scheduled
sched
j
t
)
eqn
:
SCHED
.
{
specialize
(
NOINTRA
j
j
'
t
SAMEtsk
SCHED
SCHED
'
);
subst
.
by
rewrite
ltnn
in
BEFORE
.
}
apply
negbT
in
SCHED
.
assert
(
INTERF
:
job_interference
job_cost
sched
j
j
'
t
t
.
+
1
!=
0
).
{
unfold
job_interference
;
rewrite

lt0n
.
rewrite
big_nat_recr
// /=.
by
unfold
backlogged
;
rewrite
PENDING
SCHED
SCHED
'
2
!
andbT
addn1
.
}
apply
interference_under_edf_implies_shorter_deadlines
with
(
job_deadline0
:=
job_deadline
)
in
INTERF
;
last
by
done
.
have
PARAMS
:=
(
JOBPARAMS
j
);
have
PARAMS
'
:=
(
JOBPARAMS
j
'
);
des
.
rewrite
PARAMS1
PARAMS
'1
SAMEtsk
leq_add2r
in
INTERF
.
by
apply
(
leq_trans
BEFORE
)
in
INTERF
;
rewrite
ltnn
in
INTERF
.
Qed
.
(
*
Assume
that
the
task
set
has
no
duplicates
.
Otherwise
,
counting
the
number
of
tasks
that
have
some
property
does
not
make
sense
(
for
example
,
for
stating
the
global
scheduling
invariant
as
...
...
@@ 332,11 +361,20 @@ Module ResponseTimeAnalysisEDF.
Lemma
bertogna_edf_all_cpus_busy
:
\
sum_
(
tsk_k
<
ts_interf
)
x
tsk_k
=
X
*
num_cpus
.
Proof
.
rename
H_global_scheduling_invariant
into
INV
.
rename
H_global_scheduling_invariant
into
INV
,
H_all_jobs_from_taskset
into
FROMTS
,
H_valid_task_parameters
into
PARAMS
,
H_job_of_tsk
into
JOBtsk
,
H_sporadic_tasks
into
SPO
,
H_tsk_R_in_rt_bounds
into
INbounds
,
H_all_previous_jobs_completed_on_time
into
BEFOREok
,
H_tasks_miss_no_deadlines
into
NOMISS
,
H_restricted_deadlines
into
RESTR
.
unfold
sporadic_task_model
in
*
.
unfold
x
,
X
,
total_interference
,
task_interference
.
rewrite

big_mkcond

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

backlogged
_
_
_
_
)
_
]
big_mkcond
.
apply
eq_big_nat
;
move
=>
t
LTt
.
apply
eq_big_nat
;
move
=>
t
/
andP
[
LEt
LTt
]
.
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
].
...
...
@@ 346,8 +384,32 @@ Module ResponseTimeAnalysisEDF.
task_is_scheduled
job_task
sched
i
t
)
then
1
else
0
));
last
by
intro
i
;
clear

i
;
desf
.
rewrite

big_mkcond
sum1_count
.
by
eapply
cpus_busy_with_interfering_tasks
;
try
(
by
done
);
[
by
apply
INV

by
apply
H_job_of_tsk

by
apply
BACK
].
eapply
cpus_busy_with_interfering_tasks
;
try
(
by
done
);
[
by
apply
INV

by
red
;
apply
SPO

by
apply
edf_no_intratask_parallelism_implies_task_precedence

by
apply
PARAMS
;
rewrite

JOBtsk
FROMTS

by
apply
JOBtsk

by
apply
BACK

].
{
intros
j0
TSK0
LT0
.
unfold
pending
in
*
.
apply
completion_monotonic
with
(
t0
:=
job_arrival
j0
+
R
);
try
(
by
done
).
{
apply
leq_trans
with
(
n
:=
job_arrival
j
);
last
by
done
.
apply
leq_trans
with
(
n
:=
job_arrival
j0
+
task_period
tsk
).
{
rewrite
leq_add2l
.
apply
leq_trans
with
(
n
:=
task_deadline
tsk
);
[
by
apply
NOMISS

by
apply
RESTR
;
rewrite

JOBtsk
FROMTS
].
}
rewrite

TSK0
;
apply
SPO
;
[

by
rewrite
JOBtsk
TSK0

by
apply
ltnW
].
by
unfold
not
;
intro
BUG
;
rewrite
BUG
ltnn
in
LT0
.
}
by
apply
BEFOREok
with
(
tsk_other
:=
tsk
);
rewrite
?
ltn_add2r
.
}
Qed
.
(
*
Let
(
cardGE
delta
)
be
the
number
of
interfering
tasks
whose
interference
...
...
@@ 362,7 +424,16 @@ Module ResponseTimeAnalysisEDF.
cardGE
delta
>
0
>
\
sum_
(
i
<
ts_interf

x
i
<
delta
)
x
i
>=
delta
*
(
num_cpus

cardGE
delta
).
Proof
.
rename
H_global_scheduling_invariant
into
INVARIANT
.
rename
H_global_scheduling_invariant
into
INV
,
H_all_jobs_from_taskset
into
FROMTS
,
H_valid_task_parameters
into
PARAMS
,
H_job_of_tsk
into
JOBtsk
,
H_sporadic_tasks
into
SPO
,
H_tsk_R_in_rt_bounds
into
INbounds
,
H_all_previous_jobs_completed_on_time
into
BEFOREok
,
H_tasks_miss_no_deadlines
into
NOMISS
,
H_restricted_deadlines
into
RESTR
.
unfold
sporadic_task_model
in
*
.
intros
delta
HAS
.
set
some_interference_A
:=
fun
t
=>
backlogged
job_cost
sched
j
t
&&
...
...
@@ 403,10 +474,35 @@ Module ResponseTimeAnalysisEDF.
rewrite
mul1n
;
move
:
HAS
=>
/
hasP
HAS
.
destruct
HAS
as
[
tsk_k
INk
LEk
].
generalize
INVARIANT
;
intro
COUNT
.
apply
cpus_busy_with_interfering_tasks
with
(
job_task0
:=
job_task
)
(
ts0
:=
ts
)
(
j0
:=
j
)
(
tsk0
:=
tsk
)
(
t0
:=
t
)
in
COUNT
;
try
by
done
.
generalize
INV
;
intro
COUNT
.
apply
cpus_busy_with_interfering_tasks
with
(
job_task0
:=
job_task
)
(
ts0
:=
ts
)
(
j0
:=
j
)
(
tsk0
:=
tsk
)
(
t0
:=
t
)
(
task_cost0
:=
task_cost
)
(
task_period0
:=
task_period
)
(
task_deadline0
:=
task_deadline
)
in
COUNT
;
try
(
by
done
);
[

by
apply
edf_no_intratask_parallelism_implies_task_precedence

by
apply
PARAMS
;
rewrite

JOBtsk
FROMTS

];
last
first
.
{
intros
j0
TSK0
LT0
.
unfold
pending
in
*
.
apply
completion_monotonic
with
(
t0
:=
job_arrival
j0
+
R
);
try
(
by
done
).
{
move:
BACK
=>
/
andP
[
/
andP
[
ARRIVED
NOTCOMP
]
NOTSCHED
].
apply
leq_trans
with
(
n
:=
job_arrival
j
);
last
by
done
.
apply
leq_trans
with
(
n
:=
job_arrival
j0
+
task_period
tsk
).
{
rewrite
leq_add2l
.
apply
leq_trans
with
(
n
:=
task_deadline
tsk
);
[
by
apply
NOMISS

by
apply
RESTR
;
rewrite

JOBtsk
FROMTS
].
}
rewrite

TSK0
;
apply
SPO
;
[

by
rewrite
JOBtsk
TSK0

by
apply
ltnW
].
by
unfold
not
;
intro
BUG
;
rewrite
BUG
ltnn
in
LT0
.
}
by
apply
BEFOREok
with
(
tsk_other
:=
tsk
);
rewrite
?
ltn_add2r
.
}
unfold
cardGE
.
set
interfering_tasks_at_t
:=
[
seq
tsk_k
<
ts_interf

task_is_scheduled
job_task
...
...
platform.v
View file @
8e5fabfe
Require
Import
Vbase
task
schedule
job
priority
interference
util_lemmas
Require
Import
Vbase
task
schedule
job
priority
interference
task_arrival
util_lemmas
ssreflect
ssrbool
ssrfun
eqtype
ssrnat
seq
fintype
bigop
.
Module
Platform
.
Import
ScheduleOfSporadicTask
SporadicTaskset
Interference
Priority
.
Import
Job
ScheduleOfSporadicTask
SporadicTaskset
SporadicTaskArrival
Interference
Priority
.
Section
SchedulingInvariants
.
...
...
@@ 64,10 +65,16 @@ Module Platform.
(
jobs_scheduled_at
sched
t
)
=
num_cpus
.
Section
BasicLemmas
.
End
JLDP
.
Section
Lemmas
.
Section
InterferingJobHasHigherPriority
.
Variable
higher_eq_priority
:
jldp_policy
arr_seq
.
Hypothesis
H_invariant_holds
:
JLFP_JLDP_scheduling_invariant_holds
.
JLFP_JLDP_scheduling_invariant_holds
higher_eq_priority
.
(
*
The
job
which
is
interfering
has
higher
or
equal
priority
to
the
interfered
one
.
*
)
Lemma
interfering_job_has_higher_eq_prio
:
...
...
@@ 103,199 +110,194 @@ Module Platform.
by
rewrite
ltnn
in
BUG
.
Qed
.
(
*
Assume
the
task
set
has
no
duplicates
.
*
)
Hypothesis
H_ts_is_a_set
:
uniq
ts
.
End
InterferingJobHasHigherPriority
.
Section
JobInvariantAsTaskInvariant
.
Variable
higher_eq_priority
:
jldp_policy
arr_seq
.
(
*
Assume
all
jobs
are
from
the
taskset
,
...
*
)
Hypothesis
H_invariant_holds
:
JLFP_JLDP_scheduling_invariant_holds
higher_eq_priority
.
(
*
Assume
the
task
set
has
no
duplicates
,
...
*
)
Hypothesis
H_ts_is_a_set
:
uniq
ts
.
(
*
...
all
jobs
have
valid
parameters
...
*
)
Hypothesis
H_valid_job_parameters
:
forall
(
j
:
JobIn
arr_seq
),
valid_sporadic_job
task_cost
task_deadline
job_cost
job_deadline
job_task
j
.
(
*
...
and
come
from
the
taskset
.
*
)
Hypothesis
H_all_jobs_from_taskset
:
forall
(
j
:
JobIn
arr_seq
),
job_task
j
\
in
ts
.
(
*
...,
a
single
job
does
not
execute
in
parallel
,
...
*
)
(
*
Suppose
that
a
single
job
does
not
execute
in
parallel
,
...
*
)
Hypothesis
H_no_parallelism
:
jobs_dont_execute_in_parallel
sched
.
(
*
...
and
jobs
from
the
same
task
do
not
execute
in
parallel
.
*
)
(
*
...
jobs
from
the
same
task
do
not
execute
in
parallel
,
..
.
*
)
Hypothesis
H_no_intra_task_parallelism
:
jobs_of_same_task_dont_execute_in_parallel
job_task
sched
.
(
*
...
and
jobs
do
not
execute
after
completion
.
*
)
Hypothesis
H_completed_jobs_dont_execute
:
completed_jobs_dont_execute
job_cost
sched
.
(
*
Assume
that
the
schedule
satisfies
the
sporadic
task
model
...
*
)
Hypothesis
H_sporadic_tasks
:
sporadic_task_model
task_period
arr_seq
job_task
.
Lemma
scheduled_jobs_unique
:
jobs_dont_execute_in_parallel
sched
>
forall
t
,
uniq
(
jobs_scheduled_at
sched
t
).
(
*
and
task
precedence
constraints
.
*
)
Hypothesis
H_task_precedence
:
task_precedence_constraints
job_cost
job_task
sched
.
(
*
Consider
a
valid
task
tsk
,
...
*
)
Variable
tsk
:
sporadic_task
.
Hypothesis
H_valid_task
:
is_valid_sporadic_task
task_cost
task_period
task_deadline
tsk
.
(
*
...
whose
job
j
...
*
)
Variable
j
:
JobIn
arr_seq
.
Variable
H_job_of_tsk
:
job_task
j
=
tsk
.
(
*
...
is
backlogged
at
time
t
.
*
)
Variable
t
:
time
.
Hypothesis
H_j_backlogged
:
backlogged
job_cost
sched
j
t
.
(
*
Assume
that
any
previous
jobs
of
tsk
have
completed
by
time
t
.
*
)
Hypothesis
H_all_previous_jobs_completed
:
forall
(
j0
:
JobIn
arr_seq
),
job_task
j0
=
tsk
>
job_arrival
j0
<
job_arrival
j
>
completed
job_cost
sched
j0
t
.
(
*
If
a
job
isn
'
t
scheduled
,
the
processor
are
busy
with
interfering
tasks
.
*
)
Lemma
cpus_busy_with_interfering_tasks
:
count
(
fun
j
:
sporadic_task
=>
is_interfering_task_jlfp
tsk
j
&&
task_is_scheduled
job_task
sched
j
t
)
ts
=
num_cpus
.
Proof
.
intros
_
t
;
rename
H_no_parallelism
into
SEQUENTIAL
.
unfold
jobs_dont_execute_in_parallel
in
SEQUENTIAL
.
clear

SEQUENTIAL
.
unfold
jobs_scheduled_at
.
induction
num_cpus
;
first
by
rewrite
big_ord0
.
rename
H_all_jobs_from_taskset
into
FROMTS
,
H_no_parallelism
into
SEQUENTIAL
,
H_no_intra_task_parallelism
into
NOINTRA
,
H_invariant_holds
into
INV
,
H_j_backlogged
into
BACK
,
H_job_of_tsk
into
JOBtsk
,
H_task_precedence
into
PREC
,
H_sporadic_tasks
into
SPO
,
H_valid_task
into
PARAMS
,
H_all_previous_jobs_completed
into
PREV
,
H_completed_jobs_dont_execute
into
COMP
,
H_valid_job_parameters
into
JOBPARAMS
.
unfold
JLFP_JLDP_scheduling_invariant_holds
,
valid_sporadic_job
,
valid_realtime_job
,
task_precedence_constraints
,
completed_jobs_dont_execute
,
sporadic_task_model
,
is_valid_sporadic_task
,
jobs_of_same_task_dont_execute_in_parallel
,
jobs_dont_execute_in_parallel
in
*
.
apply
/
eqP
;
rewrite
eqn_leq
;
apply
/
andP
;
split
.
{
rewrite
big_ord_recr
cat_uniq
;
apply
/
andP
;
split
.
apply
leq_trans
with
(
n
:=
count
(
fun
x
=>
task_is_scheduled
job_task
sched
x
t
)
ts
);
first
by
apply
sub_count
;
first
by
red
;
move
=>
x
/
andP
[
_
SCHED
].
unfold
task_is_scheduled
.
apply
count_exists
;
first
by
done
.
{
apply
bigcat_ord_uniq
;
first
by
intro
i
;
unfold
make_sequence
;
desf
.
intros
x
i1
i2
IN1
IN2
;
unfold
make_sequence
in
*
.
desf
;
move
:
Heq0
Heq
=>
SOME1
SOME2
.
rewrite
mem_seq1
in
IN1
;
rewrite
mem_seq1
in
IN2
.
move:
IN1
IN2
=>
/
eqP
IN1
/
eqP
IN2
;
subst
x
j0
.
specialize
(
SEQUENTIAL
j
t
(
widen_ord
(
leqnSn
n
)
i1
)
(
widen_ord
(
leqnSn
n
)
i2
)
SOME1
SOME2
).
by
inversion
SEQUENTIAL
;
apply
ord_inj
.
intros
cpu
x1
x2
SCHED1
SCHED2
.
unfold
schedules_job_of_tsk
in
*
.
destruct
(
sched
cpu
t
);
last
by
done
.
move:
SCHED1
SCHED2
=>
/
eqP
SCHED1
/
eqP
SCHED2
.
by
rewrite

SCHED1

SCHED2
.
}
apply
/
andP
;
split
;
last
by
unfold
make_sequence
;
destruct
(
sched
ord_max
).
{
rewrite

all_predC
;
apply
/
allP
;
unfold
predC
;
simpl
.
intros
x
INx
.
unfold
make_sequence
in
INx
.
destruct
(
sched
ord_max
t
)
eqn
:
SCHED
;
last
by
rewrite
in_nil
in
INx
.
apply
/
negP
;
unfold
not
;
intro
IN
'
.
have
EX
:=
mem_bigcat_ord_exists
_
x
n
.
apply
EX
in
IN
'
;
des
;
clear
EX
.
unfold
make_sequence
in
IN
'
.
desf
;
rename
Heq
into
SCHEDi
.
rewrite
mem_seq1
in
INx
;
rewrite
mem_seq1
in
IN
'
.
move:
INx
IN
'
=>
/
eqP
INx
/
eqP
IN
'
;
subst
x
j0
.
specialize
(
SEQUENTIAL
j
t
ord_max
(
widen_ord
(
leqnSn
n
)
i
)
SCHED
SCHEDi
).
inversion
SEQUENTIAL
;
destruct
i
as
[
i
EQ
];
simpl
in
*
.
clear
SEQUENTIAL
SCHEDi
.
by
rewrite
H0
ltnn
in
EQ
.
intros
x
cpu1
cpu2
SCHED1
SCHED2
.
unfold
schedules_job_of_tsk
in
*
.
destruct
(
sched
cpu1
t
)
eqn
:
SCHED1
'
;
last
by
done
.
destruct
(
sched
cpu2
t
)
eqn
:
SCHED2
'
;
last
by
done
.
move:
SCHED1
SCHED2
=>
/
eqP
SCHED1
/
eqP
SCHED2
;
subst
x
.
exploit
(
NOINTRA
j1
j0
t
SCHED2
);
[
by
apply
/
exists_inP
;
exists
cpu2
;
last
by
apply
/
eqP

by
apply
/
exists_inP
;
exists
cpu1
;
last
by
apply
/
eqP

intro
SAMEjob
;
subst
].
by
apply
SEQUENTIAL
with
(
j
:=
j0
)
(
t
:=
t
).
}
}
Qed
.
(
*
If
a
job
isn
'
t
scheduled
,
the
processor
are
busy
with
interfering
tasks
.
*
)
Lemma
cpus_busy_with_interfering_tasks
:
forall
(
j
:
JobIn
arr_seq
)
tsk
t
,
job_task
j
=
tsk
>
backlogged
job_cost
sched
j
t
>
count
(
fun
j
:
sporadic_task
=>
is_interfering_task_jlfp
tsk
j
&&
task_is_scheduled
job_task
sched
j
t
)
ts
=
num_cpus
.
Proof
.
rename
H_all_jobs_from_taskset
into
FROMTS
,
H_no_parallelism
into
SEQUENTIAL
,
H_no_intra_task_parallelism
into
NOINTRA
,
H_invariant_holds
into
INV
.
unfold
JLFP_JLDP_scheduling_invariant_holds
in
*
.
intros
j
tsk
t
JOBtsk
BACK
.
rewrite
<
INV
with
(
j
:=
j
)
(
t
:=
t
);
last
by
done
.
assert
(
EQ
:
(
preim
(
fun
j0
:
JobIn
arr_seq
=>
job_task
j0
)
(
fun
j0
:
sporadic_task
=>
is_interfering_task_jlfp
tsk
j0
&&
task_is_scheduled
job_task
sched
j0
t
))
=
1
(
fun
j0
=>
higher_eq_priority
t
j0
j
&&
(
j0
\
in
jobs_scheduled_at
sched
t
))).
{
red
;
intro
j
'
;
unfold
preim
;
simpl
.
destruct
(
j
'
\
in
jobs_scheduled_at
sched
t
)
eqn
:
SCHED
'
.
apply
leq_trans
with
(
n
:=
count
((
higher_eq_priority
t
)
^~
j
)
(
jobs_scheduled_at
sched
t
)).
rewrite
>
INV
with
(
j
:=
j
)
(
t
:=
t
);
[
by
apply
leqnn

by
done
].
apply
leq_trans
with
(
n
:=
count
(
fun
j
:
JobIn
arr_seq
=>
is_interfering_task_jlfp
tsk
(
job_task
j
)
&&
task_is_scheduled
job_task
sched
(
job_task
j
)
t
)
(
jobs_scheduled_at
sched
t
)).
{
rewrite
SCHED
'
.
destruct
(
higher_eq_priority
t
j
'
j
)
eqn
:
HP
'
.
assert
(
SUBST
:
count
((
higher_eq_priority
t
)
^~
j
)
(
jobs_scheduled_at
sched
t
)
=
count
(
fun
x
=>
(
higher_eq_priority
t
x
j
)
&&
(
x
\
in
jobs_scheduled_at
sched
t
))
(
jobs_scheduled_at
sched
t
)).
{
rewrite
andbT
;
apply
/
andP
;
split
.
by
apply
eq_in_count
;
red
;
intros
x
IN
;
rewrite
IN
andbT
.
}
rewrite
SUBST
;
clear
SUBST
.
apply
sub_count
;
red
;
move
=>
j_hp
/
andP
[
HP
IN
].
rewrite
mem_scheduled_jobs_eq_scheduled
in
IN
.
rename
IN
into
SCHED
.
apply
/
andP
;
split
.
{
unfold
is_interfering_task_jlfp
.
destruct
(
j
==
j_hp
)
eqn
:
EQjob
.
{
unfold
is_interfering_task_jlfp
;
apply
/
eqP
;
red
;
intro
BUG
.
subst
tsk
.
(
*
This
requires
further
assumptions
.
*
)
admit
.
move:
EQjob
=>
/
eqP
EQjob
;
subst
.
unfold
backlogged
in
*
.
by
rewrite
SCHED
andbF
in
BACK
.
}
apply
negbT
in
EQjob
.
apply
/
negP
;
unfold
not
;
move
=>
/
eqP
SAMEtsk
.
destruct
(
ltnP
(
job_arrival
j
)
(
job_arrival
j_hp
))
as
[
LTarr

GEarr
].
{
move:
BACK
=>
/
andP
[
PEND
NOTSCHED
].
apply
PREC
with
(
t
:=
t
)
in
LTarr
;
[

by
rewrite
SAMEtsk
JOBtsk

by
done
].
by
rewrite
SCHED
in
LTarr
.
}
subst
tsk
.
exploit
(
SPO
j_hp
j
);
try
(
by
done
).
{
unfold
jobs_scheduled_at
in
*
.
apply
mem_bigcat_ord_exists
in
SCHED
'
;
des
.
apply
/
exists_inP
;
exists
i
;
first
by
done
.
unfold
schedules_job_of_tsk
,
make_sequence
in
*
.
destruct
(
sched
i
t
);
last
by
done
.
by
rewrite
mem_seq1
in
SCHED
'
;
move
:
SCHED
'
=>
/
eqP
EQj
;
subst
.
by
unfold
not
;
intro
BUG
;
subst
;
rewrite
eq_refl
in
EQjob
.
}
intros
INTER
.
exploit
(
PREV
j_hp
SAMEtsk
).
{
apply
leq_trans
with
(
n
:=
job_arrival
j_hp
+
task_period
(
job_task
j_hp
));
last
by
done
.
by
rewrite

addn1
leq_add2l
SAMEtsk
;
des
.
}
intros
COMPLETED
.
have
BUG
:=
COMP
j_hp
t
.
+
1.
rewrite
leqNgt
in
BUG
;
move
:
BUG
=>
/
negP
BUG
;
apply
BUG
.
unfold
service
;
rewrite

addn1
big_nat_recr
?
leq0n
// /=.
apply
leq_add
;
last
by
rewrite
lt0n

not_scheduled_no_service
negbK
.
move:
COMPLETED
=>
/
eqP
COMPLETED
.
by
rewrite

COMPLETED
leqnn
.
}
{
exfalso
;
apply
negbT
in
HP
'
;
move
:
HP
'
=>
/
negP
HP
'
;
apply
HP
'
.
apply
interfering_job_has_higher_eq_prio
;
first
by
done
.
apply
mem_bigcat_ord_exists
in
SCHED
'
;
des
.
unfold
scheduled
,
jobs_scheduled_at
,
make_sequence
in
*
.
apply
/
exists_inP
;
exists
i
;
first
by
done
.
destruct
(
sched
i
t
);
last
by
done
.
by
rewrite
mem_seq1
in
SCHED
'
;
move
:
SCHED
'
=>
/
eqP
EQj
;
subst
.
}
}
{
destruct
(
is_interfering_task_jlfp
tsk
(
job_task
j
'
))
eqn
:
INTERF
'
.
{
rewrite
andTb
SCHED
'
andbF
.
admit
.
(
*
This
requires
further
assumptions
.
*
)
}
{
by
rewrite
SCHED
'
andbF
andFb
.
move:
SCHED
=>
/
exists_inP
SCHED
.
destruct
SCHED
as
[
cpu
INcpu
SCHED
].
move:
SCHED
=>
/
eqP
SCHED
.
apply
/
exists_inP
;
exists
cpu
;
first
by
done
.
by
unfold
schedules_job_of_tsk
;
rewrite
SCHED
.
}
}
}
rewrite

[
count
_
(
jobs_scheduled_at
_
_
)]
size_filter
.
assert
(
SUBST
:
[
seq
j_other
<
jobs_scheduled_at
sched
t

higher_eq_priority
t
j_other
j
]
=
[
seq
j_other
<
jobs_scheduled_at
sched
t

higher_eq_priority
t
j_other
j
&&
(
j_other
\
in
jobs_scheduled_at
sched
t
)]).
{
by
apply
eq_in_filter
;
red
;
intros
x
IN
;
rewrite
IN
andbT
.
}
rewrite
SUBST
;
clear
SUBST
.
rewrite
size_filter
.
rewrite

(
eq_count
EQ
).
rewrite

[
count
_
(
jobs_scheduled_at
_
_
)]
count_filter
.
rewrite

count_filter
.
rewrite

[
count
_
[
seq
_
<
jobs_scheduled_at
_
_

_
]]
count_map
.
apply
/
perm_eqP
.
apply
uniq_perm_eq
;
first
by
apply
filter_uniq
.
{
rewrite
map_inj_in_uniq
;
first
by
apply
filter_uniq
;
apply
scheduled_jobs_unique
.
unfold
jobs_of_same_task_dont_execute_in_parallel
in
NOINTRA
.
red
;
intros
x
y
INx
INy
EQtask
.
apply
NOINTRA
with
(
t
:=
t
);
try
(
by
done
).
have
MAP
:=
count_map
(
fun
(
x
:
JobIn
arr_seq
)
=>
job_task
x
)
(
fun
x
=>
is_interfering_task_jlfp
tsk
x
&&
task_is_scheduled
job_task
sched
x
t
).
rewrite

MAP
;
clear
MAP
.
apply
count_sub_uniqr
.
{
rewrite
mem_filter
in
INx
;
move
:
INx
=>
/
andP
[
_
SCHEDx
].
apply
mem_bigcat_ord_exists
in
SCHEDx
;
destruct
SCHEDx
as
[
cpu
SCHEDx
].
apply
/
existsP
;
exists
cpu
;
apply
/
andP
;
split
;
first
by
done
.
by
unfold
make_sequence
in
SCHEDx
;
destruct
(
sched
cpu
t
);
[
by
rewrite
mem_seq1
eq_sym
in
SCHEDx
;
apply
/
eqP
;
f_equal
;
apply
/
eqP

by
rewrite
in_nil
in
SCHEDx
].
rewrite
map_inj_in_uniq
;
first
by
apply
scheduled_jobs_uniq
.
by
red
;
ins
;
apply
NOINTRA
with
(
t
:=
t
);
rewrite
// mem_scheduled_jobs_eq_scheduled.
}
{
rewrite
mem_filter
in
INy
;
move
:
INy
=>
/
andP
[
_
SCHEDy
].
apply
mem_bigcat_ord_exists
in
SCHEDy
;
destruct
SCHEDy
as
[
cpu
SCHEDy
].
apply
/
existsP
;
exists
cpu
;
apply
/
andP
;
split
;
first
by
done
.
by
unfold
make_sequence
in
SCHEDy
;
destruct
(
sched
cpu
t
);
[
by
rewrite
mem_seq1
eq_sym
in
SCHEDy
;
apply
/
eqP
;
f_equal
;
apply
/
eqP

by
rewrite
in_nil
in
SCHEDy
].
}
}
{
red
;
intro
x
;
apply
/
idP
/
idP
.
{
unfold
task_is_scheduled
in
*
.
intros
IN
;
rewrite
mem_filter
in
IN
;
move
:
IN
=>
/
andP
[
/
exists_inP
SCHED
IN
].
destruct
SCHED
as
[
cpu
INcpu
SCHED
].
generalize
SCHED
;
intro
SCHEDjob
.
unfold
schedules_job_of_tsk
in
SCHEDjob
.
destruct
(
sched
cpu
t
)
as
[
j
'

]
eqn
:
SCHEDj
'
;
last
by
done
.
move:
SCHEDjob
=>
/
eqP
SCHEDjob
;
subst
x
.
apply
/
mapP
;
exists
j
'
;
last
by
done
.
rewrite
mem_filter
;
apply
/
andP
;
split
;
first
by
apply
/
exists_inP
;
exists
cpu
.
unfold
jobs_scheduled_at
.
apply
mem_bigcat_ord
with
(
j
:=
cpu
);
first
by
apply
ltn_ord
.
by
unfold
make_sequence
;
rewrite
SCHEDj
'
mem_seq1
eq_refl
.
}
{
intros
IN
;
rewrite
mem_filter
.
move:
IN
=>
/
mapP
IN
;
destruct
IN
as
[
j
'
IN
];
subst
x
.
rewrite
mem_filter
in
IN
;
move
:
IN
=>
/
andP
[
SCHEDj
'
IN
].
apply
/
andP
;
split
;
first
by
done
.
by
apply
FROMTS
.
red
;
intros
x
IN
.
move:
IN
=>
/
mapP
IN
;
destruct
IN
as
[
j
'
_
EQx
].
by
rewrite
EQx
;
apply
FROMTS
.
}
}
Qed
.
End
BasicLemmas
.
End
JLDP
.
End
JobInvariantAsTaskInvariant
.
End
Lemmas
.
End
SchedulingInvariants
.
...
...
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