Please use this identifier to cite or link to this item:
|Title:||Quiescent consistency: Defining and verifying relaxed linearizability|
|Keywords:||Concurrent data structures;Linearizability;Relaxed consistency requirements|
|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.|
|Appears in Collections:||Dept of Computer Science Research Papers|
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.