More Web Proxy on the site http://driver.im/

research-article

Open access

Verifying correctness of persistent concurrent data structures: a sound and complete method

Authors:

Brijesh Dongol,

Gerhard Schellhorn,

Heike WehrheimAuthors Info & Claims

Formal Aspects of Computing, Volume 33, Issue 4-5

Pages 547 - 573

https://doi.org/10.1007/s00165-021-00541-8

Published: 01 August 2021 Publication History

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.

References

References

[1]

Bila E, Doherty S, Dongol B, Derrick J, Schellhorn G, and Wehrheim H Gotsman A and Sokolova A Defining and verifying durable opacity: correctness for persistent software transactional memory FORTE, vol 12136 of LNCS 2020 Springer 39-58

[2]

Cohen N, Aksun DT, Larus JR (2018) Object-oriented recovery for non-volatile memory. PACMPL 2(OOPSLA):153:1–153:22

[3]

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

[4]

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

[5]

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

[6]

Dongol B, Derrick J (2015) Verifying linearisability: a comparative survey. ACM Comput Surv 48(2):19:1–19:43

[7]

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

[8]

Derrick J, Doherty S, Dongol B, Schellhorn G, and Wehrheim H ter Beek MH, McIver A, and Oliveira JN Verifying correctness of persistent concurrent data structures Formal methods–the next 30 years-third world congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings 2019 Springer 179-195

Digital Library

[9]

Doherty S, Groves L, Luchangco V, and Moir M de Frutos-Escrig D and Núñez M Formal verification of a practical lock-free queue algorithm Formal techniques for networked and distributed systems–FORTE 2004 2004 Berlin Springer 97-114

[10]

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

[11]

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

[12]

Derrick J, Schellhorn G, and Wehrheim H Butler MJ and Schulte W Verifying linearisability with potential linearisation points FM 2011 2011 Springer 323-337

[13]

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

[14]

Ernst G, Pfähler J, Schellhorn G, and Reif W Modular, crash-safe refinement for asms with submachines Sci Comput Program 2016 131 3-21

[15]

Friedman M, Herlihy M, Marathe VJ, and Petrank E Krall A and Gross TR A persistent lock-free queue for non-volatile memory ACM SIGPLAN symposium on principles and practice of parallel programming 2018 PPoPP ACM 28-40

[16]

Guerraoui R and Kapalka M Principles of transactional memory 2010 Synthesis lectures on distributed computing theory Morgan & Claypool Publishers

Digital Library

[17]

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

[18]

Herlihy M and Wing JM Linearizability: a correctness condition for concurrent objects ACM TOPLAS 1990 12 3 463-492

Digital Library

[19]

Izraelevitz J, Mendes H, and Scott ML Gavoille C and Ilcinkas D Linearizability of persistent memory objects under a full-system-crash failure model Distributed computing–30th international symposium, DISC 2016 Springer 313-327

[20]

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

[21]

Joshi A, Nagarajan V, Cintra M, Viglas S (2018) DHTM: durable hardware transactional memory. In: ISCA. IEEE Computer Society, pp 452–465

[22]

Jones CB Tentative steps toward a development method for interfering programs ACM Trans Program Lang Syst 1983 5 4 596-619

Digital Library

[23]

KIV proofs for the durable linearizable queue, 2020. https://kiv.isse.de/projects/Durable-Queue.html

[24]

Lynch NA and Tuttle MR Hierarchical correctness proofs for distributed algorithms PODC 1987 New York ACM 137-151

[25]

Lynch N and Vaandrager F Forward and backward simulations part I: untimed systems Inf Comput Inf Control IANDC 1995 121 214-233

Digital Library

[26]

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

[27]

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

[28]

Oukid I, Booss D, Lespinasse A, Lehner W (2016) On testing persistent-memory-based software. In: DaMoN. ACM, pp 5:1–5:7

[29]

Pavlovic M, Kogan A, Marathe VJ, Harris T (2018) Brief announcement: persistent multi-word compare-and-swap. In: PODC. ACM, pp 37–39

[30]

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

[31]

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

[32]

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

[33]

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

[34]

Tuch H and Klein G Sutcliffe G and Voronkov A A unified memory model for pointers Logic for programming, artificial intelligence, and reasoning 2005 Berlin Springer 474-488

Digital Library

Cited By

Schellhorn GBodenmüller SReif W(2025)Verification of forward simulations with thread-local, step-local proof obligationsScience of Computer Programming10.1016/j.scico.2024.103227241(103227)Online publication date: Apr-2025
https://doi.org/10.1016/j.scico.2024.103227
Vafeiadi Bila EDongol B(2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-1Online publication date: 31-Jul-2024
https://doi.org/10.1007/s10703-024-00462-1
Bodenmüller SDerrick JDongol BSchellhorn GWehrheim H(2024)A Fully Verified Persistency LibraryVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_2(26-47)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50521-8_2
Show More Cited By

Recommendations

Mirror: making lock-free data structures persistent
PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

With the recent launch of the Intel Optane memory platform, non-volatile main memory in the form of fast, dense, byte-addressable non-volatile memory has now become available. Nevertheless, designing crash-resilient algorithms and data structures is ...
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures

Efficient implementations of data structures such as queues, stacks or hash-tables allow for concurrent access by many processes at the same time. To increase concurrency, these algorithms often completely dispose with locking, or only lock small parts ...
Model checking unbounded concurrent lists

We present a model checking-based method for verifying list-based concurrent set data structures. Concurrent data structures are notorious for being hard to get right and thus, their verification has received significant attention from the verification ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 33, Issue 4-5

Aug 2021

361 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© The Author(s) 2021.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 August 2021

Accepted: 07 February 2021

Revision received: 04 January 2021

Received: 03 April 2020

Published in FAC Volume 33, Issue 4-5

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
186
Total Downloads

Downloads (Last 12 months)37
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Schellhorn GBodenmüller SReif W(2025)Verification of forward simulations with thread-local, step-local proof obligationsScience of Computer Programming10.1016/j.scico.2024.103227241(103227)Online publication date: Apr-2025
https://doi.org/10.1016/j.scico.2024.103227
Vafeiadi Bila EDongol B(2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-1Online publication date: 31-Jul-2024
https://doi.org/10.1007/s10703-024-00462-1
Bodenmüller SDerrick JDongol BSchellhorn GWehrheim H(2024)A Fully Verified Persistency LibraryVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_2(26-47)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50521-8_2
D'Osualdo ERaad AVafeiadis V(2023)The Path to Durable LinearizabilityProceedings of the ACM on Programming Languages10.1145/35712197:POPL(748-774)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571219
Schellhorn GBodenmüller SReif W(2023)Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent SystemsRigorous State-Based Methods10.1007/978-3-031-33163-3_6(70-87)Online publication date: 30-May-2023
https://dl.acm.org/doi/10.1007/978-3-031-33163-3_6
Schellhorn GBodenmüller SBitterlich MReif W(2022)Software & System Verification with KIVThe Logic of Software. A Tasting Menu of Formal Methods10.1007/978-3-031-08166-8_20(408-436)Online publication date: 4-Jul-2022
https://doi.org/10.1007/978-3-031-08166-8_20
Bila EDongol BLahav ORaad AWickerson J(2022)View-Based Owicki–Gries Reasoning for Persistent x86-TSOProgramming Languages and Systems10.1007/978-3-030-99336-8_9(234-261)Online publication date: 5-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-030-99336-8_9
Khyzha ALahav O(2022)Abstraction for Crash-Resilient ObjectsProgramming Languages and Systems10.1007/978-3-030-99336-8_10(262-289)Online publication date: 5-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-030-99336-8_10

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents