|
Réunions EVA-Flo
Documents de travail
Rapports d'avancement et autres documents pour l'ANR
Présentation générale du projet
Ce projet s'intéresse à la manière dont une formule mathématique (incluant des fonctions
transcendantes et peut-être des itérations) se retrouve évaluée en virgule flottante
dans un calculateur. Ce projet attaque cette question sous trois angles: comment évaluer une
telle formule, comment automatiser la génération de code pour cette évaluation, comment
valider la précision numérique du code obtenu.
Il s'agit d'améliorer la situation actuelle, qui est la suivante. Un programmeur expert
sait écrire un code de qualité tenant compte par exemple des propriétés mathématiques
des fonctions utilisées, des ordres de grandeurs et de l'accumulation des erreurs d'arrondis,
et de propriétés fines de l'arithmétique virgule flottante utilisée, mais ne dispose pas
des outils permettant de transmettre
cette expertise au compilateur.
Le compilateur se contente d'assembler des opérateurs de base et des appels de fonctions
de bibliothèques sans s'intéresser à la précision numérique du code produit. Quant à obtenir
une garantie sur cette précision, c'est envisageable actuellement uniquement a posteriori,
sur de tout petits codes, et de manière essentiellement manuelle.
Notre approche sera de travailler en parallèle sur trois aspects : l'étude d'algorithmes
d'évaluation de formules mathématiques (du point de vue précision et performance),
la validation de tels algorithmes (notamment des aspects numériques) au cours de leur développement,
afin de guider les choix algorithmiques, enfin l'automatisation de l'ensemble, point pour lequel
la difficulté essentielle consiste à faire coopérer les composants utilisés pour chaque étape.
Du point de vue algorithmique, on travaillera par exemple sur l'approximation d'une formule
par un polynôme à une ou plusieurs variables. Si les mathématiques sont bien établies dans
ce domaine, leur adaptation au monde du calcul flottant est souvent non triviale. Par exemple,
il existe une grande variété de schémas d'évaluation d'un polynôme donné, certains minimisant
les erreurs d'arrondis, d'autres maximisant le parallélisme, etc. De plus, si on peut construire
le ``meilleur polynôme'' théorique d'approximation d'une fonction, dans un domaine et pour une norme
donnés, obtenir le meilleur polynôme avec la contrainte que les coefficients sont exactement
représentables en virgule flottante et en tenant compte de l'erreur d'arrondi due à l'évaluation du
polynôme (et non plus seulement de l'écart entre la fonction et la valeur exacte que prend
le polynôme) reste un problème ouvert, que l'on commence à attaquer sous divers angles.
Outre cet aspect algorithmique fondamental, il s'agira essentiellement de généraliser
et mécaniser une expertise acquise par les porteurs de projets, dans le cadre notamment
de l'évaluation des fonctions élémentaires et de la géométrie algorithmique.
Enfin, on cherchera à valider formellement la précision numérique du code final par rapport
à la formule initiale. Une partie de l'automatisation est acquise, puisque des outils comme Coq, PVS ou
HOL-light savent vérifier des preuve formelles incluant des aspects numériques.
Toutefois ces outils ne rédigent pas la preuve, et notre apport sera de rechercher
une classe de formules aussi large que
possible pour laquelle cette rédaction d'une preuve de propriété numérique sera automatisable.
Plus précisément, il s'agira de produire en parallèle le code évaluant la formule, et
une preuve formelle d'une propriété de ce code, typiquement une borne de l'erreur totale
entre le résultat du code et le résultat mathématique. Ici aussi, les porteurs du projet
ont réalisé ce travail au cas par cas, et l'enjeu est de généraliser et d'automatiser.
En général, l'automatisation complète avec garantie de solution optimale n'a pas de sens
sans information supplémentaire sur le contexte de l'application, et il faudra formaliser
ce qu'un outil a besoin de connaître en plus de la formule à implémenter.
On pense naturellement au domaine d'entrée des valeurs et à la précision finale demandée,
et autres données héritées du contexte de la formule. Il faudra bien plus dans le cas général :
par exemple, s'il est envisageable qu'un outil vérifie un invariant de boucle, il ne pourra
en général pas l'inventer. De même, il faudra souvent suggérer à l'outil une identité
mathématique à utiliser, etc.
Outre un prototype intégré dans un compilateur, ce projet produira une meilleure compréhension
de la notion de formule et de preuve en arithmétique virgule flottante.
La présentation détaillée du projet (en anglais) est
disponible ici.
General introduction to the EVA-Flo project
This project focuses on the way a mathematical formula (that includes
transcendental functions and, possibly, iterations) is evaluated in floating-point
arithmetic. Our approach will be threefold:
how such a formula is evaluated, how we can automate code generation for that evaluation,
how we can validate the numerical accuracy of the obtained code.
We aim at improving the current situation, which can be described as follows.
An expert programmer knows how to write high quality code by using, for instance,
known properties of the functions being used, orders of magnitudes of the variables
being manipulated and of the accumulated round-off error. He may also use some
special properties of the floating-point arithmetic being used. And yet,
he does not know how to transfer this knowledge to a compiler.
The compiler merely uses a sequence of basic operations and functions from a library,
without having clues on the numerical quality of the obtained code. One is able to check
that quality and certify it for small and simple programs only, essentially by paper and
pencil techniques.
We will work simultaneoulsy on three topics: study of algorithms for evaluating mathematical
formulas (with accuracy and performance being at stake), validation of such algorithms
(especially their numerical accuracy) when developing them, in order to influence
the algorithmic choices, and automatization of the process.
From an algorithmic point of view, we will for instance work on the approximation of a formula
by a univariate or multivariate polynomial. The mathematics of this domain are well established.
And yet, their adaptation to floating-point computations is frequently nontrivial.
For example, there are numerous ways of evaluating a polynomial. Some minimize the round-off error,
some optimise parallelization, etc. Moreover, if building the ``best theoretical''
approximating polynomial to a function, for a given norm and a given domain, is easily done,
building the best polynomial with the additional constraint that its coefficients are exactly
representable in a given floating-point format and also taking into account the rounding error
remains an open problem, that we are beginning to tackle with on several aspects.
Beyond this algorithmic aspect, we will need to generalize and automate some expert knowledge
the applicants have accumulated these last years, especially on elementary function evaluation and
computational geometry.
Finally, we will try to bound and validate, using formal proof, the numerical accuracy
of the obtained code. Some part of the automatization is already done, since tools
such as Coq, PVS or HOL-light are able to check proofs that include numerical aspects.
And yet, these tools do not build a proof, they only check it. Our task will be to find
a class of formulas, as large as possible, for which automatically building a proof
of a numerical property is doable. More precisely, we will produce in parallel the code
and a formal proof of a property of that code (typically, a bound of the difference
between the computed result and the exact value). Up to now, the applicants have done
that in some cases, and the goal is to generalize and automate.
This is not simple and a good knowledge of the subtleties of floating-point arithmetic
is necessary for giving, for instance, a meaning to the program
A = 1.0; B = 1.0;
while ((A+1.0)-A-1 == 0.0) do A = 2.0 * A;
while ((A + B) - A - B <> 0.0) do B = B + 1.0;
that returns (in variable B) the base of the floating-point format being used.
A common problem is managing both approximation and rounding errors, and seing how
they accumulate into an algorithm. Existing techniques of numerical analysis
(forward and backward analysis) and computer science (computer algebra, interval arithmetic,
multiple-precision arithmetic) can be used: what is difficult is to use them in order
to obtain error bounds that are not overly pessimistic, and in an automated fashion.
Some tools are missing (e.g., a general technique that computes a validated infinite norm).
We will have to build these missing tools.
Complete automation of a program with a certificate of optimal solution is not really meaningful
if no further information on the application is available. We will need to formalize the information a tool
has to know beyond the formula being implemented. Examples are the input domain of the variables,
the final required accuracy. In the general case, much more information will be needed.
For instance, if a tool can check a loop invariant, it will not be able to invent it.
Also, we will frequently have to suggest to the tool a mathematical relation that might be used, etc.
Beyond a prototype integrated into a compiler, this project will produce a better understanding
of what is a formula or a proof in the domain of floating-point arithmetic.
The detailed presentation of the EVA-Flo project is available
here.