Commit 9445ab70 authored by Hai Dang's avatar Hai Dang
Browse files

reordering in README

parent df6c8179
Pipeline #42818 passed with stage
in 23 minutes and 52 seconds
......@@ -8,11 +8,21 @@ It consists of two parts: a Rust implementation with examples and benchmarks, an
To build and run the Rust code, you will need to
[install cargo](https://doc.rust-lang.org/stable/cargo/getting-started/installation.html).
## 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.
## Examples
The Rust examples in the paper can be found in [`ghostcell/examples/`](ghostcell/examples/).
More specifically:
- For Section 2, see [`branded_vec.rs`]((ghostcell/examples/branded_vec.rs).
- For Section 2, see [`branded_vec.rs`](ghostcell/examples/branded_vec.rs).
- 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`.
......@@ -20,19 +30,15 @@ More specifically:
To run an example, use `cargo run --example branded_vec` from the [`ghostcell`] directory.
## 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.
# Coq proof
Our Coq proof is based on the [RustBelt formalization](https://gitlab.mpi-sws.org/iris/lambda-rust).
## 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).
## Prerequisites
This version is known to compile with:
......@@ -58,10 +64,5 @@ 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`.
## 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).
[`ghostcell`]: ghostcell
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment