Moore's Law has not revolutionized programming. What computational technologies support programmers in the task of building complex systems? So far, four technologies have been adopted: testing, type checking, model checking, and compilers. First three focus on assuring correctness of code; compilers actually help with writing the code, by raising the level of programming abstractions. Despite adoption of high-level languages, though, it is fair to say that we don't know how to usefully burn computer cycles at the frontend of the program development process: programmers still rely on paper and pencil when writing code.
Computer-aided programming with synthesis. We are developing computer-aided programming that brings the computational power to the process of constructing programs. We pose the problem as synthesis of programs from multi-modal specifications: templates of programs, declarative assertions, executable specifications, examples and demonstrations. We are developing synthesis theories and algorithms, language constructs and tools that embed synthesis into the programming process.
Sketching: Program synthesis as constraint solving
Domain-specific synthesis, for stencil matrix codes. By default, the Sketch synthesizer verifies the synthesized program with bounded model checking, proving its correctness for all inputs of up to certain size. While verification under this small-world assumption usually suffices for correctness, it sometimes fails to sufficiently reduce the size of the problem. In particular, when inputs to the program are matrices, the "small world of inputs" may remain very large, overwhelming the synthesizer's constraint solving. In [Sketching Stencils, PLDI 2007], we show how to translate a class of matrix programs, called stencils, into logical formulas without having to adopt the small-world assumption. The key idea is to express symbolically the value of a single element of the output matrix. This symbolic representation preserves the holes from the original sketch and so we can perform synthesis on this representation. Synthesizing one matrix element symbolically, rather than all at once, greatly improves scalability. A side effect is that we guarantee functional correctness on all input sizes. As a case study, we synthesized highly optimized 3D stencils from the Multigrid solver that programmers currently write by hand.
Synthesis of Concurrent Programs. It seems straightforward to generalize constraints-based inductive synthesis to concurrent programs. In principle, it suffices to transform the concurrent program into a sequential one by lifting the schedule that governs thread interleaving into an explicit program input. While this modeling indeed reduces concurrent synthesis to sequential synthesis, it makes inductive synthesis much less effective. This is because observations to inductive synthesis are now schedules, not ordinary function inputs. Why is this a problem? An ordinary input is a powerful observation because it is valid for all programs from the candidate space; as such, a single input observation prunes out about 90% of incorrect candidates. In contrast, a schedule applies to only to some candidate programs; this is because the counterexample schedule orders statements that are not present in all candidate programs. In [Sketching Concurrent Data Structures, PLDI 2008] we show how to encode the concurrent program synthesis problem so that the inductive synthesizer exploits its counterexample schedules to as much as possible, by using the largest possible schedule prefix, thus pruning out candidates whose incorrectness has been exposed by that prefix. Our concurrent synthesizer allowed us to synthesize realistic lock-free data structures and barriers
Interactive synthesis with angelic programming.
Synthesis-based compilers.
Modular synthesis.
Synthesis with refinement.
Specification mining and synthesis of API-level codes
Distribution of tools The synthesizer SKETCH has gone through several public releases (http://bitbucket.org/gatoatigrado/sketch-frontend) and has been used by industrial and national research labs (MSR and ANL).
We also added sketching and angelic constructs into the Scala language in order to explore how to make synthesis available to mainstream programmers. Our Scala prototype, called Skalch, offers an IDE for angelic programming, a backtracking solver, and mining of oracular traces based on the notion of entanglement.
Programs that we synthesized Block ciphers [ASPLOS 2006]; highly optimized matrix code [PLDI 2007]; lock free lists and barriers [PLDI 2008]; Deutsch-Shorr-Waite [POPL 2010]; Dynamic Programming Algorithms, including parallel ones [OOPSLA 2011]; Client code for the Eclipse framework [Jungloid Mining, PLDI 2005].