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

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : wasabi.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
Creator	Doherty, Simon Schellhorn, Gerhard Bila, Eleni Derrick, John Dongol, Brijesh Wehrheim, Heike
Source	PMC
abstract	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.
has issue date	2020-05-13(xsd:dateTime)
bibo:doi	10.1007/978-3-030-50086-3_3
has license	no-cc
sha1sum (hex)	990459fd2cdabe17cab9045483c601774a0b115f
schema:url	https://doi.org/10.1007/978-3-030-50086-3_3
resource representing a document's title	Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
has PubMed Central identifier	PMC7281866
schema:publication	Formal Techniques for Distributed Objects, Components, and Systems
resource representing a document's body	covid:990459fd2cdabe17cab9045483c601774a0b115f#body_text
is schema:about of	named entity 'ITS' named entity 'power' named entity 'data structures' named entity 'Non-volatile memory' named entity 'abstractions' named entity 'proof method' named entity 'linearizability' named entity 'iff' named entity 'algorithm' named entity 'software transactional memory' named entity 'iff' named entity 'shared data' named entity 'low-level' named entity 'linearizable' named entity 'linearizability' named entity 'program execution' named entity 'program counter' named entity 'control flow' named entity 'ATLAS' named entity 'real-time' named entity 'transactional memory' named entity 'running concurrently' named entity 'shared data' named entity 'NVM' named entity 'persistent memory' named entity 'automata' named entity 'STM' named entity 'linearizable' named entity '19, 20' named entity 'program execution' named entity 'sequences of events' named entity 'BerkeleyDB' named entity 'persistent store' named entity 'persistent store' named entity 'persistent store' named entity 'NVM' named entity 'read-only' named entity 'persistent memory' named entity 'linearizability' named entity 'end-to-end' named entity 'data structures' named entity 'mutexes' named entity 'non-volatile memory' named entity 'semantics' named entity 'ACID transactions' named entity 'concurrent programming' named entity 'real-time' named entity 'persistent memory' named entity 'persistent memory' named entity 'persistent memory' named entity 'memory models' named entity 'STM' named entity 'proof techniques' named entity 'memory store' named entity 'linearizability' named entity 'algorithm' named entity 'persistent memory' named entity 'persistent memory' named entity 'critical sections' named entity 'STM' named entity 'linearizability' named entity 'linearizability' named entity 'iff' named entity 'partial function' named entity 'real-time' named entity 'local variables' named entity 'Mnemosyne' named entity 'log management' named entity 'algorithm' named entity 'formal specification' named entity 'non-empty' named entity 'thread-local' named entity 'compare-and-swap' named entity 'causally related' named entity 'linearizability' named entity 'iff' named entity '19, 20' named entity 'non-volatile memory'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software