Title
Quiescent Consistency: Defining and Verifying Relaxed Linearizability.
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.
Year
Venue
Keywords
2014
Lecture Notes in Computer Science
linearizability,concurrent data structures
Field
DocType
Volume
Linearizability,Local consistency,Sequential consistency,Computer science,Real-time computing,Weak consistency,Consistency model,Concurrent data structure,Strong consistency,Release consistency
Conference
8442
ISSN
Citations 
PageRank 
0302-9743
8
0.44
References 
Authors
18
6
Name
Order
Citations
PageRank
John Derrick117016.67
Brijesh Dongol219325.27
Gerhard Schellhorn376956.43
Bogdan Tofan4864.93
Oleg Travkin5525.66
Heike Wehrheim61013104.85