skip to main content
research-article
Open access

Proving highly-concurrent traversals correct

Published: 13 November 2020 Publication History

Editorial Notes

A corrigendum was issued for this paper on April 25, 2024. You can download the corrigendum from the supplemental material section of this citation page.

Abstract

Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any synchronization. As a result, however, these algorithms are notoriously difficult to prove linearizable, which requires identifying a point in time in which the traversal's result is correct. The problem is that traversing the data structure as it undergoes modifications leads to complex behaviors, necessitating intricate reasoning about all interleavings of reads by traversals and writes mutating the data structure.
In this paper, we present a general proof technique for proving unsynchronized traversals correct in a significantly simpler manner, compared to typical concurrent reasoning and prior proof techniques. Our framework relies only on sequential properties of traversals and on a conceptually simple and widely-applicable condition about the ways an algorithm's writes mutate the data structure. Establishing that a target data structure satisfies our condition requires only simple concurrent reasoning, without considering interactions of writes and reads. This reasoning can be further simplified by using our framework.
To demonstrate our technique, we apply it to prove several interesting and challenging concurrent binary search trees: the logical-ordering AVL tree, the Citrus tree, and the full contention-friendly tree. Both the logical-ordering tree and the full contention-friendly tree are beyond the reach of previous approaches targeted at simplifying linearizability proofs.

Supplementary Material

Auxiliary Presentation Video (oopsla20main-p13-p-video.mp4)
3428196-corrigendum (3428196-corrigendum.pdf)
Corrigendum to "Proving highly-concurrent traversals correct" by Feldman et al., Proceedings of the ACM on Programming Languages, Volume 4, Issue OOPSLA (PACMPL 4:OOPSLA).

References

[1]
Parosh Aziz Abdulla, Frédéric Haziza, Lukás Holík, Bengt Jonsson, and Ahmed Rezine. 2013. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In TACAS. 324-338.
[2]
Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, and Eran Yahav. 2007. Comparison Under Abstraction for Verifying Linearizability. In CAV '07 (LNCS), Vol. 4590. 477-490.
[3]
Maya Arbel and Hagit Attiya. 2014. Concurrent Updates with RCU: Search Tree As an Example. In PODC 2014.
[4]
Hagit Attiya, G. Ramalingam, and Noam Rinetzky. 2010. Sequential verification of serializability. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. 31-42. https://doi.org/10.1145/1706299.1706305
[5]
Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, and Matthew J. Parkinson. 2005. Permission accounting in separation logic. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005. 259-270. https://doi.org/10.1145/1040305.1040327
[6]
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. 2013. Verifying Concurrent Programs against Sequential Specifications. In ESOP '13 (LNCS), Vol. 7792. Springer, 290-309.
[7]
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. 95-107.
[8]
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. 542-563. https://doi.org/10.1007/978-3-319-63390-9_28
[9]
Nathan G. Bronson, Jared Casper, Hassan Chafi, and Kunle Olukotun. 2010. A Practical Concurrent Binary Search Tree. In PPoPP 2010.
[10]
Stephen D. Brookes. 2004. A Semantics for Concurrent Separation Logic. In CONCUR 2004-Concurrency Theory, 15th International Conference, London, UK, August 31-September 3, 2004, Proceedings. 16-34. https://doi.org/10.1007/978-3-540-28644-8_2
[11]
Trevor Brown, Faith Ellen, and Eric Ruppert. 2014. A General Technique for Non-blocking Trees. In PPoPP 2014.
[12]
Austin T. Clements, M. Frans Kaashoek, and Nickolai Zeldovich. 2012. Scalable address spaces using RCU balanced trees. In ASPLOS 2012.
[13]
Tyler Crain, Vincent Gramoli, and Michel Raynal. 2013a. A Contention-Friendly Binary Search Tree. In Euro-Par 2013.
[14]
Tyler Crain, Vincent Gramoli, and Michel Raynal. 2013b. No Hot Spot Non-blocking Skip List. In ICDCS 2013.
[15]
Tyler Crain, Vincent Gramoli, and Michel Raynal. 2016. A Fast Contention-Friendly Binary Search Tree. Parallel Processing Letters 26, 03 ( 2016 ).
[16]
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. 207-231. https://doi.org/10.1007/978-3-662-44202-9_9
[17]
Tudor David, Rachid Guerraoui, and Vasileios Trigonakis. 2015. Asynchronized Concurrency: The Secret to Scaling Concurrent Search Data Structures. In ASPLOS 2015.
[18]
Mathieu Desnoyers, Paul E. McKenney, Alan S. Stern, Michel R. Dagenais, and Jonathan Walpole. 2012. User-Level Implementations of Read-Copy Update. IEEE Trans. Parallel Distrib. Syst. 23, 2 ( 2012 ), 375-382.
[19]
Dana Drachsler, Martin Vechev, and Eran Yahav. 2014. Practical Concurrent Binary Search Trees via Logical Ordering. In PPoPP 2014.
[20]
Cezara Dragoi, Ashutosh Gupta, and Thomas A. Henzinger. 2013. Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In CAV '13 (LNCS), Vol. 8044. Springer, 174-190.
[21]
Faith Ellen, Panagiota Fatourou, Eric Ruppert, and Franck van Breugel. 2010. Non-blocking Binary Search Trees. In PODC 2010.
[22]
Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, and Sharon Shoham. 2018. Order out of Chaos: Proving Linearizability Using Local Views. In DISC 2018.
[23]
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, and Sharon Shoham. 2020. Proving Highly-Concurrent Traversals Correct. CoRR ( 2020 ). https://arxiv.org/abs/ 2010.00911
[24]
Keir Fraser. 2004. Practical lock-freedom. Ph.D. Dissertation. University of Cambridge, Computer Laboratory.
[25]
Vincent Gramoli. 2015. More than you ever wanted to know about synchronization: synchrobench, measuring the impact of the synchronization on concurrent algorithms. In PPoPP 2015.
[26]
Timothy L. Harris. 2001. A Pragmatic Implementation of Non-blocking Linked-Lists. In DISC 2001.
[27]
Steve Heller, Maurice Herlihy, Victor Luchangco, Mark Moir, Bill Scherer, and Nir Shavit. 2005. A Lazy Concurrent List-based Set Algorithm. In OPODIS 2005.
[28]
Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. 2013. Aspect-Oriented Linearizability Proofs. In CONCUR. 242-256.
[29]
Maurice Herlihy, Yossi Lev, Victor Luchangco, and Nir Shavit. 2007. A Simple Optimistic Skiplist Algorithm. In SIROCCO 2007.
[30]
Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA.
[31]
M. P. Herlihy and J. M. Wing. 1990. Linearizability: a correctness condition for concurrent objects. 12, 3 ( 1990 ).
[32]
Shane V. Howley and Jeremy Jones. 2012. A Non-blocking Internal Binary Search Tree. In SPAA 2012.
[33]
Clif B. Jones. 1983. Specification and Design of (Parallel) Programs. In IFIP Congress. 321-332.
[34]
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. https://doi.org/10.1017/S0956796818000151
[35]
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. Proc. ACM Program. Lang. 4, POPL ( 2020 ), 45 : 1-45 : 32. https://doi.org/10.1145/3371113
[36]
Siddharth Krishna, Nisarg Patel, Dennis Shasha, and Thomas Wies. 2020. Verifying Concurrent Search Structure Templates. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010. ACM.
[37]
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. https://doi.org/10.1145/3158125
[38]
Kfir Lev-Ari, Gregory V. Chockler, and Idit Keidar. 2015a. A Constructive Approach for Proving Data Structures' Linearizability. In DISC 205.
[39]
Kfir Lev-Ari, Gregory V. Chockler, and Idit Keidar. 2015b. A Constructive Approach for Proving Data Structures' Linearizability. In Distributed Computing-29th International Symposium, DISC 2015, Tokyo, Japan, October 7-9, 2015, Proceedings. 356-370. https://doi.org/10.1007/978-3-662-48653-5_24
[40]
Ruy Ley-Wild and Aleksandar Nanevski. 2013. Subjective auxiliary state for coarse-grained concurrency. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy-January 23-25, 2013. 561-574. https://doi.org/10.1145/2429069.2429134
[41]
Hongjin Liang and Xinyu Feng. 2013. 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. 459-470.
[42]
Yandong Mao, Eddie Kohler, and Robert Tappan Morris. 2012. Cache Craftiness for Fast Multicore Key-value Storage. In EuroSys 2012.
[43]
Paul McKenney. 2004. Exploiting deferred destruction: an analysis of read-copy-update techniques in operating system kernels. Ph.D. Dissertation. OGI.
[44]
Paul E. McKenney and John D. Slingwine. 1998. Read-copy update: using execution history to solve concurrency problems. In PDCS.
[45]
Maged M. Michael. 2002. High Performance Dynamic Lock-free Hash Tables and List-based Sets. In SPAA 2002.
[46]
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas. 2019. Specifying concurrent programs in separation logic: morphisms and simulations. Proc. ACM Program. Lang. 3, OOPSLA ( 2019 ), 161 : 1-161 : 30. https://doi.org/10.1145/3360587
[47]
Aravind Natarajan and Neeraj Mittal. 2014. Fast Concurrent Lock-free Binary Search Trees. In PPoPP 2014.
[48]
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. 49-67. https://doi.org/10.1007/978-3-540-28644-8_4
[49]
P. W. O'Hearn, N. Rinetzky, M. T. Vechev, E. Yahav, and G. Yorsh. 2010. Verifying Linearizability with Hindsight. In PODC 2010.
[50]
Susan S. Owicki and David Gries. 1976. Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM 19, 5 ( 1976 ), 279-285. https://doi.org/10.1145/360051.360224
[51]
Matthew J. Parkinson, Richard Bornat, and Peter W. O'Hearn. 2007. Modular verification of a non-blocking stack. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007. 297-302. https://doi.org/10.1145/1190216.1190261
[52]
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. 710-735. https: //doi.org/10.1007/978-3-662-46669-8_29
[53]
Arunmoezhi Ramachandran and Neeraj Mittal. 2015. A Fast Lock-Free Internal Binary Search Tree. In ICDCN 2015.
[54]
Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. 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. 333-358. https://doi.org/10.1007/978-3-662-46669-8_14
[55]
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. 92-110. https://doi.org/10.1145/2983990.2983999
[56]
Dennis E. Shasha and Nathan Goodman. 1988. Concurrent Search Structure Algorithms. ACM Trans. Database Syst. 13, 1 ( 1988 ), 53-90.
[57]
Josh Triplett, Paul E. McKenney, and Jonathan Walpole. 2011. Resizable, Scalable, Concurrent Hash Tables via Relativistic Programming. In USENIX ATC 2011.
[58]
Stephen Tu, Wenting Zheng, Eddie Kohler, Barbara Liskov, and Samuel Madden. 2013. Speedy Transactions in Multicore In-memory Databases. In SOSP 2013.
[59]
Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying refinement and hoare-style reasoning in a logic for higherorder concurrency. In ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA-September 25-27, 2013. 377-390. https://doi.org/10.1145/2500365.2500600
[60]
V. Vafeiadis. 2008. Modular fine-grained concurrency verification. Ph.D. Dissertation. University of Cambridge.
[61]
Viktor Vafeiadis. 2009. Shape-Value Abstraction for Verifying Linearizability. In VMCAI '09: Proc. 10th Intl. Conf. on Verification, Model Checking, and Abstract Interpretation (LNCS), Vol. 5403. Springer, 335-348.
[62]
Viktor Vafeiadis. 2010. Automatically Proving Linearizability. 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, 450-464. https://doi.org/10.1007/978-3-642-14295-6_40
[63]
Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, and Marc Shapiro. 2006. A safety proof of a lazy concurrent list-based set implementation. Technical Report UCAM-CL-TR-659. University of Cambridge, Computer Laboratory.
[64]
Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, and Marc Shapiro. 2016. Proving correctness of highly-concurrent linearisable objects. In PPOPP '06. ACM, 129-136.
[65]
He Zhu, Gustavo Petri, and Suresh Jagannathan. 2015. Poling: SMT Aided Linearizability Proofs. In Computer Aided Verification-27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II. 3-19.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages  Volume 4, Issue OOPSLA
November 2020
3108 pages
EISSN:2475-1421
DOI:10.1145/3436718
Issue’s Table of Contents
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: 13 November 2020
Published in PACMPL Volume 4, Issue OOPSLA

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. concurrent data structures
  2. linearizability
  3. proof framework
  4. traversal
  5. traversal correctness

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)208
  • Downloads (Last 6 weeks)31
Reflects downloads up to 24 Dec 2024

Other Metrics

Citations

Cited By

View all

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media