{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T02:21:31Z","timestamp":1785291691999,"version":"3.55.0"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    Using program synthesis to select instructions for and optimize input programs is receiving increasing attention. However, existing synthesis-based compilers are faced by two major challenges that prohibit the deployment of program synthesis in production compilers: exorbitantly long synthesis times spanning several minutes and hours; and scalability issues that prevent synthesis of complex modern compute and data swizzle instructions, which have been found to maximize performance of modern tensor and stencil workloads. This paper proposes\n                    <jats:sc>Misaal<\/jats:sc>\n                    , a synthesis-based compiler that employs a novel strategy to use formal semantics of hardware instructions to automatically prune a large search space of rewrite rules for modern complex instructions in an offline stage.\n                    <jats:sc>Misaal<\/jats:sc>\n                    also proposes a novel methodology to make term-rewriting process in the online stage (at compile-time) extremely lightweight so as to enable programs to compile in seconds. Our results show that\n                    <jats:sc>Misaal<\/jats:sc>\n                    reduces compilation times by up to a geomean of 16x compared to the state-of-theart synthesis-based compiler,\n                    <jats:sc>Hydride<\/jats:sc>\n                    .\n                    <jats:sc>Misaal<\/jats:sc>\n                    also delivers competitive runtime performance against the production compiler for image processing and deep learning workloads, Halide, as well as\n                    <jats:sc>Hydride<\/jats:sc>\n                    across x86, Hexagon and ARM.\n                  <\/jats:p>","DOI":"10.1145\/3729301","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1269-1292","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["MISAAL: Synthesis-Based Automatic Generation of Efficient and Retargetable Semantics-Driven Optimizations"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9979-3252","authenticated-orcid":false,"given":"Abdul Rafae","family":"Noor","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-8557-8770","authenticated-orcid":false,"given":"Dhruv","family":"Baronia","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4023-1175","authenticated-orcid":false,"given":"Akash","family":"Kothari","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-3381-2190","authenticated-orcid":false,"given":"Muchen","family":"Xu","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8140-2321","authenticated-orcid":false,"given":"Charith","family":"Mendis","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0760-9690","authenticated-orcid":false,"given":"Vikram S.","family":"Adve","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"crossref","unstructured":"Maaz Bin Safeer Ahmad Alexander J Root Andrew Adams Shoaib Kamil and Alvin Cheung. 2022. Vector instruction selection for digital signal processors using program synthesis. In Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. 1004\u20131016.","DOI":"10.1145\/3503222.3507714"},{"key":"e_1_3_2_3_2","unstructured":"Akash Kothari. [n.d.]. Hydride. https:\/\/github.com\/akothen\/Hydride."},{"key":"e_1_3_2_4_2","unstructured":"Arm. 2024. Neon. https:\/\/developer.arm.com\/Architectures\/Neon."},{"key":"e_1_3_2_5_2","unstructured":"Tianqi Chen Thierry Moreau Ziheng Jiang Lianmin Zheng Eddie Yan Haichen Shen Meghan Cowan Leyuan Wang Yuwei Hu Luis Ceze et al. 2018. TVM: An automated end-to-end optimizing compiler for deep learning. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201918). 578\u2013594."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/HOTCHIPS.2015.7477329"},{"key":"e_1_3_2_7_2","doi-asserted-by":"crossref","unstructured":"Meghan Cowan Deeksha Dangwal Armin Alaghi Caroline Trippel Vincent T Lee and Brandon Reagen. 2021. Porcupine: A synthesizing compiler for vectorized homomorphic encryption. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 375\u2013389.","DOI":"10.1145\/3453483.3454050"},{"key":"e_1_3_2_8_2","unstructured":"Halide. [n. d.]. Halide. https:\/\/github.com\/halide\/Halide."},{"key":"e_1_3_2_9_2","unstructured":"Intel. 2019. Intel Deep Learning Boost. https:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/product-overviews\/dl-boost-product-overview.pdf."},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","unstructured":"Akash Kothari Abdul Rafae Noor Muchen Xu Hassam Uddin Dhruv Baronia Stefanos Baziotis Vikram Adve Charith Mendis and Sudipta Sengupta. 2024. Hydride: A Retargetable and Extensible Synthesis-based Compiler for Modern Hardware Architectures. In Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems Volume 2. 514\u2013529.","DOI":"10.1145\/3620665.3640385"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Chris Lattner Mehdi Amini Uday Bondhugula Albert Cohen Andy Davis Jacques Pienaar River Riddle Tatiana Shpeisman Nicolas Vasilache and Oleksandr Zinenko. 2021. MLIR: Scaling Compiler Infrastructure for Domain Specific Computation. In 2021 IEEE\/ACM International Symposium on Code Generation and Optimization (CGO). 2\u201314. https:\/\/doi.org\/10.1109\/CGO51591.2021.9370308 10.1109\/CGO51591.2021.9370308","DOI":"10.1109\/CGO51591.2021.9370308"},{"key":"e_1_3_2_12_2","unstructured":"Maaz Ahmad Hongpu Ray Gong Andrew Adams. [n. d.]. Rake. https:\/\/github.com\/uwplse\/rake\/tree\/hvx-artifact."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622834"},{"key":"e_1_3_2_14_2","unstructured":"Qualcomm. 2020. Exploring the AI capabilities of the Qualcomm Snapdragon 888 Mobile Platform [video]. https:\/\/www.qualcomm.com\/news\/onq\/2020\/12\/02\/exploring-ai-capabilities-qualcomm-snapdragon-888-mobile-platform."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462176"},{"key":"e_1_3_2_16_2","doi-asserted-by":"crossref","unstructured":"Alexander J Root Maaz Bin Safeer Ahmad Dillon Sharlet Andrew Adams Shoaib Kamil and Jonathan Ragan-Kelley. 2023. Fast Instruction Selection for Fast Digital Signal Processing. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems Volume 4. 125\u2013137.","DOI":"10.1145\/3623278.3624768"},{"key":"e_1_3_2_17_2","doi-asserted-by":"crossref","unstructured":"Ross Tate Michael Stepp Zachary Tatlock and Sorin Lerner. 2009. Equality saturation: a new approach to optimization. In Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 264\u2013276.","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_2_18_2","doi-asserted-by":"crossref","unstructured":"Samuel Thomas and James Bornholt. 2024. Automatic Generation of Vectorizing Compilers for Customizable Digital Signal Processors. In Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems Volume 1. 19\u201334.","DOI":"10.1145\/3617232.3624873"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","unstructured":"Alexa VanHattum Rachit Nigam Vincent T Lee James Bornholt and Adrian Sampson. 2021. Vectorization for digital signal processors via equality saturation. In Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. 874\u2013886.","DOI":"10.1145\/3445814.3446707"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591239"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729301","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:02:32Z","timestamp":1784196152000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729301"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":20,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729301"],"URL":"https:\/\/doi.org\/10.1145\/3729301","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}