{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T03:28:28Z","timestamp":1783740508719,"version":"3.55.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>Halide is a domain-specific language for high-performance image processing and tensor computations, widely adopted in industry. Internally, the Halide compiler relies on a term rewriting system to prove properties of code required for efficient and correct compilation. This rewrite system is a collection of handwritten transformation rules that incrementally rewrite expressions into simpler forms; the system requires high performance in both time and memory usage to keep compile times low, while operating over the undecidable theory of integers. In this work, we apply formal techniques to prove the correctness of existing rewrite rules and provide a guarantee of termination. Then, we build an automatic program synthesis system in order to craft new, provably correct rules from failure cases where the compiler was unable to prove properties. We identify and fix 4 incorrect rules as well as 8 rules which could give rise to infinite rewriting loops. We demonstrate that the synthesizer can produce better rules than hand-authored ones in five bug fixes, and describe four cases in which it has served as an assistant to a human compiler engineer. We further show that it can proactively improve weaknesses in the compiler by synthesizing a large number of rules without human supervision and showing that the enhanced ruleset lowers peak memory usage of compiled code without appreciably increasing compilation times.<\/jats:p>","DOI":"10.1145\/3428234","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:40:14Z","timestamp":1606261214000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Verifying and improving Halide\u2019s term rewriting system with program synthesis"],"prefix":"10.1145","volume":"4","author":[{"given":"Julie L.","family":"Newcomb","sequence":"first","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew","family":"Adams","sequence":"additional","affiliation":[{"name":"Adobe Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Steven","family":"Johnson","sequence":"additional","affiliation":[{"name":"Google, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rastislav","family":"Bodik","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shoaib","family":"Kamil","sequence":"additional","affiliation":[{"name":"Adobe Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3306346.3322967"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314641"},{"key":"e_1_2_2_3_1","volume-title":"Term rewriting and all that","author":"Baader Franz","unstructured":"Franz Baader and Tobias Nipkow . 1999. Term rewriting and all that . Cambridge university press . Franz Baader and Tobias Nipkow. 1999. Term rewriting and all that. Cambridge university press."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/128861.128862"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3102071.3102084"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_7"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_2_2_8_1","unstructured":"The Coq Development Team. 2019. The Coq Reference Manual version 8.10. Available electronically at http:\/\/coq.inria.fr\/doc.  The Coq Development Team. 2019. The Coq Reference Manual version 8.10. Available electronically at http:\/\/coq.inria.fr\/doc."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1465482.1465513"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3410227"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-52234-0_18"},{"key":"e_1_2_2_16_1","volume-title":"Automation of Reasoning","author":"Knuth Donald E","unstructured":"Donald E Knuth and Peter B Bendix . 1983. Simple word problems in universal algebras . In Automation of Reasoning . Springer , 342-376. Donald E Knuth and Peter B Bendix. 1983. Simple word problems in universal algebras. In Automation of Reasoning. Springer, 342-376."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385996"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_12"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/36177.36194"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062372"},{"key":"e_1_2_2_22_1","unstructured":"C.G. Nelson. 1980. Techniques for program verification[ Ph. D. Thesis]. ( 1980 ).  C.G. Nelson. 1980. Techniques for program verification[ Ph. D. Thesis]. ( 1980 )."},{"key":"e_1_2_2_23_1","first-page":"1","volume-title":"ACM SIGPLAN Notices","volume":"50","author":"Panchekha Pavel","year":"2015","unstructured":"Pavel Panchekha , Alex Sanchez-Stern , James R Wilcox , and Zachary Tatlock . 2015 . Automatically improving accuracy for lfoating point expressions . In ACM SIGPLAN Notices , Vol. 50 . ACM, 1 - 11 . Pavel Panchekha, Alex Sanchez-Stern, James R Wilcox, and Zachary Tatlock. 2015. Automatically improving accuracy for lfoating point expressions. In ACM SIGPLAN Notices, Vol. 50. ACM, 1-11."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_2_2_26_1","volume-title":"Formal Semantics for the Halide Language. Master's thesis","author":"Reinking Alex","unstructured":"Alex Reinking . 2019. Formal Semantics for the Halide Language. Master's thesis . University of California at Berkeley . Alex Reinking. 2019. Formal Semantics for the Halide Language. Master's thesis. University of California at Berkeley."},{"key":"e_1_2_2_27_1","volume-title":"Souper: A Synthesizing Superoptimizer. arXiv: 1711.04422 [cs.PL]","author":"Sasnauskas Raimondas","year":"2017","unstructured":"Raimondas Sasnauskas , Yang Chen , Peter Collingbourne , Jeroen Ketema , Gratian Lup , Jubi Taneja , and John Regehr . 2017 a. Souper: A Synthesizing Superoptimizer. arXiv: 1711.04422 [cs.PL] Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Gratian Lup, Jubi Taneja, and John Regehr. 2017a. Souper: A Synthesizing Superoptimizer. arXiv: 1711.04422 [cs.PL]"},{"key":"e_1_2_2_28_1","volume-title":"Souper: A Synthesizing Superoptimizer. CoRR abs\/1711.04422 ( 2017 ). arXiv: 1711.04422 http:\/\/arxiv.org\/abs\/1711.04422","author":"Sasnauskas Raimondas","year":"2017","unstructured":"Raimondas Sasnauskas , Yang Chen , Peter Collingbourne , Jeroen Ketema , Jubi Taneja , and John Regehr . 2017 b. Souper: A Synthesizing Superoptimizer. CoRR abs\/1711.04422 ( 2017 ). arXiv: 1711.04422 http:\/\/arxiv.org\/abs\/1711.04422 Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Jubi Taneja, and John Regehr. 2017b. Souper: A Synthesizing Superoptimizer. CoRR abs\/1711.04422 ( 2017 ). arXiv: 1711.04422 http:\/\/arxiv.org\/abs\/1711.04422"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_2_2_30_1","first-page":"185","article-title":"SWAPPER: A framework for automatic generation of formula simplifiers based on conditional rewrite rules. In 2016 Formal Methods in Computer-Aided Design (FMCAD)","author":"Singh Rohit","year":"2016","unstructured":"Rohit Singh and Armando Solar-Lezama . 2016 . SWAPPER: A framework for automatic generation of formula simplifiers based on conditional rewrite rules. In 2016 Formal Methods in Computer-Aided Design (FMCAD) . IEEE , 185 - 192 . Rohit Singh and Armando Solar-Lezama. 2016. SWAPPER: A framework for automatic generation of formula simplifiers based on conditional rewrite rules. In 2016 Formal Methods in Computer-Aided Design (FMCAD). IEEE, 185-192.","journal-title":"IEEE"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_3"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Emina Torlak and Rastislav Bodik. 2014. A lightweight symbolic virtual machine for solver-aided host languages. ACM SIGPLAN Notices 49 6 ( 2014 ) 530-541.  Emina Torlak and Rastislav Bodik. 2014. A lightweight symbolic virtual machine for solver-aided host languages. ACM SIGPLAN Notices 49 6 ( 2014 ) 530-541.","DOI":"10.1145\/2666356.2594340"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428234","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428234","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428234"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":32,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428234"],"URL":"https:\/\/doi.org\/10.1145\/3428234","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}