Speculative Linearizability

paper ps   
Linearizability is a key design methodology for reasoning about implementations 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 linearizability. This property is as general as linearizability, yet it allows intra-object composability: the correctness of independent protocol phases implies the correctness of their composition. In particular, it allows the designer to focus solely on the proof of an optimization and derive the correctness of the overall protocol from the correctness of the existing, non-optimized one. Our notion of protocol phases allows processes to independently switch from one phase to another, without requiring them to reach agreement to determine the change of a phase. To illustrate the applicability of our methodology, we show how examples of speculative algorithms for shared memory and asynchronous message passing naturally fit into our framework. We rigorously define speculative linearizability and prove our intra-object composition theorem in a trace-based as well as an automaton-based model. To obtain a further degree of confidence, we also formalize and mechanically check the theorem in the automaton-based model, using the I/O automata framework within the Isabelle interactive proof assistant.

Citation

Rachid Guerraoui, Viktor Kuncak, and Giuliano Losa. Speculative linearizability. In ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2012.

BibTex Entry

@inproceedings{GuerraouiETAL12SpeculativeLinearizability,
  author = {Rachid Guerraoui and Viktor Kuncak and Giuliano Losa},
  title = {Speculative Linearizability},
  booktitle = {ACM SIGPLAN Conf. Programming Language Design and Implementation  (PLDI)},
  abstract = {Linearizability is a key design methodology for reasoning
about implementations 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: \emph{speculative linearizability}. This property is as general as
linearizability, yet it allows intra-object composability: the correctness of independent protocol phases implies the correctness of their composition.
In particular,
it allows the designer to focus solely on the proof of
an optimization and derive the
correctness of the overall protocol from the correctness of
the existing, non-optimized one.  
Our notion of protocol phases allows
processes to independently switch from one phase to another,
without requiring them to reach agreement
to determine the change of a phase.  
To illustrate the
applicability of our methodology, we show how 
examples of speculative algorithms for shared memory and
asynchronous message passing naturally
fit into our framework.
We rigorously define
speculative linearizability and prove our intra-object composition 
theorem in a trace-based
as well as an automaton-based model.
To obtain a further degree of confidence, we also 
formalize and mechanically 
check the theorem in the automaton-based model, using 
the I/O automata framework within the Isabelle interactive proof assistant.},
  year = 2012
}