{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:11:24Z","timestamp":1784200284644,"version":"3.55.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62032023,T2125013,62172391"],"award-info":[{"award-number":["62032023,T2125013,62172391"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>We introduce Stencil-Lifting, a novel system for automatically converting stencil kernels written in low-level languages within legacy code into semantically equivalent Domain-Specific Language (DSL) implementations. Targeting the efficiency bottlenecks of existing verified lifting systems, Stencil-Lifting achieves scalable stencil kernel abstraction through two key innovations. First, we propose a hierarchical recursive lifting theory that represents stencil kernels, structured as nested loops, using invariant subgraphs, which are customized data dependency graphs capturing loop-carried computations and structural invariants. Each vertex in the invariant subgraph is associated with a predicate-based summary that encodes its computational semantics. Enforcing self-consistency across these summaries enables a derivation of correct loop invariants and postconditions, without the need for external verification. Second, we design a hierarchical recursive lifting algorithm that guarantees termination through a convergent recursive process, avoiding the inefficiencies of search-based synthesis while efficiently deriving valid summaries with formally proven completeness. We evaluate Stencil-Lifting on diverse stencil benchmarks from real-world applications. Experiment results demonstrate that Stencil-Lifting achieves 31.6\u00d7 and 5.8\u00d7 speedups compared to the state-of-the-art verified lifting systems STNG and Dexter, respectively. Our work significantly improves the efficiency of translating stencil kernels into DSL implementations, effectively bridging the gap between legacy code and modern DSL-based paradigms.<\/jats:p>","DOI":"10.1145\/3763159","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"3037-3064","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4266-908X","authenticated-orcid":false,"given":"Mingyi","family":"Li","sequence":"first","affiliation":[{"name":"Institute of Computing Technology, Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0457-4709","authenticated-orcid":false,"given":"Junmin","family":"Xiao","sequence":"additional","affiliation":[{"name":"Institute of Computing Technology, Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-3778-5995","authenticated-orcid":false,"given":"Siyan","family":"Chen","sequence":"additional","affiliation":[{"name":"Institute of Computing Technology, Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7083-9552","authenticated-orcid":false,"given":"Hui","family":"Ma","sequence":"additional","affiliation":[{"name":"Institute of Computing Technology, Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-4571-0213","authenticated-orcid":false,"given":"Xi","family":"Chen","sequence":"additional","affiliation":[{"name":"Institute of Computing Technology, Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-7264-9102","authenticated-orcid":false,"given":"Peihua","family":"Bao","sequence":"additional","affiliation":[{"name":"University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3406-2907","authenticated-orcid":false,"given":"Liang","family":"Yuan","sequence":"additional","affiliation":[{"name":"Institute of Computing Technology, Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6361-5948","authenticated-orcid":false,"given":"Guangming","family":"Tan","sequence":"additional","affiliation":[{"name":"Institute of Computing Technology, Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3196891"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3355089.3356549"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","unstructured":"Rajeev Alur Rastislav Bodik Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design (FMCAD 2013). 1\u201317. doi:10.1109\/FMCAD.2013.6679385","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628071.2628092"},{"key":"e_1_3_2_6_1","volume-title":"The Landscape of Parallel Computing Research: A View from Berkeley","author":"Asanovic Krste","year":"2006","unstructured":"Krste Asanovic, Ras Bodik, Bryan Catanzaro, Joseph Gebis, Parry Husbands, Kurt Keutzer, David Patterson, William Plishker, John Shalf, Samuel Williams, and Katherine Yelick. 2006. The Landscape of Parallel Computing Research: A View from Berkeley. EECS Department, University of California, Berkeley EECS-2006-183 (12 2006)."},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1562764.1562783"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Riyadh Baghdadi Jessica Ray Malek Ben Romdhane Emanuele Del Sozzo Abdurrahman Akkas Yunming Zhang Patricia Suriana Shoaib Kamil and Saman Amarasinghe. 2019. Tiramisu: A Polyhedral Compiler for Expressing Fast and Portable Code. In 2019 IEEE\/ACM International Symposium on Code Generation and Optimization (CGO). 193\u2013205. doi:10.1109\/CGO.2019.8661197","DOI":"10.1109\/CGO.2019.8661197"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/125826.125925"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477314.3507042"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","unstructured":"Nick Brown Brandon Echols Justs Zarins and Tobias Grosser. 2022. TensorFlow as a DSL for stencil-based computation on the Cerebras Wafer Scale Engine. doi:10.48550\/ARXIV.2210.04795","DOI":"10.48550\/ARXIV.2210.04795"},{"key":"e_1_3_2_13_1","unstructured":"Bryan Catanzaro Shoaib Ashraf Kamil Yunsup Lee Krste Asanovi\u0107 James Demmel Kurt Keutzer John Shalf Katherine A. Yelick and Armando Fox. 2010. SEJITS: Getting Productivity and Performance With Selective Embedded JIT Specialization. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2010\/EECS-2010-23.html"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462180"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","unstructured":"Paul Stewart Crozier Heidi K Thornquist Robert W Numrich Alan B Williams Harold Carter Edwards Eric Richard Keiter Mahesh Rajan James M Willenbring Douglas W Doerfler and Michael Allen Heroux. 2009. Improving performance via mini-applications. In Technical report. doi:10.2172\/993908","DOI":"10.2172\/993908"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/2553197"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571283"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3173182"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","unstructured":"Tobias Gysi Carlos Osuna Oliver Fuhrer Mauro Bianco and Thomas C. Schulthess. 2015. STELLA: a domain-specific tool for structured grid methods in weather and climate models. In SC \u201915: Proceedings of the International Conference for High Performance Computing Networking Storage and Analysis. 1\u201312. doi:10.1145\/2807591.2807627","DOI":"10.1145\/2807591.2807627"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_23_1","unstructured":"Shoaib Kamil. 2013. A cross-domain stencil benchmark suite. In In Workshop on Optimizing Stencil Computations."},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908117"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/WOLFHPC.2016.06"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563336"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","unstructured":"Hanyu Li Haijing Zhou Yang Liu Xianfeng Bao and Zhenguo Zhao. 2014. Massively parallel FDTD program JEMS-FDTD and its applications in platform coupling simulation. In 2014 International Symposium on Electromagnetic Compatibility. 229\u2013233. doi:10.1109\/EMCEurope.2014.6930908","DOI":"10.1109\/EMCEurope.2014.6930908"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Mingyi Li Junmin Xiao Siyan Chen Hui Ma Xi Chen Peihua Bao Liang Yuan and Guangming Tan. 2025. Reproduction Package for Article \u2018Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes\u2019. doi:10.5281\/zenodo.16924672","DOI":"10.5281\/zenodo.16924672"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3524059.3532392"},{"key":"e_1_3_2_30_1","unstructured":"Andrew Mallinson David A Beckingsale Wayne Gaudin J Herdman John Levesque and Stephen A Jarvis. 2013. Cloverleaf: Preparing hydrodynamics codes for exascale. The Cray User Group 2013."},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2063384.2063398"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737974"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","unstructured":"William S. Moses Lorenzo Chelini Ruizhe Zhao and Oleksandr Zinenko. 2021. Polygeist: Raising C to Polyhedral MLIR. In 2021 30th International Conference on Parallel Architectures and Compilation Techniques (PACT). 45\u201359. doi:10.1109\/PACT52795.2021.00011","DOI":"10.1109\/PACT52795.2021.00011"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2404.18249"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462176"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0898-1221(81)90008-0"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","unstructured":"Gagandeep Singh Dionysios Diamantopoulos Christoph Hagleitner Juan Gomez-Luna Sander Stuijk Onur Mutlu and Henk Corporaal. 2020. NERO: A Near High-Bandwidth Memory Stencil Accelerator for Weather Prediction Modeling. In 2020 30th International Conference on Field-Programmable Logic and Applications (FPL). 9\u201317. doi:10.1109\/FPL50879.2020.00014","DOI":"10.1109\/FPL50879.2020.00014"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_3"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250754"},{"key":"e_1_3_2_40_1","unstructured":"Stencil Probe. 2025. StencilProbe: A Microbenchmark for Stencil Applications. https:\/\/people.csail.mit.edu\/skamil\/projects\/stencilprobe\/"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1989493.1989508"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO57630.2024.10444879"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523702"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","unstructured":"Christoph M. Wintersteiger Youssef Hamadi and Leonardo de Moura. 2010. Efficiently solving quantified bit-vector formulas. In Formal Methods in Computer Aided Design. 239\u2013246. doi:10.1007\/s10703-012-0156-2","DOI":"10.1007\/s10703-012-0156-2"},{"key":"e_1_3_2_45_1","unstructured":"WRF. 2022. WRF Model site. https:\/\/www.mmm.ucar.edu\/models\/wrf"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950340"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771815"},{"key":"e_1_3_2_48_1","unstructured":"Kai Zhu Chenkai Guo Kuihao Yan Xiaoqi Jia Haichao Du Qingjia Huang Yamin Xie and Jing Tang. 2024. LoopSCC: Towards Summarizing Multi-branch Loops within Determinate Cycles. (2024). https:\/\/arxiv.org\/abs\/2411.02863"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763159","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:15:39Z","timestamp":1784196939000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763159"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":47,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763159"],"URL":"https:\/\/doi.org\/10.1145\/3763159","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}