License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.OPODIS.2019.19
URN: urn:nbn:de:0030-drops-118050
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/11805/
Go to the corresponding LIPIcs Volume Portal

Cepeda, Diego ; Chowdhury, Sakib ; Li, Nan ; Lopez, Raphael ; Wang, Xinzhe ; Golab, Wojciech

Toward Linearizability Testing for Multi-Word Persistent Synchronization Primitives

pdf-format:
LIPIcs-OPODIS-2019-19.pdf (0.9 MB)

Abstract

Persistent memory makes it possible to recover in-memory data structures following a failure instead of rebuilding them from state saved in slow secondary storage. Implementing such recoverable data structures correctly is challenging as their underlying algorithms must deal with both parallelism and failures, which makes them especially susceptible to programming errors. Traditional proofs of correctness should therefore be combined with other methods, such as model checking or software testing, to minimize the likelihood of uncaught defects. This research focuses specifically on the algorithmic principles of software testing, particularly linearizability analysis, for multi-word persistent synchronization primitives such as conditional swap operations. We describe an efficient decision procedure for linearizability in this context, and discuss its practical applications in detecting previously-unknown bugs in implementations of multi-word persistent primitives.

BibTeX - Entry

@InProceedings{cepeda_et_al:LIPIcs:2020:11805,
  author =	{Diego Cepeda and Sakib Chowdhury and Nan Li and Raphael Lopez and Xinzhe Wang and Wojciech Golab},
  title =	{{Toward Linearizability Testing for Multi-Word Persistent Synchronization Primitives}},
  booktitle =	{23rd International Conference on Principles of Distributed Systems (OPODIS 2019)},
  pages =	{19:1--19:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-133-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{153},
  editor =	{Pascal Felber and Roy Friedman and Seth Gilbert and Avery Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/11805},
  URN =		{urn:nbn:de:0030-drops-118050},
  doi =		{10.4230/LIPIcs.OPODIS.2019.19},
  annote =	{Keywords: Shared memory, persistent memory, synchronization, multi-word primitives, concurrency, correctness, software testing}
}

Keywords: Shared memory, persistent memory, synchronization, multi-word primitives, concurrency, correctness, software testing
Collection: 23rd International Conference on Principles of Distributed Systems (OPODIS 2019)
Issue Date: 2020
Date of publication: 11.02.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI