README.md 4.54 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.11.2 / 8.12.0
Ralf Jung's avatar
Ralf Jung committed
10
 - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
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
## Building from source

Ralf Jung's avatar
Ralf Jung committed
15
When building from source, we recommend to use opam (2.0.0 or newer) for
Ralf Jung's avatar
Ralf Jung committed
16
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
    opam repo add coq-released https://coq.inria.fr/opam/released
Ralf Jung's avatar
Ralf Jung committed
19
    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Ralf Jung's avatar
Ralf Jung committed
20 21 22

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
* [barrier](theories/barrier): Implementation and proof of a barrier as
  described in ["Higher-Order Ghost State"](http://doi.acm.org/10.1145/2818638).
Léo Stefanesco's avatar
Léo Stefanesco committed
37
* [logrel](theories/logrel): Logical relations.
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39 40 41 42 43 44 45 46 47 48 49 50
  - [logrel/stlc](theories/logrel/stlc): A unary logical relation for semantic
    typing STLC (simply-typed lambda calculus) with De Bruijn indices (using
    Autosubst).
  - [logrel/F_mu_ref_conc](theories/logrel/F_mu_ref_conc): The logical relations
    for F_mu_ref_conc (System F with recursive types, references and concurrency)
    with De Bruijn indices (using Autosubst) from the
    [IPM paper](http://doi.acm.org/10.1145/3093333.3009855):
    + 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.
51 52
  - If you are looking for a well-explained logical relation for Iris's HeapLang,
    take a look at our [POPL20 tutorial](https://gitlab.mpi-sws.org/iris/tutorial-popl20/).
Ralf Jung's avatar
Ralf Jung committed
53
* [logatom](theories/logrel_heaplang): Proofs of various logically atomic specifications:
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55 56 57 58 59 60 61 62 63
  - 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)
    (by Rodolphe Lepigre).
  - Atomic Snapshot (by Marianna Rapoport).
  - Treiber Stack (by Zhen Zhang, and another version by Rodolphe Lepigre).
  - Flat Combiner (by Zhen Zhang, also see
    [this archived documentation](https://gitlab.mpi-sws.org/FP/iris-atomic/tree/master/docs)).
64
* [spanning_tree](theories/spanning_tree): Proof of a concurrent spanning tree
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  algorithm (by Amin Timany).
66
* [concurrent_stacks](theories/concurrent_stacks): Proof of an implementation of
Ralf Jung's avatar
Ralf Jung committed
67 68
  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).
69
* [lecture_notes](theories/lecture_notes): Coq examples for the
70
  [Iris lecture notes](http://iris-project.org/tutorial-material.html).
Robbert Krebbers's avatar
Robbert Krebbers committed
71 72 73
* [hocap](theories/hocap): Formalizations of the concurrent bag and concurrent
  runners libraries from the [HOCAP paper](https://dl.acm.org/citation.cfm?id=2450283)
  (by Dan Frumin). See the associated [README](theories/hocap/README.md).
74
* [array_based_queuing_lock](/theories/array_based_queuing_lock): Proof of
75
  safety of an implementation of the array-based queuing lock. This example is
76 77 78
  also covered in the chapter ["Case study: The Array-Based Queueing
  Lock"](https://iris-project.org/tutorial-pdfs/iris-lecture-notes.pdf#section.10)
  in the Iris lecture notes.
Ralf Jung's avatar
Ralf Jung committed
79

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

Ralf Jung's avatar
Ralf Jung committed
82 83 84 85
* 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.
86 87
  (In case you do not use opam yourself, you can see recently published versions
  [in this repository](https://gitlab.mpi-sws.org/iris/opam/commits/master).)
Ralf Jung's avatar
Ralf Jung committed
88 89
* 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
90
  mismatches.