Sketching with Partial ProgramsArmando Solar-Lezama, Liviu Tancau, David Turner, Rastislav Bodik, Vijay Saraswat∗, Sanjit SeshiaUC Berkeley∗IBM ResearchAbstractSketching is a software synthesis approach where the programmerdevelops a partial implementation — a sketch — and a separatespecification of the desired functionality. The synthesizer then com-pletes the sketch to behave like the specification. The synthesizedimplementation is correct by construction, which allows, amongother benefits, rapid sketching of many implementations withoutthe fear of introducing bugs.We develop SKETCH, a language for finite programs with lin-guistic support for sketching. Finite programs include many high-performance kernels, including cryptocodes. In contrast to priorwork, where sketches were meta-level rewrite rules, our sketchesare simple-to-understand partial programs. Partial programs areprograms with “holes” that are filled by the synthesizer. The un-specified behavior of partial programs is modeled with a singlenon-deterministic operator that we show to be surprisingly versa-tile. We also develop a synthesizer that is complete for the classof finite programs: it is guaranteed to complete any sketch in the-ory, and in practice has scaled to complex real-world programmingproblems.1. IntroductionWhen programming by sketching, the programmer develops onlya skeleton of the desired implementation, called a sketch, and asynthesizer completes the sketch such that it is equivalent to aseparate specification of the desired behavior.The goal of sketching is to bridge the abstraction gap betweena high-level task and its low-level implementation. Sketches sitbetween the two extremes: unlike specifications, sketches spellout the implementation strategy, and unlike implementations, theyomit low-level details. By separating correctness and performance,sketches allow the abstraction gap to widen: First, sketching en-courages cleaner specifications because it relies on specificationonly for behavioral specification. Second, sketching enables com-plex implementations that may be too tedious to develop and main-tain without automatic synthesis of low-level detail.We introduced the concept of sketching in StreamBit, a systemfor bit-stream programming [14]. In StreamBit, sketching proved tobe very effective. We implemented, in a single afternoon, an imple-mentation of the DES cipher that nearly matched the performanceof the best public-domain DES implementation. In another exper-iment, a sketched implementation of a cipher was produced twiceas a fast as a C implementation, and ran 50% faster.Unfortunately, we were unable to transfer the success of sketch-ing from the lab to real programmers. Even though the concept ofsketching was easy to explain, sketching as embedded in StreamBitrequired significant training. In fact, only one of the authors of [14]was able to write non-trivial sketches.This paper attacks programmability challenges observed inStreamBit: (1) Programmers could not express sketches directlyin the implementation language. Instead, they had to sketch thedesired implementation by means of meta-level rewrite rules thattranslated the specification into the desired implementation. (2) Theimplementation strategy had to be often decomposed hierarchicallyinto multiple sketches with onerous dependences. For example, thesketch specifying word-level parallelism had to plan the implemen-tation carefully so that the sketch for bit-level parallelism wouldapply. (3) Sketches had to be inserted into the rewrite sequenceof a baseline compiler. The awareness of the baseline compilermade the meta-level nature of rewrite rules even more confound-ing. (4) Sketching was embedded into a dataflow programminglanguage [15]. While the dataflow programming model helped syn-thesis and subsequent parallelization, novice programmers facedsketching simultaneously with another new programming model.This paper develops linguistic support that sidesteps these fourissues. First, sketches are expressed as partial programs, or pro-grams with “holes.” As a result, sketches are not meta-rules butstraighforward code templates. Second, the desired implementa-tion can now be sketched in a single sketch, without decomposi-tion. Third, there is no baseline compiler to cooperate with. Finally,sketching is embedded into an imperative language with a familiarprogramming model.Besides programmability limitations, sketching in [14] was alsorestricted in expressiveness. (1) Except for some high-level refac-torings, sketching worked only for programs that computed (semi)-permutations of bit-vectors. While this sufficed for DES, the mod-ern block cipher standard, AES, was beyond our power. (2) Thesketched implementations themselves could not implement permu-tations using non-permutations instructions, such as additions. Thislimitation prevented us from exploiting some efficient DES imple-mentation strategies.In contrast, the SKETCH language presented in this paper iscomplete. We can both specify any finite program and sketch anyimplementation of it. A finite program is any program whose inputis bounded in size and the program is guaranteed to terminate onany input. Most high-performance kernels have this property.In SKETCH, sketches are partial programs, i.e., programs wherecode fragments to be synthesized are indicated with a non-deterministicoperator ??. The operator is defined as returning a non-deterministicallychosen integer value; the synthesizer replaces the operator with asuitable integer such that the resolved sketch behaves like the spec-ification. The ?? operator is more versatile than it may seem: it canautomatically derive values of hard-to-compute constants, such asbitmasks; it can be used to divide the work in a divide-and-conqueralgorithm; and it can be used to synthesize the number of iterationsof a loop. It can also be used to to synthesize a polynomial, whichis useful in implementing big-integer multiplications algorithms.Programming with non-determinism can be thought of as takingprogram verification one step further. In fact, if the sketch is fullydeterministic, i.e., it is a regular program, then we are left with asimple verification problem where the compiler has to prove thatan implementation is equivalent to the specification. However, thenon-determinism allows us to use the verifier not just to prove that1 2006/1/16the program is correct but to help us write it, by searching the spaceof sketch
View Full Document
Unlocking...