Towards Data Structure Synthesis

Abstract

Designing efficient data structures and implementing them correctly is a difficult and costly process. The Data Calculator is a design engine that partially solves this problem by automatically synthesizing the most efficient data structure design for a target workload and hardware. In this thesis, we build on the Data Calculator by demonstrating how to programmatically generate formal data structure specifications of Data Calculator designs. These specifications are a key stepping stone towards the ultimate goal of data structure synthesis —the automated construction of data structure implementations that provably satisfy data structure specifications. Correct and efficient data structure implementations can thus be generated by a data structure synthesizer that uses specifications of efficient data structure designs produced by the Data Calculator.