research-article

Rely-guarantee references for refinement types over aliased mutable data

Authors:

Colin S. Gordon,

Michael D. Ernst,

Dan GrossmanAuthors Info & Claims

ACM SIGPLAN Notices, Volume 48, Issue 6

Pages 73 - 84

https://doi.org/10.1145/2499370.2462160

Published: 16 June 2013 Publication History

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.

References

[1]

L. Augustsson. Cayenne -- A Language with Dependent Types. In ICFP, 1998.

Digital Library

[2]

H. Barendregt. Lambda Calculi with Types. 1991.

[3]

M. Barnett, M. Fähndrich, K. R. M. Leino, P. Müller, W. Schulte, and H. Venter. Specification and Verification: The Spec# Experience. Commun. ACM, 54 (6): 81--91, June 2011.

Digital Library

[4]

Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development; Coq'Art: The Calculus of Inductive Constructions. Springer Verlag, 2004.

Digital Library

[5]

K. Bierhoff and J. Aldrich. Modular Typestate Checking of Aliased Objects. In OOPSLA, 2007.

Digital Library

[6]

R. L. Bocchino, Jr., V. S. Adve, D. Dig, S. V. Adve, S. Heumann, R. Komuravelli, J. Overbey, P. Simmons, H. Sung, and M. Vakilian. A Type and Effect System for Deterministic Parallel Java. In OOPSLA, 2009.

Digital Library

[7]

R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. Permission Accounting in Separation Logic. In POPL, 2005.

Digital Library

[8]

V. Capretta. A Polymorphic Representation of Induction-Recursion. Retrieved 9/12/12. URL: http://www.cs.ru.nl/venanzio/publications/induction_recursion.pdf, March 2004.

[9]

C. Chen and H. Xi. Combining Programming with Theorem Proving. In ICFP, 2005.

Digital Library

[10]

A. Chlipala. Certified Programming with Dependent Types. http://adam.chlipala.net/cpdt/.

[11]

A. Chlipala, G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky. Effective Interactive Proofs for Higher-order Imperative Programs. In ICFP, 2009.

Digital Library

[12]

Coq Development Team. Thecoq Proof Assistant Reference Manual: Version 8.4, 2012.

[13]

T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76, 1988.

Digital Library

[14]

W. Dietl, S. Drossopoulou, and P. Müller. Generic Universe Types. In phECOOP, 2007.

Digital Library

[15]

T. Dinsdale-Young, M. Dodds, P. Gardner, M. Parkinson, and V. Vafeiadis. Concurrent Abstract Predicates. In ECOOP, 2010.

Digital Library

[16]

M. Dodds, X. Feng, M. Parkinson, and V. Vafeiadis. Deny-Guarantee Reasoning. In ESOP. 2009.

Digital Library

[17]

P. Dybjer. Inductive Families. Formal Aspects of Computing, 6: 440--465, 1994.

[18]

X. Feng. Local Rely-Guarantee Reasoning. In POPL, 2009.

Digital Library

[19]

C. Flanagan and M. Abadi. Types for Safe Locking. In ESOP, 1999.

Digital Library

[20]

C. Flanagan and S. N. Freund. Type-Based Race Detection for Java. In PLDI, 2000.

Digital Library

[21]

T. Freeman and F. Pfenning. Refinement types for ml. In PLDI, 1991.

Digital Library

[22]

C. S. Gordon, M. J. Parkinson, J. Parsons, A. Bromfield, and J. Duffy. Uniqueness and Reference Immutability for Safe Parallelism. In OOPSLA, 2012.

Digital Library

[23]

C. S. Gordon, M. D. Ernst, and D. Grossman. Rely-Guarantee References for Refinement Types Over Aliased Mutable Data (Extended Version). Technical Report UW-CSE-13-03-02, University of Washington, March 2013.

[24]

C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Commun. ACM, 12 (10): 576--580, Oct. 1969.

Digital Library

[25]

M. Hofmann. Syntax and Semantics of Dependent Types, in Semantics and Logics of Computation, chapter 3. 1997.

[26]

J. B. Jensen and L. Birkedal. Fictional Separation Logic. In ESOP, 2012.

Digital Library

[27]

C. B. Jones. Tentative Steps Toward a Development Method for Interfering Programs. ACM TOPLAS, 5 (4): 596--619, Oct. 1983.

Digital Library

[28]

K. R. Leino and P. Müller. A Basis for Verifying Multi-threaded Programs. In ESOP, 2009.

Digital Library

[29]

F. Militao, J. Aldrich, and L. Caires. Aliasing Control with View-based Typestate. In FTfJP, 2010.

Digital Library

[30]

F. Militao, J. Aldrich, and L. Caires. Rely-Guarantee View Typestate. Retrieved 8/24/12, July 2012. URL http://www.cs.cmu.edu/ foliveir/papers/rgviews.pdf.

[31]

K. Naden, R. Bocchino, J. Aldrich, and K. Bierhoff. A Type System for Borrowing Permissions. In POPL, 2012.

Digital Library

[32]

A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and Separation in Hoare Type Theory. In ICFP, 2006.

Digital Library

[33]

A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal. Abstract Predicates and Mutable ADTs in Hoare Type Theory. In ESOP. 2007.

Digital Library

[34]

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: Dependent Types for Imperative Programs. In ICFP, 2008.

Digital Library

[35]

L. Nistor and J. Aldrich. Verifying Object-Oriented Code Using Object Propositions. In IWACO, 2011.

[36]

N. Nystrom, V. Saraswat, J. Palsberg, and C. Grothoff. Constrained Types for Object-Oriented Languages. In OOPSLA, 2008.

Digital Library

[37]

S. Owicki and D. Gries. An Axiomatic Proof Technique for Parallel Programs I. Acta Informatica, pages 319--340, 1976.

Digital Library

[38]

M. Parkinson and G. Bierman. Separation Logic and Abstraction. In POPL, 2005.

Digital Library

[39]

C. Paulin-Mohring. Inductive Definitions in the System Coq: Rules and Properties. In Typed Lambda Calculi and Applications, 1993.

Digital Library

[40]

A. Pilkiewicz and F. Pottier. The Essence of Monotonic State. In TLDI, 2011.

Digital Library

[41]

P. M. Rondon, M. Kawaguchi, and R. Jhala. Low-Level Liquid Types. In POPL, 2010.

Digital Library

[42]

M. Sozeau. Program-ing Finger Trees in Coq. In ICFP, 2007.

Digital Library

[43]

N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang. Secure Distributed Programming with Value-dependent Types. In ICFP, 2011.

Digital Library

[44]

M. S. Tschantz and M. D. Ernst. Javari: Adding Reference Immutability to Java. In OOPSLA, 2005.

Digital Library

[45]

V. Vafeiadis and M. Parkinson. A Marriage of Rely/Guarantee and Separation Logic. In CONCUR. 2007.

Digital Library

[46]

J. Wickerson, M. Dodds, and M. Parkinson. Explicit Stabilisation for Modular Rely-Guarantee Reasoning. In ESOP, 2010.

Digital Library

[47]

H. Xi and F. Pfenning. Dependent Types in Practical Programming. In POPL, 1999.

Digital Library

[48]

H. Xi, C. Chen, and G. Chen. Guarded Recursive Datatype Constructors. In POPL, 2003.

Digital Library

[49]

Y. Zibin, A. Potanin, M. Ali, S. Artzi, A. Kiezun, and M. D. Ernst. Object and Reference Immutability Using Java Generics. In ESEC-FSE, 2007.

Digital Library

[50]

Y. Zibin, A. Potanin, P. Li, M. Ali, and M. D. Ernst. Ownership and Immutability in Generic Java. In OOPSLA, 2010.

Digital Library

Cited By

Coughlin NSmith G(2022)Compositional noninterference on hardware weak memory modelsScience of Computer Programming10.1016/j.scico.2022.102779(102779)Online publication date: Feb-2022
https://doi.org/10.1016/j.scico.2022.102779
He PWestbrook ECarmer BPhifer CRobert VSmeltzer KŞtefănescu ATomb AWick AYacavone MZdancewic S(2021)A type system for extracting functional specifications from memory-safe imperative programsProceedings of the ACM on Programming Languages10.1145/34855125:OOPSLA(1-29)Online publication date: 20-Oct-2021
https://doi.org/10.1145/3485512
Timany ABirkedal LHriţcu CPopescu A(2021)Reasoning about monotonicity in separation logicProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3437992.3439931(91-104)Online publication date: 17-Jan-2021
https://dl.acm.org/doi/10.1145/3437992.3439931
Show More Cited By

Index Terms

Rely-guarantee references for refinement types over aliased mutable data
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Correctness
2. Theory of computation
  1. Logic
    1. Proof theory
  2. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics

Recommendations

Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types

Verifying invariants of fine-grained concurrent data structures is challenging, because interference from other threads may occur at any time. We propose a new way of proving invariants of fine-grained concurrent data structures: applying rely-guarantee ...
Rely-guarantee references for refinement types over aliased mutable data
PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation

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 ...
Gradual refinement types
POPL '17

Refinement types are an effective language-based verification technique. However, as any expressive typing discipline, its strength is its weakness, imposing sometimes undesired rigidity. Guided by abstract interpretation, we extend the gradual typing ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 48, Issue 6

PLDI '13

June 2013

515 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2499370

Issue’s Table of Contents

PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2013
546 pages
ISBN:9781450320146
DOI:10.1145/2491956
General Chair:
Hans-J. Boehm
HP Labs
,
Program Chair:
Cormac Flanagan
University of California, Santa Cruz

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 June 2013

Published in SIGPLAN Volume 48, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
339
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)2

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Coughlin NSmith G(2022)Compositional noninterference on hardware weak memory modelsScience of Computer Programming10.1016/j.scico.2022.102779(102779)Online publication date: Feb-2022
https://doi.org/10.1016/j.scico.2022.102779
He PWestbrook ECarmer BPhifer CRobert VSmeltzer KŞtefănescu ATomb AWick AYacavone MZdancewic S(2021)A type system for extracting functional specifications from memory-safe imperative programsProceedings of the ACM on Programming Languages10.1145/34855125:OOPSLA(1-29)Online publication date: 20-Oct-2021
https://doi.org/10.1145/3485512
Timany ABirkedal LHriţcu CPopescu A(2021)Reasoning about monotonicity in separation logicProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3437992.3439931(91-104)Online publication date: 17-Jan-2021
https://dl.acm.org/doi/10.1145/3437992.3439931
Moine ACharguéraud APottier FPopescu AZdancewic S(2022)Specification and verification of a transient stackProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503677(82-99)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1145/3497775.3503677
Coughlin NSmith G(2022)Compositional noninterference on hardware weak memory modelsScience of Computer Programming10.1016/j.scico.2022.102779217:COnline publication date: 1-May-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102779
He PWestbrook ECarmer BPhifer CRobert VSmeltzer KŞtefănescu ATomb AWick AYacavone MZdancewic S(2021)A type system for extracting functional specifications from memory-safe imperative programsProceedings of the ACM on Programming Languages10.1145/34855125:OOPSLA(1-29)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485512
Timany ABirkedal LHriţcu CPopescu A(2021)Reasoning about monotonicity in separation logicProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3437992.3439931(91-104)Online publication date: 17-Jan-2021
https://dl.acm.org/doi/10.1145/3437992.3439931
Swamy NRastogi AFromherz AMerigoux DAhman DMartínez G(2020)SteelCore: an extensible concurrent separation logic for effectful dependently typed programsProceedings of the ACM on Programming Languages10.1145/34090034:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3409003
Nigam RAtapattu SThomas SLi ZBauer TYe YKoti ASampson AZhang ZDonaldson ATorlak E(2020)Predictable accelerator design with time-sensitive affine typesProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3385974(393-407)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3385412.3385974
Coughlin NSmith G(2020)Rely/Guarantee Reasoning for Noninterference in Non-Blocking Algorithms2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00034(380-394)Online publication date: Jun-2020
https://doi.org/10.1109/CSF49147.2020.00034
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents