Commit ae59a004 authored by Hai Dang's avatar Hai Dang
Browse files

some updates to README

parent 2bd6f359
Pipeline #42810 passed with stage
in 25 minutes and 6 seconds
# GhostCell: A Thread-Safe Zero-Cost Abstraction for Shared Mutable State in Rust
# GhostCell: Separating Permissions from Data in Rust
This is the artifact accompanying our paper.
It consists of two parts: a Rust implementation with examples and benchmarks, and a Coq proof.
......@@ -10,33 +10,32 @@ To build and run the Rust code, you will need to
## Examples
The Rust examples in the paper can be found in `ghostcell-examples/examples/`.
The Rust examples in the paper can be found in [`ghostcell/examples/`](ghostcell/examples/).
More specifically:
- For Section 2, see `branded_vec.rs`
- For Section 3, see `linked_list_arc_rwlock.rs`
- For Section 4, see `linked_list_arc_ghostcell.rs`
- For Section 2, see `branded_vec.rs`.
- For Section 3, see `dlist_arena_paper.rs`. The doubly-linked list API and implementation is in [`ghostcell/src/dlist_arena.rs`](ghostcell/src/dlist_arena.rs)
To run an example, use `cargo run --example branded_vec` from the `ghostcell-examples` directory.
To run an example, use `cargo run --example branded_vec` from the [`ghostcell`](ghostcell) directory.
## Benchmarks
The source code for `GhostCell` and for the benchmarks that we ran can be found in `ghostcell-examples`.
The `GhostCell` code is in `ghostcell-examples/src/lib.rs`, the benchmarks are in `ghostcell-examples/benches/linked_list.rs`.
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`, the benchmarks are in `ghostcell/benches/dlist.rs`.
The benchmark results are in `criterion-data`; open `report/index.html` in a browser to view them.
You can run the benchmarks again from the `ghostcell-examples` directory with the command `cargo bench`.
The benchmark results are in `benchmarks-data`; open `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 at https://gitlab.mpi-sws.org/iris/lambda-rust (in particular, the `opam` file is unchanged from there).
Our Coq proof is based on the RustBelt formalization at https://gitlab.mpi-sws.org/iris/lambda-rust.
## Prerequisites
This version is known to compile with:
- Coq 8.11.0
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris) (see the [`opam`](opam) file for the exact version).
## Building from source
......
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