Rgref

What are Rely-Guarantee References?

Rely-Guarantee references are a marriage of ideas from rely-guarantee reasoning to ideas from reference immutability.

The core ideas of the approach are to associate a rely relation and a guarantee relation with each reference. The guarantee limits the actions (side effects) that may be performed using that reference, and thus generalizes a family of type systems called reference immutability, where a mutability restriction is associated with each reference. The rely summarizes the guarantees of all possible aliases (an invariant preserved on the creation of any new alias).

These relations grant us two useful things:

1. The guarantee provides fine-grained control over what mutation a function may perform on its arguments.
2. The rely permits us to add to a reference a refinement predicate (logical formula) that must hold of a reference's referent. If a predicate is preserved by the rely relation (i.e. if it is true in one state, and there is another state related to the first by the rely relation, then it is true in the second state as well), then it is safe to assume that predicate holds in general because the actions possible through any other alias are subsumed by the rely. For more technical details, see Publications below.

There are three implementations of rely-guarantee references:

• csgordon/rgref: A sequential rely-guarantee implementation as a shallow axiomatic DSL in Coq.
• csgordon/rgref-concurrent: A concurrent rely-guarantee implementation as a shallow axiomatic DSL in Coq, with examples of proving properties of lock-free data structures.
• csgordon/rghaskell: A restricted version of concurrent RGRefs implemented as a library for Liquid Haskell (which therefore uses inference and SMT to complete proofs, rather than interactive Coq proofs)

The Coq DSLs are implemented for Coq 8.4. The Liquid Haskell embedding requires a specific version of Liquid Haskell (see that page for details).

There's also an incomplete Agda implementation I can dig up by request.

Virtual Machine

For a virtual machine image (VirtualBox / .ova) containing the concurrent RGRef Coq DSL, the concurrent RGRef Liquid Haskell embedding, and all dependencies, click here (note: 2.7GB).

• Username: rely
• Password: guarantee

Notably, the VM includes:

• The Coq DSL and examples pre-built in the rgref-concurrent directory
  • You can rebuild by running make clean and ./compile.sh in that directory
• ProofGeneral (proofgeneral) and CoqIDE (coqide or coqide.opt) set up and ready to go
• The Liquid Haskell embedding checked out into the rghaskell directory
  • Run the test.sh script to compile the examples
• The appropriate version of Liquid Haskell compiled and installed (liquid) into a Cabal sandbox inside rghaskell

All relevant commands (proofgeneral, coqtop, liquid, etc.) are on the default PATH when you open a terminal.

Publications

For (academic) descriptions of how RGRefs can be used, see:

• Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types. Colin S. Gordon, Michael D. Ernst, Dan Grossman, and Matthew J. Parkinson. ACM Trans. on Prog. Lang. and Sys. 39(3), May 2017.
• Verifying Concurrent Programs by Controlling Alias Interference. Colin Stebbins Gordon. PhD Dissertation, University of Washington, 2014.
• Rely-Guarantee References for Refinement Types over Aliased Mutable Data. Colin S. Gordon, Michael D. Ernst, and Dan Grossman. In Proceedings of PLDI 2013.

The implementations contain examples not described in the above publications.

Support or Contact

If you have further questions or encounter technical difficulties, email @csgordon (csgordon@cs.drexel.edu).