Rely-guarantee references for refinement types over aliased mutable data

Download: PDF, slides (PDF), technical report, implementation.

“Rely-guarantee references for refinement types over aliased mutable data” by Colin S. Gordon, Michael D. Ernst, and Dan Grossman. In PLDI 2013: Proceedings of the ACM SIGPLAN 2013 Conference on Programming Language Design and Implementation, (Seattle, WA, USA), June 2013, pp. 73-84.
A previous version appeared as “Rely-guarantee references for refinement types over aliased mutable data (extended version)” by Colin S. Gordon, Michael D. Ernst, and Dan Grossman. University of Washington Department of Computer Science and Engineering technical report UW-CSE-13-03-02, (University of Washington Department of Computer Science and Engineering), Mar. 2013.

Abstract

Reasoning about side effects and aliasing is the heart of verifying imperative programs. Unrestricted side effects through one reference can invalidate assumptions about an alias. We present a new type system approach to reasoning about safe assumptions in the presence of aliasing and side effects, unifying ideas from reference immutability type systems and rely-guarantee program logics. Our approach, rely-guarantee references, treats multiple references to shared objects similarly to multiple threads in rely-guarantee program logics. We propose statically associating rely and guarantee conditions with individual references to shared objects. Multiple aliases to a given object may coexist only if the guarantee condition of each alias implies the rely condition for all other aliases. We demonstrate that existing reference immutability type systems are special cases of rely-guarantee references.

In addition to allowing precise control over state modification, rely-guarantee references allow types to depend on mutable data while still permitting flexible aliasing. Dependent types whose denotation is stable over the actions of the rely and guarantee conditions for a reference and its data will not be invalidated by any action through any alias. We demonstrate this with refinement (subset) types that may depend on mutable data. As a special case, we derive the first reference immutability type system with dependent types over immutable data.

We show soundness for our approach and describe experience using rely-guarantee references in a dependently-typed monadic DSL in Coq.

Download: PDF, slides (PDF), technical report, implementation.

BibTeX entry:

@inproceedings{GordonEG2013,
   author = {Colin S. Gordon and Michael D. Ernst and Dan Grossman},
   title = {Rely-guarantee references for refinement types over aliased
	mutable data},
   booktitle = {PLDI 2013: Proceedings of the {ACM} {SIGPLAN} 2013
	Conference on Programming Language Design and Implementation},
   pages = {73--84},
   address = {Seattle, WA, USA},
   month = jun,
   year = {2013}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.