Towards a correctly-rounded and fast power function in binary64 arithmetic (original) (raw)

Pré-Publication, Document De Travail Année : 2024

Résumé

We design algorithms for the correct rounding of the power function xyx^yxy in the binary64 IEEE 754 format, for all rounding modes, modulo the knowledge of hardest-to-round cases. Our implementation of these algorithms largely outperforms previous correctly-rounded implementations and is not far from the efficiency of current mathematical libraries, which are not correctly-rounded. Still, we expect our algorithms can be further improved for speed. The proofs of correctness are fully detailed and have been formally verified. We hope this work will motivate the next IEEE 754 revision committee to require correct rounding for mathematical functions.

Dates et versions

hal-04159652 , version 1 (12-07-2023)

hal-04159652 , version 2 (08-02-2024)

Licence

Identifiants

• HAL Id : hal-04159652 , version 2

Citer

Tom Hubrecht, Claude-Pierre Jeannerod, Paul Zimmermann, Laurence Rideau, Laurent Théry. Towards a correctly-rounded and fast power function in binary64 arithmetic. 2024. ⟨hal-04159652v2⟩

Collections

• ENS-LYON
• ENS-PARIS
• CNRS
• INRIA
• UNIV-LYON1
• LIP
• GRID5000
• CENTRALESUPELEC
• UNIV-LORRAINE
• INRIA2
• LORIA
• LORIA-ALGO
• PSL
• UNIV-COTEDAZUR
• UDL
• SLICES-FR
• AM2I-UL

1800 Consultations

1037 Téléchargements