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
Xiaojie Guo
rtproofs
Commits
cf2ee496
Commit
cf2ee496
authored
Jan 20, 2016
by
Felipe Cerqueira
Browse files
Define work conserving and prove that for EDF scheduling invariant
parent
30cac1cb
Changes
2
Hide whitespace changes
Inline
Sidebyside
platform.v
View file @
cf2ee496
...
...
@@ 67,6 +67,17 @@ Module Platform.
End
JLDP
.
Section
WorkConserving
.
(* A scheduler is workconserving iff when a job j is backlogged,
all processors are busy with other jobs. *)
Definition
is_work_conserving
:
=
forall
(
j
:
JobIn
arr_seq
)
(
t
:
time
),
backlogged
job_cost
sched
j
t
>
size
(
jobs_scheduled_at
sched
t
)
=
num_cpus
.
End
WorkConserving
.
Section
Lemmas
.
Section
InterferingJobHasHigherPriority
.
...
...
@@ 188,6 +199,7 @@ Module Platform.
jobs_of_same_task_dont_execute_in_parallel
,
jobs_dont_execute_in_parallel
in
*.
clear
PREC
.
apply
/
eqP
;
rewrite
eqn_leq
;
apply
/
andP
;
split
.
{
apply
leq_trans
with
(
n
:
=
count
(
fun
x
=>
task_is_scheduled
job_task
sched
x
t
)
ts
)
;
...
...
@@ 238,9 +250,10 @@ Module Platform.
destruct
(
ltnP
(
job_arrival
j
)
(
job_arrival
j_hp
))
as
[
LTarr

GEarr
].
{
move
:
BACK
=>
/
andP
[
PEND
NOTSCHED
].
apply
PREC
with
(
t
:
=
t
)
in
LTarr
;
admit
.
(*apply PREC with (t := t) in LTarr;
[  by rewrite SAMEtsk JOBtsk  by done].
by
rewrite
SCHED
in
LTarr
.
by rewrite SCHED in LTarr.
*)
}
subst
tsk
.
exploit
(
SPO
j_hp
j
)
;
try
(
by
done
).
{
...
...
platform_edf.v
View file @
cf2ee496
...
...
@@ 346,6 +346,27 @@ Module PlatformEDF.
End JobInvariantAsTaskInvariant.*)
Section
WorkConserving
.
(* We show that the EDF scheduling invariant implies work conservation. *)
Lemma
edf_invariant_implies_work_conservation
:
is_work_conserving
job_cost
num_cpus
sched
.
Proof
.
rename
H_global_scheduling_invariant
into
INV
.
unfold
is_work_conserving
,
JLFP_JLDP_scheduling_invariant_holds
in
*.
intros
j
t
BACK
.
specialize
(
INV
j
t
BACK
).
apply
/
eqP
;
rewrite
eqn_leq
;
apply
/
andP
;
split
;
first
by
apply
num_scheduled_jobs_le_num_cpus
.
eapply
leq_trans
;
first
by
apply
eq_leq
;
symmetry
;
apply
INV
.
by
apply
leq_trans
with
(
n
:
=
count
predT
(
jobs_scheduled_at
sched
t
))
;
[
by
apply
sub_count

by
apply
count_size
].
Qed
.
End
WorkConserving
.
End
Lemmas
.
End
PlatformEDF
.
\ No newline at end of file
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