Technion
 
         Computer Science Colloquium
 
    LECTURE on Thursday 06/01/2011
 
Time+Place : Thursday 06/01/2011 14:30 room 337-8 Taub  Bld.
Speaker    : Noam Rinetzky  SPECIAL LECTURE 
Affiliation: Queen Mary, University of London
Host       : Eran Yahav
Title      : Verifying Linearizability with Hindsight
 
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.
 
----------------------------------------------------------
Visit our home page-   <http://www.cs.technion.ac.il/~colloq>
Mon Dec 20 14:54:07 IST 2010
 
---------------------------------------------------------
Technion Math. Net (TECHMATH)
Editor: Michael Cwikel   <techm@math.technion.ac.il> 
Announcement from: Hadas Heier   <heier@cs.technion.ac.il>