research-article

Verifying concurrent search structure templates

Authors:

Siddharth Krishna,

Thomas WiesAuthors Info & Claims

PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 181 - 196

https://doi.org/10.1145/3385412.3386029

Published: 11 June 2020 Publication History

Abstract

Concurrent separation logics have had great success reasoning about concurrent data structures. This success stems from their application of modularity on multiple levels, leading to proofs that are decomposed according to program structure, program state, and individual threads. Despite these advances, it remains difficult to achieve proof reuse across different data structure implementations. For the large class of search structures, we demonstrate how one can achieve further proof modularity by decoupling the proof of thread safety from the proof of structural integrity. We base our work on the template algorithms of Shasha and Goodman that dictate how threads interact but abstract from the concrete layout of nodes in memory. Building on the recently proposed flow framework of compositional abstractions and the separation logic Iris, we show how to prove correctness of template algorithms, and how to instantiate them to obtain multiple verified implementations.

We demonstrate our approach by mechanizing the proofs of three concurrent search structure templates, based on link, give-up, and lock-coupling synchronization, and deriving verified implementations based on B-trees, hash tables, and linked lists. These case studies include algorithms used in real-world file systems and databases, which have been beyond the capability of prior automated or mechanized verification techniques. In addition, our approach reduces proof complexity and is able to achieve significant proof reuse.

References

[1]

Parosh Aziz Abdulla, Frédéric Haziza, Lukás Holík, Bengt Jonsson, and Ahmed Rezine. 2013.

[2]

An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (Lecture Notes in Computer Science), Nir Piterman and Scott A. Smolka (Eds.), Vol. 7795. Springer, 324–338.

Digital Library

[3]

Parosh Aziz Abdulla, Bengt Jonsson, and Cong Quy Trinh. 2018. Fragment Abstraction for Concurrent Shape Analysis. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (Lecture Notes in Computer Science), Amal Ahmed (Ed.), Vol. 10801. Springer, 442–471. 89884-1_16

[4]

Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, and Eran Yahav. 2007. Comparison Under Abstraction for Verifying Linearizability. In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings (Lecture Notes in Computer Science), Werner Damm and Holger Hermanns (Eds.), Vol. 4590.

[5]

Springer, 477–490.

[6]

Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, and Thomas Wies. 2015. Deciding Local Theory Extensions via E-matching. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II (Lecture Notes in Computer Science), Daniel Kroening and Corina S. Pasareanu (Eds.), Vol. 9207. Springer, 87–105. 978-3-319-21668-3_6

[7]

Ales Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal. 2019.

[8]

Iron: managing obligations in higher-order concurrent separation logic. PACMPL 3, POPL (2019), 65:1–65:30.

Digital Library

[9]

Richard Bornat, Cristiano Calcagno, and Hongseok Yang. 2005. Variables as Resource in Separation Logic. In Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics, MFPS 2005, Birmingham, UK, May 18-21, 2005 (Electronic Notes in Theoretical Computer Science), Martín Hötzel Escardó, Achim Jung, and Michael W. Mislove (Eds.), Vol. 155. Elsevier, 247–276.

Digital Library

[10]

Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. 2013. Verifying Concurrent Programs against Sequential Specifications. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16- 24, 2013. Proceedings (Lecture Notes in Computer Science), Matthias Felleisen and Philippa Gardner (Eds.), Vol. 7792. Springer, 290–309.

Digital Library

[11]

Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. 2015. On Reducing Linearizability to State Reachability. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II (Lecture Notes in Computer Science), Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann (Eds.), Vol. 9135. Springer, 95–107.

Digital Library

[12]

Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Suha Orhun Mutluergil. 2017. Proving Linearizability Using Forward Simulations. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II (Lecture Notes in Computer Science), Rupak Majumdar and Viktor Kuncak (Eds.), Vol. 10427. Springer, 542–563. 319-63390-9_28

[13]

Stephen Brookes. 2007. A semantics for concurrent separation logic. Theor. Comput. Sci. 375, 1-3 (2007), 227–270. tcs.2006.12.034

Digital Library

[14]

Stephen Brookes and Peter W. O’Hearn. 2016. Concurrent separation logic. SIGLOG News 3, 3 (2016), 47–65. https://dl.acm.org/citation. cfm?id=2984457

Digital Library

[15]

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), 10-12 July 2007, Wroclaw, Poland, Proceedings. IEEE Computer Society, 366–378. LICS.2007.30

Digital Library

[16]

Pavol Cerný, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, and Rajeev Alur. 2010.

[17]

Model Checking of Linearizability of Concurrent List Implementations. In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings (Lecture Notes in Computer Science), Tayssir Touili, Byron Cook, and Paul B. Jackson (Eds.), Vol. 6174. Springer, 465–479.

Digital Library

[18]

Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. 2015. Aspect-oriented linearizability proofs. Logical Methods in Computer Science 11, 1 (2015).

[19]

Pedro da Rocha Pinto, Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, and Mark J. Wheelhouse. 2011.

[20]

A simple abstraction for complex concurrent indexes. In Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011, Portland, OR, USA, October 22 - 27, 2011, Cristina Videira Lopes and Kathleen Fisher (Eds.). ACM, 845–864.

Digital Library

[21]

Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, July 28 - August 1, 2014. Proceedings (Lecture Notes in Computer Science), Richard E. Jones (Ed.), Vol. 8586. Springer, 207–231.

Digital Library

[22]

Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2017. Concurrent Data Structures Linked in Time. In 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Barcelona, Spain (LIPIcs), Peter Müller (Ed.), Vol. 74. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 8:1–8:30.

[23]

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, Rome, Italy - January 23 - 25, 2013, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, 287–300.

Digital Library

[24]

Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings (Lecture Notes in Computer Science), Theo D’Hondt (Ed.), Vol. 6183. Springer, 504–528.

[25]

Mike Dodds, Andreas Haas, and Christoph M. Kirsch. 2015. A Scalable, Correct Time-Stamped Stack. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 233–246.

Digital Library

[26]

2676963

[27]

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 (2016), 4:1–4:72.

Digital Library

[28]

Cezara Dragoi, Ashutosh Gupta, and Thomas A. Henzinger. 2013. Automatic Linearizability Proofs of Concurrent Objects with Cooperating Verifying Concurrent Search Structure Templates PLDI ’20, June 15–20, 2020, London, UK Updates. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 174–190. 3-642-39799-8_11

[29]

Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, and Sharon Shoham. 2018.

[30]

Order out of Chaos: Proving Linearizability Using Local Views. In 32nd International Symposium on Distributed Computing, DISC 2018, New Orleans, LA, USA, October 15-19, 2018 (LIPIcs), Ulrich Schmid and Josef Widder (Eds.), Vol. 121. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 23:1–23:21.

[31]

Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. 2007. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. In Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings (Lecture Notes in Computer Science), Rocco De Nicola (Ed.), Vol. 4421. Springer, 173–188.

[32]

Ivana Filipovic, Peter W. O’Hearn, Noam Rinetzky, and Hongseok Yang. 2009.

[33]

Abstraction for Concurrent Objects. In Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings (Lecture Notes in Computer Science), Giuseppe Castagna (Ed.), Vol. 5502. Springer, 252–266. 00590-9_19

Digital Library

[34]

Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2018.

[35]

ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, Anuj Dawar and Erich Grädel (Eds.). ACM, 442–451.

Digital Library

[36]

Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, and Yu Zhang. 2010.

[37]

Reasoning about Optimistic Concurrency Using a Program Logic for History. In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings (Lecture Notes in Computer Science), Paul Gastin and François Laroussinie (Eds.), Vol. 6269. Springer, 388–402.

[38]

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 Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, Jeffrey S. Foster and Dan Grossman (Eds.). ACM, 646–661.

Digital Library

[39]

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), Jennifer L. Welch (Ed.), Vol. 2180. Springer, 300–314.

[40]

Maurice Herlihy and Jeannette M. Wing. 1990.

[41]

Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst. 12, 3 (1990), 463–492.

Digital Library

[42]

Stefan Heule, K. Rustan M. Leino, Peter Müller, and Alexander J. Summers. 2013. Abstract Read Permissions: Fractional Permissions without the Fractions. In Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings (Lecture Notes in Computer Science), Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni (Eds.), Vol. 7737.

[43]

Springer, 315–334.

Digital Library

[44]

C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (1969), 576–580.

Digital Library

[45]

363259

[46]

Cliff B. Jones. 1983. Specification and Design of (Parallel) Programs. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983, R. E. A. Mason (Ed.). North-Holland/IFIP, 321–332.

[47]

Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016.

[48]

Higher-order ghost state. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 256–269.

Digital Library

[49]

2951943

[50]

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018), e20.

[51]

Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. 2020. The future is ours: prophecy variables in separation logic. PACMPL 4, POPL (2020), 45:1–45:32.

Digital Library

[52]

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 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 637–650.

Digital Library

[53]

Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew J. Parkinson. 2017. Proving Linearizability Using Partial Orders. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (Lecture Notes in Computer Science), Hongseok Yang (Ed.), Vol. 10201. Springer, 639–667. 3-662-54434-1_24

Digital Library

[54]

Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (Lecture Notes in Computer Science), Hongseok Yang (Ed.), Vol. 10201. Springer, 696–723.

Digital Library

[55]

Siddharth Krishna, Dennis E. Shasha, and Thomas Wies. 2018. Go with the flow: compositional abstractions for concurrent data structures. PACMPL 2, POPL (2018), 37:1–37:31.

Digital Library

[56]

Siddharth Krishna, Alexander J. Summers, and Thomas Wies. 2020.

[57]

Local Reasoning for Global Graph Properties. Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 (2020). To appear.

[58]

Justin J. Levandoski and Sudipta Sengupta. 2013.

[59]

The BW-Tree: A Latch-Free B-Tree for Log-Structured Flash Storage. IEEE Data Eng. Bull. 36, 2 (2013), 56–62. http://sites.computer.org/debull/A13june/ bwtree1.pdf

[60]

Hongjin Liang and Xinyu Feng. 2013.

[61]

Modular verification of linearizability with non-fixed linearization points. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 459–470.

Digital Library

[62]

2462189

[63]

J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. 2010. Toward a verified relational database management system. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, PLDI ’20, June 15–20, 2020, London, UK Siddharth Krishna, Nisarg Patel, Dennis Shasha, and Thomas Wies 237–248.

Digital Library

[64]

Roland Meyer and Sebastian Wolff. 2019. Decoupling lock-free data structures from memory reclamation for static analysis. PACMPL 3, POPL (2019), 58:1–58:31.

Digital Library

[65]

Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. 2014. Communicating State Transition Systems for Fine-Grained Concurrent Resources. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (Lecture Notes in Computer Science), Zhong Shao (Ed.), Vol. 8410. Springer, 290–310.

Digital Library

[66]

Peter W. O’Hearn. 2007. Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375, 1-3 (2007), 271–307. tcs.2006.12.035

Digital Library

[67]

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.

[68]

Springer, 1–19.

[69]

Peter W. O’Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, and Greta Yorsh. 2010.

[70]

Verifying linearizability with hindsight. In Proceedings of the 29th Annual ACM Symposium on Principles of Distributed Computing, PODC 2010, Zurich, Switzerland, July 25-28, 2010, Andréa W. Richa and Rachid Guerraoui (Eds.). ACM, 85–94.

Digital Library

[71]

Susan S. Owicki and David Gries. 1976. Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM 19, 5 (1976), 279– 285.

Digital Library

[72]

Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2013. Automating Separation Logic Using SMT. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13- 19, 2013. Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 773–789.

[73]

Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014. GRASShopper - Complete Heap Verification with Mixed Specifications. In Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings (Lecture Notes in Computer Science), Erika Ábrahám and Klaus Havelund (Eds.), Vol. 8413. Springer, 124–139.

[74]

Azalea Raad, Jules Villard, and Philippa Gardner. 2015. CoLoSL: Concurrent Local Subjective Logic. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings (Lecture Notes in Computer Science), Jan Vitek (Ed.), Vol. 9032. Springer, 710–735.

[75]

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.

[76]

Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015. Mechanized verification of fine-grained concurrent programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, David Grove and Steve Blackburn (Eds.). ACM, 77–87.

Digital Library

[77]

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 Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, Eelco Visser and Yannis Smaragdakis (Eds.). ACM, 92–110.

Digital Library

[78]

Dennis E. Shasha and Nathan Goodman. 1988.

[79]

Concurrent Search Structure Algorithms. ACM Trans. Database Syst. 13, 1 (1988), 53–90.

Digital Library

[80]

Kasper Svendsen and Lars Birkedal. 2014. Impredicative Concurrent Abstract Predicates. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (Lecture Notes in Computer Science), Zhong Shao (Ed.), Vol. 8410. Springer, 149–168.

Digital Library

[81]

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.

Digital Library

[82]

Viktor Vafeiadis and Matthew J. Parkinson. 2007. A Marriage of Rely/Guarantee and Separation Logic. In CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings (Lecture Notes in Computer Science), Luís Caires and Vasco Thudichum Vasconcelos (Eds.), Vol. 4703.

Digital Library

[83]

Springer, 256–271.

[84]

Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, and Philippa Gardner. 2017. Abstract Specifications for Concurrent Maps. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (Lecture Notes in Computer Science), Hongseok Yang (Ed.), Vol. 10201. Springer, 964–990. 54434-1_36

Digital Library

Cited By

Murali ARivera CMadhusudan P(2024)Predictable Verification using Intrinsic DefinitionsProceedings of the ACM on Programming Languages10.1145/36564508:PLDI(1804-1829)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656450
Nguyen DBeringer LMansky WWang STimany ATraytel DPientka BBlazy S(2024)Compositional Verification of Concurrent C Programs with Search Structure TemplatesProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636940(60-74)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636940
Meyer RWies TWolff S(2023)Embedding Hindsight Reasoning in Separation LogicProceedings of the ACM on Programming Languages10.1145/35912967:PLDI(1848-1871)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591296
Show More Cited By

Index Terms

Verifying concurrent search structure templates
1. Theory of computation
  1. Design and analysis of algorithms
    1. Parallel algorithms
      1. Shared memory algorithms
  2. Logic
    1. Logic and verification
    2. Separation logic

Recommendations

Verifying concurrent multicopy search structures

Multicopy search structures such as log-structured merge (LSM) trees are optimized for high insert/update/delete (collectively known as upsert) performance. In such data structures, an upsert on key k, which adds (k,v) where v can be a value or a ...
Model checking unbounded concurrent lists

We present a model checking-based method for verifying list-based concurrent set data structures. Concurrent data structures are notorious for being hard to get right and thus, their verification has received significant attention from the verification ...
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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2020

1174 pages

ISBN:9781450376136

DOI:10.1145/3385412

General Chair:
Alastair F. Donaldson
Imperial College London, UK
,
Program Chair:
Emina Torlak
University of Washington, USA

Copyright © 2020 ACM.

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 the author(s) 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 June 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Conference

PLDI '20

Sponsor:

SIGPLAN

PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 15 - 20, 2020

London, UK

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
272
Total Downloads

Downloads (Last 12 months)42
Downloads (Last 6 weeks)4

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Murali ARivera CMadhusudan P(2024)Predictable Verification using Intrinsic DefinitionsProceedings of the ACM on Programming Languages10.1145/36564508:PLDI(1804-1829)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656450
Nguyen DBeringer LMansky WWang STimany ATraytel DPientka BBlazy S(2024)Compositional Verification of Concurrent C Programs with Search Structure TemplatesProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636940(60-74)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636940
Meyer RWies TWolff S(2023)Embedding Hindsight Reasoning in Separation LogicProceedings of the ACM on Programming Languages10.1145/35912967:PLDI(1848-1871)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591296
Koval NKhalanskiy DAlistarh D(2023)CQS: A Formally-Verified Framework for Fair and Abortable SynchronizationProceedings of the ACM on Programming Languages10.1145/35912307:PLDI(244-266)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591230
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
Schellhorn GBodenmüller SReif W(2023)Refinement and Separation: Modular Verification of Wandering TreesiFM 202310.1007/978-3-031-47705-8_12(214-234)Online publication date: 6-Nov-2023
https://doi.org/10.1007/978-3-031-47705-8_12
Meyer ROpaterny AWies TWolff S(2023)nekton: A Linearizability Proof CheckerComputer Aided Verification10.1007/978-3-031-37706-8_9(170-183)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_9
Meyer RWies TWolff S(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
https://dl.acm.org/doi/10.1007/978-3-031-30823-9_32
Meyer RWies TWolff S(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
https://dl.acm.org/doi/10.1145/3563337
He PWestbrook ECarmer BPhifer CRobert VSmeltzer KŞtefănescu ATomb AWick AYacavone MZdancewic S(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: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485512
Show More Cited By

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents