README.md 4.76 KB
Newer Older
Joseph Tassarotti's avatar
Joseph Tassarotti committed
1
# Iris + Fair Refinements COQ DEVELOPMENT
Ralf Jung's avatar
Ralf Jung committed
2

3
4
5
** This project is no longer maintained.
It will not be adjusted to work with current versions of Iris. **

6
This is the Coq development for an extension of Iris to support
7
8
9
10
11
12
13
14
15
termination-preserving fair refinement. It is an updated version of work
described in the paper:

    A Higher-Order Logic for Concurrent Termination-Preserving Refinement
    J. Tassarotti, R. Jung, R. Harper.
    ESOP 2017

This version makes use of MoSeL, an extension to the earlier Iris Proof Mode to
support general BI logics.
Ralf Jung's avatar
Ralf Jung committed
16
17

## Prerequisites
Ralf Jung's avatar
Ralf Jung committed
18
19
20

This version is known to compile with:

21
22
 - Coq 8.9.0
 - Iris 3.2.0
23
24

The easiest way to install the correct versions of the dependencies is through
25
opam.  You will need the Coq opam repository:
26
27
28
29
30
31
32
33
34
35
36

    opam repo add coq-released https://coq.inria.fr/opam/released

Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.

## Updating

After doing `git pull`, the development may fail to compile because of outdated
dependencies.  To fix that, please run `opam update` followed by
`make build-dep`.
37

Ralf Jung's avatar
Ralf Jung committed
38
## Building Instructions
Ralf Jung's avatar
Ralf Jung committed
39
40
41

Run the following command to build the full development:

Ralf Jung's avatar
Ralf Jung committed
42
    make
Ralf Jung's avatar
Ralf Jung committed
43

Joseph Tassarotti's avatar
Joseph Tassarotti committed
44
45
46
47
48
(N.B. compiling the development results in benign debugging print outs.
that are used to diagnose performance issues with custom tactics.)

You can use "make -j n" to launch multiple build threads.

49
It takes a considerable amount of time and memory to build!
Ralf Jung's avatar
Ralf Jung committed
50

Ralf Jung's avatar
Ralf Jung committed
51
## Structure
Ralf Jung's avatar
Ralf Jung committed
52

53
54
* The folder `prelude` contains some results extending those found in the "coq-stdpp" library.
* The folder `algebra` contains the OFE and CMRA constructions as well as
Ralf Jung's avatar
Ralf Jung committed
55
56
57
58
  the solver for recursive domain equations.
* The folder `program_logic` builds the semantic domain of Iris, defines and
  verifies primitive view shifts and weakest preconditions, and builds some
  language-independent derived constructions (e.g., STSs).
Ralf Jung's avatar
Ralf Jung committed
59
* The folder `heap_lang` defines the ML-like concurrent heap language
60
61
62
* The folder `chan_lang` defines a message-passing session-typed language and a simple
  type system for it.
* The folder `proofmode` contains the iris proof mode, which extends coq with
63
  contexts for persistent and linear Iris assertions. It also contains tactics
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  for interactive proofs in Iris.
Ralf Jung's avatar
Ralf Jung committed
65
66
67
* The folder `tests` contains modules we use to test our infrastructure.
  Users of the Iris Coq library should *not* depend on these modules; they may
  change or disappear without any notice.
68
69
70
* The folder `chan2heap` describes a translation from `chan_lang` to `heap_lang`,
  in which channels are implemented as a linked list. A proof of correctness for
  this translation is included.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
71
72
73
* The folder `locks` includes an implementation of the
  Craig-Landin-Hagersten (CLH) queue lock and a fair ticket lock, and
  proves that the CLH lock refines the ticket lock.
74

75
76
## Notable files:

77
* `prelude/irelations.v` -- general lemmas about fair executions
78
* `program_logic/language.v` -- definition of termination preserving safe refinement
79
80
81
82
83
84
85
86
87
88
89
* `program_logic/refine_ectx_delay.v` -- proof rules for reasoning about source
  threads; lemmas showing that derivations done with these resources yields fair
  termination-preserving refinement
* `chan2heap/chan2heap.v` -- translation from chan to heap language, defn of
  message passing implementations
* `chan2heap/refine_protocol.v` -- derived proof rules for the above message 
  passing implementation.
* `chan2heap/simple_reln.v` -- logical relation based on type system for `chan_lang`.
  Proof of fundamental lemma and soundness of the relation
* `chan2heap/compiler_correctness.v` -- uses fundamental lemma and soundness 
  to establish correctness of translation for well-typed source programs.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
* `locks/clh.v` -- implementation of Craig-Landin-Hagersten lock, motivation
  and references for its use.
* `locks/ticket.v` -- implementation of fair ticket lock
* `locks/ticket_clh_triples.v` -- Hoare triples for proving that the CLH lock
  refines the ticket lock
* `locks/lock_reln.v` -- We give simple type directed translation for
  heap_lang between two implementations of an abstract "lock" type
  which can be used to guard functions with a "sync" command. Assuming
  certain triples (analogous to those proved in ticket_clh_triples.v),
  about primitives for creating, acquiring, and releasing locks, a
  logical relation is developed to show that this translation is a
  refinement.
* `locks/ticket_clh_refinement.v` -- Here we instantiate the results
  in lock_reln.v with the triples about ticket lock and CLH to show a
  refinement when the implementation of "sync" is changed from using
  the ticket lock primitives and the CLH primitives.
* `tests/heap_lang.v` -- contains proof rules for refinements from the
  heap language to itself; for example, proof of a invariant-hositing
  loop transformation; simple re-ordering of reads and writes.