Towards the post-ultimate libm

This article presents advances in the subject of double-precision correctly rounded elementary functions since the publication of the libultim mathematical library developed by Ziv at IBM. This library demonstrated that the performance overhead of correct rounding could be made negligible in average. However, the worst case execution time was up to 1000 times the average time, and memory consumption was also a problem. To address these questions, a range of new techniques, from the more portable to the more efficient, are presented, and demonstrated on two typical functions, exponential and arctangent. The main result of this paper is to show that the worst-case execution time can be bounded within a factor of 2 to 10 of the average time, with memory consumption comparable to current libms. This has in turn implications on the techniques and tradeoffs for correctly rounded functions. This article also shows that these techniques make it much easier to prove the correct rounding property. Thus, this article lifts the last technical obstacles to a widespread use of (at least some) correctly rounded double precision elementary functions.Cet article présente les progrès réalisés dans l'implémentation des fonctions élémentaires avec arrondi correct en double précision depuis la bibliothèque libultim réalisée par Ziv chez IBM. Cette bibliothèque avait démontré que le surcoût moyen de l'arrondi correct pouvait être rendu négligeable, toutefois le temps d'exécution au pire cas pouvait être plusieurs milliers de fois le temps moyen, avec une consommation mémoire à l'avenant. Pour résoudre ce problème,cet article présente une palette de techniques, certaines portables et certaine utilisant au mieux les spécificités des processeurs récents. Ces techniques sont testées pour deux fonctions, l'exponentielle et l'arctangente. Le résultat principal est que le temps au pire cas peut être réduit à un facteur 2-10 du temps moyen, avec une consommation mémoire similaire à celle des libm courantes. Ceci a des implications sur les techniques et les compromis d'implémentation utilisées pour garantir l'arrondi correct. Cela rend également plus facile la preuve de la propriété d'arrondi correct. Pour toutes ces raisons, cet article lève les derniers obstacles à une utilisation généralisée d'au moins quelques fonctions élémentaires avec arrondi correc