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)


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.



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


  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). 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).
  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). 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). 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). 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). Scholar
  9. 9.
    Dongol, B., Derrick, J.: Verifying linearisability: a comparative survey. ACM Comput. Surv. 48(2), 19:1–19:43 (2015). 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).
  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). 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). 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).
  18. 18.
    Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: PODC, pp. 137–151. ACM, New York (1987).
  19. 19.
    Lynch, N., Vaandrager, F.W.: Forward and backward simulations part I: untimed systems. Inf. Comput. Inf. Control - IANDC 121, 214–233 (1995). 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).
  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). 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). 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). 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). 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