iGPS & iRSL - encoding of GPS and RSL in Iris
This repository contains the Coq development of iGPS and iRSL, which are variants of GPS and RSL in Iris.
Dependencies
The master branch is known to compile with:
- Coq 8.7.2 / 8.8.0
- Iris (MoSeL branch)
Build
The recommended way to build the development is using OPAM. To avoid conflicts with existing packages, we recommend to create a new opam switch:
opam switch ra-gps --alias-of=4.02.3It should work for any compiler version upwards of 4.01.0. After compiling OCaml, the new switch needs to be activated in your current shell. opam will print the necessary instructions.
To find all the dependencies of ra-gps, opam needs to know about the Coq and Iris opam archives. This can be achieved by executing
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.gitNow, execute make build-dep to install all
dependencies of ra-gps. Finally, execute make to build the development.
Structure
The Coq development is in folder coq/ra/.
- The operational semantics is in machine.v. The language is in lang.v.
- The base logic is in the 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 (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) |
|---|---|---|---|
| 2.2 | Operational semantics |
machine_red, split into thread_red (RA reductions), drf_red (NA reductions), alloc_red (allocation reductions) |
machine.v |
| 2.3 |
\lambda_{RN} language |
expr (expressions) and step (reductions) |
lang.v |
| 3.2.1 | Base logic local assertions and invariants |
Seen Hist HInv PSInv
|
base/ghosts.v |
| 3.2.1 | Base logic NA rules |
f_read_na f_write_na f_alloc f_dealloc
|
base/na_*.v base/alloc.v base/dealloc.v |
| 3.2.2 | Message Passing in the base logic | message_passing_base_spec |
examples/message_passing_base.v |
| 4.1 | iGPS NA rules |
na_read na_write; fractional versions: na_read_frac na_write_frac
|
na.v |
| 4.1 | iGPS normal (plain) protocol rules |
GPS_PP_* lemmas |
gps/plain.v |
| 4.1, Appendix C | iGPS escrows and exchanges |
exchange_* and escrows_* lemmas |
escrows.v |
| 4.2, Appendix B | iGPS single-writer protocol rules |
GPS_SW_* lemmas; extra versions: GPS_nSW_*
|
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 gps/shared.v gps/read.v gps/write.v gps/cas.v gps/fai.v |
| 5, Appendix D | iRSL rules |
Rel_* Acq_* RMWAcq_* lemmas; fractional versions: Relp_* Acqp_* RMWAcqp_* lemmas |
rsl_instances.v; model in rsl.v |
| 5 | Allocations and Deallocations |
alloc dealloc malloc_spec
|
malloc.v |
| 5 | Fractional protocols |
single-writer: GPS_FWP_* and GPS_FRP_* lemmas; plain GPS_FP_*; extra versions: GPS_nFWP_*
|
gps/singlewriter.v gps/fractional.v |
| 5, Appendix E | Examples: message passing, circular buffer, read-copy-update (RCU), Michael-Scott queue, spin lock, bounded ticket lock | all the *_spec lemmas. Other examples: SC stack, Treiber stack |
examples/circ_buffer.v examples/message_passing.v examples/msqueue.v examples/rcu.v examples/sc_stack.v examples/spin_lock.v examples/ticket_lock.v examples/tstack.v |
| Appendix A | Correspondence between the axiomatic 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. |