Deriving efficient program transformations from rewrite rules
Deriving efficient program transformations from rewrite rules
复制标题
从重写规则中导出有效的程序转换
DOI：
10.1145/3473579
复制
发表时间：
2021
影响因子：
--
通讯作者：
Appel, Andrew W.
中科院分区：
文献类型：
--
作者：
Li, John M.;Appel, Andrew W.
一个高效的优化编译器可以使用辅助数据结构（如变量绑定映射、延迟替换和出现计数）在一次传递中执行多次级联重写。这种优化器通常根据相对简单的重写规则执行转换，但为了提高效率，数据结构之间的微妙交互使它们编写起来很棘手，证明正确性也很棘手。我们提出了一个系统，半自动地推导出一个有效的程序转换和它的正确性证明，从一个列表的重写规则和规范的辅助数据结构，它需要。依赖类型确保我们的系统留下的漏洞（供用户填充）被正确填充，允许用户对实现进行低级别控制，而不必担心出错。我们在Coq中实现了我们的系统（尽管它也可以在其他逻辑中实现），并使用它来编写优化通道，执行取消currying，内联，死代码消除以及case表达式和记录投影的静态评估。生成的实现有时比在一小组基准测试中的手写实现更快，最多慢40%;在某些情况下，它们需要编写和证明正确的代码要少得多。
An efficient optimizing compiler can perform many cascading rewrites in a single pass, using auxiliary data structures such as variable binding maps, delayed substitutions, and occurrence counts. Such optimizers often perform transformations according to relatively simple rewrite rules, but the subtle interactions between the data structures needed for efficiency make them tricky to write and trickier to prove correct. We present a system for semi-automatically deriving both an efficient program transformation and its correctness proof from a list of rewrite rules and specifications of the auxiliary data structures it requires. Dependent types ensure that the holes left behind by our system (for the user to fill in) are filled in correctly, allowing the user low-level control over the implementation without having to worry about getting it wrong. We implemented our system in Coq (though it could be implemented in other logics as well), and used it to write optimization passes that perform uncurrying, inlining, dead code elimination, and static evaluation of case expressions and record projections. The generated implementations are sometimes faster, and at most 40% slower, than hand-written counterparts on a small set of benchmarks; in some cases, they require significantly less code to write and prove correct.
登录
查看更多内容
Pilsner：用于高阶命令式语言的组合验证编译器
DOI：
--
发表时间：
2015
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Georg Neis;C. Hur;Jan;Craig McLaughlin;Derek Dreyer;Viktor Vafeiadis
通讯作者：
Viktor Vafeiadis
影响因子：
1.1
作者：
E. Kohlbecker;M. Wand
通讯作者：
M. Wand
Glasgow Haskell 编译器内联器的秘密
影响因子：
1.1
作者：
S. Jones;S. Marlow
通讯作者：
S. Marlow
DOI：
10.1007/978-3-642-24452-0_8
发表时间：
2011
期刊：
--
影响因子：
--
作者：
Giorgidze G
通讯作者：
Giorgidze G
Sharlit - 构建优化器的工具
影响因子：
3.3
作者：
S. Tjiang;J. Hennessy
通讯作者：
J. Hennessy