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.
The easiest way to use Sketch and run experiment is to use VM image:
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.
Another way to build Sketch is to use an easy-to-install tar ball:
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.