Data Representation Synthesis

Abstract

We consider the problem of specifying combinations of data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract data types are specified using relational algebra and functional dependencies. We describe a language of decompositions that permit the user to specify different concrete representations for relations, and show operations on concrete representations soundly implement their relational specification. We show that it is practical to incorporate data representations synthesized by our compiler into existing systems, allowing us to write code that is simpler, correct by construction, and comparable in performance to the code it replaces. We describe our experience with an implementation; code generated by our system can easily be dropped into existing systems in place of complex hand-written implementations with comparable performance.

Joint work with Alex Aiken, Kathleen Fisher, Martin Rinard, and Mooly Sagiv