README.md 5.98 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2
# STACKED BORROWS - ARTIFACT

Hai Dang's avatar
Hai Dang committed
3
## HOW TO START
Hai Dang's avatar
Hai Dang committed
4

Hai Dang's avatar
Hai Dang committed
5
#### Use a VM
Hai Dang's avatar
Hai Dang committed
6

Hai Dang's avatar
Hai Dang committed
7
A VM that comes with pre-compiled sources is provided, so that you can start the inspection immediately.
Hai Dang's avatar
Hai Dang committed
8

Hai Dang's avatar
Hai Dang committed
9 10 11 12 13 14 15
* [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 pre-compiled Coq sources.
* The VM is a minimal Debian 10, pre-installed 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).
Ralf Jung's avatar
Ralf Jung committed
16 17 18

#### Build dependencies (via opam)

Hai Dang's avatar
Hai Dang committed
19 20 21 22 23 24 25 26 27
The easiest way to install the correct versions of the dependencies is through
opam (1.2.2 or newer).  You will need the Coq and Iris opam repositories:

    opam repo add coq-released https://coq.inria.fr/opam/released
    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.

Hai Dang's avatar
Hai Dang committed
28 29 30
If opam fails, it is very likely that the required packages were not found.
Run `opam update` to update your opam package registry.

Ralf Jung's avatar
Ralf Jung committed
31
#### Build dependencies (manual installation)
Hai Dang's avatar
Hai Dang committed
32 33

Otherwise, you need to build and install the following dependencies yourself.
Ralf Jung's avatar
Ralf Jung committed
34
See the [opam](opam) file for the exact versions you need.
Hai Dang's avatar
Hai Dang committed
35
- Iris
Hai Dang's avatar
Hai Dang committed
36
- Paco
Hai Dang's avatar
Hai Dang committed
37
- Equations
Ralf Jung's avatar
Ralf Jung committed
38 39 40 41 42

#### Build

Once the dependencies are installed, you can `make -jN` the development,
replacing `N` by the number of your CPU cores.
Hai Dang's avatar
Hai Dang committed
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131

#### 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.rust-lang.org/?version=stable&mode=release&edition=2018&gist=18e6931728976779452f0d489f59a71c)
  (Section 3.4 of the paper)
* [`example2`](https://play.rust-lang.org/?version=stable&mode=release&edition=2018&gist=85f368db00a789caa08e2b6960ebaf01)
  (Section 3.6)
* [`example2_down`](https://play.rust-lang.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
    type-setted in Section 2 of the technical [appendix].
  - In [sim/simple.v](theories/sim/simple.v), we define an easier-to-use but
    less powerful derived simulation relation.
  - The fundamental property that the simulation is reflexive for well-formed
    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
    well-formed 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