Document Open Access Logo

Polynomial-Time Verification and Testing of Implementations of the Snapshot Data Structure

Authors Gal Amram , Avi Hayoun, Lior Mizrahi, Gera Weiss

PDF
Thumbnail PDF

File

LIPIcs.DISC.2022.5.pdf
  • Filesize: 0.83 MB
  • 20 pages

Document Identifiers

Author Details

Gal Amram
  • Ben Gurion University of the Negev, Beer-Sheva, Israel
  • IBM Research, Haifa, Israel
Avi Hayoun
  • Ben-Gurion University of the Negev, Beer-Sheva, Israel
Lior Mizrahi
  • Ben-Gurion University of the Negev, Beer-Sheva, Israel
Gera Weiss
  • Ben-Gurion University of the Negev, Beer-Sheva, Israel

Funding

This research was partially funded by grant no. 2714/19 from the Israel Science Foundation and by the Lynn and William Frankel Center for Computer Science at Ben-Gurion University.

Cite AsGet BibTex

Gal Amram, Avi Hayoun, Lior Mizrahi, and Gera Weiss. Polynomial-Time Verification and Testing of Implementations of the Snapshot Data Structure. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.DISC.2022.5

Abstract

We analyze correctness of implementations of the snapshot data structure in terms of linearizability. We show that such implementations can be verified in polynomial time. Additionally, we identify a set of representative executions for testing and show that the correctness of each of these executions can be validated in linear time. These results present a significant speedup considering that verifying linearizability of implementations of concurrent data structures, in general, is EXPSPACE-complete in the number of program-states, and testing linearizability is NP-complete in the length of the tested execution. The crux of our approach is identifying a class of executions, which we call simple, such that a snapshot implementation is linearizable if and only if all of its simple executions are linearizable. We then divide all possible non-linearizable simple executions into three categories and construct a small automaton that recognizes each category. We describe two implementations (one for verification and one for testing) of an automata-based approach that we develop based on this result and an evaluation that demonstrates significant improvements over existing tools. For verification, we show that restricting a state-of-the-art tool to analyzing only simple executions saves resources and allows the analysis of more complex cases. Specifically, restricting attention to simple executions finds bugs in 27 instances, whereas, without this restriction, we were only able to find 14 of the 30 bugs in the instances we examined. We also show that our technique accelerates testing performance significantly. Specifically, our implementation solves the complete set of 900 problems we generated, whereas the state-of-the-art linearizability testing tool solves only 554 problems.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Theory of computation → Concurrent algorithms
Keywords
  • Snapshot
  • Linearizability
  • Verification
  • Formal Methods

Metrics

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

Related Versions

Supplementary Materials

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 for highly concurrent data structures. Int. J. Softw. Tools Technol. Transf., 19(5):549-563, 2017. URL: https://doi.org/10.1007/s10009-016-0415-4.
  2. Parosh Aziz Abdulla, Bengt Jonsson, and Cong Quy Trinh. Automated verification of linearization policies. In Xavier Rival, editor, Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, volume 9837 of Lecture Notes in Computer Science, pages 61-83. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-53413-7_4.
  3. Parosh Aziz Abdulla, Bengt Jonsson, and Cong Quy Trinh. Fragment abstraction for concurrent shape analysis. In Amal Ahmed, editor, 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, volume 10801 of Lecture Notes in Computer Science, pages 442-471. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_16.
  4. Yehuda Afek, Hagit Attiya, Danny Dolev, Eli Gafni, Michael Merritt, and Nir Shavit. Atomic snapshots of shared memory. J. ACM, 40(4):873-890, 1993. URL: https://doi.org/10.1145/153724.153741.
  5. 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: https://doi.org/10.1006/inco.1999.2847.
  6. Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, and Eran Yahav. Comparison under abstraction for verifying linearizability. In Werner Damm and Holger Hermanns, editors, Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, volume 4590 of Lecture Notes in Computer Science, pages 477-490. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73368-3_49.
  7. James H. Anderson. Composite registers. Distributed Comput., 6(3):141-154, 1993. URL: https://doi.org/10.1007/BF02242703.
  8. James H. Anderson. Multi-writer composite registers. Distributed Comput., 7(4):175-195, 1994. URL: https://doi.org/10.1007/BF02280833.
  9. James Aspnes and Maurice Herlihy. Wait-free data structures in the asynchronous PRAM model. In Frank Thomson Leighton, editor, Proceedings of the 2nd Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA '90, Island of Crete, Greece, July 2-6, 1990, pages 340-349. ACM, 1990. URL: https://doi.org/10.1145/97444.97701.
  10. Hagit Attiya, Maurice Herlihy, and Ophir Rachman. Efficient atomic snapshots using lattice agreement (extended abstract). In Adrian Segall and Shmuel Zaks, editors, Distributed Algorithms, 6th International Workshop, WDAG '92, Haifa, Israel, November 2-4, 1992, Proceedings, volume 647 of Lecture Notes in Computer Science, pages 35-53. Springer, 1992. URL: https://doi.org/10.1007/3-540-56188-9_3.
  11. Hagit Attiya and Ophir Rachman. Atomic snapshots in o(n log n) operations. SIAM J. Comput., 27(2):319-340, 1998. URL: https://doi.org/10.1137/S0097539795279463.
  12. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  13. Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, and Shmuel Sagiv. Thread quantification for concurrent shape analysis. In Aarti Gupta and Sharad Malik, editors, Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, volume 5123 of Lecture Notes in Computer Science, pages 399-413. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70545-1_37.
  14. 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: https://doi.org/10.1007/978-3-642-37036-6_17.
  15. Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. On reducing linearizability to state reachability. Inf. Comput., 261:383-400, 2018. URL: https://doi.org/10.1016/j.ic.2018.02.014.
  16. Ahmed Bouajjani, Constantin Enea, and Chao Wang. Checking linearizability of concurrent priority queues. In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 16:1-16:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.16.
  17. Jack R Bowman. Obstruction-free snapshot, obstruction-free consensus, and fetch-and-add modulo k. Technical report, Technical Report TR2011-681, Dartmouth College, Computer Science, Hanover, NH, 2011. Google Scholar
  18. Sebastian Burckhardt, Rajeev Alur, and Milo M. K. Martin. Checkfence: checking consistency of concurrent data types on relaxed memory models. In Jeanne Ferrante and Kathryn S. McKinley, editors, Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007, pages 12-21. ACM, 2007. URL: https://doi.org/10.1145/1250734.1250737.
  19. Sebastian Burckhardt, Chris Dern, Madanlal Musuvathi, and Roy Tan. Line-up: a complete and automatic linearizability checker. In Benjamin G. Zorn and Alexander Aiken, editors, Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010, pages 330-340. ACM, 2010. URL: https://doi.org/10.1145/1806596.1806634.
  20. Jacob Burnim, George C. Necula, and Koushik Sen. Specifying and checking semantic atomicity for multithreaded programs. In Rajiv Gupta and Todd C. Mowry, editors, Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2011, Newport Beach, CA, USA, March 5-11, 2011, pages 79-90. ACM, 2011. URL: https://doi.org/10.1145/1950365.1950377.
  21. CAVE Website. https://people.mpi-sws.org/~viktor/cave/. Last Accessed: Aug. 31, 2021.
  22. Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. Aspect-oriented linearizability proofs. Log. Methods Comput. Sci., 11(1), 2015. URL: https://doi.org/10.2168/LMCS-11(1:20)2015.
  23. Edmund M. Clarke, William Klieber, Milos Novácek, and Paolo Zuliani. Model checking and the state explosion problem. In Bertrand Meyer and Martin Nordio, editors, Tools for Practical Software Verification, LASER, International Summer School 2011, Elba Island, Italy, Revised Tutorial Lectures, volume 7682 of Lecture Notes in Computer Science, pages 1-30. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-35746-6_1.
  24. David Detlefs, Christine H. Flood, Alex Garthwaite, Paul Alan Martin, Nir Shavit, and Guy L. Steele Jr. Even better dcas-based concurrent deques. In Maurice Herlihy, editor, Distributed Computing, 14th International Conference, DISC 2000, Toledo, Spain, October 4-6, 2000, Proceedings, volume 1914 of Lecture Notes in Computer Science, pages 59-73. Springer, 2000. URL: https://doi.org/10.1007/3-540-40026-5_4.
  25. Simon Doherty, David Detlefs, Lindsay Groves, Christine H. Flood, Victor Luchangco, Paul Alan Martin, Mark Moir, Nir Shavit, and Guy L. Steele Jr. DCAS is not a silver bullet for nonblocking algorithm design. In Phillip B. Gibbons and Micah Adler, editors, SPAA 2004: Proceedings of the Sixteenth Annual ACM Symposium on Parallelism in Algorithms and Architectures, June 27-30, 2004, Barcelona, Spain, pages 216-224. ACM, 2004. URL: https://doi.org/10.1145/1007912.1007945.
  26. Cynthia Dwork, Maurice Herlihy, Serge A. Plotkin, and Orli Waarts. Time-lapse snapshots. SIAM J. Comput., 28(5):1848-1874, 1999. URL: https://doi.org/10.1137/S0097539793243685.
  27. Michael Emmi and Constantin Enea. Sound, complete, and tractable linearizability monitoring for concurrent collections. Proc. ACM Program. Lang., 2(POPL):25:1-25:27, 2018. URL: https://doi.org/10.1145/3158113.
  28. Phillip B. Gibbons and Ephraim Korach. Testing shared memories. SIAM J. Comput., 26(4):1208-1244, 1997. URL: https://doi.org/10.1137/S0097539794279614.
  29. Jad Hamza. On the complexity of linearizability. Comput., 101(9):1227-1240, 2019. URL: https://doi.org/10.1007/s00607-018-0596-7.
  30. Maurice Herlihy, Victor Luchangco, and Mark Moir. Obstruction-free synchronization: Double-ended queues as an example. In 23rd International Conference on Distributed Computing Systems (ICDCS 2003), 19-22 May 2003, Providence, RI, USA, pages 522-529. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/ICDCS.2003.1203503.
  31. Maurice Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, 1990. URL: https://doi.org/10.1145/78969.78972.
  32. Alex Horn and Daniel Kroening. Faster linearizability checking via p-compositionality. In Susanne Graf and Mahesh Viswanathan, editors, Formal Techniques for Distributed Objects, Components, and Systems - 35th IFIP WG 6.1 International Conference, FORTE 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, 2015, Proceedings, volume 9039 of Lecture Notes in Computer Science, pages 50-65. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-19195-9_4.
  33. Tzu-Han Hsu, César Sánchez, and Borzoo Bonakdarpour. Bounded model checking for hyperproperties. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I, volume 12651 of Lecture Notes in Computer Science, pages 94-112. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72016-2_6.
  34. Prasad Jayanti. f-arrays: implementation and applications. In Aleta Ricciardi, editor, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Distributed Computing, PODC 2002, Monterey, California, USA, July 21-24, 2002, pages 270-279. ACM, 2002. URL: https://doi.org/10.1145/571825.571875.
  35. Prasad Jayanti. An optimal multi-writer snapshot algorithm. In Harold N. Gabow and Ronald Fagin, editors, Proceedings of the 37th Annual ACM Symposium on Theory of Computing, Baltimore, MD, USA, May 22-24, 2005, pages 723-732. ACM, 2005. URL: https://doi.org/10.1145/1060590.1060697.
  36. Lefteris M. Kirousis, Paul G. Spirakis, and Philippas Tsigas. Reading many variables in one atomic operation: Solutions with linear or sublinear complexity. IEEE Trans. Parallel Distrib. Syst., 5(7):688-696, 1994. URL: https://doi.org/10.1109/71.296315.
  37. Linearizability Tester Website. http://www.cs.ox.ac.uk/people/gavin.lowe/LinearizabiltyTesting/. Last Accessed: Aug. 31, 2021.
  38. Yang Liu, Wei Chen, Yanhong A. Liu, and Jun Sun. Model checking linearizability via refinement. In Ana Cavalcanti and Dennis Dams, editors, Proceedings of the Second World Congress on Formal Methods (FM'09), volume 5850 of Lecture Notes in Computer Science, pages 321-337. Springer, 2009. Google Scholar
  39. Yang Liu, Wei Chen, Yanhong A. Liu, and Jun Sun. Model checking linearizability via refinement. In Ana Cavalcanti and Dennis Dams, editors, FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings, volume 5850 of Lecture Notes in Computer Science, pages 321-337. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-05089-3_21.
  40. Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun, Shao Jie Zhang, and Jin Song Dong. Verifying linearizability via optimized refinement checking. IEEE Trans. Software Eng., 39(7):1018-1039, 2013. URL: https://doi.org/10.1109/TSE.2012.82.
  41. Gavin Lowe. Testing for linearizability. Concurr. Comput. Pract. Exp., 29(4), 2017. URL: https://doi.org/10.1002/cpe.3928.
  42. Maged M Michael and Michael L Scott. Correction of a memory management method for lock-free data structures. Technical report, University of Rochester, Computer Science, 1995. Google Scholar
  43. Sean Ovens and Philipp Woelfel. Strongly linearizable implementations of snapshots and other types. In Peter Robinson and Faith Ellen, editors, Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC 2019, Toronto, ON, Canada, July 29 - August 2, 2019, pages 197-206. ACM, 2019. URL: https://doi.org/10.1145/3293611.3331632.
  44. PAT Website. https://pat.comp.nus.edu.sg/. Last Accessed: Aug. 31, 2021.
  45. Poling Website. https://github.com/rowangithub/Poling/. Last Accessed: Aug. 31, 2021.
  46. Yaron Riany, Nir Shavit, and Dan Touitou. Towards a practical snapshot algorithm. Theor. Comput. Sci., 269(1-2):163-201, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00412-6.
  47. Vineet Singh, Iulian Neamtiu, and Rajiv Gupta. Proving concurrent data structures linearizable. In 27th IEEE International Symposium on Software Reliability Engineering, ISSRE 2016, Ottawa, ON, Canada, October 23-27, 2016, pages 230-240. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/ISSRE.2016.31.
  48. Jun Sun, Yang Liu, and Bin Cheng. Model checking a model checker: A code contract combined approach. In Jin Song Dong and Huibiao Zhu, editors, Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings, volume 6447 of Lecture Notes in Computer Science, pages 518-533. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-16901-4_34.
  49. Supporting materials. URL: https://github.com/hayounav/Thesis_experiments/tree/main/snapshot%20verification%20and%20testing.
  50. Viktor Vafeiadis. Shape-value abstraction for verifying linearizability. In Neil D. Jones and Markus Müller-Olm, editors, Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings, volume 5403 of Lecture Notes in Computer Science, pages 335-348. Springer, 2009. URL: https://doi.org/10.1007/978-3-540-93900-9_27.
  51. 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: https://doi.org/10.1007/978-3-642-14295-6_40.
  52. Martin T. Vechev and Eran Yahav. Deriving linearizable fine-grained concurrent objects. In Rajiv Gupta and Saman P. Amarasinghe, editors, Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, pages 125-135. ACM, 2008. URL: https://doi.org/10.1145/1375581.1375598.
  53. Jeannette M. Wing and Chun Gong. Testing and verifying concurrent objects. J. Parallel Distributed Comput., 17(1-2):164-182, 1993. URL: https://doi.org/10.1006/jpdc.1993.1015.
  54. 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: https://doi.org/10.1145/512644.512661.
  55. He Zhu, Gustavo Petri, and Suresh Jagannathan. Poling: SMT aided linearizability proofs. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, volume 9207 of Lecture Notes in Computer Science, pages 3-19. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21668-3_1.
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 Imprint Privacy Contact