Abstract:

Verifying  concurrent algorithms that manipulate unbounded pointer-linked  
data structures is a challenging problem because it involves reasoning about
spatial and temporal interaction between concurrently running threads.
We suggest a novel approach for verification of concurrent algorithms which
separates the reasoning about the algorithmic insight from the verification 
of its implementation.

In this talk, we exemplify our approach by presenting a proof of safety, 
linearizability, and  progress 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 allows us to avoid one of the most complex
and non-intuitive steps in reasoning about highly concurrent linearizable 
algorithms: considering the linearization point of an operation to be in
a different thread than the one executing it.

The Hindsight Lemma assumes that the algorithm maintains certain
simple invariants which are resilient to interference, and which
can themselves be verified using purely thread-local proofs. As a
consequence, the 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.

The talk is based on joint work with Peter O'Hearn, Martin Vechev, 
Eran Yahav and Greta Yorsh, published in PODC'10, and on ongoing 
research with Richard Bornat, Peter O'Hearn, and Hongseok Yang. 

No prior knowledge regarding linearizability, concurrent algorithms, or
verification is assumed.


Short Bio:
Noam Rinetzky is a Royal Academy of Engineering/EPSRC Research Fellow at
Queen Mary, University of London. His research interests span all aspects of
software systems, including, in particular, their design, construction,
understanding and verification. His current research focuses on studying the
implementations of existing concurrent software systems and building program
analyses and reasoning techniques that are specialized to the ways systems
are actually being built.

Noam obtained his Ph.D. from the School of Computer Science in Tel Aviv
University.  He received the IBM PhD. Fellowship award for the academic 
year 2005-2006.  His dissertation, titled "Interprocedural and Modular 
Shape Analysis", addresses the problem of automatic verification of procedural 
sequential programs that manipulate unbounded pointer-linked data structures.

Prior to his doctoral studies, Noam worked for three years in IBM Haifa
Research Laboratory on secure distributed storage systems.