Necessary and sufficient conditions for exact floating point operations

Marc Daumas 1 Sylvie Boldo 1
1 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : Studying floating point arithmetic, authors have shown that the implemented operations (addition, subtraction, multiplication, division and square root) can compute a result and an exact correcting term using the same format as the inputs. Following a path initiated in 1965, all the authors supposed that neither underflow nor overflow occurred in the process. Overflow is not critical as some kind of exception is triggered by such an event that creates remanent non numeric quantities. Underflow may be fatal to the process as it returns wrong numeric values with little warning. Our new necessary and sufficient conditions guarantee that the exact floating point operations are correct when the result is a number. We also present properties when precise rounding is not available in hardware and faithful rounding alone is performed such as using some digital signal processing circuit. We have validated our proofs against the Coq automatic proof checker. Our development has raised many questions, some of them were expected while other ones were very surprising.
Document type :
Reports
Complete list of metadatas

Cited literature [33 references]  Display  Hide  Download

https://hal.inria.fr/inria-00071941
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 7:19:15 PM
Last modification on : Monday, April 29, 2019 - 11:00:19 AM

Identifiers

  • HAL Id : inria-00071941, version 1

Collections

Citation

Marc Daumas, Sylvie Boldo. Necessary and sufficient conditions for exact floating point operations. [Research Report] RR-4644, LIP RR-2002-44, INRIA, LIP. 2002. ⟨inria-00071941⟩

Share

Metrics

Record views

204

Files downloads

468