When double rounding is odd - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2004

When double rounding is odd

Sylvie Boldo
Guillaume Melquiond

Résumé

Many general purpose processors (including Intel's) may not always produce the correctly rounded result of a floating-point operation due to double rounding. Instead of rounding the value to the working precision, the value is first rounded in an intermediate extended precision and then rounded in the working precision; this often means a loss of accuracy. We suggest the use of rounding to odd as the first rounding in order to regain this accuracy: we prove that the double rounding then gives the correct rounding to the nearest value. To increase the trust on this result, as this rounding is unusual and this property is surprising, we formally proved this property using the Coq automatic proof checker.
Fichier principal
Vignette du fichier
BolMel.pdf (118.74 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00070603 , version 1 (19-05-2006)
inria-00070603 , version 2 (05-12-2014)

Identifiants

  • HAL Id : inria-00070603 , version 2

Citer

Sylvie Boldo, Guillaume Melquiond. When double rounding is odd. 17th IMACS World Congress, Jul 2005, Paris, France. pp.11. ⟨inria-00070603v2⟩
577 Consultations
574 Téléchargements

Partager

Gmail Facebook X LinkedIn More