Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact)
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact)
复制标题
CakeML 中浮点程序的经过验证的编译和优化（Artifact）
DOI：
10.4230/darts.8.2.10
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
A. Fox
中科院分区：
文献类型：
--
作者：
Heiko Becker;R. Rabe;Eva Darulova;Magnus O. Myreen;Zachary Tatlock;Ramana Kumar;Yong Kiam Tan;A. Fox
经过验证的编译器（例如 CompCert 和 CakeML）在过去几年中变得越来越现实，但迄今为止它们对浮点运算的支持仍然有限。特别是，它们缺乏未经验证的主流编译器执行的“快速数学式”优化。在经过验证的编译器设置中支持此类优化具有挑战性，因为这些优化在大多数情况下不会保留 IEEE-754 浮点语义。然而，IEEE-754 浮点数是实数的有限近似，我们认为快速数学优化的任何编译器正确性结果都应该诉诸实值语义，而不是严格的 IEEE-754 浮点数。本文介绍了 RealCake，它是 CakeML 的扩展，可实现浮点算术的快速数学式优化编译的端到端正确性结果。这一结果是通过为 CakeML 提供灵活的浮点语义并集成外部证明生成准确性分析来实现的。 RealCake 的端到端定理将实数语义下原始源程序的 I/O 行为与编译器生成和快速数学优化的机器代码的可观察 I/O 行为联系起来。
Verified compilers such as CompCert and CakeML have become increasingly realistic over the last few years, but their support for floating-point arithmetic has thus far been limited. In particular, they lack the “fast-math-style” optimizations that unverified mainstream compilers perform. Supporting such optimizations in the setting of verified compilers is challenging because these optimizations, for the most part, do not preserve the IEEE-754 floating-point semantics. However, IEEE-754 floating-point numbers are finite approximations of the real numbers, and we argue that any compiler correctness result for fast-math optimizations should appeal to a real-valued semantics rather than the rigid IEEE-754 floating-point numbers. This paper presents RealCake, an extension of CakeML that achieves end-to-end correctness results for fast-math-style optimized compilation of floating-point arithmetic. This result is achieved by giving CakeML a flexible floating-point semantics and integrating an external proof-producing accuracy analysis. RealCake’s end-to-end theorems relate the I/O behavior of the original source program under real-number semantics to the observable I/O behavior of the compiler generated and fast-math-optimized machine code.
影响因子：
2.1
作者：
通讯作者：
--