skip to main content
10.1145/2429069.2429104acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
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)Program Logics à la CarteProceedings of the ACM on Programming Languages10.1145/37048479:POPL(300-331)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 Logical Approach to Type SoundnessJournal of the ACM10.1145/367695471:6(1-75)Online publication date: 11-Nov-2024
  • Show More Cited By

Index Terms

  1. Views: compositional reasoning for concurrent programs

      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. axiomatic semantics
      2. compositional reasoning
      3. concurrency

      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)126
      • Downloads (Last 6 weeks)12
      Reflects downloads up to 19 Feb 2025

      Other Metrics

      Citations

      Cited By

      View all
      • (2025)Program Logics à la CarteProceedings of the ACM on Programming Languages10.1145/37048479:POPL(300-331)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 Logical Approach to Type SoundnessJournal of the ACM10.1145/367695471:6(1-75)Online publication date: 11-Nov-2024
      • (2024)Scenario-Based Proofs for Concurrent ObjectsProceedings of the ACM on Programming Languages10.1145/36498578:OOPSLA1(1294-1323)Online publication date: 29-Apr-2024
      • (2024)An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL LogicProceedings of the ACM on Programming Languages10.1145/36328638:POPL(604-637)Online publication date: 5-Jan-2024
      • (2024) SimplMMJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2023.103049147:COnline publication date: 17-Apr-2024
      • (2024) ThreadAbsJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2023.103046147:COnline publication date: 17-Apr-2024
      • (2024)Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore ArchitecturesThe Practice of Formal Methods10.1007/978-3-031-66676-6_4(65-87)Online publication date: 4-Sep-2024
      • (2023)When Concurrency Matters: Behaviour-Oriented ConcurrencyProceedings of the ACM on Programming Languages10.1145/36228527:OOPSLA2(1531-1560)Online publication date: 16-Oct-2023
      • (2023)Simple Reference Immutability for System F<:Proceedings of the ACM on Programming Languages10.1145/36228287:OOPSLA2(857-881)Online publication date: 16-Oct-2023
      • 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