# Iris + Fair Refinements COQ DEVELOPMENT
** This project is no longer maintained.
It will not be adjusted to work with current versions of Iris. **
This is the Coq development for an extension of Iris to support
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.
## Prerequisites
This version is known to compile with:
- Coq 8.9.0
- Iris 3.2.0
The easiest way to install the correct versions of the dependencies is through
opam. You will need the Coq opam repository:
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`.
## Building Instructions
Run the following command to build the full development:
make
(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.
It takes a considerable amount of time and memory to build!
## Structure
* 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
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).
* The folder `heap_lang` defines the ML-like concurrent heap language
* 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
contexts for persistent and linear Iris assertions. It also contains tactics
for interactive proofs in Iris.
* 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.
* 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.
* 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.
## Notable files:
* `prelude/irelations.v` -- general lemmas about fair executions
* `program_logic/language.v` -- definition of termination preserving safe refinement
* `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.
* `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.