README.md 5.71 KB
Newer Older
1
2
3
4
# Warning: this repository is no longer maintained

Please check out [GPFSL](https://gitlab.mpi-sws.org/iris/gpfsl), a betterment of iGPS.

Hai Dang's avatar
Hai Dang committed
5
# iGPS & iRSL - encoding of GPS and RSL in Iris
Hai Dang's avatar
Hai Dang committed
6

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

Hai Dang's avatar
Hai Dang committed
10
## Dependencies
Hai Dang's avatar
Hai Dang committed
11

Hai Dang's avatar
Hai Dang committed
12
The master branch is known to compile with:
Ralf Jung's avatar
Ralf Jung committed
13
* Coq 8.6.1 / 8.7.0
Ralf Jung's avatar
Ralf Jung committed
14
* Ssreflect 1.6.4
Hai Dang's avatar
Hai Dang committed
15
* A development version of Iris (see [opam](opam) for the exact version)
Hai Dang's avatar
Hai Dang committed
16

Hai Dang's avatar
Hai Dang committed
17
## Build
Hai Dang's avatar
Hai Dang committed
18

Hai Dang's avatar
Hai Dang committed
19
The recommended way to build the development is using OPAM (version 1.2.2). To avoid conflicts
20
with existing packages, we recommend to create a new opam switch:
Ralf Jung's avatar
Ralf Jung committed
21
22
23
```
opam switch ra-gps --alias-of=4.02.3
```
24
25
26
27
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.

Ralf Jung's avatar
Ralf Jung committed
28
29
30
31
32
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.git
```
33

Ralf Jung's avatar
Ralf Jung committed
34
35
Now, 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
36

Hai Dang's avatar
Hai Dang committed
37
38
## Structure

Hai Dang's avatar
Hai Dang committed
39
The Coq development is in folder [theories/](theories).
Hai Dang's avatar
Hai Dang committed
40

Hai Dang's avatar
Hai Dang committed
41
* The language is in folder [lang/](theories/lang). The operational semantics is in [lang/machine.v](theories/lang/machine.v).
Hai Dang's avatar
Hai Dang committed
42
* The base logic is in folder [base/](theories/base).
Hai Dang's avatar
Hai Dang committed
43
  Each base rule is proven in a separate file.
Hai Dang's avatar
Hai Dang committed
44
* View predicates definitions are in folder [viewpred/](theories/viewpred).
Hai Dang's avatar
Hai Dang committed
45
* Non-atomic rules are in [base/na.v](theories/base/na.v).
Hai Dang's avatar
Hai Dang committed
46
* iRSL is in [theories/rsl/](theories/rsl). The main rules are in [rsl/rsl_instances.v](theories/rsl/rsl_instances.v). The model is in [rsl/rsl.v](theories/rsl/rsl.v).
Hai Dang's avatar
Hai Dang committed
47
* iGPS's rules are in the [gps/](theories/gps) folder. The model is in [gps/shared.v](theories/gps/shared.v)
Hai Dang's avatar
Hai Dang committed
48
* Examples are in the [examples/](theories/examples) folder.
Hai Dang's avatar
Hai Dang committed
49
* [tests/message_passing.v](theories/tests/message_passing.v) contains a closed proof (adequacy) of MP without Iris statements.
Hai Dang's avatar
Hai Dang committed
50
51
52

#### Mapping with ECOOP 2017 paper submission

Hai Dang's avatar
Hai Dang committed
53
| Paper section | Paper definitions/rules/lemmas | Coq definitions/lemmas | in Coq file  (under [theories](theories))                            |
Hai Dang's avatar
Hai Dang committed
54
| ------------- | ------------------------------ | ---------------------- | ------------------------------------- |
Hai Dang's avatar
Hai Dang committed
55
56
57
58
59
60
61
62
63
64
65
66
67
68
| 2.2           | Operational semantics          | `machine_red`, split into `thread_red` (RA reductions), `drf_red` (NA reductions), `alloc_red` (allocation reductions)        | [lang/machine.v](theories/lang/machine.v)  |
| 2.3           | $`\lambda_{RN}`$ language      | `expr` (expressions) and `step` (reductions) | [lang/lang.v](theories/lang/lang.v)   |
| 3.2.1           | Base logic local assertions and invariants | `Seen` `Hist` `HInv` `PSInv` | [base/ghosts.v](theories/base/ghosts.v) |
| 3.2.1           | Base logic NA rules            | `f_read_na` `f_write_na` `f_alloc` `f_dealloc` | [base](theories/base)/na_*.v  [base/alloc.v](theories/base/alloc.v) [base/dealloc.v](theories/base/dealloc.v) |
| 3.2.2         | Message Passing in the base logic | `message_passing_base_spec` | [examples/message_passing_base.v](theories/examples/message_passing_base.v) |
| 4.1           | iGPS NA rules                   | `na_read` `na_write`; **fractional versions**: `na_read_frac` `na_write_frac` | [base/na.v](theories/base/na.v) |
| 4.1           | iGPS normal (*plain*) protocol rules | `GPS_PP_*` lemmas    | [gps/plain.v](theories/gps/plain.v)  |
| 4.1, Appendix C | iGPS escrows and exchanges | `exchange_*` and `escrows_*` lemmas | [gps/escrows.v](theories/gps/escrows.v) |
| 4.2, Appendix B | iGPS single-writer protocol rules | `GPS_SW_*` lemmas; **extra versions**: `GPS_nSW_*` | [gps/singlewriter.v](theories/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/viewpred.v](theories/viewpred/viewpred.v) [gps/shared.v](theories/gps/shared.v) [gps/read.v](theories/gps/read.v) [gps/write.v](theories/gps/write.v) [gps/cas.v](theories/gps/cas.v) [gps/fai.v](theories/gps/fai.v) |
| 5, Appendix D  | iRSL rules | `Rel_*` `Acq_*` `RMWAcq_*` lemmas; **fractional versions**: `Relp_*` `Acqp_*` `RMWAcqp_*` lemmas | [rsl/rsl_instances.v](theories/rsl/rsl_instances.v); model in [rsl/rsl.v](theories/rsl/rsl.v) |
| 5              | Allocations and Deallocations | `alloc` `dealloc` `malloc_spec`   | [base/malloc.v](theories/base/malloc.v)   |
| 5              | Fractional protocols | **single-writer**: `GPS_FWP_*` and `GPS_FRP_*` lemmas; **plain** `GPS_FP_*`; **extra versions**: `GPS_nFWP_*` | [gps/singlewriter.v](theories/gps/singlewriter.v) [gps/fractional.v](theories/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](theories/examples/circ_buffer.v) [examples/message_passing.v](theories/examples/message_passing.v) [examples/msqueue.v](theories/examples/msqueue.v) [examples/rcu.v](theories/examples/rcu.v) [examples/sc_stack.v](theories/examples/sc_stack.v) [examples/spin_lock.v](theories/examples/spin_lock.v) [examples/ticket_lock.v](theories/examples/ticket_lock.v) [examples/tstack.v](theories/examples/tstack.v)  |
Hai Dang's avatar
Hai Dang committed
69
| 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. | |