Adaptive Concretization for Parallel Program Synthesis

Program synthesis tools work by searching for an implementation that satisfies a given specification. Two popular search strategies are symbolic search, which reduces synthesis to a formula passed to a SAT solver, and explicit search, which uses brute force or random search to find a solution. In this paper, we propose adaptive concretization, a novel synthesis algorithm that combines the best of symbolic and explicit search. Our algorithm works by partially concretizing a randomly chosen, but likely highly influential, subset of the unknowns to be synthesized. Adaptive concretization uses an online search process to find the optimal size of the concretized subset using a combination of exponential hill climbing and binary search, employing a statistical test to determine when one degree of concretization is sufficiently better than another. Moreover, our algorithm lends itself to a highly parallel implementation, further speeding up search. We implemented adaptive concretization for Sketch, and we evaluated it on a range of benchmarks. We found adaptive concretization is effective in practice, outperforming Sketch in many cases, sometimes significantly, and has good parallel scalability.

VM image

The easiest way to use Sketch and run experiment is to use VM image:

OVA login credential: ( id: cav, password: ae )

This VM image includes Sketch, this testing infrastructure, and database setup, along with the raw data for the submitted version of our paper. You can directly move to short version of experiment to learn the usages of this testing infrastructure and experiments in detail; visit full version of experiment to conduct the whole experiments discussed in the paper; see how to interpret statistics output; and learn how to retrieve statistics from raw data.

Notice that the VM image is set to use just one single core. This means that even experiments for multi-core will be run on a single core if you don't change the setting. To reproduce all the experiments we reported in the paper, you should use a machine with more than 32 cores and accordingly change the number of cores for the VM image by yourself. Instead of the VM image, we provide two more options: an easy-to-install tar ball (below) or building Sketch from source.

Tar ball

Another way to build Sketch is to use an easy-to-install tar ball:

sketch-1.6.9.tgz (as of May 22, 2015) sketch-1.6.8.tgz (as of Feb 5, 2015)

Inside the tar ball, all Java files in sketch-frontend are already compiled, so all you need to do is building sketch-backend. Make sure that you have gcc, g++, bison, and flex. (You may need to install autoconf, automake, and libtool, too.) Then, build the beck-end as follows:

.../ae $ tar xvfz sketch-1.6.9.tgz
.../ae $ cd sketch-1.6.9/sketch-backend
.../ae/sketch-1.6.9/sketch-backend $ chmod +x ./configure
.../ae/sketch-1.6.9/sketch-backend $ ./configure
.../ae/sketch-1.6.9/sketch-backend $ make clean; make

Skip to the Usage section to learn how to use Sketch.