论文标题
使用双精度浮点算术正式验证的32-和64位整数部门
Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic
论文作者
论文摘要
一些最近的处理器不配备整数部门。 然后，编译器通过调用处理器设计人员提供的特殊功能的呼叫来实施部门，该功能通过循环实现分区，从而产生一点点迭代的商。这会阻碍编译器的优化并导致非恒定时间计算，这在某些应用中是一个问题。 我们提倡使用处理器的浮点单元，并提出编译器可以轻松与其他计算交织的代码。我们完全证明了我们的算法的正确性，该算法使用COQ证明助手混合了浮点数和固定 - 宽度整数计算，并成功地将其集成到了CompCert正式验证的编译器中。
Some recent processors are not equipped with an integer division unit. Compilers then implement division by a call to a special function supplied by the processor designers, which implements division by a loop producing one bit of quotient per iteration. This hinders compiler optimizations and results in non-constant time computation, which is a problem in some applications. We advocate instead using the processor's floating-point unit, and propose code that the compiler can easily interleave with other computations. We fully proved the correctness of our algorithm, which mixes floating-point and fixed-bitwidth integer computations, using the Coq proof assistant and successfully integrated it into the CompCert formally verified compiler.
