Adaptive Concretization for Parallel Program Synthesis
Program synthesis tools work by searching for an implementation that satisfies a given specification. Two popular search strategies are symbolic search, which reduces synthesis to a formula passed to a SAT solver, and explicit search, which uses brute force or random search to find a solution. In th...
| Principais autores: | , , , |
|---|---|
| Outros Autores: | |
| Formato: | Artigo |
| Idioma: | en_US |
| Publicado em: |
Springer-Verlag
2017
|
| Acesso em linha: | http://hdl.handle.net/1721.1/111033 https://orcid.org/0000-0001-9476-7349 https://orcid.org/0000-0001-7604-8252 |
| _version_ | 1826216502003499008 |
|---|---|
| author | Jeon, Jinseong Foster, Jeffrey S. Qiu, Xiaokang Solar Lezama, Armando |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Jeon, Jinseong Foster, Jeffrey S. Qiu, Xiaokang Solar Lezama, Armando |
| author_sort | Jeon, Jinseong |
| collection | MIT |
| description | Program synthesis tools work by searching for an implementation that satisfies a given specification. Two popular search strategies are symbolic search, which reduces synthesis to a formula passed to a SAT solver, and explicit search, which uses brute force or random search to find a solution. In this paper, we propose adaptive concretization, a novel synthesis algorithm that combines the best of symbolic and explicit search. Our algorithm works by partially concretizing a randomly chosen, but likely highly influential, subset of the unknowns to be synthesized. Adaptive concretization uses an online search process to find the optimal size of the concretized subset using a combination of exponential hill climbing and binary search, employing a statistical test to determine when one degree of concretization is sufficiently better than another. Moreover, our algorithm lends itself to a highly parallel implementation, further speeding up search. We implemented adaptive concretization for Sketch and evaluated it on a range of benchmarks. We found adaptive concretization is very effective, outperforming Sketch in many cases, sometimes significantly, and has good parallel scalability. |
| first_indexed | 2024-09-23T16:48:23Z |
| format | Article |
| id | mit-1721.1/111033 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T16:48:23Z |
| publishDate | 2017 |
| publisher | Springer-Verlag |
| record_format | dspace |
| spelling | mit-1721.1/1110332022-09-29T21:38:25Z Adaptive Concretization for Parallel Program Synthesis Jeon, Jinseong Foster, Jeffrey S. Qiu, Xiaokang Solar Lezama, Armando Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Qiu, Xiaokang Solar Lezama, Armando Program synthesis tools work by searching for an implementation that satisfies a given specification. Two popular search strategies are symbolic search, which reduces synthesis to a formula passed to a SAT solver, and explicit search, which uses brute force or random search to find a solution. In this paper, we propose adaptive concretization, a novel synthesis algorithm that combines the best of symbolic and explicit search. Our algorithm works by partially concretizing a randomly chosen, but likely highly influential, subset of the unknowns to be synthesized. Adaptive concretization uses an online search process to find the optimal size of the concretized subset using a combination of exponential hill climbing and binary search, employing a statistical test to determine when one degree of concretization is sufficiently better than another. Moreover, our algorithm lends itself to a highly parallel implementation, further speeding up search. We implemented adaptive concretization for Sketch and evaluated it on a range of benchmarks. We found adaptive concretization is very effective, outperforming Sketch in many cases, sometimes significantly, and has good parallel scalability. National Science Foundation (U.S.) (CCF-1139021) National Science Foundation (U.S.) (CCF-1139056) National Science Foundation (U.S.) (CCF-1161775) 2017-08-28T18:44:36Z 2017-08-28T18:44:36Z 2017-08-28 Article http://purl.org/eprint/type/ConferencePaper 978-3-319-21667-6 978-3-319-21668-3 0302-9743 1611-3349 http://hdl.handle.net/1721.1/111033 Jeon, Jinseong, et al. “Adaptive Concretization for Parallel Program Synthesis.” Lecture Notes in Computer Science (2015): 377–394. © 2015 Springer International Publishing Switzerland https://orcid.org/0000-0001-9476-7349 https://orcid.org/0000-0001-7604-8252 en_US http://dx.doi.org/10.1007/978-3-319-21668-3_22 Computer Aided Verification Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Springer-Verlag Other univ. web domain |
| spellingShingle | Jeon, Jinseong Foster, Jeffrey S. Qiu, Xiaokang Solar Lezama, Armando Adaptive Concretization for Parallel Program Synthesis |
| title | Adaptive Concretization for Parallel Program Synthesis |
| title_full | Adaptive Concretization for Parallel Program Synthesis |
| title_fullStr | Adaptive Concretization for Parallel Program Synthesis |
| title_full_unstemmed | Adaptive Concretization for Parallel Program Synthesis |
| title_short | Adaptive Concretization for Parallel Program Synthesis |
| title_sort | adaptive concretization for parallel program synthesis |
| url | http://hdl.handle.net/1721.1/111033 https://orcid.org/0000-0001-9476-7349 https://orcid.org/0000-0001-7604-8252 |
| work_keys_str_mv | AT jeonjinseong adaptiveconcretizationforparallelprogramsynthesis AT fosterjeffreys adaptiveconcretizationforparallelprogramsynthesis AT qiuxiaokang adaptiveconcretizationforparallelprogramsynthesis AT solarlezamaarmando adaptiveconcretizationforparallelprogramsynthesis |