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 joint work with Alex Aiken and Peter Hawkins(Stanford),
Kathleen Fisher(DARPA), and Martin Rinard(MIT).
The work is part of Peter Hawkins's Ph.D. thesis
(http://theory.stanford.edu/~hawkinsp/).
Please also see the article about the work that appeared
in the December 2012 issue of CACM.