Please use this identifier to cite or link to this item:
Title: Quiescent consistency: Defining and verifying relaxed linearizability
Authors: Derrick, J
Dongol, B
Schellhorn, G
Tofan, B
Travkin, O
Wehrheim, H
Keywords: Concurrent data structures;Linearizability;Relaxed consistency requirements
Issue Date: 2014
Publisher: Springer Verlag
Citation: Lecture Notes in Computer Science: 8442, pp. 200 - 214, 2014
Abstract: Concurrent data structures like stacks, sets or queues need to be highly optimized to provide large degrees of parallelism with reduced contention. Linearizability, a key consistency condition for concurrent objects, sometimes limits the potential for optimization. Hence algorithm designers have started to build concurrent data structures that are not linearizable but only satisfy relaxed consistency requirements. In this paper, we study quiescent consistency as proposed by Shavit and Herlihy, which is one such relaxed condition. More precisely, we give the first formal definition of quiescent consistency, investigate its relationship with linearizability, and provide a proof technique for it based on (coupled) simulations. We demonstrate our proof technique by verifying quiescent consistency of a (non-linearizable) FIFO queue built using a diffraction tree. © 2014 Springer International Publishing Switzerland.
ISSN: 0302-9743
Appears in Collections:Dept of Computer Science Research Papers

Files in This Item:
File Description SizeFormat 
Fulltext.pdf242.56 kBAdobe PDFView/Open

Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.