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 induct...
| Main Authors: | , , , , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Association for Computing Machinery (ACM)
2017
|
| Online Access: | http://hdl.handle.net/1721.1/112349 https://orcid.org/0000-0002-3306-5084 https://orcid.org/0000-0002-8927-3018 https://orcid.org/0000-0001-7604-8252 https://orcid.org/0000-0001-5959-5254 |
| _version_ | 1811095689358213120 |
|---|---|
| author | Chowdhury, Rezaul Itzhaky, Shachar Singh, Rohit Solar Lezama, Armando Yessenov, Kuat T Lu, Yongquan Leiserson, Charles E |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Chowdhury, Rezaul Itzhaky, Shachar Singh, Rohit Solar Lezama, Armando Yessenov, Kuat T Lu, Yongquan Leiserson, Charles E |
| author_sort | Chowdhury, Rezaul |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T16:24:34Z |
| format | Article |
| id | mit-1721.1/112349 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T16:24:34Z |
| publishDate | 2017 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/1123492022-10-02T07:56:12Z Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations Chowdhury, Rezaul Itzhaky, Shachar Singh, Rohit Solar Lezama, Armando Yessenov, Kuat T Lu, Yongquan Leiserson, Charles E Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Massachusetts Institute of Technology. Department of Mathematics Itzhaky, Shachar Singh, Rohit Solar Lezama, Armando Yessenov, Kuat T Lu, Yongquan Leiserson, Charles E 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. National Science Foundation (U.S.) (CCF-1139056) National Science Foundation (U.S.) (CCF- 1439084) National Science Foundation (U.S.) (CNS-1553510) 2017-12-01T22:41:24Z 2017-12-01T22:41:24Z 2016-11 Article http://purl.org/eprint/type/ConferencePaper 9781450344449 http://hdl.handle.net/1721.1/112349 Itzhaky, Shachar, Rohit Singh, Armando Solar-Lezama, Kuat Yessenov, Yongquan Lu, Charles Leiserson, and Rezaul Chowdhury. “Deriving Divide-and-Conquer Dynamic Programming Algorithms Using Solver-Aided Transformations.” Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications - OOPSLA 2016 (2016). https://orcid.org/0000-0002-3306-5084 https://orcid.org/0000-0002-8927-3018 https://orcid.org/0000-0001-7604-8252 https://orcid.org/0000-0001-5959-5254 en_US http://dx.doi.org/10.1145/2983990.2983993 Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications - OOPSLA 2016 Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Association for Computing Machinery (ACM) MIT Web Domain |
| spellingShingle | Chowdhury, Rezaul Itzhaky, Shachar Singh, Rohit Solar Lezama, Armando Yessenov, Kuat T Lu, Yongquan Leiserson, Charles E Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations |
| title | Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations |
| title_full | Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations |
| title_fullStr | Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations |
| title_full_unstemmed | Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations |
| title_short | Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations |
| title_sort | deriving divide and conquer dynamic programming algorithms using solver aided transformations |
| url | http://hdl.handle.net/1721.1/112349 https://orcid.org/0000-0002-3306-5084 https://orcid.org/0000-0002-8927-3018 https://orcid.org/0000-0001-7604-8252 https://orcid.org/0000-0001-5959-5254 |
| work_keys_str_mv | AT chowdhuryrezaul derivingdivideandconquerdynamicprogrammingalgorithmsusingsolveraidedtransformations AT itzhakyshachar derivingdivideandconquerdynamicprogrammingalgorithmsusingsolveraidedtransformations AT singhrohit derivingdivideandconquerdynamicprogrammingalgorithmsusingsolveraidedtransformations AT solarlezamaarmando derivingdivideandconquerdynamicprogrammingalgorithmsusingsolveraidedtransformations AT yessenovkuatt derivingdivideandconquerdynamicprogrammingalgorithmsusingsolveraidedtransformations AT luyongquan derivingdivideandconquerdynamicprogrammingalgorithmsusingsolveraidedtransformations AT leisersoncharlese derivingdivideandconquerdynamicprogrammingalgorithmsusingsolveraidedtransformations |