Concurrent Data Structures Linked in Time

Authors Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee



PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.8.pdf
  • Filesize: 0.77 MB
  • 30 pages

Document Identifiers

Author Details

Germán Andrés Delbianco
Ilya Sergey
Aleksandar Nanevski
Anindya Banerjee

Cite AsGet BibTex

Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Concurrent Data Structures Linked in Time. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 8:1-8:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ECOOP.2017.8

Abstract

Arguments about correctness of a concurrent data structure are typically carried out by using the notion of linearizability and specifying the linearization points of the data structure's procedures. Such arguments are often cumbersome as the linearization points' position in time can be dynamic (depend on the interference, run-time values and events from the past, or even future), non-local (appear in procedures other than the one considered), and whose position in the execution trace may only be determined after the considered procedure has already terminated. In this paper we propose a new method, based on a separation-style logic, for reasoning about concurrent objects with such linearization points. We embrace the dynamic nature of linearization points, and encode it as part of the data structure's auxiliary state, so that it can be dynamically modified in place by auxiliary code, as needed when some appropriate run-time event occurs. We name the idea linking-in-time, because it reduces temporal reasoning to spatial reasoning. For example, modifying a temporal position of a linearization point can be modeled similarly to a pointer update in separation logic. Furthermore, the auxiliary state provides a convenient way to concisely express the properties essential for reasoning about clients of such concurrent objects. We illustrate the method by verifying (mechanically in Coq) an intricate optimal snapshot algorithm due to Jayanti, as well as some clients.
Keywords
  • Separation logic
  • Linearization Points
  • Concurrent snapshots
  • FCSL

Metrics

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

References

  1. FCSL: Fine-grained concurrent separation logic. URL: http://software.imdea.org/fcsl/.
  2. Martín Abadi and Leslie Lamport. The existence of refinement mappings. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), pages 165-175. IEEE Computer Society, 1988. URL: http://dx.doi.org/10.1109/LICS.1988.5115.
  3. Christian J. Bell, Andrew W. Appel, and David Walker. Concurrent separation logic for pipelined parallelization. In Radhia Cousot and Matthieu Martel, editors, Static Analysis - 17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010. Proceedings, volume 6337 of Lecture Notes in Computer Science, pages 151-166. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15769-1_10.
  4. Andrea Cerone, Alexey Gotsman, and Hongseok Yang. Parameterised linearisability. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Proceedings, Part II, volume 8573 of LNCS, pages 98-109. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-43951-7_9.
  5. Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. Aspect-oriented linearizability proofs. Logical Methods in Computer Science, 11(1), 2015. URL: http://dx.doi.org/10.2168/LMCS-11(1:20)2015.
  6. Robert Colvin, Simon Doherty, and Lindsay Groves. Verifying concurrent data structures by simulation. Electr. Notes Theor. Comput. Sci., 137(2):93-110, 2005. URL: http://dx.doi.org/10.1016/j.entcs.2005.04.026.
  7. Robert Colvin, Lindsay Groves, Victor Luchangco, and Mark Moir. Formal verification of a lazy concurrent list-based set algorithm. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 475-488. Springer, 2006. URL: http://dx.doi.org/10.1007/11817963_44.
  8. Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. Tada: A logic for time and data abstraction. In Richard Jones, editor, ECOOP 2014 - Object-Oriented Programming - 28th European Conference. Proceedings, volume 8586 of LNCS, pages 207-231. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44202-9_9.
  9. Mike Dodds, Andreas Haas, and Christoph M. Kirsch. A scalable, correct time-stamped stack. In Rajamani and Walker [35], pages 233-246. URL: http://dx.doi.org/10.1145/2676726.2676963.
  10. Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, and Lars Birkedal. Verifying custom synchronization constructs using higher-order separation logic. ACM Trans. Program. Lang. Syst., 38(2):4:1-4:72, 2016. URL: http://dx.doi.org/10.1145/2818638.
  11. Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, and Hongseok Yang. Abstraction for concurrent objects. Theor. Comput. Sci., 411(51-52):4379-4398, 2010. URL: http://dx.doi.org/10.1016/j.tcs.2010.09.021.
  12. Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, and Yu Zhang. Reasoning about optimistic concurrency using a program logic for history. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 388-402. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15375-4_27.
  13. Alexey Gotsman, Noam Rinetzky, and Hongseok Yang. Verifying concurrent memory reclamation algorithms with grace. 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 249-269. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-37036-6_15.
  14. Alexey Gotsman and Hongseok Yang. Linearizability with ownership transfer. In Maciej Koutny and Irek Ulidowski, editors, CONCUR 2012 - Concurrency Theory - 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings, volume 7454 of Lecture Notes in Computer Science, pages 256-271. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-32940-1_19.
  15. Steve Heller, Maurice Herlihy, Victor Luchangco, Mark Moir, William N. Scherer III, and Nir Shavit. A lazy concurrent list-based set algorithm. In James H. Anderson, Giuseppe Prencipe, and Roger Wattenhofer, editors, Principles of Distributed Systems, 9th International Conference, OPODIS 2005, Pisa, Italy, December 12-14, 2005, Revised Selected Papers, volume 3974 of Lecture Notes in Computer Science, pages 3-16. Springer, 2005. URL: http://dx.doi.org/10.1007/11795490_3.
  16. Nir Hemed, Noam Rinetzky, and Viktor Vafeiadis. Modular verification of concurrency-aware 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 371-387. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-48653-5_25.
  17. Danny Hendler, Itai Incze, Nir Shavit, and Moran Tzafrir. Flat combining and the synchronization-parallelism tradeoff. In Friedhelm Meyer auf der Heide and Cynthia A. Phillips, editors, SPAA 2010: Proceedings of the 22nd Annual ACM Symposium on Parallelism in Algorithms and Architectures, Thira, Santorini, Greece, June 13-15, 2010, pages 355-364. ACM, 2010. URL: http://dx.doi.org/10.1145/1810479.1810540.
  18. 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.
  19. 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.
  20. Moshe Hoffman, Ori Shalev, and Nir Shavit. The baskets queue. In Eduardo Tovar, Philippas Tsigas, and Hacène Fouchal, editors, Principles of Distributed Systems, 11th International Conference, OPODIS 2007, Guadeloupe, French West Indies, December 17-20, 2007. Proceedings, volume 4878 of Lecture Notes in Computer Science, pages 401-414. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-77096-1_29.
  21. Bart Jacobs and Frank Piessens. Expressive modular fine-grained concurrency specification. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 271-282. ACM, 2011. URL: http://dx.doi.org/10.1145/1926385.1926417.
  22. Prasad Jayanti. An optimal multi-writer snapshot algorithm. In Proceedings of the 37th Annual ACM Symposium on Theory of Computing, Baltimore, MD, USA, May 22-24, 2005, pages 723-732. ACM, 2005. URL: http://dx.doi.org/10.1145/1060590.1060697.
  23. Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. Higher-order ghost state. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, pages 256-269. ACM, 2016. URL: http://dx.doi.org/10.1145/2951913.2951943.
  24. 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 Rajamani and Walker [35], pages 637-650. URL: http://dx.doi.org/10.1145/2676726.2676980.
  25. Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew J. Parkinson. Proving linearizability using partial orders. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017. Proceedings, volume 10201 of LNCS, pages 639-667. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54434-1_24.
  26. Artem Khyzha, Alexey Gotsman, and Matthew J. Parkinson. A generic logic for proving linearizability. In John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou, editors, FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of Lecture Notes in Computer Science, pages 426-443, 2016. URL: http://dx.doi.org/10.1007/978-3-319-48989-6_26.
  27. 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, pages 561-574. ACM, 2013. URL: http://dx.doi.org/10.1145/2429069.2429134.
  28. Hongjin Liang and Xinyu Feng. Modular verification of linearizability with non-fixed linearization points. In Hans-Juergen Boehm and Cormac Flanagan, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013, pages 459-470. ACM, 2013. URL: http://dx.doi.org/10.1145/2462156.2462189.
  29. Adam Morrison and Yehuda Afek. Fast concurrent queues for x86 processors. In Alex Nicolau, Xiaowei Shen, Saman P. Amarasinghe, and Richard W. Vuduc, editors, ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '13, Shenzhen, China, February 23-27, 2013, pages 103-112. ACM, 2013. URL: http://dx.doi.org/10.1145/2442516.2442527.
  30. Aleksandar Nanevski. Separation logic and concurrency. Oregon programming languages summer school, 2016. URL: http://software.imdea.org/~aleks/oplss16/notes.pdf.
  31. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. Communicating state transition systems for fine-grained concurrent resources. In Shao [40], pages 290-310. URL: http://dx.doi.org/10.1007/978-3-642-54833-8_16.
  32. Peter W. O'Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, and Greta Yorsh. Verifying linearizability with hindsight. In Andréa W. Richa and Rachid Guerraoui, editors, Proceedings of the 29th Annual ACM Symposium on Principles of Distributed Computing, PODC 2010, Zurich, Switzerland, July 25-28, 2010, pages 85-94. ACM, 2010. URL: http://dx.doi.org/10.1145/1835698.1835722.
  33. 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.
  34. Erez Petrank and Shahar Timnat. Lock-free data-structure iterators. In Yehuda Afek, editor, Distributed Computing - 27th International Symposium, DISC 2013, Jerusalem, Israel, October 14-18, 2013. Proceedings, volume 8205 of Lecture Notes in Computer Science, pages 224-238. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-41527-2_16.
  35. 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
  36. Gerhard Schellhorn, Heike Wehrheim, and John Derrick. How to prove algorithms linearisable. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 243-259. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31424-7_21.
  37. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Mechanized verification of fine-grained concurrent programs. In David Grove and Steve Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pages 77-87. ACM, 2015. URL: http://dx.doi.org/10.1145/2737924.2737964.
  38. 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. Proceedings, volume 9032 of LNCS, pages 333-358. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46669-8_14.
  39. Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, and Germán Andrés Delbianco. Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. In Eelco Visser and Yannis Smaragdakis, editors, Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, pages 92-110. ACM, 2016. URL: http://dx.doi.org/10.1145/2983990.2983999.
  40. Zhong Shao, editor. Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Proceedings, volume 8410 of LNCS. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54833-8.
  41. Kasper Svendsen and Lars Birkedal. Impredicative Concurrent Abstract Predicates. In Shao [40], pages 149-168. URL: http://dx.doi.org/10.1007/978-3-642-54833-8_9.
  42. 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, pages 377-390. ACM, 2013. URL: http://dx.doi.org/10.1145/2500365.2500600.
  43. Viktor Vafeiadis. Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, 2007. URL: http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-726.pdf.
  44. Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, and Marc Shapiro. Proving correctness of highly-concurrent linearisable objects. In Josep Torrellas and Siddhartha Chatterjee, editors, Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2006, New York, New York, USA, March 29-31, 2006, pages 129-136. ACM, 2006. URL: http://dx.doi.org/10.1145/1122971.1122992.
  45. Viktor Vafeiadis and Matthew J. Parkinson. A marriage of rely/guarantee and separation logic. In Luís Caires and Vasco Thudichum Vasconcelos, editors, CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings, volume 4703 of Lecture Notes in Computer Science, pages 256-271. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-74407-8_18.
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