Academic literature on the topic 'Arithmétique en précision finie'

International audience Let $X$ be a $(d \times N)$-matrix. We consider the variable polytope $\Pi_X(u) = \left\{ w \geq 0 : Xw = u \right\}$. It is known that the function $T_X$ that assigns to a parameter $u \in \mathbb{R}^N$ the volume of the polytope $\Pi_X(u)$ is piecewise polynomial. Formulas of Khovanskii-Pukhlikov and Brion-Vergne imply that the number of lattice points in $\Pi_X(u)$ can be obtained by applying a certain differential operator to the function $T_X$. In this extended abstract we slightly improve the formulas of Khovanskii-Pukhlikov and Brion-Vergne and we study the space of differential operators that are relevant for $T_X$ (ıe operators that do not annihilate $T_X$) and the space of nice differential operators (ıe operators that leave $T_X$ continuous). These two spaces are finite-dimensional homogeneous vector spaces and their Hilbert series are evaluations of the Tutte polynomial of the (arithmetic) matroid defined by $X$. Soit $X$ une matrice $(d \times N)$. Nous considérons le polytope variable $\Pi_X(u) = \left\{ w \geq 0 : Xw = u \right\}$. Il est connu que la fonction $T_X$ qui attribue à un paramètre $u$ le volume du polytope $\Pi_X(u)$ est polynomiale par morceaux. Des formules de Khovanskii-Pukhlikov et de Brion-Vergne impliquent que le nombre de points de réseau dans $\Pi_X(u)$ peut être obtenu en appliquant un certain opérateur différentiel à la fonction $T_X$. Dans ce résumé élargi nous améliorons un peu les formules de Khovanskii-Pukhlikov et de Brion-Vergne et nous étudions l’espaced’opérateurs différentiels qui sont importants pour $T_X$ (c’est-à-dire les opérateurs qui n’annulent pas $T_X$) et l’espace d’opérateurs différentiels bons (c’est-à-dire les opérateurs qui laissent $T_X$ continue). Ces deux espaces sont espaces vectoriels homogène de dimension finie et leurs séries de Hilbert sont des évaluations du polynôme de Tutte du matroïde (arithmétique) défini par $X$.

Nous avons développé un code de calcul de valeurs propres pour matrices non symétriques de grande taille utilisant la méthode d'Arnoldi-Tchebycheff. Une étude a été menée pour mettre en évidence le rôle du défaut de normalité sur l'instabilité spectrale et la stabilité numérique d'algorithmes de calcul de valeurs propres. Des outils, tels que les méthodes de perturbations associées à des méthodes statistiques, ont été expérimentés afin d'apporter des informations qualitatives sur le spectre étudié. Ces outils permettent de comprendre le comportement numérique du problème traite en précision finie, dans les cas ou le calcul direct échoue

Les travaux présentés dans cette thèse concernent la mise au point d'une méthode automatique de réduction et de contrôle des erreurs d'arrondi intervenant dans tout calcul en arithmétique à virgule flottante. L'évaluation informatique d'une fonction f est perturbée par l'introduction d'une erreur d'arrondi élémentaire lors de chaque opération arithmétique. Le résultat calculé s'interprète donc comme une fonction f des données X et des erreurs d'arrondi élémentaires. L'erreur globale commise sur f, qui s'écrit f = ƒ (X,) –f (X, 0), est approchée par une linéarisation à l'ordre un par rapport aux erreurs d'arrondi élémentaires ; c'est à dire en fonction des erreurs d'arrondi élémentaires et des dérivées partielles de f par rapport à ces erreurs. Les dérivées partielles sont calculées grâce à un algorithme de différentiation automatique en mode inverse. Les erreurs d'arrondi élémentaires sont calculées exactement ou estimées pour les quatres opérations de base et la racine carrée. Ainsi, la linéarisation de l'erreur globale est évaluée numériquement ce qui permet de corriger le résultat initial de l'algorithme. Ce résultat corrigé est entaché d'une erreur de calcul Ec et d'une erreur de linéarisation El. Une borne sur Ec est calculée afin de majorer l'erreur résiduelle qui affecte le résultat corrigé lorsque El est négligeable. Dans ce cas, une série de tests pour des évaluations numériquement instables montrent l'efficacité de la méthode : correction totale ou presque totale de l'erreur initiale et majoration fiable de l'erreur résiduelle.

Les filtres numériques sont utilisés dans de nombreux domaines, des télécommunications à l'aérospatiale. En pratique, ces filtres sont calculés sur machine en précision finie (virgule flottante ou virgule fixe). Les erreurs d'arrondi résultantes peuvent être particulièrement problématiques dans les systèmes embarqués. En effet, de fortes contraintes énergétiques et spatiales peuvent amener à privilégier l'efficacité des calculs, souvent au détriment de leur précision. De plus, les algorithmes de filtres enchaînent de nombreux calculs, au cours desquels les erreurs d'arrondi se propagent et risquent de s'accumuler. Comme certains domaines d'application sont critiques, j'analyse les erreurs d'arrondi dans les algorithmes de filtre en utilisant l'assistant de preuve Coq. Il s'agit d'un logiciel qui garantit formellement que cette analyse est correcte. Un premier objectif est d'obtenir des bornes certifiées sur la différence entre les valeurs produites par un filtre implémenté (calculé en précision finie) et par le filtre modèle initial (défini par des calculs théoriques exacts). Un second objectif est de garantir l'absence de comportement catastrophique comme un dépassement de capacité supérieur imprévu. Je définis en Coq les filtres numériques linéaires invariants dans le temps (LTI), considérés dans le domaine temporel. Je formalise une forme universelle appelée la SIF, à laquelle on peut ramener n'importe quel algorithme de filtre LTI sans modifier ses propriétés numériques. Je prouve ensuite le théorème des filtres d'erreurs et le théorème du Worst-Case Peak Gain, qui sont deux théorèmes essentiels à l'analyse numérique d'un filtre sous forme de SIF. Par ailleurs, cette analyse dépend aussi de l'algorithme de somme de produits utilisé dans l'implémentation. Je formalise donc plusieurs algorithmes de somme de produits offrant différents compromis entre précision du résultat et vitesse de calcul, dont un algorithme original correctement arrondi au plus proche. Je définis également en Coq les dépassements de capacité supérieurs modulaires, afin de prouver la correction d'un de ces algorithmes même en présence de tels dépassements de capacité
Digital filters have numerous applications, from telecommunications to aerospace. To be used in practice, a filter needs to be implemented using finite precision (floating- or fixed-point arithmetic). Resulting rounding errors may become especially problematic in embedded systems: tight time, space, and energy constraints mean that we often need to cut into the precision of computations, in order to improve their efficiency. Moreover, digital filter programs are strongly iterative: rounding errors may propagate and accumulate through many successive iterations. As some of the application domains are critical, I study rounding errors in digital filter algorithms using formal methods to provide stronger guaranties. More specifically, I use Coq, a proof assistant that ensures the correctness of this numerical behavior analysis. I aim at providing certified error bounds over the difference between outputs from an implemented filter (computed using finite precision) and from the original model filter (theoretically defined with exact operations). Another goal is to guarantee that no catastrophic behavior (such as unexpected overflows) will occur. Using Coq, I define linear time-invariant (LTI) digital filters in time domain. I formalize a universal form called SIF: any LTI filter algorithm may be expressed as a SIF while retaining its numerical behavior. I then prove the error filters theorem and the Worst-Case Peak Gain theorem. These two theorems allow us to analyze the numerical behavior of the filter described by a given SIF. This analysis also involves the sum-of-products algorithm used during the computation of the filter. Therefore, I formalize several sum-of-products algorithms, that offer various trade-offs between output precision and computation speed. This includes a new algorithm whose output is correctly rounded-to-nearest. I also formalize modular overflows, and prove that one of the previous sum-of-products algorithms remains correct even when such overflows are taken into account

Cette thèse CIFRE, réalisée en collaboration industrielle entre l'IRCCyN et PSA Peugeot-Citroën, s'intéresse à l'aspect numérique de l'implémentation, au sein de calculateurs embarqués, de lois de contrôle/commande. Ces travaux ont porté sur l'implémentation de lois de contrôle-commande (provenant de l'automatique ou du traitement du signal) sous les contraintes de précision finie. Le processus d'implémentation amène de nombreuses dégradations de la loi et nous nous intéressons plus particulièrement à la quantification des coefficients intervenant dans les calculs. Pour une loi (filtre ou régulateur) donnée, il existe une infinité de réalisations numériques possibles qui, bien que mathématiquement équivalentes, ne le sont plus en précision finie : de nombreuses réalisations équivalentes existent : forme d'état, réalisations en delta, formes directes, structures retour d'état observateur, décompositions en cascade, en parallèle,. . . Après avoir présenté ces différentes possibilités, ce mémoire de thèse, propose un formalisme mathématique — la forme implicite spécialisée —qui permet de décrire de manière unifiée un ensemble élargi d'implémentations. Celui-ci, bien que macroscopique, permet d'exprimer précisément les calculs à réaliser et les paramètres réellement mis en jeu. Différentes mesures, appliquées à ce formalisme et qui permettent d'évaluer l'impact de la quantification (en virgule fixe et virgule flottante) et d'analyser la dégradation induite, sont ensuite proposées. Via un problème d'optimisation, la réalisation qui présente la meilleure robustesse face aux détériorations induites par les processus d'implémentation en précision finie est trouvée
These thesis, done in industrial context with PSA Peugeot-Citroën and IRCCyN, deals with the numerical aspect of the implementation of filters or controllers in embedded processors. The implementation of a controller or a filter in a Finite Word Length context may lead to a deterioration of the global performance, due to parametric errors and numerical noises. We focus here on the effect of the quantization of the embedded coefficients. It exists an infinity of equivalent relalizations of a given controller, and these realizations are no more equivalent in finite precision : classical state-space realizations, delta-realizations, direct forms, observer-state feedback, cascade or parallel decomposition, etc. After having exhibits theses possibilites, this Phd thesis proposes an unifying framework — the implicit specialized state-space — that encompasses usual realizations (and many others unexplored). This specialized form, but still macroscopic, is directly connected to the in-line calculations to be performed and the involved coefficients. Various analysis tools, applied to our formalism, may be used to determine how the realization will be altered during the FWL process (with floating point and fixed point considerations). Then, according to these tools, optimal realizations with the best FWL robustness can be found, via an optimization problem

L'implantation efficace des algorithmes de traitement numérique du signal (TNS) dans les systèmes embarqués requiert l'utilisation de l'arithmétique virgule fixe afin de satisfaire les contraintes de coût, de consommation et d'encombrement exigées par ces applications. Le codage manuel des données en virgule fixe est une tâche fastidieuse et source d'erreurs. De plus, la réduction du temps de mise sur le marché des applications exige l'utilisation d'outils de développement de haut niveau, permettant d'automatiser certaines tâches. Ainsi, le développement de méthodologies de codage automatique des données en virgule fixe est nécessaire. Dans le cadre des processeurs programmables de traitement du signal, la méthodologie doit déterminer le codage optimal, permettant de maximiser la précision et de minimiser le temps d'exécution et la taille du code. L'objectif de ce travail de recherche est de définir une nouvelle méthodologie de compilation d'algorithmes spécifiés en virgule flottante au sein d'architectures programmables en virgule fixe sous contrainte de respect des critères de qualité associés à l'application. Ce travail de recherche s'articule autour de trois points principaux. Le premier aspect de notre travail a consisté à définir la structure de la méthodologie. L'analyse de l'influence de l'architecture sur la précision des calculs montre la nécessité de tenir compte de l'architecture cible pour obtenir une implantation optimisée d'un point de vue du temps d'exécution et de la précision. De plus, l'étude de l'interaction entre les phases de compilation et de codage des données permet de définir le couplage nécessaire entre les phases de conversion en virgule fixe et le processus de génération de code. Le second aspect de ce travail de recherche concerne l'évaluation de la précision au sein d'un système en virgule fixe à travers la détermination du Rapport Signal à Bruit de Quantification (RSBQ). Une méthodologie permettant de déterminer automatiquement l'expression analytique du RSBQ en fonction du format des données en virgule fixe est proposée. Dans un premier temps, un nouveau modèle de bruit est présenté. Ensuite, les concepts théoriques pour déterminer la puissance du bruit de quantification en sortie des systèmes linéaires et des systèmes non-linéaires et non-récursifs sont détaillés. Finalement, la méthodologie mise en oeuvre pour obtenir automatiquement l'expression du RSBQ dans le cadre des systèmes linéaires est exposée. Le troisième aspect de ce travail de recherche correspond à la mise en oeuvre de la méthodologie de codage des données en virgule fixe. Dans un premier temps, la dynamique des données est déterminée à l'aide d'une approche analytique combinant deux techniques différentes. Ces informations sur la dynamique permettent de déterminer la position de la virgule de chaque donnée en tenant compte de la présence éventuelle de bits de garde au sein de l'architecture. Pour obtenir un format des données en virgule fixe complet, la largeur de chaque donnée est déterminée en prenant en compte l'ensemble des types des données manipulées au sein du DSP. La méthode sélectionne la séquence d'instructions permettant de fournir une précision suffisante en sortie de l'algorithme et de minimiser le temps d'exécution du code. La dernière phase du processus de codage correspond à l'optimisation du format des données en vue d'obtenir une implantation plus efficace. Les différentes opérations de recadrage sont déplacées afin de minimiser le temps d'exécution global tant que la précision en sortie de l'algorithme est supérieure à la contrainte. Deux types de méthode ont été mis en {\oe}uvre en fonction des capacités de parallélisme au niveau instruction de l'architecture ciblée. Cette méthodologie a été testée sur différents algorithmes de traitement numérique du signal présents au sein des systèmes de radio-communications de troisième génération. Les résultats obtenus montrent l'intérêt de notre méthodologie pour réduire le temps de développement des systèmes en virgule fixe.

Nous présentons une théorie générale pour l'étude de la qualité du calcul en précision finie qui s'appuie sur la notion clé de calculabilité en précision finie. Une fois la calculabilité démontrée, se pose alors la question cruciale de la qualité des solutions obtenues par un calcul à précision finie. Pour y répondre, on utilise les notions d'erreur inverses et de conditionnement qui font partie de l'analyse inverse des erreurs introduite par Wilkinson. Nous appliquons cette théorie sur différents exemples issus de l'Algèbre Linéaire et de l'Optimisation. Nous présentons des formules explicites de conditionnement et d'erreur inverses sur divers problèmes d'Algèbre Linéaire. Nous proposons aussi une méthode systématique, fondée sur le produit de Kronecker, qui permet d'obtenir des formules explicites de conditionnements pour de nombreux problèmes. Nous étudions la notion de distance à la singularité dans le cas de polynômes d'une variable réelle ou complexe, ainsi que son lien avec le conditionnement. Nous montrons l'importance de cette notion pour la compréhension du comportement d'algorithmes de recherche de racines de polynômes en précision finie. Conditionnement et erreur inverse sont au cœur de l'étude approfondie que nous consacrons à deux méthodes numériques : les itérations successives pour la résolution de systèmes linéaires, et la méthode de Gauss-Newton pour la résolution de problèmes de moindres carrés non linéaires. Il apparaît que, même prouvé convergent en arithmétique exacte, un algorithme peut diverger lorsqu'il est employé en précision finie, et nous insistons sur la nécessité de disposer de condition de convergence robustes à la précision finie. De nombreux résultats développés dans cette thèse ont été obtenus dans le cadre d'une collaboration entre le CERFACS et le CNES centrée autour d'un problème de restitution d'orbite de satellite.

Les erreurs d'arrondi peuvent dégrader la précision d'un calcul en arithmétique flottante. Comment améliorer et valider la précision d'un résultat calculé, tout en conservant de bonnes performances ? Nous étudions cette problématique au travers de deux exemples : l'évaluation polynomiale et la résolution de systèmes linéaires triangulaires. Dans les deux cas, nous utilisons la compensation des erreurs d'arrondi pour d'améliorer la précision du résultat. Nos contributions se situent à trois niveaux. 1) Amélioration de la précision : Nous proposons un schéma de Horner compensé, qui permet une évaluation polynomiale aussi précise que celle calculée par le schéma de Horner classique avec une précision interne doublée. En généralisant cet algorithme, nous proposons une autre version compensée du schéma de Horner simulant K fois la précision de travail (K>1). Nous montrons également comment compenser les erreurs d'arrondis générées par l'algorithme de substitution pour la résolution de systèmes triangulaires. 2) Validation de la qualité du résultat : Nous montrons comment valider la qualité du résultat de l'évaluation polynomiale compensée, en proposant le calcul d'une borne d'erreur aposteriori qui ne repose que sur des opérations élémentaires de l'arithmétique flottante: cela assure la portabilité de la méthode et de bonnes performances pratiques. 3) Performances des algorithmes compensés : Nos mesures de performances montrent l'intérêt des algorithmes compensés face aux autres solutions logicielles simulant une précision équivalente. Nous justifions aussi les performances pratiques des algorithmes compensés par une étude du parallélisme d'instructions qu'ils présentent
Rounding error may totally corrupt the result of a floating point computation. How to improve and validate the accuracy of a floating point computation, without large computing time overheads ? We consider two case studies: polynomial evaluation and linear triangular system solving. In both cases we use compensation of the rounding errors to improve the accuracy of the computed result. The contributions of this work are divided into three levels. 1) Improving the accuracy: We propose a compensated Horner scheme that computes polynomial evaluation with the same accuracy as the classic Horner algorithm performed in twice the working precision. Generalizing this algorithm, we present another compensated version of the Horner scheme simulating K times the working precision (K>1). We also show how to compensate the rounding errors generated by the substitution algorithm for triangular system solving. 2) Validating the computed result: we show how to validate the quality of the compensated polynomial evaluation. We propose a method to compute an aposteriori error bound together with the compensated result. This error bound is computed using only basic floating point operations, which ensures portability and efficiency of the method. 3) Performances of compensated algorithms: Our computing time measures show the interest of compensated algorithms compared to other software solutions that provide the same output accuracy. We also justify good practical performances of compensated algorithms thanks to a detailed study of the instruction-level parallelism they contain

Dans cette thèse, nous analysons les problèmes liés à la représentation finie des nombres réels et nous contrôlons la déviation induite par cette approximation. Nous nous intéressons particulièrement à deux problèmes. Le premier est l'étude de l'influence de la représentation finie sur les protocoles de confidentialité différentielle. Nous présentons une méthode pour étudier les perturbations d'une distribution de probabilité causées par la représentation finie des nombres. Nous montrons qu'une implémentation directe des protocoles théoriques pour garantir la confidentialité différentielle n'est pas fiable, tandis qu'après l'ajout de correctifs, la propriété est conservée en précision finie avec une faible perte de confidentialité. Notre deuxième contribution est une méthode pour étudier les programmes qui ne peuvent pas être analysés par composition à cause de branchements conditionnels au comportement trop erratique. Cette méthode, basée sur la théorie des systèmes de réécriture, permet de partir de la preuve de l'algorithme en précision exacte pour fournir la preuve que le programme en précision finie ne déviera pas trop.

Les nombres p-adiques sont un analogue des nombres réels plus proche de l’arithmétique. L’avènement ces dernières décennies de la géométrie arithmétique a engendré la création de nombreux algorithmes utilisant ces nombres. Ces derniers ne peuvent être de manière générale manipulés qu’à précision finie. Nous proposons une méthode, dite de précision différentielle, pour étudier ces problèmes de précision. Elle permet de se ramener à un problème au premier ordre. Nous nous intéressons aussi à la question de savoir quelles bases de Gröbner peuvent être calculées sur les p-adiques
P-Adic numbers are a field in arithmetic analoguous to the real numbers. The advent during the last few decades of arithmetic geometry has yielded many algorithms using those numbers. Such numbers can only by handled with finite precision. We design a method, that we call differential precision, to study the behaviour of the precision in a p-adic context. It reduces the study to a first-order problem. We also study the question of which Gröbner bases can be computed over a p-adic number field

La certification de programmes embarqués dans des systèmes critiques est, aujourd'hui encore, un enjeu majeur pour l'industrie et un défi pour la recherche. En outre, la précision numérique de programmes utilisant l'arithmétique des nombres à virgule flottante a fait l'objet de nombreux travaux et outils. À ce jour, il est possible de déterminer statiquement des sur-approximations fiables des erreurs d'arrondi pouvant apparaître lors des exécutions possibles d'un programme. Néanmoins, ces techniques n'indiquent pas comment corriger ou réduire ces erreurs. Ce travail de thèse présente une méthode automatique de transformation de programmes synchrones permettant de réduire la part des erreurs d'arrondi générées durant leurs exécutions. Pour cela nous utilisons une nouvelle représentation intermédiaire de programmes, appelée APEG, qui constitue une sous-approximation de l'ensemble des programmes mathématiquement équivalents à celui que l'on souhaite optimiser. Cette représentation permet de synthétiser, en temps polynomial, une version plus précise numériquement d'un programme, tout en lui étant mathématiquement équivalent. De plus, nous présentons de nombreux résultats expérimentaux obtenus à l'aide de l'outil que nous avons développé, Sardana, et qui implante toutes les contributions de ce travail
The certification of programs embedded in critical systems is still a challenge for both the industry and the research communities. The numerical accuracy of programs using the floating-point arithmetics is one aspect of this issue which has been addressed by manytechniques and tools. Nowadays we can statically infer a sound over-approximation of the rounding errors introduced by all the possible executions of a program. However, these techniques do not indicate how to correct or even how to reduce these errors. This work presents a new automatic technique to transform a synchronous program in order to reduce the rounding errors arising during its execution. We introduce a new intermediate representation of programs, called APEG, which is an under-approximation of the set of all the programs that are mathematically equivalent to the original one. This representation allows us to synthesize, in polynomial time, a program with a better numerical accuracy, while being mathematically equivalent to the original one. In addition, we present many experimental results obtained with the tool we have developed, Sardana, and which implements all of our contributions