Emulation of a FMA and correctly-rounded sums: proved algorithms using rounding to odd

Sylvie Boldo 1 Guillaume Melquiond 2
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
2 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : Rounding to odd is a non-standard 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 to emulate the fused multiply-and-add operator. We also present an iterative algorithm for computing the correctly rounded sum of a set 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 using the Coq proof checker.
Keywords : Coq proof assistant floating-point arithmetic Floating-point Rounding to odd Accurate summation FMA Formal proof Coq
Type de document :
Article dans une revue
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2008, 57 (4), pp.462-471. 〈10.1109/TC.2007.70819〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger
https://hal-ens-lyon.archives-ouvertes.fr/inria-00080427
Contributeur : Guillaume Melquiond <>
Soumis le : mercredi 10 novembre 2010 - 14:45:24
Dernière modification le : vendredi 20 avril 2018 - 15:44:23
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 15:25:25

Fichier

odd-rounding.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | LIP | ENS-LYON | UNIV-LYON1 | INRIA-RENGRE

Citation

Sylvie Boldo, Guillaume Melquiond. Emulation of a FMA and correctly-rounded sums: proved algorithms using rounding to odd. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2008, 57 (4), pp.462-471. 〈10.1109/TC.2007.70819〉. 〈inria-00080427v2〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

624

Téléchargements de fichiers

660

Contact


archive-ouverte@inria.fr