Speculative linearizability

Linearizability is a key design methodology for reasoning about tations of concurrent abstract data types in both shared memory and message passing systems. It provides the illusion that operations execute sequentially and fault-free, despite the asynchrony and faults inherent to a concurrent system, especially a distributed one. A key property of linearizability is inter-object composability: a system composed of linearizable objects is itself linearizable. However, devising linearizable objects is very difficult, requiring complex algorithms to work correctly under general circumstances, and often resulting in bad average-case behavior. Concurrent algorithm designers therefore resort to speculation: optimizing algorithms to handle common scenarios more efficiently. The outcome are even more complex protocols, for which it is no longer tractable to prove their correctness. To simplify the design of efficient yet robust linearizable protocols, we propose a new notion: speculative l...

• Type: Journal
• Year: 2012
• Where: PLDI
• Authors: Rachid Guerraoui, Viktor Kuncak, Giuliano Losa
• Keywords: Abstract Data Types, Algorithm Designers, Composition Theorem, PLDI 2012, Programming Languages