research-article

Open access

Specifying concurrent programs in separation logic: morphisms and simulations

Authors:

Aleksandar Nanevski,

Anindya Banerjee,

Germán Andrés Delbianco,

Ignacio FábregasAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue OOPSLA

Article No.: 161, Pages 1 - 30

https://doi.org/10.1145/3360587

Published: 10 October 2019 Publication History

Abstract

In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources—a form of state transition systems—to describe the state-based program invariants that must be preserved, and to record the permissible atomic changes to program state. In this paper we introduce a novel notion of resource morphism, i.e. structure-preserving function on resources, and show how to effectively integrate it into separation logic, using an associated notion of morphism-specific simulation. We apply morphisms and simulations to programs verified under one resource, to compositionally adapt them to operate under another resource, thus facilitating proof reuse.

Supplementary Material

a161-nanevski (a161-nanevski.webm)

Presentation at OOPSLA '19

Download
88.96 MB

References

[1]

Martín Abadi and Leslie Lamport. 1991. The existence of refinement mappings. Theoretical Computer Science (TCS) 82, 2 (1991), 253–284.

Digital Library

[2]

Afshin Amighi, Marieke Huisman, and Stefan Blom. 2018. Verification of shared-reading synchronisers. In International Workshop on Methods and Tools for Rigorous System Design (MeTRiD@ETAPS). 107–120.

[3]

James Aspnes, Maurice Herlihy, and Nir Shavit. 1994. Counting Networks. J. ACM 41, 5 (1994), 1020–1048.

Digital Library

[4]

Bruno Barras and Bruno Bernardo. 2008. The Implicit Calculus of Constructions as a Programming Language with Dependent Types. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS). 365–379.

[5]

Stefan Blom and Marieke Huisman. 2014. The VerCors tool for verification of concurrent programs. In International Symposium on Formal Methods (FM) (LNCS), Vol. 8442. 127–131.

Digital Library

[6]

Richard Bornat, Cristiano Calcagno, Peter W. O’Hearn, and Matthew J. Parkinson. 2005. Permission accounting in separation logic. In ACM Symposium on Principles of Programming Languages (POPL). 259–270.

Digital Library

[7]

Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Suha Orhun Mutluergil. 2017. Proving linearizability using forward simulations. In Computer Aided Verification (CAV). 542–563.

[8]

Stephen Brookes. 2007. A semantics for concurrent separation logic. Theoretical Computer Science (TCS) 375, 1-3 (2007), 227–270.

Digital Library

[9]

Andrea Cerone, Alexey Gotsman, and Hongseok Yang. 2014. Parameterised linearisability. In International Colloquium on Automata, Languages and Programming (ICALP). 98–109.

[10]

P. J. Courtois, F. Heymans, and D. L. Parnas. 1971. Concurrent control with "readers" and "writers". Commun. ACM 14, 10 (1971), 667–668.

Digital Library

[11]

Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A logic for time and data abstraction. In European Conference on Object-Oriented Programming (ECOOP). 207–231.

Digital Library

[12]

Luca de Alfaro and Thomas A. Henzinger. 2001. Interface Automata. ACM Software Engineering Notes (SEN) 26, 5 (2001), 109–120.

Digital Library

[13]

Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2017. Concurrent data structures linked in time. In European Conference on Object-Oriented Programming (ECOOP). 8:1–8:30.

[14]

John Derrick, Gerhard Schellhorn, and Heike Wehrheim. 2011. Mechanically verified proof obligations for linearizability. ACM Transactions on Programming Languages and Systems (TOPLAS) 33, 1 (2011), 4:1–4:43.

Digital Library

[15]

Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent abstract predicates. In European Conference on Object-Oriented Programming (ECOOP). 504–528.

[16]

Ivana Filipović, Peter W. O’Hearn, Noam Rinetzky, and Hongseok Yang. 2010a. Abstraction for concurrent objects. Theoretical Computer Science (TCS) 411, 51–52 (2010), 4379–4398.

Digital Library

[17]

Ivana Filipović, Peter W. O’Hearn, Noah Torp-Smith, and Hongseok Yang. 2010b. Blaming the client: on data refinement in the presence of pointers. Formal Aspects of Computing 22, 5 (2010), 547–583.

[18]

Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2018. ReLoC: a mechanised relational logic for fine-grained concurrency. In IEEE Symposium on Logic in Computer Science (LICS). 442–451.

Digital Library

[19]

Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. 2019. Definitional proof-irrelevance without K. PACMPL 3, POPL (2019), 3:1–3:28.

Digital Library

[20]

Abraham Ginzburg. 1968. Algebraic Theory of Automata. Academic Press.

[21]

Alexey Gotsman and Hongseok Yang. 2012. Linearizability with ownership transfer. In International Conference on Concurrency Theory (CONCUR). 256–271.

Digital Library

[22]

Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep specifications and certified abstraction layers. In ACM Symposium on Principles of Programming Languages (POPL). 595–608.

Digital Library

[23]

Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. 2018. Certified concurrent abstraction layers. In ACM Conference on Programming Languages Design and Implementation (PLDI). 646–661.

Digital Library

[24]

Ichiro Hasuo, Chris Heunen, Bart Jacobs, and Ana Sokolova. 2009. Coalgebraic Components in a Many-Sorted Microcosm. In Algebra and Coalgebra in Computer Science. 64–80.

[25]

Danny Hendler, Itai Incze, Nir Shavit, and Moran Tzafrir. 2010. Flat combining and the synchronization-parallelism tradeoff. In ACM Symposium on Parallelism in Algorithms and Architectures (SPAA). 355–364.

Digital Library

[26]

Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. 2013. Aspect-oriented linearizability proofs. In International Conference on Concurrency Theory (CONCUR). 242–256.

Digital Library

[27]

Maurice Herlihy and Nir Shavit. 2008. The art of multiprocessor programming. M. Kaufmann.

[28]

Maurice Herlihy and Jeannette M. Wing. 1990. Linearizability: a correctness condition for concurrent objects. ACM Transactions on Computer Systems (TOCS) 12, 3 (1990), 463–492.

Digital Library

[29]

C. A. R. Hoare. 1972. Towards a theory of parallel programming. In Operating Systems Techniques. 61–71.

[30]

Bart Jacobs. 2016. Introduction to coalgebra: towards mathematics of states and observation. Cambridge University Press.

[31]

Bart Jacobs and Frank Piessens. 2011. Expressive modular fine-grained concurrency specification. In ACM Symposium on Principles of Programming Languages (POPL). 271–282.

Digital Library

[32]

Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In Proceedings of the Third International Symposium on NASA Formal Methods (NFM 2011).

[33]

Radha Jagadeesan and James Riely. 2014. Between linearizability and quiescent consistency - quantitative quiescent consistency. In International Colloquium on Automata, Languages and Programming (ICALP). 220–231.

[34]

Cliff B. Jones. 1983. Tentative Steps Toward a Development Method for Interfering Programs. ACM Trans. Comput. Syst. 5, 4 (1983).

Digital Library

[35]

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming (JFP) 28 (2018), e20.

[36]

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In ACM Symposium on Principles of Programming Languages (POPL). 637–650.

Digital Library

[37]

Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew J. Parkinson. 2017. Proving linearizability using partial orders. In European Symposium on Programming (ESOP). 639–667.

Digital Library

[38]

Ruy Ley-Wild and Aleksandar Nanevski. 2013. Subjective auxiliary state for coarse-grained concurrency. In ACM Symposium on Principles of Programming Languages (POPL). 561–574.

Digital Library

[39]

Hongjin Liang and Xinyu Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In ACM Conference on Programming Languages Design and Implementation (PLDI). 459–470.

Digital Library

[40]

Hongjin Liang and Xinyu Feng. 2018. Progress of concurrent objects with partial methods. In ACM Symposium on Principles of Programming Languages (POPL). 20:1–20:31.

Digital Library

[41]

Hongjin Liang, Xinyu Feng, and Ming Fu. 2012. A rely-guarantee-based simulation for verifying concurrent program transformations. In ACM Symposium on Principles of Programming Languages (POPL). 455–468.

Digital Library

[42]

Hongjin Liang, Xinyu Feng, and Zhong Shao. 2014. Compositional verification of termination-preserving refinement of concurrent programs. In IEEE Symposium on Logic in Computer Science (LICS). 65:1–65:10.

Digital Library

[43]

Nancy A. Lynch and Frits W. Vaandrager. 1995. Forward and Backward Simulations: I. Untimed Systems. Inf. Comput. 121, 2 (1995), 214–233.

Digital Library

[44]

John M. Mellor-Crummey and Michael L. Scott. 1991. Algorithms for Scalable Synchronization on Shared-memory Multiprocessors. ACM Transactions on Computer Systems (TOCS) 9, 1 (1991), 21–65.

Digital Library

[45]

Robin Milner. 1978. A theory of type polymorphism in programming. J. Comput. System Sci. 17 (1978), 348–375.

[46]

P. Müller, M. Schwerhoff, and A. J. Summers. 2016. Viper: a verification infrastructure for permission-based reasoning. In Verification, Model Checking, and Abstract Interpretation (VMCAI) (LNCS), Vol. 9583. 41–62.

Digital Library

[47]

Aleksandar Nanevski. 2016. Separation Logic and Concurrency. Lecture Notes for the Oregon Programming Languages Summer School (OPLSS). https://www.cs.uoregon.edu/research/summerschool/summer16/curriculum.php

[48]

Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas. 2019a. Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations. (2019).

Digital Library

[49]

Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas. 2019b. Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations. (2019). arXiv: 1904.07136

[50]

Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. 2014. Communicating state transition systems for fine-grained concurrent resources. In European Symposium on Programming (ESOP). 290–310.

Digital Library

[51]

Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. 2006. Polymorphism and separation in Hoare Type Theory. In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming (ICFP 2006).

Digital Library

[52]

Aleksandar Nanevski, Greg Morrisett, Avi Shinnar, Paul Govereau, and Lars Birkedal. 2008. Ynot: Dependent Types for Imperative Programs. In Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008).

Digital Library

[53]

Peter W. O’Hearn. 2007. Resources, concurrency, and local reasoning. Theoretical Computer Science (TCS) 375, 1-3 (2007).

Digital Library

[54]

Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In Conference of the European Association for Computer Science Logic (CSL). 1–19.

[55]

Susan S. Owicki and David Gries. 1976. Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19, 5 (1976), 279–285.

Digital Library

[56]

Frank Pfenning. 2001. Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In IEEE Symposium on Logic in Computer Science (LICS). 221–230.

[57]

John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002).

[58]

J.J.M.M. Rutten. 2000. Universal coalgebra: a theory of systems. Theoretical Computer Science 249, 1 (2000), 3 – 80.

Digital Library

[59]

Gerhard Schellhorn, Heike Wehrheim, and John Derrick. 2012. How to prove algorithms linearisable. In Computer Aided Verification (CAV). 243–259.

Digital Library

[60]

Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015a. Mechanized Verification of Fine-grained Concurrent Programs. In ACM Conference on Programming Languages Design and Implementation (PLDI).

Digital Library

[61]

Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015b. Specifying and verifying concurrent algorithms with histories and subjectivity. In European Symposium on Programming (ESOP). 333–358.

Digital Library

[62]

Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, and Germán Andrés Delbianco. 2016. Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. In ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). 92–110.

Digital Library

[63]

Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2018. Programming and proving with distributed protocols. In ACM Symposium on Principles of Programming Languages (POPL). 28:1–28:30.

Digital Library

[64]

Kasper Svendsen and Lars Birkedal. 2014. Impredicative concurrent abstract predicates. In European Symposium on Programming (ESOP). 149–168.

Digital Library

[65]

Kasper Svendsen, Lars Birkedal, and Aleksandar Nanevski. 2011. Partiality, State and Dependent Types. In International Conference on Typed Lambda Calculi and Applications (TLCA). 198–212.

[66]

Kasper Svendsen, Lars Birkedal, and Matthew J. Parkinson. 2013. Modular reasoning about separation of concurrent data structures. In European Symposium on Programming (ESOP). 169–188.

Digital Library

[67]

R. Kent Treiber. 1986. Systems programming: coping with parallelism. Technical Report RJ 5118. IBM Almaden Research Center.

[68]

Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying refinement and Hoare-style reasoning in a logic for higherorder concurrency. In ACM International Conference on Functional Programming (ICFP). 377–390.

Digital Library

Cited By

Enea CKoskinen E(2024)Scenario-Based Proofs for Concurrent ObjectsProceedings of the ACM on Programming Languages10.1145/36498578:OOPSLA1(1294-1323)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649857
Mulder IKrebbers R(2023)Proof Automation for Linearizability in Separation LogicProceedings of the ACM on Programming Languages10.1145/35860437:OOPSLA1(462-491)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586043
Jacobs JBalzer S(2023)Higher-Order Leak and Deadlock Free LocksProceedings of the ACM on Programming Languages10.1145/35712297:POPL(1027-1057)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571229
Show More Cited By

Index Terms

Specifying concurrent programs in separation logic: morphisms and simulations

Recommendations

On algebraic abstractions for concurrent separation logics

Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins ownership transfer is that of partial commutative monoids (PCMs). Extant research considers ...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Interactive proofs in higher-order concurrent separation logic
POPL '17

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue OOPSLA

October 2019

2077 pages

EISSN:2475-1421

DOI:10.1145/3366395

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 October 2019

Published in PACMPL Volume 3, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Ministerio de Ciencia e Innovación
European Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
500
Total Downloads

Downloads (Last 12 months)83
Downloads (Last 6 weeks)18

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Enea CKoskinen E(2024)Scenario-Based Proofs for Concurrent ObjectsProceedings of the ACM on Programming Languages10.1145/36498578:OOPSLA1(1294-1323)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649857
Mulder IKrebbers R(2023)Proof Automation for Linearizability in Separation LogicProceedings of the ACM on Programming Languages10.1145/35860437:OOPSLA1(462-491)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586043
Jacobs JBalzer S(2023)Higher-Order Leak and Deadlock Free LocksProceedings of the ACM on Programming Languages10.1145/35712297:POPL(1027-1057)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571229
Spies SGäher LTassarotti JJung RKrebbers RBirkedal LDreyer D(2022)Later credits: resourceful reasoning for the later modalityProceedings of the ACM on Programming Languages10.1145/35476316:ICFP(283-311)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547631
Cook VPeterson CPainter ZDechev D(2022)Quantifiability: a concurrent correctness condition modeled in vector spaceComputing10.1007/s00607-022-01092-3105:5(955-978)Online publication date: 7-Jun-2022
https://doi.org/10.1007/s00607-022-01092-3
Fromherz ARastogi ASwamy NGibson SMartínez GMerigoux DRamananandro T(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
https://dl.acm.org/doi/10.1145/3473590
Farka FNanevski ABanerjee ADelbianco GFábregas I(2021)On algebraic abstractions for concurrent separation logicsProceedings of the ACM on Programming Languages10.1145/34342865:POPL(1-32)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434286
Schwarz MSaan SSeidl HApinis KErhard JVojdani V(2021)Improving Thread-Modular Abstract InterpretationStatic Analysis10.1007/978-3-030-88806-0_18(359-383)Online publication date: 13-Oct-2021
https://doi.org/10.1007/978-3-030-88806-0_18
Peterson CCook VDechev D(2021)Concurrent Correctness in Vector SpaceVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-67067-2_8(151-173)Online publication date: 12-Jan-2021
https://doi.org/10.1007/978-3-030-67067-2_8
Feldman YKhyzha AEnea CMorrison ANanevski ARinetzky NShoham S(2020)Proving highly-concurrent traversals correctProceedings of the ACM on Programming Languages10.1145/34281964:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428196

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents