The pitfalls of verifying floating-point computations

by syoyo

The pitfalls of verifying floating-point computations
David Monniaux


This is a good article about floating point computation, especially problematic behaviour of x87.
(double-rounding, extended exponent bits, etc…)

Although x87’s extended precision(80bits) is a part of IEEE 754 standard,
this article tells us that we must not use x87 and must use SSE2 as a FPU.

Now days, there are alot of SSE2 capable x86 CPUs(Pentium4 or later) and
gcc uses SSE2 as a FPU on x86_64 environment by default.
Thus we are going to have no scruples about using SSE2 as FPU.


CRlibm [1] のマニュアルのすごさ(誤差を抑える計算のテクニック)に影響されて、

いくつか調べた中でも、The pitfalls of verifying floating-point computations は例題がいろいろと
取り上げられてまとまっていて役に立ちます(とくに x87 のひどさについて)。

クロスプラットフォームを考えて、IEEE 754 準拠の他 CPU との浮動小数点計算と
結果を合わせるためにも、SSE2 を使い、x87 は使わないようにしましょう.

CRlibm, an efficient and proven correctly-rounded mathematical library