skip to main content
10.1145/2429069.2429131acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

The ramifications of sharing in data structures

Published: 23 January 2013 Publication History

Abstract

Programs manipulating mutable data structures with intrinsic sharing present a challenge for modular verification. Deep aliasing inside data structures dramatically complicates reasoning in isolation over parts of these objects because changes to one part of the structure (say, the left child of a dag node) can affect other parts (the right child or some of its descendants) that may point into it. The result is that finding intuitive and compositional proofs of correctness is usually a struggle. We propose a compositional proof system that enables local reasoning in the presence of sharing.
While the AI "frame problem" elegantly captures the reasoning required to verify programs without sharing, we contend that natural reasoning about programs with sharing instead requires an answer to a different and more challenging AI problem, the "ramification problem": reasoning about the indirect consequences of actions. Accordingly, we present a RAMIFY proof rule that attacks the ramification problem head-on and show how to reason with it. Our framework is valid in any separation logic and permits sound compositional and local reasoning in the context of both specified and unspecified sharing. We verify the correctness of a number of examples, including programs that manipulate dags, graphs, and overlaid data structures in nontrivial ways.

Supplementary Material

JPG File (r2d3_talk4.jpg)
MP4 File (r2d3_talk4.mp4)

References

[1]
R. Bornat, C. Calcagno, and P. O'Hearn. Local reasoning, separation and aliasing. In SPACE, 2004.
[2]
R. Bornat, C. Calcagno, and H. Yang. Variables as resource in separation logic. ENTCS, 155, 2006.
[3]
R. Bornat. Proving pointer programs in Hoare logic. In MPC, 2000.
[4]
R. Cherini and J. O. Blanco. Local reasoning for abstraction and sharing. In SAC, 2009.
[5]
C. J. Cheney. A nonrecursive list compacting algorithm. C. ACM, 13(11), 1970.
[6]
C. Calcagno, P. W. O'Hearn, and H. Yang. Local action and abstract separation logic. In LICS, 2007.
[7]
R. Dockins, A. Hobor, and A. W. Appel. A fresh look at separation algebras and share accounting. In APLAS, 2009.
[8]
J. Finger. Exploiting constraints in design synthesis. PhD thesis, Stanford University, 1987.
[9]
H. Gast. Developer-oriented correctness proofs - a case study of Cheney's algorithm. In ICFEM, 2011.
[10]
P. Gardner, S. Maffeis, and G. D. Smith. Towards a program logic for JavaScript. In POPL, 2012.
[11]
A. Hobor, A. W. Appel, and F. Zappa Nardelli. Oracle semantics for concurrent separation logic. In ESOP, 2008.
[12]
A. Hobor, R. Dockins, and A. W. Appel. A logical mix of approximation and separation. In APLAS, ENTCS, 2010.
[13]
C. Hawblitzel and E. Petrank. Automated verification of practical garbage collectors. In POPL, 2009.
[14]
S. S. Ishtiaq and P. W. O'Hearn. BI as an assertion language for mutable data structures. In POPL, 2001.
[15]
N. Krishnaswami, L. Birkedal, and J. Aldrich. Verifying event-driven programs using ramified frame properties. In TLDI, 2010.
[16]
K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In LPAR, 2010.
[17]
J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In POPL, 1988.
[18]
O. Lee, H. Yang, and R. Petersen. Program analysis for overlaid data structures. In CAV, 2011.
[19]
N. Marti, R. Affeldt, and A. Yonezawa. Formal verification of the heap manager of an operating system using separation logic. In ICFEM, 2006.
[20]
F. Mehta and T. Nipkow. Proving pointer programs in higher-order logic. Inf. Comput., 199(1--2), 2005.
[21]
H. Mehnert, F. Sieczkowski, L. Birkedal, and P. Sestoft. Formalized verification of snapshotable trees: Separation and sharing. In VSTTE, 2012.
[22]
R. Manevich, S. Sagiv, G. Ramalingam, and J. Field. Partially disjunctive heap abstraction. In SAS, 2004.
[23]
J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science, Cornerstones of Computing, 2000.
[24]
J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, 2002.
[25]
J. C. Reynolds. A short course on separation logic. http://www.cs.cmu.edu/afs/cs.cmu.edu/project/fox-19/member/jcr/wwwaac2003/notes7.ps, 2003.
[26]
M. Thielscher. The qualification problem: A solution to the problem of anomalous models. Artificial Intelligence, 131(1), 2001.
[27]
N. Torp-Smith, L. Birkedal, and J. C. Reynolds. Local reasoning about a copying garbage collector. ACM TOPLAS, 30(4), 2008.
[28]
A. Urquhart. Semantics for relevant logics. J. Symb. Log., 37(1), 1972.
[29]
V. Vafeiadis. Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, 2007.
[30]
V. Vafeiadis and M. J. Parkinson. A marriage of rely/guarantee and separation logic. In CONCUR, 2007.
[31]
T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. C. Rinard. Field constraint analysis. In VMCAI, 2006.
[32]
H. Yang. Local Reasoning for Stateful Programs. PhD thesis, University of Illinois, 2001.

Cited By

View all
  • (2024)Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation LogicProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636944(45-59)Online publication date: 9-Jan-2024
  • (2024)Extending Symbolic Heap to Support Shared OwnershipDependable Software Engineering. Theories, Tools, and Applications10.1007/978-981-96-0602-3_3(46-63)Online publication date: 25-Nov-2024
  • (2023)A First-order Logic with FramesACM Transactions on Programming Languages and Systems10.1145/358305745:2(1-44)Online publication date: 15-May-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2013
586 pages
ISBN:9781450318327
DOI:10.1145/2429069
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 48, Issue 1
    POPL '13
    January 2013
    561 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2480359
    Issue’s Table of Contents
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]

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. aliasing
  2. heap/shape
  3. modularity
  4. separation logic

Qualifiers

  • Research-article

Conference

POPL '13
Sponsor:

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)25
  • Downloads (Last 6 weeks)7
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation LogicProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636944(45-59)Online publication date: 9-Jan-2024
  • (2024)Extending Symbolic Heap to Support Shared OwnershipDependable Software Engineering. Theories, Tools, and Applications10.1007/978-981-96-0602-3_3(46-63)Online publication date: 25-Nov-2024
  • (2023)A First-order Logic with FramesACM Transactions on Programming Languages and Systems10.1145/358305745:2(1-44)Online publication date: 15-May-2023
  • (2023)Omnisemantics: Smooth Handling of NondeterminismACM Transactions on Programming Languages and Systems10.1145/357983445:1(1-43)Online publication date: 8-Mar-2023
  • (2022)Diaframe: automated verification of fine-grained concurrent programs in IrisProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523432(809-824)Online publication date: 9-Jun-2022
  • (2021)Steel: proof-oriented programming in a dependently typed concurrent separation logicProceedings of the ACM on Programming Languages10.1145/34735905:ICFP(1-30)Online publication date: 19-Aug-2021
  • (2021)Functional Correctness of C Implementations of Dijkstra’s, Kruskal’s, and Prim’s AlgorithmsComputer Aided Verification10.1007/978-3-030-81688-9_37(801-826)Online publication date: 15-Jul-2021
  • (2019)Effective lock handling in stateless model checkingProceedings of the ACM on Programming Languages10.1145/33605993:OOPSLA(1-26)Online publication date: 10-Oct-2019
  • (2019)Duet: an expressive higher-order language and linear type system for statically enforcing differential privacyProceedings of the ACM on Programming Languages10.1145/33605983:OOPSLA(1-30)Online publication date: 10-Oct-2019
  • (2019)Certifying graph-manipulating C programs via localizations within data structuresProceedings of the ACM on Programming Languages10.1145/33605973:OOPSLA(1-30)Online publication date: 10-Oct-2019
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media