Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911154945654784 |
|---|---|
| author | Li, Mingyi Xiao, Junmin Chen, Siyan Ma, Hui Chen, Xi Bao, Peihua Yuan, Liang Tan, Guangming |
| author_facet | Li, Mingyi Xiao, Junmin Chen, Siyan Ma, Hui Chen, Xi Bao, Peihua Yuan, Liang Tan, Guangming |
| contents | We introduce Stencil-Lifting, a novel system for automatically converting stencil kernels written in low-level languages in 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 that capture loop-carried computation and structural invariants. Each vertex in the invariant subgraph is associated with a predicate-based summary, encoding its computational semantics. By enforcing self-consistency across these summaries, Stencil-Lifting ensures the derivation of correct loop invariants and postconditions for nested loops, eliminating the need for external verification. Second, we develop a hierarchical recursive lifting algorithm that guarantees termination through a convergent recursive process, avoiding the inefficiencies of search-based synthesis. The algorithm efficiently derives the valid summaries of stencil kernels, and its completeness is formally proven. We evaluate Stencil-Lifting on diverse stencil benchmarks from two different suites and on four real-world applications. Experimental results demonstrate that Stencil-Lifting achieves 31.62$\times$ and 5.8$\times$ speedups compared to the state-of-the-art verified lifting systems STNG and Dexter, respectively, while maintaining full semantic equivalence. Our work significantly enhances the translation efficiency of low-level stencil kernels to DSL implementations, effectively bridging the gap between legacy optimization techniques and modern DSL-based paradigms. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_10236 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes Li, Mingyi Xiao, Junmin Chen, Siyan Ma, Hui Chen, Xi Bao, Peihua Yuan, Liang Tan, Guangming Software Engineering Performance Programming Languages We introduce Stencil-Lifting, a novel system for automatically converting stencil kernels written in low-level languages in 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 that capture loop-carried computation and structural invariants. Each vertex in the invariant subgraph is associated with a predicate-based summary, encoding its computational semantics. By enforcing self-consistency across these summaries, Stencil-Lifting ensures the derivation of correct loop invariants and postconditions for nested loops, eliminating the need for external verification. Second, we develop a hierarchical recursive lifting algorithm that guarantees termination through a convergent recursive process, avoiding the inefficiencies of search-based synthesis. The algorithm efficiently derives the valid summaries of stencil kernels, and its completeness is formally proven. We evaluate Stencil-Lifting on diverse stencil benchmarks from two different suites and on four real-world applications. Experimental results demonstrate that Stencil-Lifting achieves 31.62$\times$ and 5.8$\times$ speedups compared to the state-of-the-art verified lifting systems STNG and Dexter, respectively, while maintaining full semantic equivalence. Our work significantly enhances the translation efficiency of low-level stencil kernels to DSL implementations, effectively bridging the gap between legacy optimization techniques and modern DSL-based paradigms. |
| title | Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes |
| topic | Software Engineering Performance Programming Languages |
| url | https://arxiv.org/abs/2509.10236 |