University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Verifying Correctness of Persistent Concurrent Data Structures

Derrick, John, Doherty, Simon, Dongol, Brijesh, Schellhorn, Gerhard and Wehrheim, Heike (2019) Verifying Correctness of Persistent Concurrent Data Structures In: 23rd International Symposium on Formal Methods (FM'19), 07-11 Oct 2019, Porto, Portugal.

Verifying Correctness of Persistent Concurrent Data Structures.pdf - Accepted version Manuscript

Download (595kB) | Preview


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.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computer Science
Authors :
Derrick, John
Doherty, Simon
Schellhorn, Gerhard
Wehrheim, Heike
Date : 2019
Funders : Engineering and Physical Sciences Research Council (EPSRC)
Copyright Disclaimer : © 2019 Springer International Publishing.
Related URLs :
Depositing User : Clive Harris
Date Deposited : 19 Aug 2019 12:25
Last Modified : 07 Oct 2019 02:08

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800