Document Open Access Logo

Order out of Chaos: Proving Linearizability Using Local Views

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

PDF
Thumbnail PDF

File

LIPIcs.DISC.2018.23.pdf
  • Filesize: 0.76 MB
  • 21 pages

Document Identifiers

Author Details

Yotam M. Y. Feldman
  • Tel Aviv University, Israel
Constantin Enea
  • IRIF, Univ. Paris Diderot & CNRS, France
Adam Morrison
  • Tel Aviv University, Israel
Noam Rinetzky
  • Tel Aviv University, Israel
Sharon Shoham
  • Tel Aviv University, Israel

Cite As Get BibTex

Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, and Sharon Shoham. Order out of Chaos: Proving Linearizability Using Local Views. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.DISC.2018.23

Abstract

Proving the linearizability of highly concurrent data structures, such as those using optimistic concurrency control, is a challenging task. The main difficulty is in reasoning about the view of the memory obtained by the threads, because as they execute, threads observe different fragments of memory from different points in time. Until today, every linearizability proof has tackled this challenge from scratch.
We present a unifying proof argument for the correctness of unsynchronized traversals, and apply it to prove the linearizability of several highly concurrent search data structures, including an optimistic self-balancing binary search tree, the Lazy List and a lock-free skip list. Our framework harnesses sequential reasoning about the view of a thread, considering the thread as if it traverses the data structure without interference from other operations. Our key contribution is showing that properties of reachability along search paths can be deduced for concurrent traversals from such interference-free traversals, when certain intuitive conditions are met. Basing the correctness of traversals on such local view arguments greatly simplifies linearizability proofs. At the heart of our result lies a notion of order on the memory, corresponding to the order in which locations in memory are read by the threads, which guarantees a certain notion of consistency between the view of the thread and the actual memory.
To apply our framework, the user proves that the data structure satisfies two conditions: (1) acyclicity of the order on memory, even when it is considered across intermediate memory states, and (2) preservation of search paths to locations modified by interfering writes. Establishing the conditions, as well as the full linearizability proof utilizing our proof argument, reduces to simple concurrent reasoning. The result is a clear and comprehensible correctness proof, and elucidates common patterns underlying several existing data structures.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Shared memory algorithms
  • Theory of computation → Program verification
Keywords
  • concurrency and synchronization
  • concurrent data structures
  • lineariazability
  • optimistic concurrency control
  • verification and formal methods

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Parosh Aziz Abdulla, Frédéric Haziza, Lukás Holík, Bengt Jonsson, and Ahmed Rezine. An integrated specification and verification technique for highly concurrent data structures. In TACAS, pages 324-338, 2013. URL: http://dx.doi.org/10.1007/978-3-642-36742-7_23.
  2. Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, and Eran Yahav. Comparison under abstraction for verifying linearizability. In CAV '07, volume 4590 of LNCS, pages 477-490, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73368-3_49.
  3. Maya Arbel and Hagit Attiya. Concurrent Updates with RCU: Search Tree As an Example. In Proceedings of the 2014 ACM Symposium on Principles of Distributed Computing, PODC '14, pages 196-205, New York, NY, USA, 2014. ACM. URL: http://dx.doi.org/10.1145/2611462.2611471.
  4. Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, and Matthew J. Parkinson. Permission accounting in separation logic. In Jens Palsberg and Martín Abadi, editors, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pages 259-270. ACM, 2005. URL: http://dx.doi.org/10.1145/1040305.1040327.
  5. Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. Verifying concurrent programs against sequential specifications. In ESOP '13, volume 7792 of LNCS, pages 290-309. Springer, 2013. Google Scholar
  6. Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. 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, pages 95-107, 2015. Google Scholar
  7. Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Suha Orhun Mutluergil. Proving linearizability using forward simulations. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 542-563. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-63390-9_28.
  8. Nathan Grasso Bronson, Jared Casper, Hassan Chafi, and Kunle Olukotun. A practical concurrent binary search tree. In Proceedings of the 15th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2010, Bangalore, India, January 9-14, 2010, pages 257-268, 2010. Google Scholar
  9. Stephen D. Brookes. A semantics for concurrent separation logic. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, pages 16-34, 2004. URL: http://dx.doi.org/10.1007/978-3-540-28644-8_2.
  10. Trevor Brown, Faith Ellen, and Eric Ruppert. A general technique for non-blocking trees. In PPoPP, 2014. Google Scholar
  11. Austin T. Clements, M. Frans Kaashoek, and Nickolai Zeldovich. Scalable address spaces using RCU balanced trees. In ASPLOS, 2012. Google Scholar
  12. Tyler Crain, Vincent Gramoli, and Michel Raynal. A contention-friendly binary search tree. In Felix Wolf, Bernd Mohr, and Dieter an Mey, editors, Euro-Par 2013 Parallel Processing, pages 229-240, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  13. Tyler Crain, Vincent Gramoli, and Michel Raynal. No Hot Spot Non-blocking Skip List. In ICDCS, 2013. Google Scholar
  14. Tyler Crain, Vincent Gramoli, and Michel Raynal. A fast contention-friendly binary search tree. Parallel Processing Letters, 26(03):1650015, 2016. URL: http://dx.doi.org/10.1142/S0129626416500158.
  15. Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. Tada: A logic for time and data abstraction. In Richard E. Jones, editor, ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, July 28 - August 1, 2014. Proceedings, volume 8586 of Lecture Notes in Computer Science, pages 207-231. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44202-9_9.
  16. Tudor David, Rachid Guerraoui, and Vasileios Trigonakis. Asynchronized Concurrency: The Secret to Scaling Concurrent Search Data Structures. In ASPLOS, 2015. Google Scholar
  17. Dana Drachsler, Martin Vechev, and Eran Yahav. Practical Concurrent Binary Search Trees via Logical Ordering. In PPoPP, 2014. Google Scholar
  18. Cezara Dragoi, Ashutosh Gupta, and Thomas A. Henzinger. Automatic linearizability proofs of concurrent objects with cooperating updates. In CAV '13, volume 8044 of LNCS, pages 174-190. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39799-8_11.
  19. Faith Ellen, Panagiota Fatourou, Eric Ruppert, and Franck van Breugel. Non-blocking Binary Search Trees. In PODC, 2010. Google Scholar
  20. Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, and Sharon Shoham. Order out of chaos: Proving linearizability using local views. CoRR, abs/1805.03992, 2018. URL: http://arxiv.org/abs/1805.03992.
  21. Keir Fraser. Practical lock-freedom. PhD thesis, University of Cambridge, Computer Laboratory, University of Cambridge, Computer Laboratory, February 2004. Google Scholar
  22. Timothy L. Harris. A Pragmatic Implementation of Non-blocking Linked-Lists. In DISC, 2001. Google Scholar
  23. Steve Heller, Maurice Herlihy, Victor Luchangco, Mark Moir, Bill Scherer, and Nir Shavit. A lazy concurrent list-based set algorithm. In OPODIS, 2005. Google Scholar
  24. Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. Aspect-oriented linearizability proofs. In CONCUR, pages 242-256, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40184-8_18.
  25. M. P. Herlihy and J. M. Wing. Linearizability: a correctness condition for concurrent objects. TOPLAS, 12(3), 1990. Google Scholar
  26. Maurice Herlihy, Yossi Lev, Victor Luchangco, and Nir Shavit. A Simple Optimistic Skiplist Algorithm. In SIROCCO, 2007. Google Scholar
  27. Maurice Herlihy and Nir Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2008. Google Scholar
  28. Shane V. Howley and Jeremy Jones. A Non-blocking Internal Binary Search Tree. In SPAA, 2012. Google Scholar
  29. Cliff B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321-332, 1983. Google Scholar
  30. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 637-650. ACM, 2015. URL: http://dx.doi.org/10.1145/2676726.2676980.
  31. Siddharth Krishna, Dennis E. Shasha, and Thomas Wies. Go with the flow: compositional abstractions for concurrent data structures. PACMPL, 2(POPL):37:1-37:31, 2018. URL: http://dx.doi.org/10.1145/3158125.
  32. Kfir Lev-Ari, Gregory V. Chockler, and Idit Keidar. A constructive approach for proving data structures' linearizability. In Yoram Moses, editor, Distributed Computing - 29th International Symposium, DISC 2015, Tokyo, Japan, October 7-9, 2015, Proceedings, volume 9363 of Lecture Notes in Computer Science, pages 356-370. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-48653-5_24.
  33. Ruy Ley-Wild and Aleksandar Nanevski. Subjective auxiliary state for coarse-grained concurrency. In Roberto Giacobazzi and Radhia Cousot, editors, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pages 561-574. ACM, 2013. URL: http://dx.doi.org/10.1145/2429069.2429134.
  34. Hongjin Liang and Xinyu Feng. 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, pages 459-470, 2013. Google Scholar
  35. Maged M. Michael. High Performance Dynamic Lock-free Hash Tables and List-based Sets. In SPAA, 2002. Google Scholar
  36. Aravind Natarajan and Neeraj Mittal. Fast Concurrent Lock-free Binary Search Trees. In PPoPP, 2014. Google Scholar
  37. P. W. O'Hearn, N. Rinetzky, M. T. Vechev, E. Yahav, and G. Yorsh. Verifying linearizability with hindsight. In 29th Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC), pages 85-94, 2010. Google Scholar
  38. Peter W. O'Hearn. Resources, concurrency and local reasoning. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, pages 49-67, 2004. URL: http://dx.doi.org/10.1007/978-3-540-28644-8_4.
  39. Susan S. Owicki and David Gries. Verifying properties of parallel programs: An axiomatic approach. Commun. ACM, 19(5):279-285, 1976. URL: http://dx.doi.org/10.1145/360051.360224.
  40. Matthew J. Parkinson, Richard Bornat, and Peter W. O'Hearn. Modular verification of a non-blocking stack. In Martin Hofmann and Matthias Felleisen, editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 297-302. ACM, 2007. URL: http://dx.doi.org/10.1145/1190216.1190261.
  41. Arunmoezhi Ramachandran and Neeraj Mittal. A Fast Lock-Free Internal Binary Search Tree. In ICDCN, 2015. Google Scholar
  42. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Specifying and verifying concurrent algorithms with histories and subjectivity. In Jan Vitek, editor, 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, volume 9032 of Lecture Notes in Computer Science, pages 333-358. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46669-8_14.
  43. Dennis E. Shasha and Nathan Goodman. Concurrent search structure algorithms. ACM Trans. Database Syst., 13(1):53-90, 1988. URL: http://dx.doi.org/10.1145/42201.42204.
  44. Joseph R Shoenfield. The problem of predicativity. In Mathematical Logic In The 20th Century, pages 427-434. World Scientific, 2003. Google Scholar
  45. Josh Triplett, Paul E. McKenney, and Jonathan Walpole. Resizable, Scalable, Concurrent Hash Tables via Relativistic Programming. In USENIX ATC, 2011. Google Scholar
  46. Aaron Turon, Derek Dreyer, and Lars Birkedal. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 377-390. ACM, 2013. URL: http://dx.doi.org/10.1145/2500365.2500600.
  47. V. Vafeiadis. Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, 2008. Google Scholar
  48. V. Vafeiadis, M. Herlihy, T. Hoare, and M. Shapiro. Proving correctness of highly-concurrent linearisable objects. In PPoPP, 2006. Google Scholar
  49. Viktor Vafeiadis. Shape-value abstraction for verifying linearizability. In VMCAI '09: Proc. 10th Intl. Conf. on Verification, Model Checking, and Abstract Interpretation, volume 5403 of LNCS, pages 335-348. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-540-93900-9_27.
  50. Viktor Vafeiadis. Automatically proving linearizability. In CAV '10, volume 6174 of LNCS, pages 450-464, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14295-6_40.
  51. Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, and Marc Shapiro. Proving correctness of highly-concurrent linearisable objects. In PPOPP '06, pages 129-136. ACM, 2006. URL: http://dx.doi.org/10.1145/1122971.1122992.
  52. Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, and Marc Shapiro. A safety proof of a lazy concurrent list-based set implementation. Technical Report UCAM-CL-TR-659, University of Cambridge, Computer Laboratory, 2006. Google Scholar
  53. He Zhu, Gustavo Petri, and Suresh Jagannathan. 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, pages 3-19, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact