CITATION — REFERENCE ENTRY
Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes — Proceedings of the ACM on Programming Languages
- Key
- li2025stencil
- Authors
- Li, Mingyi; Xiao, Junmin; Chen, Siyan; Ma, Hui; Chen, Xi; Bao, Peihua; Yuan, Liang; Tan, Guangming
- Issued
- 2025-10
- Type
- article-journal
- Container
- Proceedings of the ACM on Programming Languages
- Volume
- 9
- Issue
- OOPSLA2
- DOI
- 10.1145/3763159
Raw CSL JSON
{
"DOI": "10.1145/3763159",
"URL": "https://dl.acm.org/doi/10.1145/3763159",
"type": "article-journal",
"issue": "OOPSLA2",
"title": "Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes",
"author": [
{
"given": "Mingyi",
"family": "Li"
},
{
"given": "Junmin",
"family": "Xiao"
},
{
"given": "Siyan",
"family": "Chen"
},
{
"given": "Hui",
"family": "Ma"
},
{
"given": "Xi",
"family": "Chen"
},
{
"given": "Peihua",
"family": "Bao"
},
{
"given": "Liang",
"family": "Yuan"
},
{
"given": "Guangming",
"family": "Tan"
}
],
"issued": {
"date-parts": [
[
2025,
10
]
]
},
"volume": "9",
"container-title": "Proceedings of the ACM on Programming Languages"
}
Claims
-
Syntax-guided pattern matching for code conversion relies on syntax rules and struggles with limited pattern coverage and a lack of semantic guarantees, in contrast to verified lifting which uses synthesis to derive a formally verified summary.
"Pattern matching relies on syntax rules to convert code into DSLs, but struggles with limited pattern coverage and a lack of semantic guarantees. In contrast, verified lifting uses synthesis to derive a formally verified summary."
-
Search-based verified lifting (as used in STNG and Dexter) can fail to find valid summaries within bounded time; Stencil-Lifting replaces this with a hierarchical recursive algorithm that guarantees termination through a convergent recursive process.
"its reliance on search-based strategies means that valid summaries may not always be found within a bounded time"
-
Stencil-Lifting achieves 31.62× and 5.8× speedups compared to prior verified lifting systems STNG and Dexter respectively, while maintaining full semantic equivalence.
"Stencil-Lifting achieves 31.62× and 5.8× speedups compared to the state-of-the-art verified lifting systems STNG and Dexter, respectively, while maintaining full semantic equivalence."
Available in