## Verifying Linearizability with Hindsight

*Noam Rinetzky, Peter O'Hearn, Martin Vechev, Eran Yahav, Greta Yorsh*

In *Proc. Principles of Distributed Computing*, 2010
(**PODC'10**)

Preliminary version appeared as a position paper in EC^2 2009 (CAV 2009 workshop)

**Verifying Optimistic Algorithms Should be Easy**

We present a formal proof of safety and linearizability of a highly-concurrent optimistic set algorithm.
The key step in our proof is the Hindsight lemma which allows a thread to infer the existence of a global state
in which its operation can be linearized based on limited local atomic observations about the shared state.
The Hindsight lemma *eliminates the need for explicitly reasoning about linearization points
by allowing a temporal non-constructive approach to verify linearizability*.
Furthermore, it is independent of the particular algorithm considered,
and thus can be reused to verify other algorithms.

The Hindsight lemma assumes that the algorithm maintains certain simple invariants
which are resilient to interference, and thus can be verified using purely thread-local proofs.
As a consequence, the Hindsight lemma allows us to unlock a perhaps-surprising intuition:
a high degree of interference makes non-trivial highly-concurrent algorithms
in some cases much easier to verify than less concurrent ones.

Click here to access the position paper:
PDF;
PS