Abstract
Concurrent separation logics have helped to significantly simplify correctness proofs for concurrent data structures. However, a recurring problem in such proofs is that data structure abstractions that work well in the sequential setting are much harder to reason about in a concurrent setting due to complex sharing and overlays. To solve this problem, we propose a novel approach to abstracting regions in the heap by encoding the data structure invariant into a local condition on each individual node. This condition may depend on a quantity associated with the node that is computed as a fixpoint over the entire heap graph. We refer to this quantity as a flow. Flows can encode both structural properties of the heap (e.g. the reachable nodes from the root form a tree) as well as data invariants (e.g. sortedness). We then introduce the notion of a flow interface, which expresses the relies and guarantees that a heap region imposes on its context to maintain the local flow invariant with respect to the global heap. Our main technical result is that this notion leads to a new semantic model of separation logic. In this model, flow interfaces provide a general abstraction mechanism for describing complex data structures. This abstraction mechanism admits proof rules that generalize over a wide variety of data structures. To demonstrate the versatility of our approach, we show how to extend the logic RGSep with flow interfaces. We have used this new logic to prove linearizability and memory safety of nontrivial concurrent data structures. In particular, we obtain parametric linearizability proofs for concurrent dictionary algorithms that abstract from the details of the underlying data structure representation. These proofs cannot be easily expressed using the abstraction mechanisms provided by existing separation logics.
Supplemental Material
- Josh Berdine, Cristiano Calcagno, and Peter O’Hearn. 2004. A Decidable Fragment of Separation Logic. In FSTTCS. Springer. Google ScholarDigital Library
- Richard Bornat, Cristiano Calcagno, Peter O’Hearn, and Matthew Parkinson. 2005. Permission Accounting in Separation Logic. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’05). ACM, New York, NY, USA, 259–270. Google ScholarDigital Library
- Richard Bornat, Cristiano Calcagno, and Hongseok Yang. 2006. Variables As Resource in Separation Logic. Electron. Notes Theor. Comput. Sci. 155 (May 2006), 247–276. Google ScholarDigital Library
- Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. 2012. Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data. In ATVA (LNCS), Vol. 7561. Springer, 167–182. Google ScholarDigital Library
- Stephen Brookes and Peter W. O’Hearn. 2016. Concurrent separation logic. SIGLOG News 3, 3 (2016), 47–65. Google ScholarDigital Library
- James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. 2011. Automated Cyclic Entailment Proofs in Separation Logic. In 23rd International Conference on Automated Deduction, CADE-23 (Lecture Notes in Computer Science), Vol. 6803. Springer, 131–146. Google ScholarCross Ref
- Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2009. Compositional shape analysis by means of bi-abduction. In POPL. Google ScholarDigital Library
- Cristiano Calcagno, Peter W. O’Hearn, and Hongseok Yang. 2007. Local Action and Abstract Separation Logic. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007). IEEE Computer Society, 366–378. Google ScholarDigital Library
- Adam Chlipala. 2011. Mostly-automated verification of low-level programs in computational separation logic. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011. ACM, 234–245. Google ScholarDigital Library
- Byron Cook, Christoph Haase, Joël Ouaknine, Matthew Parkinson, and James Worrell. 2011. Tractable Reasoning in a Fragment of Separation Logic. In CONCUR. Springer. Google ScholarCross Ref
- Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th POPL. Google ScholarDigital Library
- Pedro da Rocha Pinto, Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, and Mark J. Wheelhouse. 2011. A simple abstraction for complex concurrent indexes. In Proceedings of the 26th Annual ACM SIGPLAN Conference on ObjectOriented Programming, Systems, Languages, and Applications, OOPSLA 2011. ACM, 845–864. Google ScholarDigital Library
- Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In 28th European Conference on Object-Oriented Programming, ECOOP 2014 (Lecture Notes in Computer Science), Vol. 8586. Springer, 207–231. Google ScholarDigital Library
- Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. 2016. Modular Termination Verification for Non-blocking Concurrency. In 25th European Symposium on Programming, ESOP 2016 (Lecture Notes in Computer Science), Vol. 9632. Springer, 176–201. Google ScholarCross Ref
- Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, and Hongseok Yang. 2013. Views: compositional reasoning for concurrent programs. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13. ACM, 287–300. Google ScholarDigital Library
- Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In 24th European Conference on Object-Oriented Programming, ECOOP 2010 (Lecture Notes in Computer Science), Vol. 6183. Springer, 504–528. Google ScholarCross Ref
- Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2006. A Local Shape Analysis Based on Separation Logic. In Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 (Lecture Notes in Computer Science), Vol. 3920. Springer, 287–302. Google ScholarDigital Library
- Robert Dockins, Aquinas Hobor, and Andrew W. Appel. 2009. A Fresh Look at Separation Algebras and Share Accounting. In Proceedings of the 7th Asian Symposium on Programming Languages and Systems, APLAS 2009. Springer-Verlag, Berlin, Heidelberg, 161–177. Google ScholarDigital Library
- Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, and Lars Birkedal. 2016. Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic. ACM Trans. Program. Lang. Syst. 38, 2, Article 4 (Jan. 2016), 72 pages. Google ScholarDigital Library
- Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomás Vojnar. 2017. SPEN: A Solver for Separation Logic. In NASA Formal Methods, NFM 2017 (Lecture Notes in Computer Science), Vol. 10227. Springer, 302–309. Google ScholarCross Ref
- Constantin Enea, Mihaela Sighireanu, and Zhilin Wu. 2015. On Automated Lemma Generation for Separation Logic with Inductive Definitions. In 13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015 (Lecture Notes in Computer Science), Vol. 9364. Springer, 80–96. Google ScholarCross Ref
- Xinyu Feng. 2009. Local rely-guarantee reasoning. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 315–327. Google ScholarDigital Library
- Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. 2007. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. In 16th European Symposium on Programming, ESOP 2007 (Lecture Notes in Computer Science), Vol. 4421. Springer, 173–188. Google ScholarCross Ref
- Didier Galmiche and Dominique Larchey-Wendling. 2006. Expressivity Properties of Boolean BI Through Relational Models. In 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006, S. Arun-Kumar and Naveen Garg (Eds.). Springer, Berlin, Heidelberg, 357–368. Google ScholarDigital Library
- 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 Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015. ACM, 595–608. Google ScholarDigital Library
- Timothy L. Harris. 2001. A Pragmatic Implementation of Non-blocking Linked-Lists. In Distributed Computing, 15th International Conference, DISC 2001, Lisbon, Portugal, October 3-5, 2001, Proceedings (Lecture Notes in Computer Science), Vol. 2180. Springer, 300–314. Google ScholarCross Ref
- Maurice Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst. 12, 3 (1990), 463–492. Google ScholarDigital Library
- Stefan Heule, K. Rustan M. Leino, Peter Müller, and Alexander J. Summers. 2013. Abstract Read Permissions: Fractional Permissions without the Fractions. In 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013 (Lecture Notes in Computer Science), Vol. 7737. Springer, 315–334. Google ScholarDigital Library
- Aquinas Hobor and Jules Villard. 2013. The Ramifications of Sharing in Data Structures. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’13). ACM, New York, NY, USA, 523–536. Google ScholarDigital Library
- Zhé Hóu, Ranald Clouston, Rajeev Goré, and Alwen Tiu. 2014. Proof Search for Propositional Abstract Separation Logics via Labelled Sequents. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014. ACM, New York, NY, USA, 465–476. Google ScholarDigital Library
- Radu Iosif, Adam Rogalewicz, and Tomás Vojnar. 2014. Deciding Entailments in Inductive Separation Logic with Tree Automata. In 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014 (Lecture Notes in Computer Science), Vol. 8837. Springer, 201–218. Google ScholarCross Ref
- 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 Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). ACM, New York, NY, USA, 637–650. Google ScholarDigital Library
- Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In 26th European Symposium on Programming, ESOP 2017 (Lecture Notes in Computer Science), Vol. 10201. Springer, 696–723. Google ScholarDigital Library
- Siddharth Krishna, Dennis Shasha, and Thomas Wies. 2017. Go with the Flow: Compositional Abstractions for Concurrent Data Structures (Extended Version). CoRR abs/1711.03272 (2017). arXiv: 1711.03272 http://arxiv.org/abs/1711.03272Google Scholar
- Philip L. Lehman and s. Bing Yao. 1981. Efficient Locking for Concurrent Operations on B-trees. ACM Trans. Database Syst. 6, 4 (Dec. 1981), 650–670. Google ScholarDigital Library
- Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, and Peter Sestoft. 2012. Formalized Verification of Snapshotable Trees: Separation and Sharing. In Verified Software: Theories, Tools, Experiments - 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings (Lecture Notes in Computer Science), Vol. 7152. Springer, 179–195. Google ScholarDigital Library
- Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2016. Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. In Computer Aided Verification CAV (Lecture Notes in Computer Science), Vol. 9779. Springer, 405–425. Google ScholarCross Ref
- Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. 2014. Communicating State Transition Systems for Fine-Grained Concurrent Resources. In 23rd European Symposium on Programming, ESOP 2014 (Lecture Notes in Computer Science), Vol. 8410. Springer, 290–310. Google ScholarDigital Library
- Huu Hai Nguyen and Wei-Ngan Chin. 2008. Enhancing Program Verification with Lemmas. In 20th International Conference on Computer Aided Verification, CAV 2008 (Lecture Notes in Computer Science), Vol. 5123. Springer, 355–369. Google ScholarDigital Library
- Peter W. O’Hearn. 2004. Resources, Concurrency and Local Reasoning. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings (Lecture Notes in Computer Science), Vol. 3170. Springer, 49–67. Google ScholarCross Ref
- Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings (Lecture Notes in Computer Science), Laurent Fribourg (Ed.), Vol. 2142. Springer, 1–19. Google ScholarCross Ref
- Edgar Pek, Xiaokang Qiu, and P. Madhusudan. 2014. Natural proofs for data structure manipulation in C using separation logic. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014. ACM, 440–451. Google ScholarDigital Library
- Juan Antonio Navarro Pérez and Andrey Rybalchenko. 2011. Separation logic + superposition calculus = heap theorem prover. In PLDI. ACM, 556–566.Google Scholar
- Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2013. Automating Separation Logic Using SMT. In CAV (LNCS), Vol. 8044. Springer, 773–789. Google ScholarDigital Library
- Azalea Raad, Aquinas Hobor, Jules Villard, and Philippa Gardner. 2016. Verifying Concurrent Graph Algorithms. In Asian Symposium on Programming Languages and Systems APLAS (Lecture Notes in Computer Science), Vol. 10017. 314–334. Google ScholarCross Ref
- Andrew Reynolds, Radu Iosif, and Cristina Serban. 2017. Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic. In Verification, Model Checking, and Abstract Interpretation, VMCAI 2017 (Lecture Notes in Computer Science), Vol. 10145. Springer, 462–482. Google ScholarCross Ref
- John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. IEEE Computer Society, 55–74. Google ScholarCross Ref
- Shmuel Sagiv, Thomas W. Reps, and Reinhard Wilhelm. 2002. Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24, 3 (2002), 217–298. Google ScholarDigital Library
- Dennis E. Shasha and Nathan Goodman. 1988. Concurrent Search Structure Algorithms. ACM Trans. Database Syst. 13, 1 (1988), 53–90. Google ScholarDigital Library
- Makoto Tatsuta, Quang Loc Le, and Wei-Ngan Chin. 2016. Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic. In 14th Asian Symposium on Programming Languages and Systems, APLAS 2016 (Lecture Notes in Computer Science), Vol. 10017. Springer, 423–443. Google ScholarCross Ref
- Viktor Vafeiadis. 2008. Modular fine-grained concurrency verification. Ph.D. Dissertation. University of Cambridge, UK. http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.612221Google Scholar
- Viktor Vafeiadis. 2009. Shape-Value Abstraction for Verifying Linearizability. In Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings (Lecture Notes in Computer Science), Neil D. Jones and Markus Müller-Olm (Eds.), Vol. 5403. Springer, 335–348. Google ScholarDigital Library
- Viktor Vafeiadis. 2010. RGSep Action Inference. In Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceedings (Lecture Notes in Computer Science), Gilles Barthe and Manuel V. Hermenegildo (Eds.), Vol. 5944. Springer, 345–361. Google ScholarDigital Library
- Viktor Vafeiadis and Matthew J. Parkinson. 2007. A Marriage of Rely/Guarantee and Separation Logic. In 18th International Conference on Concurrency Theory, CONCUR 2007 (Lecture Notes in Computer Science), Vol. 4703. Springer, 256–271. Google ScholarCross Ref
- Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, and Philippa Gardner. 2017. Abstract Specifications for Concurrent Maps. In 26th European Symposium on Programming, ESOP 2017 (Lecture Notes in Computer Science), Vol. 10201. Springer, 964–990. Google ScholarDigital Library
- Hongseok Yang. 2001. An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. In Proceedings of the SPACE Workshop.Google Scholar
Index Terms
- Go with the flow: compositional abstractions for concurrent data structures
Recommendations
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
Efficient implementations of data structures such as queues, stacks or hash-tables allow for concurrent access by many processes at the same time. To increase concurrency, these algorithms often completely dispose with locking, or only lock small parts ...
Looking for efficient implementations of concurrent objects
PaCT'11: Proceedings of the 11th international conference on Parallel computing technologiesAs introduced by Taubenfeld, a contention-sensitive implementation of a concurrent object is an implementation such that the overhead introduced by locking is eliminated in the common cases, i.e., when there is no contention or when the operations ...
Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement
SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied ComputingCompiling concurrent and managed languages involves implementing sophisticated interactions between client code and the runtime system. An emblematic runtime service, whose implementation is particularly error-prone, is concurrent garbage collection. In ...
Comments