Paper Info
Title
Verifying correctness of persistent concurrent data structures: a sound and complete method
Abstract
AbstractAbstractNon-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 persistentconcurrent 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.
Year
DOI
Venue
2021
10.1007/s00165-021-00541-8
Formal Aspects of Computing
Keywords
DocType
Volume
Non-volatile memory, Concurrent data structures, Refinement, Linearizability
Journal
33
Issue
ISSN
Citations 
4-5
0934-5043
0
PageRank 
References 
Authors
0.34
0
5
Name
Order
Citations
PageRank
John Derrick11023.90
Simon Doherty200.34
Brijesh Dongol319325.27
Gerhard Schellhorn476956.43
Heike Wehrheim51013104.85