Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • stdpp
2 results
Compare
Name Last commit Last update
algebra
array_lang
benchmark
chan2heap
chan_lang
docs
heap_lang
locks
prelude
program_logic
proofmode
tests
.gitignore
.gitlab-ci.yml
CHANGELOG.md
LICENSE
Makefile
ProofMode.md
README.md
_CoqProject
naming.txt
README.md

IRIS COQ DEVELOPMENT

This is the Coq development for an extension of Iris to support termination-preserving refinement.

Prerequisites

This version is known to compile with:

  • Coq 8.5pl2
  • Ssreflect 1.6+, or built from mathcomp library commit ad273277ab38bf

However, it is quite likely that it does NOT compile with recent trunk versions of Coq. Indeed, it uses features (nested proofs) that are deprecated and will be removed in the next release of Coq.

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, ~27 minutes using make -j 8 on an i7-3770 with 16gb RAM.

Structure

  • The folder prelude contains an extended "Standard Library" by Robbert Krebbers http://robbertkrebbers.nl/thesis.html, with some subsequent modifications.
  • The folder algebra contains the COFE 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 array_lang extends heap_lang with block-allocated memory arrays.
  • 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.

Documentation

A LaTeX version of the core logic definitions and some derived forms NOT including our extensions is available in docs/iris.tex.