SKETCH is a sketching system based on combinatorial search. In this system, the sketch is given in the form of a partial program - a program with integer holes - and the SKETCH compiler synthesizes code to fill in the holes. The programmer can easily define new kinds of holes, e.g. through array indexing.
SKETCH completes sketches by means of a combinatorial search based on generalized boolean satisfiability. The central method is the '''synthesis-verification loop'''. In the synthesis stage, values for the holes are synthesized for some input. In the verification stage, the holes are either found to satisfy all inputs, or a counterexample is found, which is checked next time holes are synthesized.
Sketches and specifications are written using The SKETCH language. This is a simple imperative language; its syntax is similar to C.
How the SKETCH solver works
First, the sketch file is parsed by Java, and various preprocessing is done to eliminate higher level constructs (provided for programmer convenience), make necessary simplifications (e.g. loop unrolling), and typical compiler optimizations. Next, random values are chosen for the holes, so the verification will find some counterexample. This starts the synthesis verify loop. For synthesis, the sketch is converted to a boolean circuit, and holes can be found by a SAT (boolean satisfiability) solver library, such as MiniSAT or ABC. For verification, the sketch is converted to a language such as Promela (for spin), and it is found to be either valid or a counterexample is generated.
After the synthesized program is valid for all inputs, postprocessing is done. This begins with the sketch before preprocessing, so higher constructs remain, e.g. loops are not unrolled in the completed sketch. The sketch is then returned to the user.
There are several projects that make up sketching (led by Dr. Ras Bodik and Dr. Armando Solar-Lezama). The CEGIS solver (for sequential sketches) is written in C++, and in the "sketch-backend" repository. Support for sequential sketches, parallel sketches, and stencil sketches is done in Java in the "sketch-frontend" project.
- Sketching for Structured Grid Computations - A talk on sketching for stencils given at the OSQ lunch on Oct 5 2006
- Combinatorial Sketching for Finite Programs - Paper presented at ASPLOS 2006
- Sketching Stencils - Paper presented at PLDI 2007
- Sketching Concurrent Data Structures - Paper presented at PLDI 2007