Concurrent Data Representation Synthesis

August 14, 2012
Mooly Sagiv | Tel-Aviv University

We describe an approach for synthesizing data representations
for concurrent programs. Our compiler takes as input a program
written using concurrent relations and synthesizes a representation
of the relations as sets of cooperating data structures as well as the
placement and acquisition of locks to synchronize concurrent access
to those data structures. The resulting code is correct by construction:
individual relational operations are implemented correctly and the
aggregate set of operations is serializable and deadlock free. The
relational specification also permits a high-level optimizer to choose
the best performing of many possible legal data representations
and locking strategies, which we demonstrate with an experiment
autotuning a graph benchmark.

This is a joint work with Peter Hawkins (Google), Alex Aiken
(Stanford), Kathleen Fisher (Tufts University) and Martin Rinard
(MIT).

Speaker Details

1991 Ph.D., Computer Science, Technion, Israel Institute of Technology, Haifa
High Level Formalisms for Program Flow Analysis
1991-93 Research Staff Member, IBM Haifa Research Group,
Programming Languages
1993-94 Visiting Professor, Datalogisk Institute, University of Copenhagen, Copenhagen
1994-95 Visiting Associate Research Scientist, Computer Science Department, University of Madison-Wisconsin
1996-1997 Visiting Professor, Computer Science Department, University of Chicago
1997-00 Lecturer, Computer Science Department, Tel-Aviv University
2000-present Senior Lecturer, Computer Science Department, Tel-Aviv University