Towards a correctly-rounded and fast power function in binary64 arithmetic - Grid'5000 Access content directly
Preprints, Working Papers, ... Year : 2024

Towards a correctly-rounded and fast power function in binary64 arithmetic

Abstract

We design algorithms for the correct rounding of the power function $x^y$ 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.
Fichier principal
Vignette du fichier
pow.pdf (455.91 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-04159652 , version 1 (12-07-2023)
hal-04159652 , version 2 (08-02-2024)

Licence

Attribution

Identifiers

  • HAL Id : hal-04159652 , version 2

Cite

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⟩
406 View
216 Download

Share

Gmail Facebook X LinkedIn More