Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
P
PROSA  Formally Proven Schedulability Analysis
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
2
Issues
2
List
Boards
Labels
Milestones
Merge Requests
2
Merge Requests
2
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Vedant Chavda
PROSA  Formally Proven Schedulability Analysis
Commits
fbcbb997
Commit
fbcbb997
authored
Dec 02, 2019
by
Björn Brandenburg
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
address spellchecking issues in EDF optimality proof
parent
22a76ba8
Changes
4
Hide whitespace changes
Inline
Sidebyside
Showing
4 changed files
with
74 additions
and
70 deletions
+74
70
restructuring/analysis/facts/transform/edf_opt.v
restructuring/analysis/facts/transform/edf_opt.v
+32
28
restructuring/analysis/facts/transform/replace_at.v
restructuring/analysis/facts/transform/replace_at.v
+17
15
restructuring/analysis/facts/transform/swaps.v
restructuring/analysis/facts/transform/swaps.v
+3
3
restructuring/analysis/transform/edf_trans.v
restructuring/analysis/transform/edf_trans.v
+22
24
No files found.
restructuring/analysis/facts/transform/edf_opt.v
View file @
fbcbb997
...
...
@@ 7,9 +7,9 @@ Require Export rt.restructuring.analysis.facts.readiness.basic.
(** This file contains the main argument of the EDF optimality proof,
starting with an analysis of the individual functions that drive
the
"EDFication" of a given reference schedule and ending with
the proofs of individual properties of the obtained EDF
schedule. *)
the
piecewise transformation of a given reference schedule in an
EDF schedule, and ending with proofs of individual properties of
the obtained EDF
schedule. *)
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require
Import
rt
.
restructuring
.
model
.
processor
.
ideal
.
...
...
@@ 170,7 +170,7 @@ End FindSwapCandidateFacts.
(** In the next section, we analyze properties of [make_edf_at], which
we abbreviate as "
mea
" in the following. *)
we abbreviate as "
[mea]
" in the following. *)
Section
MakeEDFAtFacts
.
(** For any given type of jobs... *)
...
...
@@ 279,13 +279,14 @@ Section MakeEDFAtFacts.
(** Next comes a big step in the optimality proof: we observe that
[make_edf_at] indeed ensures that [EDF_at] holds at time [t_edf] in
sched'
. As this is a larger argument, we proceed by case analysis and
[sched']
. As this is a larger argument, we proceed by case analysis and
first establish a couple of helper lemmas in the following section. *)
Section
GuaranteeCaseAnalysis
.
(** Let j_orig denote the job scheduled in sched at time t_edf, let j_edf
denote the job scheduled in sched' at time t_edf, and let j' denote any
job scheduled in sched' at some time t' after t_edf... *)
(** Let [j_orig] denote the job scheduled in [sched] at time
[t_edf], let [j_edf] denote the job scheduled in [sched'] at
time [t_edf], and let [j'] denote any job scheduled in
[sched'] at some time [t'] after [t_edf]... *)
Variable
j_orig
j_edf
j'
:
Job
.
Variable
t'
:
instant
.
...
...
@@ 295,18 +296,18 @@ Section MakeEDFAtFacts.
Hypothesis
H_sched_edf
:
scheduled_at
sched'
j_edf
t_edf
.
Hypothesis
H_sched'
:
scheduled_at
sched'
j'
t'
.
(** ... and that arrives before time
t_edf
. *)
(** ... and that arrives before time
[t_edf]
. *)
Hypothesis
H_arrival_j'
:
job_arrival
j'
<=
t_edf
.
(** We begin by observing three simple facts that will be used repeatedly in
the case analysis. *)
the case analysis. *)
(** First, the deadline of
j_orig is later than t_edf
. *)
(** First, the deadline of
[j_orig] is later than [t_edf]
. *)
Fact
mea_guarantee_dl_orig
:
t_edf
<
job_deadline
j_orig
.
Proof
.
by
apply
(
scheduled_job_in_sched_has_later_deadline
j_orig
t_edf
H_sched_orig
).
Qed
.
(** Second, by the definition of
sched', j_edf is scheduled in sched at the time
returned by [find_swap_candidate]. *)
(** Second, by the definition of
[sched'], [j_edf] is scheduled in
[sched] at the time
returned by [find_swap_candidate]. *)
Fact
mea_guarantee_fsc_is_j_edf
:
sched
(
find_swap_candidate
sched
t_edf
j_orig
)
=
Some
j_edf
.
Proof
.
move
:
(
H_sched_orig
).
rewrite
scheduled_at_def
=>
/
eqP
SCHED
.
...
...
@@ 317,7 +318,8 @@ Section MakeEDFAtFacts.

by
rewrite
ifT
//
=>
/
eqP
.
Qed
.
(** Third, the deadline of j_edf is no later than the deadline of j_orig. *)
(** Third, the deadline of [j_edf] is no later than the deadline
of [j_orig]. *)
Fact
mea_guarantee_deadlines
:
job_deadline
j_edf
<=
job_deadline
j_orig
.
Proof
.
apply
:
(
fsc_no_later_deadline
sched
_
_
t_edf
)
=>
//.
...
...
@@ 327,11 +329,12 @@ Section MakeEDFAtFacts.
(** With the setup in place, we are now ready to begin the case analysis. *)
(** First, we consider the simpler case where t' is no earlier than the
deadline of j_orig. This case is simpler because t' being no earlier
than j_orig's deadline implies that j' has deadline no earlier than
j_orig (since no scheduled job in sched misses a deadline), which in
turn has a deadline no earlier than j_edf. *)
(** First, we consider the simpler case where [t'] is no earlier
than the deadline of [j_orig]. This case is simpler because
[t'] being no earlier than [j_orig]'s deadline implies that
[j'] has deadline no earlier than [j_orig] (since no scheduled
job in [sched] misses a deadline), which in turn has a
deadline no earlier than [j_edf]. *)
Lemma
mea_guarantee_case_t'_past_deadline
:
job_deadline
j_orig
<=
t'
>
job_deadline
j_edf
<=
job_deadline
j'
.
...
...
@@ 343,8 +346,8 @@ Section MakeEDFAtFacts.
by
apply
ltnW
.
Qed
.
(** Next, we consider the more difficult case, where
t' is before the
deadline of j_orig
. *)
(** Next, we consider the more difficult case, where
[t'] is
before the deadline of [j_orig]
. *)
Lemma
mea_guarantee_case_t'_before_deadline
:
t'
<
job_deadline
j_orig
>
job_deadline
j_edf
<=
job_deadline
j'
.
...
...
@@ 378,8 +381,9 @@ Section MakeEDFAtFacts.
End
GuaranteeCaseAnalysis
.
(** Finally, putting the preceding case analysis together, we obtain the
result that [make_edf_at] establishes [EDF_at] at time [t_edf]. *)
(** Finally, putting the preceding cases together, we obtain the
result that [make_edf_at] establishes [EDF_at] at time
[t_edf]. *)
Lemma
make_edf_at_guarantee
:
EDF_at
sched'
t_edf
.
Proof
.
...
...
@@ 394,8 +398,8 @@ Section MakeEDFAtFacts.
by
apply
:
(
mea_guarantee_case_t'_past_deadline
j_orig
j_edf
j'
t'
).
Qed
.
(** We observe that [make_edf_at] maintains the property that jobs
must arrive
to execute. *)
(** We observe that [make_edf_at] maintains the property that jobs
must arrive
to execute. *)
Lemma
mea_jobs_must_arrive
:
jobs_must_arrive_to_execute
sched'
.
Proof
.
...
...
@@ 535,7 +539,7 @@ Section EDFPrefixFacts.
(** Consider any point in time, denoted [horizon], and... *)
Variable
horizon
:
instant
.
(** ...let [sched'] denote the schedule obtained by
EDFify
ing
(** ...let [sched'] denote the schedule obtained by
transform
ing
[sched] up to the horizon. *)
Let
sched'
:
=
edf_transform_prefix
sched
horizon
.
...
...
@@ 707,8 +711,8 @@ Section EDFPrefixInclusion.
End
EDFPrefixInclusion
.
(** In the following section, we finally establish properties of the
overall
EDFication operation
[edf_transform]. *)
(** In the following section, we finally establish properties of the
overall EDF transformation
[edf_transform]. *)
Section
EDFTransformFacts
.
(** For any given type of jobs... *)
...
...
restructuring/analysis/facts/transform/replace_at.v
View file @
fbcbb997
...
...
@@ 21,12 +21,12 @@ Section ReplaceAtFacts.
(** ...and a replacement state [state]. *)
Variable
nstate
:
PState
.
(** In the following, let
sched'
denote the schedule with replacement at time
(** In the following, let
[sched']
denote the schedule with replacement at time
t'. *)
Let
sched'
:
=
replace_at
sched
t'
nstate
.
(** We begin with the trivial observation that the schedule doesn't change at
other times. *)
other times. *)
Lemma
rest_of_schedule_invariant
:
forall
t
,
t
<>
t'
>
sched'
t
=
sched
t
.
Proof
.
...
...
@@ 36,8 +36,8 @@ Section ReplaceAtFacts.
by
move
/
eqP
in
TT
;
rewrite
TT
in
DIFF
;
contradiction
.
Qed
.
(** As a result, the service in intervals that do not intersect with
t' is
invariant, too. *)
(** As a result, the service in intervals that do not intersect with
[t'] is
invariant, too. *)
Lemma
service_at_other_times_invariant
:
forall
t1
t2
,
t2
<=
t'
\/
t'
<
t1
>
...
...
@@ 54,10 +54,10 @@ Section ReplaceAtFacts.
apply
/
andP
;
by
split
.
Qed
.
(** Next, we consider the amount of service received in intervals
that do span
across the replacement point. We can relate the service received in
the
original and the new schedules by adding the service in the respective
"missing" state... *)
(** Next, we consider the amount of service received in intervals
that do span across the replacement point. We can relate
the
service received in the original and the new schedules by adding
the service in the respective
"missing" state... *)
Lemma
service_delta
:
forall
t1
t2
,
t1
<=
t'
<
t2
>
...
...
@@ 82,10 +82,11 @@ Section ReplaceAtFacts.
service_during
sched
j
t1
t2
+
service_at
sched'
j
t'

service_at
sched
j
t'
.
Proof
.
move
=>
t1
t2
ORDER
j
.
by
rewrite
service_delta
//
addnK
.
Qed
.
(** As another simple invariant (useful for case analysis), we observe that if
a job is scheduled neither in the replaced nor in the new state, then at
any time it receives exactly the same amount of service in the new
schedule with replacements as in the original schedule. *)
(** As another simple invariant (useful for case analysis), we
observe that if a job is scheduled neither in the replaced nor
in the new state, then at any time it receives exactly the same
amount of service in the new schedule with replacements as in
the original schedule. *)
Lemma
service_at_of_others_invariant
(
j
:
Job
)
:
~~
scheduled_in
j
(
sched'
t'
)
>
~~
scheduled_in
j
(
sched
t'
)
>
...
...
@@ 99,9 +100,10 @@ Section ReplaceAtFacts.

rewrite
rest_of_schedule_invariant
//.
Qed
.
(** Based on the previous observation, we can trivially lift the invariant
that jobs not involved in the replacement receive equal service to the
cumulative service received in any interval. *)
(** Based on the previous observation, we can trivially lift the
invariant that jobs not involved in the replacement receive
equal service to the cumulative service received in any
interval. *)
Corollary
service_during_of_others_invariant
(
j
:
Job
)
:
~~
scheduled_in
j
(
sched'
t'
)
>
~~
scheduled_in
j
(
sched
t'
)
>
...
...
restructuring/analysis/facts/transform/swaps.v
View file @
fbcbb997
...
...
@@ 295,11 +295,11 @@ Section SwappedScheduleProperties.
Hypothesis
H_order
:
t1
<=
t2
.
(** We let [sched'] denote the schedule in which the allocations at
[t1] and [t2] have been swapped. *)
[t1] and [t2] have been swapped. *)
Let
sched'
:
=
swapped
sched
t1
t2
.
(** First, we observe that if jobs never acc
o
mulate more service than
required, then that's still the case after the swap. *)
(** First, we observe that if jobs never acc
u
mulate more service than
required, then that's still the case after the swap. *)
Lemma
swapped_service_bound
:
(
forall
j
t
,
service
sched
j
t
<=
job_cost
j
)
>
(
forall
j
t
,
service
sched'
j
t
<=
job_cost
j
).
...
...
restructuring/analysis/transform/edf_trans.v
View file @
fbcbb997
Require
Export
rt
.
restructuring
.
analysis
.
transform
.
prefix
.
Require
Export
rt
.
restructuring
.
analysis
.
transform
.
swap
.
(** In this file we define the "EDFification" of a schedule, the
operation at the core of the EDF optimality proof. *)
(** In this file we define the EDF transformation of a schedule, which turns a
(finite prefix of a) schedule into an EDF schedule. This operation is at
the core of the EDF optimality proof. *)
Section
EDFTransformation
.
(** Consider any given type of jobs... *)
...
...
@@ 12,37 +13,34 @@ Section EDFTransformation.
Let
PState
:
=
ideal
.
processor_state
Job
.
Let
SchedType
:
=
schedule
(
PState
).
(** We say that a state s1 "has an earlier or equal deadline" than a
state s2 if the job scheduled in state s1 has has an earlier or
equal deadline than the job scheduled in state s2. This function
is never used on idle states, so the default values are
irrelevant. *)
(** We say that a state [s1] "has an earlier or equal deadline" than a state
[s2] if the job scheduled in state [s1] has has an earlier or equal
deadline than the job scheduled in state [s2]. This function is never
used on idle states, so the default values are irrelevant. *)
Definition
earlier_deadline
(
s1
s2
:
PState
)
:
=
(
oapp
job_deadline
0
s1
)
<=
(
oapp
job_deadline
0
s2
).
(** We say that a state is relevant (for the purpose of the
transformation) if it is not idle and if the job scheduled in it
has arrived prior to
some given reference time. *)
(** We say that a state is relevant (for the purpose of the
transformation)
if it is not idle and if the job scheduled in it has arrived prior to
some given reference time. *)
Definition
relevant_pstate
(
reference_time
:
instant
)
(
s
:
PState
)
:
=
match
s
with

None
=>
false

Some
j'
=>
job_arrival
j'
<=
reference_time
end
.
(** Next, we define a central element of the "EDFification"
procedure: given a job scheduled at a time t1, find a later time
t2 before the job's deadlineat which a job with an
earlierorequal deadline is scheduled. In other words, find a
job that causes the [EDF_at] property to be violated at time
t1. *)
(** Next, we define a central element of the EDF transformation procedure:
given a job scheduled at a time [t1], find a later time [t2] before the
job's deadline at which a job with an earlierorequal deadline is
scheduled. In other words, find a job that causes the [EDF_at] property
to be violated at time [t1]. *)
Definition
find_swap_candidate
(
sched
:
SchedType
)
(
t1
:
instant
)
(
j
:
Job
)
:
=
if
search_arg
sched
(
relevant_pstate
t1
)
earlier_deadline
t1
(
job_deadline
j
)
is
Some
t
then
t
else
0
.
(** The pointwise EDFification procedure: given a schedule and a
time t1, ensure that the schedule satisfies [EDF_at] at time
t1. *)
(** The pointwise EDF transformation procedure: given a schedule and a time
[t1], ensure that the schedule satisfies [EDF_at] at time [t1]. *)
Definition
make_edf_at
(
sched
:
SchedType
)
(
t1
:
instant
)
:
SchedType
:
=
match
sched
t1
with

None
=>
sched
(* leave idle instants alone *)
...
...
@@ 53,14 +51,14 @@ Section EDFTransformation.
end
.
(** To transform a finite prefix of a given reference schedule, apply
[make_edf_at] to every point up to the given finite horizon. *)
[make_edf_at] to every point up to the given finite horizon. *)
Definition
edf_transform_prefix
(
sched
:
SchedType
)
(
horizon
:
instant
)
:
SchedType
:
=
prefix_map
sched
make_edf_at
horizon
.
(** Finally, a full EDF schedule (i.e., one that satisfies [EDF_at]
at any time) is obtained by first computing an EDF prefix up to
and including the requested time t, and by then looking at
the
last point of the
prefix. *)
(** Finally, a full EDF schedule (i.e., one that satisfies [EDF_at]
at any
time) is obtained by first computing an EDF prefix up to and including
the requested time [t], and by then looking at the last point of
the
prefix. *)
Definition
edf_transform
(
sched
:
SchedType
)
(
t
:
instant
)
:
ideal
.
processor_state
Job
:
=
let
edf_prefix
:
=
edf_transform_prefix
sched
t
.+
1
...
...
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