[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: round32 ( round64 ( X ) ) ?= round32 ( X )



This is the infamous "double rounding" problem with round-to-nearest
with ties broken by rounding to even. It is especially a problem for x86
using the x87 registers, since the operations are performed in 80-bit
arithmetic (thus incurring rounding to "extended precision") and then
data is saved to memory generally in 64-bit (thus incurring rounding
from double precision to "extended precision").

This problem may result in various inconsistencies (on one occasion,
somebody emailed the developers of the Objective Caml language alleging
there was a bug in OCaml, because of inconsistencies in results between
programs compiled as bytecode and native code, which could be traced to
double rounding on one of the implementations).

In addition to David Golberg's article, may I make a shameless plug for
my own article

Article{Monniaux_TOPLAS08,
  author =       {David Monniaux},
  title =        {The pitfalls of verifying floating-point
                  computations},
  journal =      {TOPLAS},
  fjournal =     {ACM Transactions on programming languages and systems},
  year =         2008,
  month = may,
  publisher =    {ACM},
  fpublisher =   {Association for Computing Machinery},
  issn =         {0164-0925},
  volume =       30,
  number =       3,
  pages =        12
}

-- 
David Monniaux, chargé de recherche au CNRS, laboratoire VERIMAG
http://www-verimag.imag.fr/~monniaux/


754 | revision | FAQ | references | list archive