Abstract
Non-volatile memory (NVM), aka persistent memory, is a new memory paradigm that preserves 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 a formal proof technique for durable linearizability, which is a correctness criterion that extends linearizability to handle crashes and recovery in the context ofNVM.Our proofs are based on refinement of Input/Output automata (IOA) representations of concurrent data structures. To this end, we develop a generic procedure for transforming any standard sequential data structure into a durable specification and prove that this transformation is both sound and complete. 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 persistentmemory queue that builds on Michael and Scott’s lock-free queue. To support the proofs, we describe an automated translation procedure from code to IOA and a thread-local proof technique for verifying correctness of invariants.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Bila, E., Doherty, S., Dongol, B., Derrick, J., Schellhorn, G., Wehrheim, H.: Defining and verifying durable opacity: correctness for persistent software transactional memory. In: Gotsman, A., Sokolova, A. (eds.) FORTE, vol 12136 of LNCS, pp. 39–58. Springer (2020)
Cohen N, Aksun DT, Larus JR (2018) Object-oriented recovery for non-volatile memory. PACMPL 2(OOPSLA):153:1–153:22
Cepeda D, Chowdhury S, Li N, Lopez R, Wang X, Golab W (2019) Toward linearizability testing for multi-word persistent synchronization primitives. In: Felber P, Friedman R, Gilbert S, Miller A (eds) OPODIS, vol 153 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp 19:1–19:17
Chajed T, Tassarotti J, Kaashoek MF, Zeldovich N (2019) Verifying concurrent, crash-safe systems with perennial. In: Brecht T, Williamson C (eds) SOSP. ACM, pp 243–258
Chen H, Ziegler D, Chajed T, Chlipala A, Kaashoek MF, Zeldovich N (2015) Using crash hoare logic for certifying the FSCQ file system. In: Miller EL, Hand S (eds) SOSP. ACM, pp 18–37
Dongol B, Derrick J (2015) Verifying linearisability: a comparative survey. ACM Comput Surv 48(2):19:1–19:43
Doherty S, Dongol B, Derrick J, Schellhorn G, Wehrheim H (2016) Proving opacity of a pessimistic STM. In: OPODIS, vol 70 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp 35:1–35:17
Derrick, J., Doherty, S., Dongol, B., Schellhorn, G., Wehrheim, H.: Verifying correctness of persistent concurrent data structures. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal methods–the next 30 years-third world congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings. Lecture notes in computer science, vol. 11800, pp. 179–195. Springer (2019)
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.) Formal techniques for networked and distributed systems–FORTE 2004, pp. 97–114. Springer, Berlin (2004)
Denny JE, Lee S, Vetter JS (2016) NVL-C: static analysis techniques for efficient, correct programming of non-volatile main memory systems. In: Nakashima H, Taura K, Lange J (eds) HPDC. ACM, pp 125–136
de Roever WP, de Boer FS, Hannemann U, Hooman J, Lakhnech Y, Poel M, Zwiers J (2001) Concurrency verification: introduction to compositional and noncompositional methods, vol. 54 of Cambridge tracts in theoretical computer science. Cambridge University Press
Derrick, J., Schellhorn, G., Wehrheim, H.: Verifying linearisability with potential linearisation points. In: Butler, M.J., Schulte, W. (eds.) FM 2011. Lecture notes in computer science, vol. 6664, pp. 323–337. Springer (2011)
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
Ernst, G., Pfähler, J., Schellhorn, G., Reif, W.: Modular, crash-safe refinement for asms with submachines. Sci Comput Program 131, 3–21 (2016)
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, pp. 28–40. ACM, PPoPP (2018)
Guerraoui, R., Kapalka, M.: Principles of transactional memory. Morgan & Claypool Publishers, Synthesis lectures on distributed computing theory (2010)
Huang Y, Pavlovic M, Marathe VJ, Seltzer M, Harris T, Byan S (2018) Closing the performance gap between volatile and persistent key-value stores using cross-referencing logs. In USENIX annual technical conference. USENIX Association, pp 967–979
Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM TOPLAS 12(3), 463–492 (1990)
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.) Distributed computing–30th international symposium, DISC. Lecture notes in computer science, vol. 9888, pp. 313–327. Springer (2016)
Iiboshi H, Ugawa T (2018) Towards model checking library for persistent data structures. In: IEEE 7th non-volatile memory systems and applications symposium, NVMSA 2018, Hakodate, Sapporo, Japan, August 28–31, 2018. IEEE, pp 119–120
Joshi A, Nagarajan V, Cintra M, Viglas S (2018) DHTM: durable hardware transactional memory. In: ISCA. IEEE Computer Society, pp 452–465
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans Program Lang Syst 5(4), 596–619 (1983)
KIV proofs for the durable linearizable queue, 2020. https://kiv.isse.de/projects/Durable-Queue.html
Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. PODC, pp. 137–151. ACM, New York (1987)
Lynch, N., Vaandrager, F.: Forward and backward simulations part I: untimed systems. Inf Comput Inf Control IANDC 121, 214–233 (1995)
Liu S, Wei Y, Zhao J, Kolli A, Khan SM (2019) Pmtest: a fast and flexible testing framework for persistent memory programs. In: Bahar I, Herlihy M, Witchel E, Lebeck AR (eds) ASPLOS. ACM, pp 411–425
Michael MM, Scott ML (1996) Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings 15th ACM symposium on principles of distributed computing, pp 267–275
Oukid I, Booss D, Lespinasse A, Lehner W (2016) On testing persistent-memory-based software. In: DaMoN. ACM, pp 5:1–5:7
Pavlovic M, Kogan A, Marathe VJ, Harris T (2018) Brief announcement: persistent multi-word compare-and-swap. In: PODC. ACM, pp 37–39
Raad A, Vafeiadis V (2018) Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model. PACMPL, 2(OOPSLA):137:1–137:27
Raad A, Wickerson J, Neiger G, Vafeiadis V (2020) Persistency semantics of the intel-x86 architecture. Proc ACM Program Lang 4(POPL):11:1–11:31
Sigurbjarnarson H, Bornholt J, Torlak E, Wang X (2016) Push-button verification of file systems via crash refinement. In: Keeton K, Roscoe T (eds) OSDI. USENIX Association, pp 1–16
Schellhorn G, Derrick J, Wehrheim H (2014) A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans Comput Log 15(4):31:1–31:37
Tuch, H., Klein, G.: A unified memory model for pointers. In: Sutcliffe, G., Voronkov, A. (eds.) Logic for programming, artificial intelligence, and reasoning, pp. 474–488. Springer, Berlin (2005)
Acknowledgements
We thank Lindsay Groves for comments that have helped improve an earlier version of this paper. Alexander Lindermayr and Kilian Kotelewsky helped to implement the framework for IOA in KIV while doing their Bachelor theses. Derrick, Dongol and Doherty are supported by EPSRC Grants EP/R032351/1, EP/R032556/1, EP/R019045/2; Wehrheim by DFG Grant WE 2290/12-1, Schellhorn by RE 828/13-2.
Author information
Authors and Affiliations
Corresponding author
Additional information
Annabelle McIver, Maurice ter Beek, Cliff Jones and Jim Woodcock
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Derrick, J., Doherty, S., Dongol, B. et al. Verifying correctness of persistent concurrent data structures: a sound and complete method. Form Asp Comp 33, 547–573 (2021). https://doi.org/10.1007/s00165-021-00541-8
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-021-00541-8