README.md 3.97 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5 6 7 8
# IRIS EXAMPLES

Some example verification demonstrating the use of Iris.

## Prerequisites

This version is known to compile with:

9
 - Coq 8.9.0
Ralf Jung's avatar
Ralf Jung committed
10
 - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
Ralf Jung's avatar
Ralf Jung committed
11
 - The coq86-devel branch of [Autosubst](https://github.com/uds-psl/autosubst)
Ralf Jung's avatar
Ralf Jung committed
12

Ralf Jung's avatar
Ralf Jung committed
13 14 15 16
## Building from source

When building from source, we recommend to use opam (1.2.2 or newer) for
installing the dependencies.  This requires the following two repositories:
Ralf Jung's avatar
Ralf Jung committed
17

Ralf Jung's avatar
Ralf Jung committed
18 19 20 21 22
    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

Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
Ralf Jung's avatar
Ralf Jung committed
23

Ralf Jung's avatar
Ralf Jung committed
24 25
Run `make -jN` to build the full development, where `N` is the number of your
CPU cores.
Ralf Jung's avatar
Ralf Jung committed
26

Ralf Jung's avatar
Ralf Jung committed
27 28 29
To update, do `git pull`.  After an update, the development may fail to compile
because of outdated dependencies.  To fix that, please run `opam update`
followed by `make build-dep`.
Ralf Jung's avatar
Ralf Jung committed
30

Ralf Jung's avatar
Ralf Jung committed
31 32 33 34
## Case Studies

This repository contains the following case studies:

Ralf Jung's avatar
Ralf Jung committed
35 36 37 38
* [barrier](theories/barrier): Implementation and proof of a barrier as
  described in ["Higher-Order Ghost State"](http://doi.acm.org/10.1145/2818638).
* [logrel](theories/logrel): Logical relations from the
  [IPM paper](http://doi.acm.org/10.1145/3093333.3009855):
Ralf Jung's avatar
Ralf Jung committed
39
  - STLC
Ralf Jung's avatar
Ralf Jung committed
40
      - Unary logical relations proving type safety
Ralf Jung's avatar
Ralf Jung committed
41
  - F_mu (System F with recursive types)
Ralf Jung's avatar
Ralf Jung committed
42
      - Unary logical relations proving type safety
Ralf Jung's avatar
Ralf Jung committed
43
  - F_mu_ref (System F with recursive types and references)
Ralf Jung's avatar
Ralf Jung committed
44 45
      - Unary logical relations proving type safety
      - Binary logical relations for proving contextual refinements
Ralf Jung's avatar
Ralf Jung committed
46
  - F_mu_ref_conc (System F with recursive types, references and concurrency)
Ralf Jung's avatar
Ralf Jung committed
47 48 49 50 51 52
      - Unary logical relations proving type safety
      - Binary logical relations for proving contextual refinements
          - Proof of refinement for a pair of fine-grained/coarse-grained
            concurrent counter implementations
          - Proof of refinement for a pair of fine-grained/coarse-grained
            concurrent stack implementations
Robbert Krebbers's avatar
Robbert Krebbers committed
53 54
* [logrel_heaplang](theories/logrel_heaplang): A unary logical relation for
  semantic typing of heap lang.
Ralf Jung's avatar
Ralf Jung committed
55
* [logatom](theories/logrel_heaplang): Proofs of various logically atomic specifications:
Ralf Jung's avatar
Ralf Jung committed
56 57 58 59 60
  - Elimination Stack (by Ralf Jung)
  - Conditional increment (inspired by [this paper](https://people.mpi-sws.org/~dreyer/papers/relcon/paper.pdf)) and RDCSS (as in [this paper](https://timharris.uk/papers/2002-disc.pdf)) (by Marianna Rapoport, Rodolphe Lepigre and Gaurav Parthasarathy)
  - [Herlihy-Wing-Queue](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf)
  - Atomic Snapshot (by Marianna Rapoport)
  - Treiber Stack (by Zhen Zhang, and another version by Rodolphe Lepigre)
Ralf Jung's avatar
Ralf Jung committed
61
  - Flat Combiner (by Zhen Zhang, also see [this archived documentation](https://gitlab.mpi-sws.org/FP/iris-atomic/tree/master/docs))
Ralf Jung's avatar
Ralf Jung committed
62
* [spanning-tree](theories/spanning_tree): Proof of a concurrent spanning tree
63
  algorithm by Amin Timany.
64
* [concurrent-stacks](theories/concurrent_stacks): Proof of an implementation of
65 66
  concurrent stacks with helping by Daniel Gratzer et. al., as described in the
  [report](http://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf).
67 68
* [lecture-notes](theories/lecture_notes): Coq examples for the
  [Iris lecture notes](http://iris-project.org/tutorial-material.html).
Dan Frumin's avatar
Dan Frumin committed
69
* [hocap](theories/hocap): Formalisations of the concurrent bag and concurrent runners libraries from the [HOCAP paper](https://dl.acm.org/citation.cfm?id=2450283). See the associated [README](theories/hocap/README.md).
Ralf Jung's avatar
Ralf Jung committed
70

Ralf Jung's avatar
Ralf Jung committed
71 72
## For Developers: How to update the Iris dependency

Ralf Jung's avatar
Ralf Jung committed
73 74 75 76 77 78
* Do the change in Iris, push it.
* Wait for CI to publish a new Iris version on the opam archive, then run
  `opam update iris-dev`.
* In iris-examples, change the `opam` file to depend on the new version.
* Run `make build-dep` (in iris-examples) to install the new version of Iris.
  You may have to do `make clean` as Coq will likely complain about .vo file
Ralf Jung's avatar
Ralf Jung committed
79
  mismatches.