README.md 5.21 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1
# iGPS & iRSL - encoding of GPS and RSL in Iris
Hai Dang's avatar
Hai Dang committed
2

Hai Dang's avatar
Hai Dang committed
3
This repository contains the Coq development of **iGPS** and **iRSL**,
Hai Dang's avatar
Hai Dang committed
4
which are variants of **GPS** and **RSL** in Iris.
Hai Dang's avatar
Hai Dang committed
5

Hai Dang's avatar
Hai Dang committed
6
## Dependencies
Hai Dang's avatar
Hai Dang committed
7

Hai Dang's avatar
Hai Dang committed
8 9 10 11
The master branch is known to compile with:
* Coq 8.6
* Ssreflect 1.6.1
* Iris 3.0
Hai Dang's avatar
Hai Dang committed
12

Hai Dang's avatar
Hai Dang committed
13
## Build
Hai Dang's avatar
Hai Dang committed
14

15 16
The recommended way to build the development is using OPAM. To avoid conflicts
with existing packages, we recommend to create a new opam switch:
Hai Dang's avatar
Hai Dang committed
17

18 19 20 21 22 23 24 25 26 27 28
`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.
Hai Dang's avatar
Hai Dang committed
29

Hai Dang's avatar
Hai Dang committed
30 31 32
## Structure

The Coq development is in folder [coq/ra/](coq/ra).
Hai Dang's avatar
Hai Dang committed
33

Hai Dang's avatar
Hai Dang committed
34 35
* 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.
Hai Dang's avatar
Hai Dang committed
36
  Each base rule is proven in a separate file.
Hai Dang's avatar
Hai Dang committed
37 38 39 40 41 42 43 44 45 46 47 48
* 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)   |
Hai Dang's avatar
Hai Dang committed
49 50
| 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) |
Hai Dang's avatar
Hai Dang committed
51
| 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) |
Hai Dang's avatar
Hai Dang committed
52 53 54 55 56 57 58 59
| 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) |
Hai Dang's avatar
Hai Dang committed
60
| 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)  |
Hai Dang's avatar
Hai Dang committed
61
| 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. | |
Hai Dang's avatar
Hai Dang committed
62 63 64


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