Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
FP
Stacked Borrows Coq
Commits
fdfe3232
Commit
fdfe3232
authored
Oct 09, 2019
by
Hai Dang
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
fix README
parent
151d4e46
Changes
2
Hide whitespace changes
Inline
Sidebyside
Showing
2 changed files
with
99 additions
and
56 deletions
+99
56
README.md
README.md
+99
56
appendix.pdf
appendix.pdf
+0
0
No files found.
README.md
View file @
fdfe3232
# STACKED BORROWS  ARTIFACT
## Technical Appendix
The technical appendix in
`appendix.pdf`
contains a complete coherent
description of the Stacked Borrows semantics, as well as the definition of our
key simulation relation that we used for the Coq formalization.
## Rust Counterexamples and Miri
You can run the counterexamples from the paper in Rust by clicking the following links, and then selecting "Run".
You can also run them in Miri via "Tools"  "Miri", which will show a Stacked Borrows violation.
*
[
`example1`
](
https://play.rustlang.org/?version=stable&mode=release&edition=2018&gist=18e6931728976779452f0d489f59a71c
)
*
[
`example2`
](
https://play.rustlang.org/?version=stable&mode=release&edition=2018&gist=85f368db00a789caa08e2b6960ebaf01
)
*
[
`example2_down`
](
https://play.rustlang.org/?version=stable&mode=release&edition=2018&gist=66c928ddf745a779272a73262b921a56
)
## Coq Formalization
We have given informal proof sketches of optimizations based on Stacked Borrows
in the paper. To further increase confidence in the semantics, we formalized
these arguments in Coq (about 14KLOC). We have carried out the proofs of the
transformations mentioned in the paper:
`example1`
,
`example2`
,
`example2_down`
,
`example3_down`
; as well as two more variants to complete the picture,
`example1_down`
and
`example3`
.
## HOW TO START
###
What to look for
###
# Use a VM
The directory structure is as follows:
*
`theories/lang`
: Definitions and properties of the language.

The language syntax is defined in
`lang/lang_base.v`
.

The expression and heap semantics is defined in
`lang/expr_semantics.v`
.

The semantics of Stacked Borrows itself is in
`lang/bor_semantics.v`
.

The complete language is then combined in
`lang/lang.v`
.
*
`theories/sim`
: The simulation framework and its adequacy proofs.

The local simulation definition is in
`sim/local.v`
.

It is then lifted up to the global simulation definition in
`sim/global.v`
.

Adequacy (that the simulation implies behavior inclusion) is in
`sim/local_adequacy.v`
,
`sim/global_adequacy.v`
, and
`sim/program.v`
.

Properties of the simulation with respect to the operational semantics are
proven in
`sim/body.v`
,
`sim/refl_pure_step.v`
,
`sim/refl_mem_step.v`
,
`sim/left_step.v`
,
`sim/right_step.v`
.

The main invariant needed for these properties is defined in
`sim/invariant.v`
.

In
`sim/simple.v`
, we define an easiertouse but less powerful derived simulation relation.

The fundamental property that the simulation is reflexive for wellformed terms is proven in
`sim/refl.v`
.
*
`theories/opt`
: Proofs of optimizations.
For example, `theories/opt/ex1.v` provides the proof that the optimized
program refines the behavior of the unoptimized program, where the optimized
program simply replaces the unoptimized one's `ex1_unopt` function with the
`ex1_opt` function.
For this proof, we need to show that (1) `ex1_opt` refines `ex1_unopt`, and (2) all other unchanged functions refine themselves.
The proof of (1) is in the Lemma `ex1_sim_fun`.
The proof of (2) is the reflexivity of our simulation relation for wellformed programs, provided in `theories/sim/refl.v`.
A VM that comes with precompiled sources is provided, so that you can start the inspection immediately.

For
`example1`
(Section 3.4 in the paper), see
`opt/ex1.v`
;
`example1_down`
did not appear in the paper but we verified it in
`opt/ex1_down.v`
.

For
`example2`
(Section 3.6) and
`example2_down`
(Section 4), see
`opt/ex2.v`
and
`opt/ex2_down.v`
, respectively.

For
`example3_down`
(Section 4), see
`opt/ex3_down.v`
;
`example3`
did not appear in the paper but we verified it in
`opt/ex3.v`
.
### How to build
*
[
artifact.ova
](
artifact.ova
)
can be imported in to VirtualBox.
Please give it at least 4GB of RAM.
*
The username/password are both
`artifact`
. After logging in with
`artifact`
,
please navigate to
`~/sources`
for the precompiled Coq sources.
*
The VM is a minimal Debian 10, preinstalled with
`coq`
and
`coqide`
8.9.1.
If you want to install extra packages, the
`root`
password is also
`artifact`
(please use
`su`
as
`sudo`
is not installed).
#### Build dependencies (via opam)
...
...
@@ 86,3 +40,92 @@ See the [opam](opam) file for the exact versions you need.
Once the dependencies are installed, you can
`make jN`
the development,
replacing
`N`
by the number of your CPU cores.
#### Rebuild
If you do not trust the precompiled results, you can use
`make clean`
to remove
them and follow the build instructions above to rebuild.
## Technical Appendix
The technical [appendix] contains a complete coherent
description of the Stacked Borrows semantics, as well as the definition of our
key simulation relation that we used for the Coq formalization.
## Rust Counterexamples and Miri
You can run the counterexamples from the paper in Rust by clicking the following links, and then selecting "Run".
You can also run them in Miri via "Tools"  "Miri", which will show a Stacked Borrows violation.
*
[
`example1`
](
https://play.rustlang.org/?version=stable&mode=release&edition=2018&gist=18e6931728976779452f0d489f59a71c
)
(Section 3.4 of the paper)
*
[
`example2`
](
https://play.rustlang.org/?version=stable&mode=release&edition=2018&gist=85f368db00a789caa08e2b6960ebaf01
)
(Section 3.6)
*
[
`example2_down`
](
https://play.rustlang.org/?version=stable&mode=release&edition=2018&gist=66c928ddf745a779272a73262b921a56
)
(Section 4)
## Coq Formalization
We have given informal proof sketches of optimizations based on Stacked Borrows
in the paper. To further increase confidence in the semantics, we formalized
these arguments in Coq (about 14KLOC). We have carried out the proofs of the
transformations mentioned in the paper:
`example1`
,
`example2`
,
`example2_down`
,
`example3_down`
; as well as two more variants to complete the picture,
`example1_down`
and
`example3`
.
### STRUCTURE
The directory structure is as follows:
*
[
theories/lang
](
theories/lang
)
: Definitions and properties of the language.

The language syntax is defined in
[
lang/lang_base.v
](
theories/lang/lang_base.v
)
.

The expression and heap semantics is defined in
[
lang/expr_semantics.v
](
theories/lang/expr_semantics.v
)
.

The semantics of Stacked Borrows itself is in
[
lang/bor_semantics.v
](
theories/lang/bor_semantics.v
)
.

The complete language is then combined in
[
lang/lang.v
](
theories/lang/lang.v
)
.
*
[
theories/sim
](
theories/sim
)
: The simulation framework and its adequacy proofs.

The
*local*
simulation definition is in
[
sim/local.v
](
theories/sim/local.v
)
.

It is then lifted up to the
*global*
simulation definition in
[
sim/global.v
](
theories/sim/global.v
)
.

Adequacy, which states that the simulation implies behavior inclusion, is in
[
sim/local_adequacy.v
](
theories/sim/local_adequacy.v
)
,
[
sim/global_adequacy.v
](
theories/sim/global_adequacy.v
)
,
[
sim/program.v
](
theories/sim/program.v
)
.

Properties of the simulation with respect to the operational semantics are
proven in
[
sim/body.v
](
theories/sim/body.v
)
,
[
sim/refl_pure_step.v
](
theories/sim/refl_pure_step.v
)
,
[
sim/refl_mem_step.v
](
theories/sim/refl_mem_step.v
)
,
[
sim/left_step.v
](
theories/sim/left_step.v
)
,
[
sim/right_step.v
](
theories/sim/right_step.v
)
.

The main invariant needed for these properties is defined in
[
sim/invariant.v
](
theories/sim/invariant.v
)
. The invariant is properly
typesetted in Section 2 of the technical [appendix].

In
[
sim/simple.v
](
theories/sim/simple.v
)
, we define an easiertouse but
less powerful derived simulation relation.

The fundamental property that the simulation is reflexive for wellformed
terms is proven in
[
sim/refl.v
](
theories/sim/refl.v
)
.
*
[
theories/opt
](
theories/opt
)
: Proofs of optimizations.
For example, [opt/ex1.v](theories/opt/ex1.v) provides the proof that the
optimized program refines the behavior of the unoptimized program, where the
optimized program simply replaces the unoptimized one's `ex1_unopt` function
with the `ex1_opt` function.
For this proof, we need to show that (1) `ex1_opt` refines `ex1_unopt`, and
(2) all other unchanged functions refine themselves.
The proof of (1) is in the Lemma `ex1_sim_fun`.
The proof of (2) is the reflexivity of our simulation relation for
wellformed programs, provided in [theories/sim/refl.v](theories/sim/refl.v).

For
`example1`
(Section 3.4 in the paper),
see
[
opt/ex1.v
](
theories/opt/ex1.v
)
;
`example1_down`
did not appear in the paper but we verified it in
[
opt/ex1_down.v
](
theories/opt/ex1_down.v
)
.

For
`example2`
(Section 3.6) and
`example2_down`
(Section 4),
see
[
opt/ex2.v
](
theories/opt/ex2.v
)
and
[
opt/ex2_down.v
](
theories/opt/ex2_down.v
)
, respectively.

For
`example3_down`
(Section 4), see
[
opt/ex3_down.v
](
theories/opt/ex3_down.v
)
;
`example3`
did not appear in the paper but we verified it in
[
opt/ex3.v
](
theories/opt/ex3.v
)
.
[
appendix
]:
appendix.pdf
appendix.pdf
0 → 100644
View file @
fdfe3232
File added
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