Cargando…

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory

Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistenc...

Descripción completa

Detalles Bibliográficos
Autores principales: Bila, Eleni, Doherty, Simon, Dongol, Brijesh, Derrick, John, Schellhorn, Gerhard, Wehrheim, Heike
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7281866/
http://dx.doi.org/10.1007/978-3-030-50086-3_3
_version_ 1783544014677475328
author Bila, Eleni
Doherty, Simon
Dongol, Brijesh
Derrick, John
Schellhorn, Gerhard
Wehrheim, Heike
author_facet Bila, Eleni
Doherty, Simon
Dongol, Brijesh
Derrick, John
Schellhorn, Gerhard
Wehrheim, Heike
author_sort Bila, Eleni
collection PubMed
description Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistency. So far, this has lead to the design of a number of persistent concurrent data structures, built to satisfy an associated notion of correctness: durable linearizability. In this paper, we transfer the principle of durable concurrent correctness to the area of software transactional memory (STM). Software transactional memory algorithms allow for concurrent access to shared state. Like linearizability for concurrent data structures, opacity is the established notion of correctness for STMs. First, we provide a novel definition of durable opacity extending opacity to handle crashes and recovery in the context of NVM. Second, we develop a durably opaque version of an existing STM algorithm, namely the Transactional Mutex Lock (TML). Third, we design a proof technique for durable opacity based on refinement between TML and an operational characterisation of durable opacity by adapting the TMS2 specification. Finally, we apply this proof technique to show that the durable version of TML is indeed durably opaque. The correctness proof is mechanized within Isabelle.
format Online
Article
Text
id pubmed-7281866
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-72818662020-06-09 Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory Bila, Eleni Doherty, Simon Dongol, Brijesh Derrick, John Schellhorn, Gerhard Wehrheim, Heike Formal Techniques for Distributed Objects, Components, and Systems Article Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistency. So far, this has lead to the design of a number of persistent concurrent data structures, built to satisfy an associated notion of correctness: durable linearizability. In this paper, we transfer the principle of durable concurrent correctness to the area of software transactional memory (STM). Software transactional memory algorithms allow for concurrent access to shared state. Like linearizability for concurrent data structures, opacity is the established notion of correctness for STMs. First, we provide a novel definition of durable opacity extending opacity to handle crashes and recovery in the context of NVM. Second, we develop a durably opaque version of an existing STM algorithm, namely the Transactional Mutex Lock (TML). Third, we design a proof technique for durable opacity based on refinement between TML and an operational characterisation of durable opacity by adapting the TMS2 specification. Finally, we apply this proof technique to show that the durable version of TML is indeed durably opaque. The correctness proof is mechanized within Isabelle. 2020-05-13 /pmc/articles/PMC7281866/ http://dx.doi.org/10.1007/978-3-030-50086-3_3 Text en © IFIP International Federation for Information Processing 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Bila, Eleni
Doherty, Simon
Dongol, Brijesh
Derrick, John
Schellhorn, Gerhard
Wehrheim, Heike
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
title Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
title_full Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
title_fullStr Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
title_full_unstemmed Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
title_short Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
title_sort defining and verifying durable opacity: correctness for persistent software transactional memory
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7281866/
http://dx.doi.org/10.1007/978-3-030-50086-3_3
work_keys_str_mv AT bilaeleni definingandverifyingdurableopacitycorrectnessforpersistentsoftwaretransactionalmemory
AT dohertysimon definingandverifyingdurableopacitycorrectnessforpersistentsoftwaretransactionalmemory
AT dongolbrijesh definingandverifyingdurableopacitycorrectnessforpersistentsoftwaretransactionalmemory
AT derrickjohn definingandverifyingdurableopacitycorrectnessforpersistentsoftwaretransactionalmemory
AT schellhorngerhard definingandverifyingdurableopacitycorrectnessforpersistentsoftwaretransactionalmemory
AT wehrheimheike definingandverifyingdurableopacitycorrectnessforpersistentsoftwaretransactionalmemory