2026-07-22T06:26:53Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11805 2024-03-06T10:48:49Z ddc:004 open_access

Toward Linearizability Testing for Multi-Word Persistent Synchronization Primitives Cepeda, Diego Chowdhury, Sakib Li, Nan Lopez, Raphael Wang, Xinzhe Golab, Wojciech Shared memory persistent memory synchronization multi-word primitives concurrency correctness software testing 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Diego Cepeda and Sakib Chowdhury and Nan Li and Raphael Lopez and Xinzhe Wang and Wojciech Golab 2020 Is Part Of LIPIcs, Volume 153, 23rd International Conference on Principles of Distributed Systems (OPODIS 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.OPODIS.2019.19 urn:nbn:de:0030-drops-118050 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2019.19 eng https://creativecommons.org/licenses/by/3.0/legalcode