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.
The master branch is known to compile with:
- Coq 8.6
- Ssreflect 1.6.1
- Iris 3.0
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.3
It 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 opam archive. This can be achieved by executing
opam repo add coq-released https://coq.inria.fr/opam/released
Now, go to coq/ra and execute
make build-dep to install all
dependencies of ra-gps. Finally, execute "make" to build the development.
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)|
|3.2.1||Base logic local assertions and invariants||
|3.2.1||Base logic NA rules||
||base/na_*.v base/alloc.v base/dealloc.v|
|3.2.2||Message Passing in the base logic||
|4.1||iGPS NA rules||
|4.1||iGPS normal (plain) protocol rules||
|4.1, Appendix C||iGPS escrows and exchanges||
|4.2, Appendix B||iGPS single-writer protocol rules||
|4.3, Appendix F||iGPS model||GPS assertions defined by
||viewpred.v gps/shared.v gps/read.v gps/write.v gps/cas.v gps/fai.v|
|5, Appendix D||iRSL rules||
||rsl_instances.v; model in rsl.v|
|5||Allocations and Deallocations||
|5, Appendix E||Examples: message passing, circular buffer, read-copy-update (RCU), Michael-Scott queue, spin lock, bounded ticket lock||all the
||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.|