Stencil-Lifting：用于提取遗留代码中 Stencil Kernel 摘要的分层递归提升系统

我们介绍了 Stencil-Lifting，这是一种新颖的系统，用于将遗留代码中用低级语言编写的 stencil kernel 自动转换为语义等价的领域特定语言（DSL）实现。针对现有已验证提升系统的效率瓶颈，Stencil-Lifting 通过两项关键创新实现了可扩展的 stencil kernel 抽象。首先，我们提出了一种分层递归提升理论，该理论使用不变子图来表示由嵌套循环构成的 stencil kernel，其中不变子图是定制的、捕获循环携带计算和结构不变性的数据依赖图。不变子图中的每个顶点都与一个基于谓词的摘要相关联，编码其计算语义。通过在这些摘要之间强制执行自洽性，Stencil-Lifting 确保了嵌套循环的正确循环不变量和后置条件的推导，从而无需外部验证。其次，我们开发了一种分层递归提升算法，该算法通过收敛递归过程保证终止，避免了基于搜索的综合方法的低效性。该算法能高效地推导出 stencil kernel 的有效摘要，并且其完备性得到了形式化证明。我们在来自两个不同套件的各种 stencil 基准测试和四个实际应用上评估了 Stencil-Lifting。实验结果表明，与最先进的已验证提升系统 STNG 和 Dexter 相比，Stencil-Lifting 分别实现了 31.62$\times$ 和 5.8$\times$ 的加速，同时保持了完全的语义等价性。我们的工作显著提高了低级 stencil kernel 到 DSL 实现的转换效率，有效地弥合了遗留优化技术与现代基于 DSL 的范式之间的差距。