Skip to content
Snippets Groups Projects
Verified Commit d28a2de2 authored by Johannes Hostert's avatar Johannes Hostert
Browse files

more readme work

parent ffc3fd5a
No related branches found
No related tags found
1 merge request!18Tree Borrows update
Pipeline #111445 passed
# Simuliris Coq development # Simuliris Coq development
This repository contains the Coq development of Simuliris (paper presented at POPL22: https://iris-project.org/pdfs/2022-popl-simuliris.pdf). This repository contains the Coq development of Simuliris, additionally including the Tree Borrows Optimization Program Logic, and also some Tree Borrows optimizations not proven via Simuliris.
## Prerequisites ## Prerequisites
...@@ -21,9 +21,10 @@ installing the dependencies. This requires the following two repositories: ...@@ -21,9 +21,10 @@ installing the dependencies. This requires the following two repositories:
Once you got opam set up, run `make build-dep` to install the right versions Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies. of the dependencies.
Then run `make` to build everything.
## Structure ## Structure
We include our fork of simuliris in its entirety. Our fork of simuliris in particular includes the upstream version, which proves things about Simuliris, or about data races (in weak memory model), which is part of this archive file but not relevant for the paper.
In particular, that includes the data-race reasoning examples from the simuliris paper, as well as the Stacked Borrows development, which are not the focus of our paper.
The Tree Borrows development lives in `theories/tree_borrows` and has its own `README.md`, please consult that. The Tree Borrows development lives in `theories/tree_borrows` and has its own `README.md`, please consult that.
...@@ -45,4 +46,4 @@ The project follows the following structure below the `theories` folder: ...@@ -45,4 +46,4 @@ The project follows the following structure below the `theories` folder:
## More information ## More information
See the `README.md` in `theories/tree_borrows` See the `README.md` in `theories/tree_borrows`
\ No newline at end of file
...@@ -43,7 +43,7 @@ This example corresponds to the one in `examples/protected/mutable_reorder_write ...@@ -43,7 +43,7 @@ This example corresponds to the one in `examples/protected/mutable_reorder_write
This Coq example corresponds very closely to the one in the paper. This Coq example corresponds very closely to the one in the paper.
The only difference is that `f` and `g` have an extra argument in Coq, which corresponds to the implicit environment that closures have in Rust. The only difference is that `f` and `g` have an extra argument in Coq, which corresponds to the implicit environment that closures have in Rust.
### Paragraph 3: Reordering Reads (Example 18) ### Paragraph 4: Reordering Reads (Example 18)
This is proven in `read_read_reorder`, particularly in `refinement.v`. This is proven in `read_read_reorder`, particularly in `refinement.v`.
These proofs do not use the `simuliris` library, but instead they do a much simpler equivalence proof directly against the operational semantics. These proofs do not use the `simuliris` library, but instead they do a much simpler equivalence proof directly against the operational semantics.
...@@ -62,6 +62,6 @@ We have not shown Example 14, but two examples similar to it: ...@@ -62,6 +62,6 @@ We have not shown Example 14, but two examples similar to it:
But note that this does not insert a read if there is none. Also, the tag is not protected. But note that this does not insert a read if there is none. Also, the tag is not protected.
* `examples/protected/shared_insert_read.v` demonstrates that reads can be inserted on protected tags. * `examples/protected/shared_insert_read.v` demonstrates that reads can be inserted on protected tags.
For the artifact submission, we will create a new example that corresponds to Example 14 more closely. For the artifact evaluation submission, we will create a new example that corresponds to Example 14 more closely.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment