Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations
Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations
复制标题
使用求解器辅助变换导出分治动态规划算法
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
R. Chowdhury
中科院分区：
文献类型：
--
作者：
Shachar Itzhaky;Rohit Singh;Armando Solar;Kuat Yessenov;Yongquan Lu;C. Leiserson;R. Chowdhury
我们引入了一个框架，允许领域专家操纵计算术语，以获得更好、更有效的实现。它采用演绎推理从一个非常高级的算法规范生成可证明正确的高效实现，并采用基于约束的归纳综合来提高自动化。语义信息通过使用细化类型编码到程序术语中。在本文中，我们在一个名为Bellmania的系统中开发了该技术，该系统使用求解器辅助策略来推导动态规划算法的并行分治实现，这些算法具有更好的局部性，并且比传统的基于循环的实现更有效。Bellmania包括一个用于指定动态规划算法的高级语言，以及一个有助于将这些规范逐步转换为有效实现的演算。这些转换形式化了分治技术；可视化界面帮助用户交互式地指导流程，而基于smt的后端验证每个步骤，并负责并行性所需的低级推理。我们已经使用该系统生成了几种算法的可证明的正确实现，包括计算生物学中的一些重要算法，并表明其性能可与最佳的手动优化代码相媲美。
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.