Advertisement

Verifying Correctness of Persistent Concurrent Data Structures

  • John Derrick
  • Simon Doherty
  • Brijesh DongolEmail author
  • Gerhard Schellhorn
  • Heike Wehrheim
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)

Abstract

Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory preserving its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of persistent concurrent data structures, together with associated notions of correctness. In this paper, we present the first formal proof technique for durable linearizability, which is a correctness criterion that extends linearizability to handle crashes and recovery in the context of NVM. Our proofs are based on refinement of IO-automata representations of concurrent data structures. To this end, we develop a generic procedure for transforming any standard sequential data structure into a durable specification. Since the durable specification only exhibits durably linearizable behaviours, it serves as the abstract specification in our refinement proof. We exemplify our technique on a recently proposed persistent memory queue that builds on Michael and Scott’s lock-free queue.

Notes

Acknowledgements

We thank Lindsay Groves for comments that have helped improve this paper.

References

  1. 1.
    Abdulla, P.A., Haziza, F., Holík, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 324–338. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36742-7_23CrossRefzbMATHGoogle Scholar
  2. 2.
    Batty, M., Dodds, M., Gotsman, A.: Library abstraction for C/C++ concurrency. In: Giacobazzi, R., Cousot, R. (eds.) Symposium on Principles of Programming Languages, POPL, pp. 235–248. ACM (2013).  https://doi.org/10.1145/2429069.2429099
  3. 3.
    Cohen, N., Aksun, D.T., Larus, J.R.: Object-oriented recovery for non-volatile memory. PACMPL 2(OOPSLA), 153:1–153:22 (2018)Google Scholar
  4. 4.
    Derrick, J., Schellhorn, G., Wehrheim, H.: Verifying linearisability with potential linearisation points. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 323–337. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-21437-0_25CrossRefGoogle Scholar
  5. 5.
    Derrick, J., Smith, G., Groves, L., Dongol, B.: A proof method for linearizability on TSO architectures. In: Hinchey, M.G., Bowen, J.P., Olderog, E.-R. (eds.) Provably Correct Systems. NMSSE, pp. 61–91. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-48628-4_4CrossRefGoogle Scholar
  6. 6.
    Doherty, S., Dongol, B., Derrick, J., Schellhorn, G., Wehrheim, H.: Proving opacity of a pessimistic STM. In: OPODIS, LIPIcs, vol. 70, pp. 35:1–35:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)Google Scholar
  7. 7.
    Doherty, S., Dongol, B., Wehrheim, H., Derrick, J.: Making linearizability compositional for partially ordered executions. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 110–129. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-98938-9_7CrossRefGoogle Scholar
  8. 8.
    Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97–114. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30232-2_7CrossRefzbMATHGoogle Scholar
  9. 9.
    Dongol, B., Derrick, J.: Verifying linearisability: a comparative survey. ACM Comput. Surv. 48(2), 19:1–19:43 (2015).  https://doi.org/10.1145/2796550CrossRefGoogle Scholar
  10. 10.
    Ernst, G., Pfähler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV–overview and verifythis competition. Softw. Tools Technol. Transf. (STTT) 17(6), 677–694 (2015)CrossRefGoogle Scholar
  11. 11.
    Friedman, M., Herlihy, M., Marathe, V.J., Petrank, E.: A persistent lock-free queue for non-volatile memory. In: Krall, A., Gross, T.R. (eds.) ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP, pp. 28–40. ACM (2018).  https://doi.org/10.1145/3178487.3178490
  12. 12.
    Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM TOPLAS 12(3), 463–492 (1990)CrossRefGoogle Scholar
  13. 13.
    Huang, Y., Pavlovic, M., Marathe, V.J., Seltzer, M., Harris, T., Byan, S.: Closing the performance gap between volatile and persistent key-value stores using cross-referencing logs. In: USENIX Annual Technical Conference, pp. 967–979. USENIX Association (2018)Google Scholar
  14. 14.
    Izraelevitz, J., Mendes, H., Scott, M.L.: Linearizability of persistent memory objects under a full-system-crash failure model. In: Gavoille, C., Ilcinkas, D. (eds.) DISC 2016. LNCS, vol. 9888, pp. 313–327. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-53426-7_23CrossRefGoogle Scholar
  15. 15.
    Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983).  https://doi.org/10.1145/69575.69577CrossRefzbMATHGoogle Scholar
  16. 16.
    Joshi, A., Nagarajan, V., Cintra, M., Viglas, S.: DHTM: durable hardware transactional memory. In: ISCA, pp. 452–465. IEEE Computer Society (2018)Google Scholar
  17. 17.
    KIV proofs for the durable linearizable queue (2019). http://www.informatik.uni-augsburg.de/swt/projects/Durable-Queue.html
  18. 18.
    Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: PODC, pp. 137–151. ACM, New York (1987).  https://doi.org/10.1145/41840.41852
  19. 19.
    Lynch, N., Vaandrager, F.W.: Forward and backward simulations part I: untimed systems. Inf. Comput. Inf. Control - IANDC 121, 214–233 (1995).  https://doi.org/10.1006/inco.1995.1134CrossRefzbMATHGoogle Scholar
  20. 20.
    Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of 15th ACM Symposium on Principles of Distributed Computing, pp. 267–275 (1996)Google Scholar
  21. 21.
    Pavlovic, M., Kogan, A., Marathe, V.J., Harris, T.: Brief announcement: persistent multi-word compare-and-swap, In: PODC, pp. 37–39. ACM (2018)Google Scholar
  22. 22.
    Raad, A., Doko, M., Rozic, L., Lahav, O., Vafeiadis, V.: On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. PACMPL 3(POPL), 68:1–68:31 (2019). https://dl.acm.org/citation.cfm?id=3290381
  23. 23.
    Raad, A., Vafeiadis, V.: Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model. PACMPL 2(OOPSLA), 137:1–137:27 (2018)Google Scholar
  24. 24.
    Schellhorn, G., Derrick, J., Wehrheim, H.: A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Logic 15(4), 31:1–31:37 (2014).  https://doi.org/10.1145/2629496MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Travkin, O., Mütze, A., Wehrheim, H.: SPIN as a linearizability checker under weak memory models. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 311–326. Springer, Cham (2013).  https://doi.org/10.1007/978-3-319-03077-7_21CrossRefGoogle Scholar
  26. 26.
    Travkin, O., Wehrheim, H.: Verification of concurrent programs on weak memory models. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 3–24. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-46750-4_1CrossRefzbMATHGoogle Scholar
  27. 27.
    Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450–464. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14295-6_40CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • John Derrick
    • 1
  • Simon Doherty
    • 1
  • Brijesh Dongol
    • 2
    Email author
  • Gerhard Schellhorn
    • 3
  • Heike Wehrheim
    • 4
  1. 1.University of SheffieldSheffieldUK
  2. 2.University of SurreyGuildfordUK
  3. 3.University of AugsburgAugsburgGermany
  4. 4.Paderborn UniversityPaderbornGermany

Personalised recommendations