Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code
Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code
复制标题
性能关键型应用程序的关系编译：将功能模型转换为低级代码的可扩展证明生成
DOI：
10.1145/3519939.3523706
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Chlipala, Adam
中科院分区：
文献类型：
--
作者：
Pit-Claudel, Clément;Philipoom, Jade;Jamner, Dustin;Erbsen, Andres;Chlipala, Adam
通常有两种方法可以编译和运行使用交互式定理证明器（ITP）验证的纯函数式程序：自动将其提取到类似的语言（通常是未经验证的过程，如Coq到OCaml），或者手动证明它等同于较低级别的重新实现（如C程序）。传统上，只有后者才能同时产生出色的性能和端到端证明。本文展示了如何将程序提取转换为一个证明搜索问题，从而从纯功能程序中自动导出构造正确的高性能代码。我们称这种思想为关系编译——它扩展了最近的发展，为循环不变推理和各种副作用的泛型提供了新的解决方案。关键是，关系编译器是不完整的，与传统编译器不同，它们生成好的代码不是因为一组固定的聪明的内置优化，而是因为它们允许专家插入特定领域的扩展，使他们能够完全控制编译器的输出。我们用Rupicola演示了这种方法的好处，Rupicola是一种新的编译器构建工具包，用于从带注释的功能模型中提取快速、经过验证、惯用的低级代码。通过案例研究和性能基准测试，我们证明了它可以用最少的努力进行扩展，并且可以达到与手写C程序相当的性能。
There are typically two ways to compile and run a purely functional program verified using an interactive theorem prover (ITP): automatically extracting it to a similar language (typically an unverified process, like Coq to OCaml) or manually proving it equivalent to a lower-level reimplementation (like a C program). Traditionally, only the latter produced both excellent performance and end-to-end proofs.This paper shows how to recast program extraction as a proof-search problem to automatically derive correct-by-construction, high-performance code from purely functional programs. We call this idea relational compilation — it extends recent developments with novel solutions to loop-invariant inference and genericity in kinds of side effects.Crucially, relational compilers are incomplete, and unlike traditional compilers, they generate good code not because of a fixed set of clever built-in optimizations but because they allow experts to plug in domain--specific extensions that give them complete control over the compiler's output.We demonstrate the benefits of this approach with Rupicola, a new compiler-construction toolkit designed to extract fast, verified, idiomatic low-level code from annotated functional models. Using case studies and performance benchmarks, we show that it is extensible with minimal effort and that it achieves performance on par with that of handwritten C programs.
登录
查看更多内容
Perceus：具有重用性的无垃圾引用计数
DOI：
10.1145/3453483.3454032
发表时间：
2020
期刊：
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Alex Reinking;Ningning Xie;L. de Moura;Daan Leijen
通讯作者：
Daan Leijen
用高级语言设计高效系统的类型安全元编程和编译技术
DOI：
10.1145/1040305.1040335
发表时间：
2020
影响因子：
11.1
作者：
L. Parreaux
通讯作者：
L. Parreaux
从重写规则中导出有效的程序转换
影响因子：
--
作者：
Li, John M.;Appel, Andrew W.
通讯作者：
Appel, Andrew W.
影响因子：
--
作者：
Watanabe, Yasunari;Gopinathan, Kiran;Pîrlea, George;Polikarpova, Nadia;Sergey, Ilya
通讯作者：
Sergey, Ilya
非确定性术语重写系统的编译器
DOI：
10.1007/3-540-61464-8_50
发表时间：
1996
期刊：
J. Symb. Comput.
影响因子：
--
作者：
M. Vittek
通讯作者：
M. Vittek