一句话：提出层次化递归提升系统 Stencil-Lifting，自动将遗留代码中的 stencil 核转换为语义等价的 DSL 实现。
论文面向遗留代码中低层语言编写的 stencil 核难以迁移到现代 DSL 的问题，提出自动转换系统 Stencil-Lifting。针对已有验证提升（verified lifting）系统效率低、依赖搜索式合成的瓶颈，作者提出两项创新：其一，层次化递归提升理论，将嵌套循环结构的 stencil 核表示为不变子图（invariant subgraph）——一种刻画循环携带计算与结构不变式的定制数据依赖图，每个顶点附带基于谓词的摘要以编码其计算语义；通过强制这些摘要之间的自一致性，无需外部验证即可推导正确的循环不变式与后置条件。其二，设计层次化递归提升算法，通过收敛的递归过程保证终止，避免搜索式合成的低效，并形式化证明其完备性。作者在来自真实应用的多类 stencil 基准上评估系统，结果显示相比最先进的验证提升系统 STNG 和 Dexter 分别取得 31.6 倍与 5.8 倍的加速，显著提升了 stencil 核向 DSL 实现转换的效率，弥合了遗留代码与现代 DSL 范式之间的鸿沟。
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× and 5.8× 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.
@article{paperbot2957,
title = {Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes},
author = {Mingyi Li and Junmin Xiao and Siyan Chen and Hui Ma and Xi Chen and Peihua Bao and Liang Yuan and Guangming Tan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763159}
}