Implementation sketching:

Programming with sketches is a semi-automatic approach for high-performance applications. Sketching is a search-based approach that both simplifies programming and guarantees full correctness of the resulting implementation. With sketching, programmers write clean and portable reference code, and then obtain a high-quality implementation by simply sketching an outline of the desired implementation. The compiler then fills in the missing detail. The detail is filled in by searching for such ``completions'' of the sketch that are guaranteed to implement the reference code.

A sketch is a partial specification of the implementation, and as such, it has several benefits to programmer productivity and code correctness: (1) a sketch is easier to write compared to a complete implementation; (2) the sketching compiler rejects a ``buggy'' sketch, thus allowing the programmer to quickly evaluate sophisticated implementation ideas because he can focus on exploring algorithmic details rather than on orchestrating low-level details; and (3) the compiler completes the sketch in such a way that the implementation becomes a the result of a sequence of semantics-preserving transformations, which constitutes a proof that the (complex) implementation is equivalent to the (simple) reference code.

Sketching is a domain-specific programming approach. This proposal develops sketching algorithms and tools for the important class of cryptographic programs. Our preliminary results indicate significant gains in programmer productivity. Our user study shows that given the same time budget, a cipher developed in our system ran 3~to 5-times faster than same cipher coded in C. Furthermore, our sketching-based implementation of the DES cipher, developed and tuned in just four hours matched the performance of libDES, the best publicly available DES implementation.