Document Open Access Logo

Checking Linearizability of Concurrent Priority Queues

Authors Ahmed Bouajjani, Constantin Enea, Chao Wang

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2017.16.pdf
  • Filesize: 0.65 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • Concurrency
  • Linearizability
  • Model Checking

Metrics

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

Abstract

Efficient implementations of concurrent objects such as atomic collections are essential to modern computing. Unfortunately their correctness criteria — linearizability with respect to given ADT specifications — are hard to verify. Verifying linearizability is undecidable in general, even on classes of implementations where the usual control-state reachability is decidable. In this work we consider concurrent priority queues which are fundamental to many multi-threaded applications like task scheduling or discrete event simulation, and show that verifying linearizability of such implementations is reducible to control-state reachability. This reduction entails the first decidability results for verifying concurrent priority queues with an unbounded number of threads, and it enables the application of existing safety-verification tools for establishing their correctness.

Cite As Get BibTex

Ahmed Bouajjani, Constantin Enea, and Chao Wang. Checking Linearizability of Concurrent Priority Queues. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 16:1-16:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CONCUR.2017.16

Author Details

Ahmed Bouajjani
Constantin Enea
Chao Wang

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 Nir Piterman and Scott A. Smolka, editors, 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, volume 7795 of Lecture Notes in Computer Science, pages 324-338. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-36742-7_23.
  2. Dan Alistarh, Justin Kopinsky, Jerry Li, and Nir Shavit. The spraylist: a scalable relaxed priority queue. In Albert Cohen and David Grove, editors, Proceedings of the 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2015, San Francisco, CA, USA, February 7-11, 2015, pages 11-20. ACM, 2015. URL: http://dx.doi.org/10.1145/2688500.2688523.
  3. Rajeev Alur, Kenneth L. McMillan, and Doron A. Peled. Model-checking of correctness conditions for concurrent objects. Inf. Comput., 160(1-2):167-188, 2000. URL: http://dx.doi.org/10.1006/inco.1999.2847.
  4. Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. Verifying concurrent programs against sequential specifications. In Matthias Felleisen and Philippa Gardner, editors, 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, volume 7792 of Lecture Notes in Computer Science, pages 290-309. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-37036-6_17.
  5. Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. On reducing linearizability to state reachability. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 95-107. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-47666-6_8.
  6. Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. Tractable refinement checking for concurrent objects. In Rajamani and Walker [17], pages 651-662. URL: http://dx.doi.org/10.1145/2676726.2677002.
  7. Ahmed Bouajjani, Constantin Enea, and Chao Wang. Checking linearizability of concurrent priority queues. Arxiv, 2017. URL: https://arxiv.org/abs/1707.00639.
  8. Irina Calciu, Hammurabi Mendes, and Maurice Herlihy. The adaptive priority queue with elimination and combining. In Fabian Kuhn, editor, Distributed Computing - 28th International Symposium, DISC 2014, Austin, TX, USA, October 12-15, 2014. Proceedings, volume 8784 of Lecture Notes in Computer Science, pages 406-420. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-45174-8_28.
  9. Karlis Cerans. Deciding properties of integral relational automata. In Serge Abiteboul and Eli Shamir, editors, Automata, Languages and Programming, 21st International Colloquium, ICALP94, Jerusalem, Israel, July 11-14, 1994, Proceedings, volume 820 of Lecture Notes in Computer Science, pages 35-46. Springer, 1994. URL: http://dx.doi.org/10.1007/3-540-58201-0_56.
  10. Mike Dodds, Andreas Haas, and Christoph M. Kirsch. A scalable, correct time-stamped stack. In Rajamani and Walker [17], pages 233-246. URL: http://dx.doi.org/10.1145/2676726.2676963.
  11. Phillip B. Gibbons and Ephraim Korach. Testing shared memories. SIAM J. Comput., 26(4):1208-1244, 1997. URL: http://dx.doi.org/10.1137/S0097539794279614.
  12. Jad Hamza. On the complexity of linearizability. In Ahmed Bouajjani and Hugues Fauconnier, editors, Networked Systems - Third International Conference, NETYS 2015, Agadir, Morocco, May 13-15, 2015, Revised Selected Papers, volume 9466 of Lecture Notes in Computer Science, pages 308-321. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-26850-7_21.
  13. Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. Aspect-oriented linearizability proofs. In Pedro R. D'Argenio and Hernán C. Melgratti, editors, CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8052 of Lecture Notes in Computer Science, pages 242-256. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40184-8_18.
  14. Maurice Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, 1990. URL: http://dx.doi.org/10.1145/78969.78972.
  15. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. URL: http://dx.doi.org/10.1016/0304-3975(94)90242-9.
  16. Jonatan Lindén and Bengt Jonsson. A skiplist-based concurrent priority queue with minimal memory contention. In Roberto Baldoni, Nicolas Nisse, and Maarten van Steen, editors, Principles of Distributed Systems - 17th International Conference, OPODIS 2013, Nice, France, December 16-18, 2013. Proceedings, volume 8304 of Lecture Notes in Computer Science, pages 206-220. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-319-03850-6_15.
  17. 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. ACM, 2015. Google Scholar
  18. Luc Segoufin and Szymon Toruńczyk. Automata based verification over linearly ordered data domains. In Thomas Schwentick and Christoph Dürr, editors, 28th International Symposium on Theoretical Aspects of Computer Science, STACS 2011, March 10-12, 2011, Dortmund, Germany, volume 9 of LIPIcs, pages 81-92. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2011.81.
  19. Nir Shavit and Itay Lotan. Skiplist-based concurrent priority queues. In Proceedings of the 14th International Parallel & Distributed Processing Symposium (IPDPS'00), Cancun, Mexico, May 1-5, 2000, pages 263-268. IEEE Computer Society, 2000. URL: http://dx.doi.org/10.1109/IPDPS.2000.845994.
  20. Nir Shavit and Asaph Zemach. Scalable concurrent priority queue algorithms. In Brian A. Coan and Jennifer L. Welch, editors, Proceedings of the Eighteenth Annual ACM Symposium on Principles of Distributed Computing, PODC, '99Atlanta, Georgia, USA, May 3-6, 1999, pages 113-122. ACM, 1999. URL: http://dx.doi.org/10.1145/301308.301339.
  21. Viktor Vafeiadis. Automatically proving linearizability. In Tayssir Touili, Byron Cook, and Paul B. Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, pages 450-464. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14295-6_40.
  22. Pierre Wolper. Expressing interesting properties of programs in propositional temporal logic. In Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, USA, January 1986, pages 184-193. ACM Press, 1986. URL: http://dx.doi.org/10.1145/512644.512661.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact