A soundness proof for GPS and RSL with Release-Acquire semantics in Iris.

Name Last Update
coq Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
LICENSE Loading commit data...
README.md Loading commit data...
opam Loading commit data...
opam.pins Loading commit data...

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/.

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 example/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.