From 61064dbf1dd1bf6d845b157265d35c0dfdea416d Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 19 Apr 2017 15:55:09 +0200
Subject: [PATCH] update README
---
README.md | 49 +++++++++++++++++++++++++++++++++++--------------
1 file changed, 35 insertions(+), 14 deletions(-)
diff --git a/README.md b/README.md
index fe6d11d9..cf4e1db4 100644
--- a/README.md
+++ b/README.md
@@ -1,18 +1,16 @@
# iGPS & iRSL - encoding of GPS and RSL in Iris
-## Content
-
This repository contains the Coq development of **iGPS** and **iRSL**,
which are variants of **GPS** and **RSL** in Iris.
-### Dependencies
+## Dependencies
The master branch is known to compile with:
* Coq 8.6
* Ssreflect 1.6.1
* Iris 3.0
-### Build
+## Build
The easiest way to build the development is to use OPAM.
Go to [coq/ra](coq/ra) and then `make build-dep`.
@@ -20,17 +18,40 @@ All the dependencies will be built and installed by OPAM before
the actual compilation of the development.
Manually, one can build and install Iris
-(currently
-[Iris@01d12014](https://gitlab.mpi-sws.org/FP/iris-coq/commit/01d12014855abe6adaea20bbb35b1e9beadff14e)),
+(currently [Iris@01d12014][iris]),
and then `make` in [coq/ra](coq/ra).
-### Structure
+## Structure
+
+The Coq development is in folder [coq/ra/](coq/ra).
-* The operational semantics is in `machine.v`. The language is in `lang.v`.
-* The base logic is in the `base` folder. The model is in `base/ghosts.v`.
+* The operational semantics is in [machine.v](coq/ra/machine.v). The language is in [lang.v](coq/ra/lang.v).
+* The base logic is in the [base/](coq/ra/base) folder.
Each base rule is proven in a separate file.
-* iRSL's main rules are in `rsl_instances.v`. The model is in `rsl.v`.
-* Non-atomic rules are in `na.v`.
-* iGPS's rules are in the `gps` folder. The model is in `gps/shared.v`
-* Examples are in the `examples` folder.
-* `tests/message_passing.v` contains a closed proof of MP without Iris statements.
\ No newline at end of file
+* iRSL's main rules are in [rsl_instances.v](coq/ra/rsl_instances.v). The model is in [rsl.v](coq/ra/rsl.v).
+* Non-atomic rules are in [na.v](coq/ra/na.v).
+* iGPS's rules are in the [gps/](coq/ra/gps) folder. The model is in [gps/shared.v](coq/ra/gps/shared.v)
+* Examples are in the [examples](coq/ra/examples) folder.
+* [tests/message_passing.v](coq/ra/tests/message_passing.v) contains a closed proof (adequacy) of MP without Iris statements.
+
+#### Mapping with ECOOP 2017 paper submission
+
+| Paper section | Paper definitions/rules/lemmas | Coq definitions/lemmas | in Coq file (under [coq/ra](coq/ra)) |
+| ------------- | ------------------------------ | ---------------------- | ------------------------------------- |
+| 2.2 | Operational semantics | `machine_red`, split into `thread_red` (RA reductions), `drf_red` (NA reductions), `alloc_red` (allocation reductions) | [machine.v](coq/ra/machine.v) |
+| 2.3 | $`\lambda_{RN}`$ language | `expr` (expressions) and `step` (reductions) | [lang.v](coq/ra/lang.v) |
+| 3.2 | Base logic local assertions and invariants | `Seen` `Hist` `HInv` `PSInv` | [base/ghosts.v](coq/ra/base/ghosts.v) |
+| 3.2 | Base logic NA rules | `f_read_na` `f_write_na` `f_alloc` `f_dealloc` | [base](coq/ra/base)/na_*.v [base/alloc.v](coq/ra/base/alloc.v) [base/dealloc.v](coq/ra/base/dealloc.v) |
+| 4.1 | iGPS NA rules | `na_read` `na_write`; **fractional versions**: `na_read_frac` `na_write_frac` | [na.v](coq/ra/na.v) |
+| 4.1 | iGPS normal (*plain*) protocol rules | `GPS_PP_*` lemmas | [gps/plain.v](coq/ra/gps/plain.v) |
+| 4.1, Appendix C | iGPS escrows and exchanges | `exchange_*` and `escrows_*` lemmas | [escrows.v](coq/ra/escrows.v) |
+| 4.2, Appendix B | iGPS single-writer protocol rules | `GPS_SW_*` lemmas; **extra versions**: `GPS_nSW_*` | [gps/singlewriter.v](coq/ra/gps/singlewriter.v) |
+| 4.3, Appendix F | iGPS model | GPS assertions defined by `vPred_*`; GPS invariant `gps_inv`; soundness proofs depend on **raw protocols** rules `RawProto_*` | [viewpred.v](coq/ra/viewpred.v) [gps/shared.v](coq/ra/gps/shared.v) [gps/read.v](coq/ra/gps/read.v) [gps/write.v](coq/ra/gps/write.v) [gps/cas.v](coq/ra/gps/cas.v) [gps/fai.v](coq/ra/gps/fai.v) |
+| 5, Appendix D | iRSL rules | `Rel_*` `Acq_*` `RMWAcq_*` lemmas; **fractional versions**: `Relp_*` `Acqp_*` `RMWAcqp_*` lemmas | [rsl_instances.v](coq/ra/rsl_instances.v); model in [rsl.v](coq/ra/rsl.v) |
+| 5 | Allocations and Deallocations | `alloc` `dealloc` `malloc_spec` | [malloc.v](coq/ra/malloc.v) |
+| 5 | Fractional protocols | **single-writer**: `GPS_FWP_*` and `GPS_FRP_*` lemmas; **plain** `GPS_FP_*`; **extra versions**: `GPS_nFWP_*` | [gps/singlewriter.v](coq/ra/gps/singlewriter.v) [gps/fractional.v](coq/ra/gps/fractional.v) |
+| 5, Appendix E | Examples: message passing, circular buffer, read-copy-update (RCU), spin lock, bounded ticket lock | all the `*_spec` lemmas. Other examples: Michael-Scott queue, SC stack, Treiber stack | [examples/circ_buffer.v](coq/ra/examples/circ_buffer.v) [examples/message_passing.v](coq/ra/examples/message_passing.v) [examples/msqueue.v](coq/ra/examples/msqueue.v) [examples/rcu.v](coq/ra/examples/rcu.v) [examples/sc_stack.v](coq/ra/examples/sc_stack.v) [examples/spin_lock.v](coq/ra/examples/spin_lock.v) [examples/ticket_lock.v](coq/ra/examples/ticket_lock.v) [examples/tstack.v](coq/ra/examples/tstack.v) |
+| Appendix A | Equivalence between the axiomantic and operational semantics | No Coq formalization, partly follows from the promising semantics (POPL'17), which already has a Coq formalization, except for the non-atomic race detector. | |
+
+
+[iris]: https://gitlab.mpi-sws.org/FP/iris-coq/commit/01d12014855abe6adaea20bbb35b1e9beadff14e
--
GitLab