Deriving Divide-and-Conquer Dynamic Programming Algorithms using Solver-Aided Transformations
We introduce a framework allowing domain experts to manipulate computational terms in the interest of deriving better, more efficient implementations.It employs deductive reasoning to generate provably correct efficient implementations from a very high-level specification of an algorithm, and inductive constraint-based synthesis to improve automation. Semantic information is encoded into program terms through the use of refinement types.
In this paper, we develop the technique in the context of a system called Bellmania that uses solver-aided tactics to derive parallel divide-and-conquer implementations of dynamic programming algorithms that have better locality and are significantly more efficient than traditional loop-based implementations. Bellmania includes a high-level language for specifying dynamic programming algorithms and a calculus that facilitates gradual transformation of these specifications into efficient implementations. These transformations formalize the divide-and conquer technique; a visualization interface helps users to interactively guide the process, while an SMT-based back-end verifies each step and takes care of low-level reasoning required for parallelism.
We have used the system to generate provably correct implementations of several algorithms, including some important algorithms from computational biology, and show that the performance is comparable to that of the best manually optimized code.
Wed 2 NovDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:10
Program SynthesisOOPSLA at Matterhorn 2
Chair(s): Martin Odersky EPFL, Switzerland
|Deriving Divide-and-Conquer Dynamic Programming Algorithms using Solver-Aided Transformations|
Shachar Itzhaky MIT CSAIL, Rohit Singh MIT, Rezaul Chowdhury Stony Brook University, Kuat Yessenov MIT, Yongquan Lu MIT, Charles E. Leiserson MIT, Armando Solar-Lezama MIT CSAILDOI Pre-print Media Attached
|Speeding Up Machine-Code Synthesis|
Venkatesh Srinivasan University of Wisconsin - Madison, Tushar Sharma University of Wisconsin - Madison, USA, Thomas Reps University of Wisconsin - Madison and Grammatech Inc.DOI Pre-print Media Attached
|Automated Reasoning for Web Page Layout|
Pavel Panchekha University of Washington, Emina Torlak University of WashingtonDOI Media Attached
|FIDEX: Filtering Spreadsheet Data using Examples|
Xinyu Wang UT Austin, Sumit Gulwani Microsoft Research, Rishabh Singh Microsoft ResearchDOI Media Attached