README.md 3.08 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1
# GhostCell: Separating Permissions from Data in Rust
Ralf Jung's avatar
Ralf Jung committed
2

Ralf Jung's avatar
Ralf Jung committed
3
This is the artifact accompanying our paper.
Ralf Jung's avatar
Ralf Jung committed
4
5
6
7
It consists of two parts: a Rust implementation with examples and benchmarks, and a Coq proof.

# Rust implementation

8
9
10
To build and run the Rust code, you will need to
[install cargo](https://doc.rust-lang.org/stable/cargo/getting-started/installation.html).

Hai Dang's avatar
Hai Dang committed
11
12
13
14
15
16
17
18
19
20

## Source code and Benchmarks

The source code for `GhostCell` and for the benchmarks that we ran can be found in [`ghostcell`].
The `GhostCell` code is in [`ghostcell/src/lib.rs`](ghostcell/src/lib.rs), the benchmarks are in [`ghostcell/benches/dlist.rs`](ghostcell/benches/dlist.rs).

The benchmark results are in [`benchmarks-data`](benchmarks-data); open [`report/index.html`](benchmarks-data/report/index.html) in a browser to view them.
You can run the benchmarks again from the [`ghostcell`] directory with the command `cargo bench`.
You can filter benchmarks to run by keywords, for example `cargo bench "ghostcell"` will run all GhostCell benchmarks.

Ralf Jung's avatar
Ralf Jung committed
21
## Examples
Ralf Jung's avatar
Ralf Jung committed
22

Hai Dang's avatar
Hai Dang committed
23
The Rust examples in the paper can be found in [`ghostcell/examples/`](ghostcell/examples/).
Hai Dang's avatar
Hai Dang committed
24
More specifically:
Hai Dang's avatar
Hai Dang committed
25
- For Section 2, see [`branded_vec.rs`](ghostcell/examples/branded_vec.rs).
Hai Dang's avatar
Hai Dang committed
26
27
28
29
- For Section 3, see [`dlist_arena_paper.rs`](ghostcell/examples/dlist_arena_paper.rs).
  The doubly-linked list API and implementation is in [`ghostcell/src/dlist_arena.rs`](ghostcell/src/dlist_arena.rs).
- [`dlist_arc.rs`](ghostcell/examples/dlist_arc.rs) contains an example using a doubly-linked list built with `GhostCell` and `Arc`.
  The implementation is in [`ghostcell/src/dlist_arc.rs`](ghostcell/src/dlist_arc.rs)
Hai Dang's avatar
Hai Dang committed
30

Hai Dang's avatar
Hai Dang committed
31
To run an example, use `cargo run --example branded_vec` from the [`ghostcell`] directory.
Hai Dang's avatar
Hai Dang committed
32

Ralf Jung's avatar
Ralf Jung committed
33
34
# Coq proof

Hai Dang's avatar
Hai Dang committed
35
Our Coq proof is based on the [RustBelt formalization](https://gitlab.mpi-sws.org/iris/lambda-rust).
Ralf Jung's avatar
Ralf Jung committed
36

Hai Dang's avatar
Hai Dang committed
37
38
39
40
## Where to find the proofs

- The `BrandedVec` soundness proof is in [`theories/typing/lib/brandedvec.v`](theories/typing/lib/brandedvec.v).
- The `GhostCell` soundness proof is in [`theories/typing/lib/ghostcell.v`](theories/typing/lib/ghostcell.v).
Ralf Jung's avatar
Ralf Jung committed
41
- The new version of the "lifetime equalization" rule is `type_equivalize_lft` in [`theories/typing/programs.v`](theories/typing/programs.v).
Hai Dang's avatar
Hai Dang committed
42

Ralf Jung's avatar
Ralf Jung committed
43
44
45
46
## Prerequisites

This version is known to compile with:

Hai Dang's avatar
Hai Dang committed
47
 - Coq 8.11.2
Hai Dang's avatar
Hai Dang committed
48
 - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris) (see the [`opam`](opam) file for the exact version).
Ralf Jung's avatar
Ralf Jung committed
49

Ralf Jung's avatar
Ralf Jung committed
50
51
## Building from source

Hai Dang's avatar
Hai Dang committed
52
When building from source, we recommend to use opam (2.0.0 or newer) for
Ralf Jung's avatar
Ralf Jung committed
53
installing the dependencies.  This requires the following two repositories:
Ralf Jung's avatar
Ralf Jung committed
54

Ralf Jung's avatar
README    
Ralf Jung committed
55
    opam repo add coq-released https://coq.inria.fr/opam/released
Hai Dang's avatar
Hai Dang committed
56
    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Ralf Jung's avatar
README    
Ralf Jung committed
57

Ralf Jung's avatar
Ralf Jung committed
58
Once you got opam set up, run `make build-dep` to install the right versions
Ralf Jung's avatar
Ralf Jung committed
59
60
of the dependencies.

Ralf Jung's avatar
Ralf Jung committed
61
62
Run `make -jN` to build the full development, where `N` is the number of your
CPU cores.
63

Ralf Jung's avatar
Ralf Jung committed
64
65
66
67
To update, do `git pull`.  After an update, the development may fail to compile
because of outdated dependencies.  To fix that, please run `opam update`
followed by `make build-dep`.

Hai Dang's avatar
Hai Dang committed
68

Hai Dang's avatar
Hai Dang committed
69
[`ghostcell`]: ghostcell