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
RTPROOFS
PROSA  Formally Proven Schedulability Analysis
Commits
0f810f31
Commit
0f810f31
authored
Mar 24, 2022
by
Marco Maida
🌱
Browse files
Clean, polish
parent
fe5b0fdf
Pipeline
#63828
failed with stages
in 1 minute and 28 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Sidebyside
implementation/facts/ideal_uni/preemption_aware.v
View file @
0f810f31
...
...
@@ 110,12 +110,25 @@ Section NPUniprocessorScheduler.
sequence and only ready jobs are scheduled. *)
Section
Validity
.
(** Any reasonable job selection policy will not create jobs "out of thin
air," i.e., if a job is selected, it was among those given to choose
from. *)
Hypothesis
H_chooses_from_set
:
forall
t
s
j
,
choose_job
t
s
=
Some
j
>
j
\
in
s
.
(** First, any reasonable job selection policy will not create jobs "out
of thin air," i.e., if a job is selected, it was among those given
to choose from. *)
Hypothesis
H_chooses_from_set
:
forall
t
s
j
,
choose_job
t
s
=
Some
j
>
j
\
in
s
.
(** Second, for the schedule to be valid, we require the notion of readiness
to be consistent with the preemption model: a nonpreemptive job remains
ready until (at least) the end of its current nonpreemptive section. *)
Hypothesis
H_valid_preemption_behavior
:
valid_nonpreemptive_readiness
RM
schedule
.
(** Finally, we assume the readiness model to be nonclairvoyant. *)
Hypothesis
H_nonclairvoyant_readiness
:
nonclairvoyant_readiness
RM
.
(** For brevity, we define the notion of the prefix of the schedule. *)
Let
sched_prefix
t
:
=
if
t
is
t'
.+
1
then
schedule_up_to
policy
None
t'
else
empty_schedule
None
.
(** We begin by showing that any job in the schedule must come from the arrival
sequence used to generate it. *)
Lemma
np_schedule_jobs_from_arrival_sequence
:
jobs_come_from_arrival_sequence
schedule
arr_seq
.
Proof
.
...
...
@@ 131,16 +144,8 @@ Section NPUniprocessorScheduler.
by
apply
backlogged_job_arrives_in
.
Qed
.
(*** NEW STUFF ***)
Let
sched_prefix
t
:
=
if
t
is
t'
.+
1
then
schedule_up_to
policy
None
t'
else
empty_schedule
None
.
Hypothesis
H_nonclairvoyant_readiness
:
nonclairvoyant_readiness
RM
.
(** Next, we show that any job selected by the job selection policy must
be ready. *)
Theorem
chosen_job_is_ready
:
forall
j
t
,
choose_job
t
(
jobs_backlogged_at
arr_seq
(
sched_prefix
t
)
t
)
==
Some
j
>
...
...
@@ 157,31 +162,22 @@ Section NPUniprocessorScheduler.
rewrite

schedule_up_to_def
.
by
apply
schedule_up_to_prefix_inclusion
.
Qed
.
Theorem
jobs_must_be_ready
:
(** Starting from the previous result we show that, at any instant, only
a ready job can be scheduled. *)
Theorem
jobs_must_be_ready
:
jobs_must_be_ready_to_execute
schedule
.
Proof
.
move
=>
j
t
SCHED
.
rewrite
scheduled_at_def
in
SCHED
.
rewrite
/
schedule
/
uni_schedule
/
np_uni_schedule
in
SCHED
.
rewrite
/
allocation_at
/
generic_schedule
in
SCHED
.
rewrite
schedule_up_to_def
//=
in
SCHED
.
rewrite
scheduled_at_def
/
schedule
/
uni_schedule
/
np_uni_schedule
/
allocation_at
/
generic_schedule
schedule_up_to_def
//=
in
SCHED
.
destruct
(
prev_job_nonpreemptive
_
)
eqn
:
PREV
.
{
destruct
t
=>
//.
rewrite
//=
in
SCHED
,
PREV
.
{
destruct
t
=>
//
;
rewrite
//=
in
SCHED
,
PREV
.
destruct
(
schedule_up_to
)
=>
//.
move
:
PREV
=>
/
andP
[
READY
_
].
move
:
SCHED
=>
/
eqP
SCHED
.
injection
SCHED
=>
EQ
;
rewrite
>
EQ
in
*.
rewrite
(
H_nonclairvoyant_readiness
_
(
schedule_up_to
(
fun
(
sched_prefix
:
schedule
.
schedule
(
processor_state
Job
))
(
t
:
instant
)
=>
if
prev_job_nonpreemptive
sched_prefix
t
then
sched_prefix
t
.
1
else
choose_job
t
(
jobs_backlogged_at
arr_seq
sched_prefix
t
))
None
t
)
j
t
.+
1
)
//=.
erewrite
(
H_nonclairvoyant_readiness
_
_
j
t
.+
1
)
;
[
by
apply
READY


by
done
].
move
=>
t'
LT
.
rewrite
/
schedule
/
np_uni_schedule
/
generic_schedule
//=.
rewrite
/
allocation_at
//=.
...
...
@@ 189,40 +185,18 @@ Section NPUniprocessorScheduler.
{
by
apply
chosen_job_is_ready
.
}
Qed
.
(***  ***)
(** For the schedule to be valid, we require the notion of readiness to be
consistent with the preemption model: a nonpreemptive job remains
ready until (at least) the end of its current nonpreemptive
section. *)
Hypothesis
H_valid_preemption_behavior
:
valid_nonpreemptive_readiness
RM
schedule
.
(** First, we show that if a job is chosen from the list of backlogged jobs, then it must be ready. *)
Lemma
choose_job_implies_job_ready
:
forall
t
j
,
choose_job
t
.+
1
(
jobs_backlogged_at
arr_seq
(
schedule_up_to
policy
idle_state
t
)
t
.+
1
)
=
Some
j
>
job_ready
schedule
j
t
.+
1
.
Proof
.
move
=>
t
j
IN
.
move
:
(
H_chooses_from_set
_
_
_
IN
).
rewrite
mem_filter
/
backlogged
=>
/
andP
[/
andP
[
READY
_
]
_
].
rewrite
(
H_nonclairvoyant_job_readiness
(
schedule_up_to
policy
idle_state
t
)
schedule
j
t
.+
1
)
//.
by
apply
schedule_up_to_identical_prefix
.
Qed
.
(** Next, we show that, under these natural assumptions, the generated schedule is valid. *)
(** Finally, we show that the generated schedule is valid. *)
Theorem
np_schedule_valid
:
valid_schedule
schedule
arr_seq
.
Proof
.
rewrite
/
valid_schedule
;
split
;
first
by
apply
np_schedule_jobs_from_arrival_sequence
.
move
=>
j
t
;
rewrite
scheduled_at_def
/
schedule
/
np_uni_schedule
/
generic_schedule
.
elim
:
t
=>
[/
eqP

t'
IH
/
eqP
].

rewrite
schedule_up_to_def
/
allocation_at
/
prev_job_nonpreemptive
=>
IN
.
{
rewrite
schedule_up_to_def
/
allocation_at
/
prev_job_nonpreemptive
=>
IN
.
move
:
(
H_chooses_from_set
_
_
_
IN
).
rewrite
mem_filter
/
backlogged
=>
/
andP
[/
andP
[
READY
_
]
_
].
now
rewrite
(
H_nonclairvoyant_job_readiness
(
empty_schedule
idle_state
)
schedule
j
0
).

rewrite
schedule_up_to_def
/
allocation_at
/
prev_job_nonpreemptive
.
now
rewrite
(
H_nonclairvoyant_job_readiness
(
empty_schedule
idle_state
)
schedule
j
0
).
}
{
rewrite
schedule_up_to_def
/
allocation_at
/
prev_job_nonpreemptive
.
have
JOB
:
choose_job
t'
.+
1
(
jobs_backlogged_at
arr_seq
(
schedule_up_to
policy
idle_state
t'
)
t'
.+
1
)
=
Some
j
>
job_ready
schedule
j
t'
.+
1
.
...
...
@@ 243,7 +217,7 @@ Section NPUniprocessorScheduler.
apply
equal_prefix_implies_same_service_during
=>
t
/
andP
[
_
BOUND
].
now
rewrite
(
schedule_up_to_prefix_inclusion
_
_
t
t'
).
rewrite
//=.
by
move
=>
/
andP
[?
?].
by
move
=>
/
andP
[?
?].
}
Qed
.
End
Validity
.
...
...
@@ 294,41 +268,6 @@ Section NPUniprocessorScheduler.
End
PreemptionTimes
.
(** Finally, we establish the main feature: the generated schedule respects
the preemptionmodel semantics. *)
Section
PreemptionCompliance
.
(** As a minimal validity requirement (which is a part of
[valid_preemption_model]), we require that any job in [arr_seq] must
start execution to become nonpreemptive. *)
Hypothesis
H_valid_preemption_function
:
forall
j
,
arrives_in
arr_seq
j
>
job_cannot_become_nonpreemptive_before_execution
j
.
(*
(** Given such a valid preemption model, we establish that the generated
schedule indeed respects the preemption model semantics. *)
Lemma np_respects_preemption_model :
schedule_respects_preemption_model arr_seq schedule.
Proof.
move=> j.
elim => [ t' IH]; first by rewrite service0 => ARR /negP NP; move: (H_valid_preemption_function j ARR).
move=> ARR NP.
have: scheduled_at schedule j t'.
{ apply contraT => NOT_SCHED.
move: (not_scheduled_implies_no_service _ _ _ NOT_SCHED) => NO_SERVICE.
rewrite (service_last_plus_before) NO_SERVICE addn0 in NP; apply IH in NP => //.
by move /negP in NOT_SCHED. }
rewrite !scheduled_at_def /schedule/np_uni_schedule/generic_schedule => /eqP SCHED.
rewrite SCHED (schedule_up_to_prefix_inclusion _ _ t' t'.+1) // np_job_remains_scheduled //.
rewrite /prev_job_nonpreemptive SCHED (identical_prefix_service _ schedule) //.
by apply schedule_up_to_identical_prefix.
Qed.
*)
End
PreemptionCompliance
.
End
NPUniprocessorScheduler
.
Write
Preview
Supports
Markdown
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