# 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.6
* Ssreflect 1.6.1
* Iris 3.0

## 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.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](coq/ra) and 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/](coq/ra).

* 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](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.1           | Base logic local assertions and invariants | `Seen` `Hist` `HInv` `PSInv` | [base/ghosts.v](coq/ra/base/ghosts.v) |
| 3.2.1           | 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) |
| 3.2.2         | Message Passing in the base logic | `message_passing_base_spec` | [examples/message_passing_base.v](coq/ra/examples/message_passing_base.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), Michael-Scott queue, spin lock, bounded ticket lock | all the `*_spec` lemmas. Other examples: 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    | 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. | |


[iris]: https://gitlab.mpi-sws.org/FP/iris-coq/commit/01d12014855abe6adaea20bbb35b1e9beadff14e