Synthesis and Analysis of Heap Data Structures

Stanford University, Stanford CA

Investigators

Abstract

Almost all software today is developed in two stages. First, a human writes a program and subsequently various automated tools process that program to produce the actual computer code that is the software application. Over time, researchers have found ways to shift more of the burden of developing software from the programmer to the automated tools, which has gradually made software development more and more productive. One area of software development that has not changed for a couple of decades is the way in which the structure of data is programmed. The organization of data is still described in relatively low-level terms as links between individual objects in memory, which is too low-level for the tools to reason successfully about. As a result, programmers must spend significant time hand-coding and tuning their data structures, and there are significant missed opportunities for improvements to program performance, correctness, and security. We propose to try a new approach to this problem, consisting of two parts: we will synthesize data structures from high-level relational specifications. We will also use inference techniques to automatically analyze the program?s use of the relations. In a relational style of programming explicit pointers are eliminated, removing one of the biggest impediments to automatic reasoning. We believe recent advances in the analysis of control flow, destructive updates, and low-level indexing operations make it feasible to capture most other aspects of programs. If successful, programs, including concurrent programs, will be written at a higher level and be more easily retargeted to new situations because the data representations are not fixed in advance, and tools will be able to do a more reliable, efficient, and scalable job of optimizing resources and verifying properties of programs. As part of the project, we will seek to demonstrate these benefits by conducting studies of our techniques applied to realistic challenge applications.