Back to Search Start Over

Toward Linearizability Testing for Multi-Word Persistent Synchronization Primitives

Authors :
Diego Cepeda and Sakib Chowdhury and Nan Li and Raphael Lopez and Xinzhe Wang and Wojciech Golab
Cepeda, Diego
Chowdhury, Sakib
Li, Nan
Lopez, Raphael
Wang, Xinzhe
Golab, Wojciech
Diego Cepeda and Sakib Chowdhury and Nan Li and Raphael Lopez and Xinzhe Wang and Wojciech Golab
Cepeda, Diego
Chowdhury, Sakib
Li, Nan
Lopez, Raphael
Wang, Xinzhe
Golab, Wojciech
Publication Year :
2020

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.

Details

Database :
OAIster
Notes :
application/pdf, English
Publication Type :
Electronic Resource
Accession number :
edsoai.on1358726957
Document Type :
Electronic Resource
Full Text :
https://doi.org/10.4230.LIPIcs.OPODIS.2019.19