Verified Compilation of Floating-Point Computations
Verified Compilation of Floating-Point Computations
复制标题
DOI：
10.1007/s10817-014-9317-x
复制
发表时间：
2015-02-01
期刊：
影响因子：
--
通讯作者：
Melquiond, Guillaume
中科院分区：
文献类型：
--
作者：
Boldo, Sylvie;Jourdan, Jacques-Henri;Melquiond, Guillaume
众所周知，浮点运算很棘手：舍入、格式、异常值。 IEEE-754 标准推动了该领域的发展，并使浮点计算的形式推理变得更加容易和繁荣。不幸的是，这不足以保证程序的最终结果，因为还涉及其他几个参与者：编程语言、编译器和体系结构。经过正式验证的 CompCert 编译器为此问题提供了解决方案：该编译器附带了源语言（ISO C99 的一个大子集）和目标平台（ARM、PowerPC、x86-SSE2）语义的数学规范，并提供了编译保留语义的证明。在本文中，我们报告了我们最近在正式指定和证明 CompCert 浮点算术编译正确性方面所取得的成功。由于 CompCert 是使用 Coq 证明助手进行验证的，因此这项工作需要对 IEEE-754 标准进行适当的 Coq 形式化；为此，我们扩展了 Flocq 库。结果，我们获得了第一个经过正式验证的编译器，该编译器可证明保留了浮点程序的语义。
Floating-point arithmetic is known to be tricky: roundings, formats, exceptional values. The IEEE-754 standard was a push towards straightening the field and made formal reasoning about floating-point computations easier and flourishing. Unfortunately, this is not sufficient to guarantee the final result of a program, as several other actors are involved: programming language, compiler, and architecture. The CompCert formally-verified compiler provides a solution to this problem: this compiler comes with a mathematical specification of the semantics of its source language (a large subset of ISO C99) and target platforms (ARM, PowerPC, x86-SSE2), and with a proof that compilation preserves semantics. In this paper, we report on our recent success in formally specifying and proving correct CompCert's compilation of floating-point arithmetic. Since CompCert is verified using the Coq proof assistant, this effort required a suitable Coq formalization of the IEEE-754 standard; we extended the Flocq library for this purpose. As a result, we obtain the first formally verified compiler that provably preserves the semantics of floating-point programs.