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

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

Peter Lawrence asks about the infamous problem of double rounding on
systems with long internal registers (Honeywell mainframes of 1970s,
Motorola 68K, and current Intel x86 and x86_64 families).

Double rounding is indeed a nuisance, and there is a surprising recent
discovery that it could have been prevented if there were an unusual
rounding mode, round-to-odd (RO(x)).  The authors of the paper below
show how to implement that rounding in software, and discuss how it
can be used to fix the double-rounding problem.

It is too late now to repair the mistakes of the past that are present
in millions of installed systems, but it is good to know that careful
research before designing hardware can be helpful.

@String{j-IEEE-TRANS-COMPUT     = "IEEE Transactions on Computers"}

  author =       "Sylvie Boldo and Guillaume Melquiond",
  title =        "Emulation of a {FMA} and Correctly Rounded Sums:
                 Proved Algorithms Using Rounding to Odd",
  journal =      j-IEEE-TRANS-COMPUT,
  volume =       "54",
  number =       "4",
  pages =        "462--471",
  month =        apr,
  year =         "2008",
  CODEN =        "ITCOB4",
  DOI =          "http://dx.doi.org/10.1109/TC.2007.70819";,
  ISSN =         "0018-9340",
  bibdate =      "Sat Feb 19 18:44:18 2011",
  abstract =     "Rounding to odd is a nonstandard rounding on
                 floating-point numbers. By using it for some
                 intermediate values instead of rounding to nearest,
                 correctly rounded results can be obtained at the end of
                 computations. We present an algorithm for emulating the
                 fused multiply-and-add operator. We also present an
                 iterative algorithm for computing the correctly rounded
                 sum of a set of floating-point numbers under mild
                 assumptions. A variation on both previous algorithms is
                 the correctly rounded sum of any three floating-point
                 numbers. This leads to efficient implementations, even
                 when this rounding is not available. In order to
                 guarantee the correctness of these properties and
                 algorithms, we formally proved them by using the Coq
                 proof checker.",
  acknowledgement = ack-nhfb,
  fjournal =     "IEEE Transactions on Computers",
  keyword =      "round-to-odd (RO(x))",

See also discussions of the double-rounding problem in this recent
useful book:

@String{pub-BIRKHAUSER-BOSTON   = "Birkh{\"a}user Boston Inc."}
@String{pub-BIRKHAUSER-BOSTON:adr = "Cambridge, MA, USA"}

  author =       "Jean-Michel Muller and Nicolas Brisebarre and Florent
                 de Dinechin and Claude-Pierre Jeannerod and Vincent
                 Lef{\`e}vre and Guillaume Melquiond and Nathalie Revol
                 and Damien Stehl{\'e} and Serge Torres",
  title =        "Handbook of Floating-Point Arithmetic",
  publisher =    pub-BIRKHAUSER-BOSTON,
  address =      pub-BIRKHAUSER-BOSTON:adr,
  pages =        "xxiii + 572",
  year =         "2010",
  DOI =          "http://dx.doi.org/10.1007/978-0-8176-4704-9";,
  ISBN =         "0-8176-4704-X",
  ISBN-13 =      "978-0-8176-4704-9",
  LCCN =         "QA76.9.C62 H36 2010",
  bibdate =      "Thu Jan 27 16:18:58 2011",
  price =        "US\$90 (est.)",
  acknowledgement = ack-nhfb,

- Nelson H. F. Beebe                    Tel: +1 801 581 5254                  -
- University of Utah                    FAX: +1 801 581 4148                  -
- Department of Mathematics, 110 LCB    Internet e-mail: beebe@xxxxxxxxxxxxx  -
- 155 S 1400 E RM 233                       beebe@xxxxxxx  beebe@xxxxxxxxxxxx -
- Salt Lake City, UT 84112-0090, USA    URL: http://www.math.utah.edu/~beebe/ -

754 | revision | FAQ | references | list archive