In case you are interested, here is a harder way to build Sketch. To reclaim what we claim in the paper, clone the specific versions of sketch-frontend and sketch-backend:
.../ae $ hg clone -r e026b22d00ee131b4ecf8ffa3845083626c1e40f \
> https://bitbucket.org/gatoatigrado/sketch-frontend
.../ae $ hg clone -r d9f004c9a54c063ee57a14f09fa5e0d7d81a1291 \
> https://bitbucket.org/gatoatigrado/sketch-backend
Make sure that you have java, javac,
and mvn for sketch-frontend;
gcc, g++, bison, and flex
for sketch-backend.
(You may need to install autoconf, automake,
and libtool, too.)
Then, build Sketch as follows:
.../ae $ cd sketch-frontend
.../ae/sketch-frontend $ make assemble-noarch
.../ae $ cd sketch-backend
.../ae/sketch-backend $ ./autogen.sh
.../ae/sketch-backend $ chmod +x ./configure
.../ae/sketch-backend $ ./configure
.../ae/sketch-backend $ make clean; make
You can run a simple test case to make sure the build is correct:
.../ae $ cd sketch-frontend
.../ae/sketch-frontend $ make run-local-seq EXEC_ARGS="src/test/sk/seq/miniTest1.sk"
One possible issue you may encounter while building sketch-frontend is
the inconsistent Java version in Maven, e.g., Maven refers to Java 1.6
while the main Java you're using is 1.7 or higher. In that case, set up
$JAVA_HOME properly:
stackoverflow.
If you suffer from any other build errors, please contact the authors.
To use sketch from anywhere,
we recommend you to set up your environment accordingly.
For the tar ball users:
export SKETCH_HOME=/path/to/sketch-1.6.9/sketch-frontend/runtime
export PATH=$PATH:$SKETCH_HOME/..
For the source users:
export SKETCH_HOME=/path/to/sketch-frontend
export PATH=$PATH:$SKETCH_HOME/target/sketch-1.6.9-noarch-launchers
If you are using the up-to-date Sketch, double-check Sketch version number, which can be seen while building sketch-frontend.
Our testing infrastructure takes care of all the Sketch options that will be explained below. Therefore, if you are not interested, you can move to the Experiments page now.
The option to enable (random) concretization is:
--slv-randassign.
You can also specify the degree of concretization via
--slv-randdegree n.
(Please refer to the paper for the notions of concretization and its degree.)
$ sketch --slv-randassign [--slv-randdegree n] ... target.sk
Since concretized values for holes are random,
the UNSAT result from the back-end doesn't mean the given sketch is indeed UNSAT.
That is, if you are sure that the target sketch is satisfiable,
you need to run concretized sub-problems many times until resolved.
The option --slv-parallel will run many instances of sketch-backend
in parallel. Note that that option merely runs same instances of
sketch-backend in parallel if you don't pass any options about concretization.
Thus, the preferred usage is using it along with --slv-randassign:
$ sketch --slv-parallel --slv-randassign [--slv-randdegree n] ... target.sk
You can also run parallel instances of sketch-backend with different degrees:
$ sketch --slv-parallel --slv-randassign --slv-randdegrees n1,n2,n3,n4 ... target.sk
Rather than a fixed degree of concretization,
the option --slv-strategy WILCOXON will adjust the degree adaptively
until it figures out a statistically better degree than another.
$ sketch --slv-parallel --slv-randassign --slv-strategy WILCOXON ... target.sk
There are couple more minor options to tune Sketch behavior:
--slv-p-cpus n: number of cores to use
Thread pool.
So, if it's set something bigger than what the system has,
Sketch will still use what the system has.
--slv-p-timeout t: (adaptive) timeout for parallel trials
--slv-p-trials n: number of parallel trials
--slv-timeout t: timeout for overall Sketch (in minute)
--slv-p-trials.
First of all, don't be alarmed if you saw a bunch of Rejected
and/or UNSATISFIABLE messages. Those messages are definitely
normal (as long as you run Sketch with this adaptive concretization feature).
With (random) concretization, we can make a sub-synthesis problem smaller,
but its chance of getting lucky (i.e., being correct) is getting lower,
resulting in those many 'Rejected' cases;
we just repeat it until the concretization is (partially) correct.
The key idea is that solving both unlucky (due to the wrong concretization)
and lucky sub-synthesis problems is really quick, and thus repeating such process
again and again is way faster than solving an original synthesis problem
in a purely symbolic manner.
Therefore, the output of Sketch will be comprised of a sequence of failed trials,
followed by one single successful trial.
Each trial begins and ends with a noticeable separator:
=== parallel trial ... (n) ... ===.
Between those trials, messages attached with [wilcoxon] will
show the detailed steps during the adaption phase, such as
1) starting sampling, 2) calculating distributions, 3) Wilcoxon test, and
4) comparing degrees. In general, the outputs generated by
Sketch with the adaptive concretization would look like as follows:
SKETCH version 1.6.9
Benchmark = benchmark_name
...
... [wilcoxon] start sampling: degree 16
...
... [wilcoxon] start sampling: degree 32
...
... === parallel trial ... (i) started ===
...
... === parallel trial ... (i) failed ===
...
... === parallel trial ... (j) started ===
...
... === parallel trial ... (j) failed ===
...
... [wilcoxon] degree 16 dist: [ ... ]
... [wilcoxon] degree 32 dist: [ ... ]
... [wilcoxon] test (16, 32): 0.xyz
...
... [wilcoxon] compareDegree(16, 32) = (-1 | 0 | 1)
...
... [wilcoxon] degree choice: d
...
... === parallel trial w/ degree d (n-1) started ===
...
... === parallel trial w/ degree d (n-1) failed ===
...
... === parallel trial w/ degree d (n) started ===
...
... === parallel trial w/ degree d (n) solved ===
...
SYNTHESIZED_CODE_OCCURS_HERE
Note that the above example is based on up-to-date Sketch, so earlier versions may not have same messages.