The pitfalls of verifying floating-point computations

by syoyo

The pitfalls of verifying floating-point computations
David Monniaux
http://hal.archives-ouvertes.fr/hal-00128124

[En]

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.

[Ja]

CRlibm [1] のマニュアルのすごさ(誤差を抑える計算のテクニック)に影響されて、
浮動小数点計算をいろいろと調べています。

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

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

[1] http://lipforge.ens-lyon.fr/www/crlibm/index.html
CRlibm, an efficient and proven correctly-rounded mathematical library

Advertisements