skip to main content
research-article

Views: compositional reasoning for concurrent programs

Published: 23 January 2013 Publication History

Abstract

Compositional abstractions underly many reasoning principles for concurrent programs: the concurrent environment is abstracted in order to reason about a thread in isolation; and these abstractions are composed to reason about a program consisting of many threads. For instance, separation logic uses formulae that describe part of the state, abstracting the rest; when two threads use disjoint state, their specifications can be composed with the separating conjunction. Type systems abstract the state to the types of variables; threads may be composed when they agree on the types of shared variables.
In this paper, we present the "Concurrent Views Framework", a metatheory of concurrent reasoning principles. The theory is parameterised by an abstraction of state with a notion of composition, which we call views. The metatheory is remarkably simple, but highly applicable: the rely-guarantee method, concurrent separation logic, concurrent abstract predicates, type systems for recursive references and for unique pointers, and even an adaptation of the Owicki-Gries method can all be seen as instances of the Concurrent Views Framework. Moreover, our metatheory proves each of these systems is sound without requiring induction on the operational semantics.

Supplementary Material

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

References

[1]
A. Ahmed, M. Fluet, and G. Morrisett. L3: A linear language with locations. Fundam. Inform., 77(4):397--449, 2007.
[2]
L. Birkedal, N. Torp-Smith, and H. Yang. Semantics of separationlogic typing and higher-order frame rules for Algol-like languages. LMCS, 2(5:1), 2006.
[3]
L. Birkedal, B. Reus, J. Schwinghammer, and H. Yang. A simple model of separation logic for higher-order store. In ICALP, 2008.
[4]
R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. Permission accounting in separation logic. In POPL'05, 2005.
[5]
C. Calcagno, P. Gardner, and U. Zarfaty. Local reasoning about data update. ENTCS, 172:133--175, 2007.
[6]
C. Calcagno, P. W. O'Hearn, and H. Yang. Local action and abstract separation logic. In LICS, 2007.
[7]
A. Charguéraud and F. Pottier. Functional translation of a calculus of capabilities. In ICFP, pages 213--224, 2008.
[8]
T. Dinsdale-Young. Abstract Data and Local Reasoning. PhD thesis, Imperial College, Department of Computing, 2010.
[9]
T. Dinsdale-Young, M. Dodds, P. Gardner, M. J. Parkinson, and V. Vafeiadis. Concurrent abstract predicates. In ECOOP, 2010.
[10]
T. Dinsdale-Young, P. Gardner, and M. Wheelhouse. Abstraction and refinement for local reasoning. In VSTTE, 2010.
[11]
T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, and H. Yang. Views: Compositional reasoning for concurrent programs (technical report and addditional material). http://sites.google.com/site/viewsmodel/, 2012.
[12]
R. Dockins, A. Hobor, and A. W. Appel. A fresh look at separation algebras and share accounting. In APLAS, 2009.
[13]
M. Dodds, X. Feng, M. J. Parkinson, and V. Vafeiadis. Deny-guarantee reasoning. In ESOP, pages 363--377, 2009.
[14]
X. Feng. Local rely-guarantee reasoning. In POPL, 2009.
[15]
X. Feng, R. Ferreira, and Z. Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP, pages 173--188, 2007.
[16]
P. Gardner, G. Nzik, and A. Wright. Reasoning about POSIX file systems using structural separation logic. Draft, 2012.
[17]
C. Gordon, M. Parkinson, J. Parsons, A. Bromfield, and J. Duffy. Uniqueness and reference immutability for safe parallelism. In OOPSLA, 2012.
[18]
S. S. Ishtiaq and P. W. O'Hearn. BI as an assertion language for mutable data structures. In POPL, pages 14--26, 2001.
[19]
J. B. Jensen and L. Birkedal. Fictional separation logic. In ESOP, 2012.
[20]
C. B. Jones. Tentative steps toward a development method for interfering programs. ACM TOPLAS, 5(4):596--619, 1983.
[21]
N. Krishnaswami, L. Birkedal, and J. Aldrich. Verifying event-driven programs using ramified frame properties. In TLDI, 2010.
[22]
N. Krishnaswami, A. Turon, D. Dreyer, and D. Garg. Superficially substructural types. In ICFP, 2012.
[23]
G. Morrisett, D. Walker, K. Crary, and N. Glew. From system F to typed assembly language. TOPLAS, 21(3):527--568, 1999.
[24]
S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6(4):319--340, 1976.
[25]
M. J. Parkinson, R. Bornat, and P. O'Hearn. Modular verification of a non-blocking stack. In POPL, 2007.
[26]
F. Pottier. Syntactic soundness proof of a type-and-capability system with hidden state. Technical report, INRIA, 2011.
[27]
J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, 2002.
[28]
J. Smans, B. Jacobs, and F. Piessens. Implicit dynamic frames: Combining dynamic frames and separation logic. In ECOOP, 2009.
[29]
F. Smith, D. Walker, and J. G. Morrisett. Alias types. In ESOP, 2000.
[30]
K. Svendsen, L. Birkedal, and M. Parkinson. A specification of the joins library in higher-order separation logic. Technical report, IT University of Copenhagen, 2012.
[31]
V. Vafeiadis and M. J. Parkinson. A marriage of rely/guarantee and separation logic. In CONCUR, pages 256--271, 2007.

Cited By

View all
  • (2025)Generically Automating Separation Logic by Functors, Homomorphisms, and ModulesProceedings of the ACM on Programming Languages10.1145/37049039:POPL(1992-2024)Online publication date: 9-Jan-2025
  • (2024)Realistic Realizability: Specifying ABIs You Can Count OnProceedings of the ACM on Programming Languages10.1145/36897558:OOPSLA2(1249-1278)Online publication date: 8-Oct-2024
  • (2024)A Rely-Guarantee Framework for Proving Deadlock Freedom Under Causal ConsistencyThe Practice of Formal Methods10.1007/978-3-031-66676-6_5(88-108)Online publication date: 4-Sep-2024
  • Show More Cited By

Index Terms

  1. Views: compositional reasoning for concurrent programs

      Recommendations

      Comments

      Information & Contributors

      Information

      Published In

      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
      • 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
      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: 23 January 2013
      Published in SIGPLAN Volume 48, Issue 1

      Check for updates

      Author Tags

      1. axiomatic semantics
      2. compositional reasoning
      3. concurrency

      Qualifiers

      • Research-article

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

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

      Other Metrics

      Citations

      Cited By

      View all
      • (2025)Generically Automating Separation Logic by Functors, Homomorphisms, and ModulesProceedings of the ACM on Programming Languages10.1145/37049039:POPL(1992-2024)Online publication date: 9-Jan-2025
      • (2024)Realistic Realizability: Specifying ABIs You Can Count OnProceedings of the ACM on Programming Languages10.1145/36897558:OOPSLA2(1249-1278)Online publication date: 8-Oct-2024
      • (2024)A Rely-Guarantee Framework for Proving Deadlock Freedom Under Causal ConsistencyThe Practice of Formal Methods10.1007/978-3-031-66676-6_5(88-108)Online publication date: 4-Sep-2024
      • (2023)Concise outlines for a complex logic: a proof outline checker for TaDAFormal Methods in System Design10.1007/s10703-023-00427-w61:1(110-136)Online publication date: 31-Jul-2023
      • (2023)Make Flows Small Again: Revisiting the Flow FrameworkTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30823-9_32(628-646)Online publication date: 22-Apr-2023
      • (2023)A Fine-Grained Semantics for Arrays and Pointers Under Weak Memory ModelsFormal Methods10.1007/978-3-031-27481-7_18(301-320)Online publication date: 6-Mar-2023
      • (2022)A concurrent program logic with a future and historyProceedings of the ACM on Programming Languages10.1145/35633376:OOPSLA2(1378-1407)Online publication date: 31-Oct-2022
      • (2022)Reasoning about distributed reconfigurable systemsProceedings of the ACM on Programming Languages10.1145/35632936:OOPSLA2(145-174)Online publication date: 31-Oct-2022
      • (2022)Decision Problems in a Logic for Reasoning About Reconfigurable Distributed SystemsAutomated Reasoning10.1007/978-3-031-10769-6_40(691-711)Online publication date: 8-Aug-2022
      • (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
      • 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