Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic
Logic in Computer Science
2022-07-19 v1
Abstract
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.
Keywords
Cite
@article{arxiv.2207.08420,
title = {Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic},
author = {David Monniaux and Alice Pain},
journal= {arXiv preprint arXiv:2207.08420},
year = {2022}
}