Arrondi correct de fonctions mathématiques : fonctions univariées et bivariées, certification et automatisation
Institution:
École normale supérieure (Lyon ; 1987-2009)Disciplines:
Directors:
Abstract EN:
This thesis broadens the research space for the implementations of correctly rounded mathematical functions in floating-point arithmetic. Interest goes first to the functions xn and to the function xy. A novel approach for detecting the rounding boundary cases of xy is proposed. This innovation yields to a consequent speed-up of this function. Further, this thesis proposes automatic approaches for certifying a correctly rounded implementation of a function. A new algorithm for the safe computation of infinite norms is presented and made practically usable. Finally, algorithms are developed that allow for an automation of the implementation process of functions. A first realization in the Sollya tool permits generating and certifying the code for evaluating a mathematical function without human interaction. In the future, an integration of such techniques in a compiler can be considered.
Abstract FR:
Cette thèse élargit l'espace de recherche accessible en pratique pour des implantations de fonctions mathématiques correctement arrondies en virgule flottante. Elle passe d'abord de l'arrondi correct de fonctions univariées comme log à des familles de fonctions univariées xn , puis à la fonction bivariées xy. Une approche innovatrice pour la détection de cas de frontière d'arrondi de xy à l'aide d'une information partielle sur les pires cas de cette fonction est proposée. Cette innovation provoque un gain en vitesse conséquent. Ensuite, cette thèse propose des approches automatiques pour certifier une implantation de fonction correctement arrondie. Pour la certification des bornes d'erreur d'approximation, un nouvel algorithme pour le calcul de normes infini certifiées est présenté et mis en pratique. Puis les erreurs d'arrondi dans une implantation de fonction mathématique sont analysées par des techniques développées pour l'outil de preuve formelle Gappa. Finalement, des algorithmes sont développées qui permettent l'automatisation de l'implantation de fonctions. Une première mise en œuvre dans l'outil Sollya permet de générer et certifier, sans aucune intervention humaine, le code pour évaluer une fonction mathématique. A l'aide d'un tel outil automatique, de larges espaces de recherches peuvent être parcouru afin d'optimiser une implantation. Au futur, une intégration de ces techniques dans un compilateur est envisageable.