Computer Science Colloquium
Time+Place : Tuesday 14/02/2012 14:30 room 337-8 Taub Bld.
Speaker : Roman Manevich
Affiliation: UT Austin
Host : Eran Yahav
Title : Synthesizing Concurrent Relational Data Structures
Efficient concurrent data structures are extremely important for obtaining
good performance for most parallel programs. However, ensuring the
correctness of concurrent data structure implementations can be very tricky
because of concurrency bugs such as race conditions and deadlocks. In
systems that use optimistic parallel execution such as boosted transactional
memory systems and the Galois system, the implementation of concurrent data
structures is even more complex because data structure implementations must
also detect conflicts between concurrent activities and support the rollback
of conflicting activities.
At present, these types of concurrent data structures are implemented
manually by expert programmers who write explicitly parallel code packaged
into libraries for use by application programmers. This solution has its
limitations; for example, it does not permit the customization or tuning of
a data structure implementation for a particular application.
In this talk, we present Autograph, which is the first concurrent data
structure compiler that can synthesize concurrent relational data structure
implementations for use by application programmers. The input to Autograph
is a high-level declarative specification of an abstract data type (ADT);
the output is a concurrent implementation of that ADT with conflict
detection and rollback baked in. Our synthesizer is parameterized by a set
of data structures called "tiles", which are building blocks that the
compiler composes to create the overall data structure. Application
programmers can use a simple expression language to tune the composition of
these tiles, thereby exercising high level, fine-grain control of data
We have used Autograph to synthesize concurrent sparse graph data structures
for a number of complex parallel graph benchmarks. Our results show that the
synthesized concurrent data structures usually perform better than the
handwritten ones; for some applications and thread counts, they improve
performance by a factor of 2.
Roman Manevich is a postdoctoral fellow at the university of Texas, Austin.
Roman's research interests are software verification of sequential and
concurrent programs manipulating dynamically allocated (heap) memory by
static analysis, and synthesis of sequential and concurrent programs.
He obtained a B.Sc. Cum Laude in Computer Science in 2001, an M.Sc. Cum
Laude in Computer Science in 2003, and Ph.D. in Computer Science in 2009,
all from Tel Aviv University. His doctoral dissertation concerns the
problem of static analysis of heap-manipulating programs for an unbounded
number of objects and parallel processes. In 2009 he conducted post-doc
research in UCLA on verifying transactional memories for an unbounded number
of threads. He was cited in the Dean's list in 2000 as an outstanding
undergraduate student and received an outstanding graduate student award in
2005. He was awarded the Clore Fellowship for outstanding Ph.D. students in
Israel, in 2005-2008.
Roman has worked in i-Logix (now part of IBM) in 2001-2003 on adding
automatic web-connectivity to embedded devices for UML models using code
generation. He has interned in MSR Redmond, MSR India, and in IBM Watson,
developing efficient static analysis techniques.
Refreshments served from 14:15 on,
Lecture starts at 14:30
Visit our home page- <http://www.cs.technion.ac.il/~colloq>
Technion Math. Net (TECHMATH)
Editor: Michael Cwikel <firstname.lastname@example.org>
Announcement from: Hadas Heier <email@example.com>