Global ETD Search

81	Complexity issues in counting, polynomial evaluation and zero finding / Complexité de problèmes de comptage, d’évaluation et de recherche de racines de polynômes Briquel, Irénée 29 November 2011 (has links) Dans cette thèse, nous cherchons à comparer la complexité booléenne classique et la complexité algébrique, en étudiant des problèmes sur les polynômes. Nous considérons les modèles de calcul algébriques de Valiant et de Blum, Shub et Smale (BSS). Pour étudier les classes de complexité algébriques, il est naturel de partir des résultats et des questions ouvertes dans le cas booléen, et de regarder ce qu'il en est dans le contexte algébrique. La comparaison des résultats obtenus dans ces deux domains permet ainsi d'enrichir notre compréhension des deux théories. La première partie suit cette approche. En considérant un polynôme canoniquement associé à toute formule booléenne, nous obtenons un lien entre les questions de complexité booléenne sur la formule booléenne et les questions de complexité algébrique sur le polynôme. Nous avons étudié la complexité du calcul de ce polynôme dans le modèle de Valiant en fonction de la complexité de la formule booléenne, et avons obtenu des analogues algébriques à certains résultats booléens. Nous avons aussi pu utiliser des méthodes algébriques pour améliorer certains résultats booléens, en particulier de meilleures réductions de comptage. Une autre motivation aux modèles de calcul algébriques est d'offrir un cadre pour l‘analyse d’algorithmes continus. La seconde partie suit cette approche. Nous sommes partis d’algorithmes nouveaux pour la recherche de zéros approchés d'un système de n polynômes complexes à n inconnues. Jusqu'à présent il s'agissait d'algorithmes pour le modèle BSS. Nous avons étudié l'implémentabilité de ces algorithmes sur un ordinateur booléen et proposons un algorithme booléen. / In the present thesis, we try to compare the classical boolean complexity with the algebraic complexity, by studying problems related to polynomials. We consider the algebraic models from Valiant and from Blum, Shub and Smale (BSS). To study the algebraic complexity classes, one can start from results and open questions from the boolean case, and look at their translation in the algebraic context. The comparison of the results obtained in the two settings will then boost our understanding of both complexity theories. The first part follows this framework. By considering a polynomial canonically associated to a boolean formula, we get a link between boolean complexity issues on the formula and algebraic complexity problems on the polynomial. We studied the complexity of computing the polynomial in Valiant's model, as a function of the complexity of the boolean formula. We found algebraic counterparts to some boolean results. Along the way, we could also use some algebraic methods to improve boolean results, in particular by getting better counting reductions. Another motivation for algebraic models of computation is to offer an elegant framework to the study of numerical algorithms. The second part of this thesis follows this approach. We started from new algorithms for the search of approximate zeros of complex systems of n polynomials in n variables. Up to now, those were BSS machine algorithms. We studied the implementation of these algorithms on digital computers, and propose an algorithm using floating arithmetic for this problem. Complexité algorithmique Complexité algébrique Modèle de Valiant Machine BSS Algorithmic complexity Algebraic complexity Valiant's model BSS machine Constraint Satisfaction Problems Floating point arithmetic
82	Analyse statique des systèmes de contrôle-commande : invariants entiers et flottants / Static analysis of control-command systems : floating-point and integer invariants Maisonneuve, Vivien 06 February 2015 (has links) Un logiciel critique est un logiciel dont le mauvais fonctionnement peut avoir un impact important sur la sécurité ou la vie des personnes, des entreprises ou des biens.L'ingénierie logicielle pour les systèmes critiques est particulièrement difficile et combine différentes méthodes pour garantir la qualité des logiciels produits.Parmi celles-ci, les méthodes formelles peuvent être utilisées pour prouver qu'un logiciel respecte ses spécifications.Le travail décrit dans cette thèse s'inscrit dans le contexte de la validation de propriétés de sûreté de programmes critiques, et plus particulièrement des propriétés numériques de logiciels embarqués dans des systèmes de contrôle-commande.La première partie de cette thèse est consacrée aux preuves de stabilité au sens de Lyapunov.Ces preuves s'appuient sur des calculs en nombres réels, et ne sont pas valables pour décrire le comportement d'un programme exécuté sur une plateforme à arithmétique machine.Nous présentons un cadre théorique générique pour adapter les arguments des preuves de stabilité de Lyapunov aux arithmétiques machine.Un outil effectue automatiquement la traduction de la preuve en nombres réels vers une preuve en nombres a virgule flottante.La seconde partie de la thèse porte sur l'analyse des relations affines, en utilisant une interprétation abstraite basée sur l'approximation des valuations associées aux points de contrôle d'un programme par des polyèdres convexes.Nous présentons ALICe, un framework permettant de comparer différentes techniques de génération d'invariants.Il s'accompagne d'une collection de cas de tests tirés de publications sur l'analyse de programmes, et s'interface avec trois outils utilisant différents algorithmes de calcul d'invariants: Aspic, iscc et PIPS.Afin d'affiner les résultats de PIPS, deux techniques de restructuration de code sont introduites, et plusieurs améliorations sont apportées aux algorithmes de génération d'invariants et évaluées à l'aide d'ALICe. / A critical software is a software whose malfunction may result in death or serious injury to people, loss or severe damage to equipment or environmental harm.Software engineering for critical systems is particularly difficult, and combines different methods to ensure the quality of produced software.Among them, formal methods can be used to prove that a software obeys its specifications.This thesis falls within the context of the validation of safety properties for critical software, and more specifically, of numerical properties for embedded software in control-command systems.The first part of this thesis deals with Lyapunov stability proofs.These proofs rely on computations with real numbers, and do not accurately describe the behavior of a program run on a platform with machine arithmetic.We introduce a generic, theoretical framework to adapt the arguments of Lyapunov stability proofs to machine arithmetic.A tool automatically translates the proof on real numbers to a proof with floating-point numbers.The second part of the thesis focuses on linear relation analysis, using an abstract interpretation based on the approximation by convex polyhedrons of valuations associated with each control point in a program.We present ALICe, a framework to compare different invariant generation techniques.It comes with a collection of test cases taken from the program analysis literature, and interfaces with three tools, that rely on different algorithms to compute invariants: Aspic, iscc and PIPS.To refine PIPS results, two code restructuring techniques are introduced, and several improvements are made to the invariant generation algorithms and evaluated using ALICe. Analyse statique Analyse des relations linéaires Calcul en virgule flottante Sécurité et sûreté Stabilité de Lyapunov Static Analysis Linear Relation Analysis Floating-Point Computation Security and Safety Lyapunov Stability 004
83	Hardwarová realizace numerického integrátoru s metodou vyššího řádu / Hardware Realization of Higher Order Numerical Integrator Matečný, František January 2018 (has links) This work describes numerical integration and solution for ordinary differential equations by the Taylor series by different types of integrators. The next part is a description of floating point and fixed point arithmetic. Subsequently, we are presenting designs and calculation methods for parallels multiplication and division integrators in floating point and fixed point arithmetic. The designs were realized in VHDL and implemented on FPGA. Finally we summarizes the proposed solution and compare time complexity with another numerical methods.
84	How to improve the numerical reproducibility of hydrodynamics simulations : analysis and solutions for one open-source HPC software Nheili, Rafife 07 December 2016 (has links) La non-reproductibilité numérique apparait dans divers domaines d'application de la simulation HPC. En effet, les différentes distributions d'un calcul parallèle peuvent mener à des résultats numériques différents, à cause des particularités de l'arithmétique flottante. Le besoin de reproductibilité numérique est motivé pour le débogage, le test et la validation des codes de calcul scientifique. Nous nous intéressons aux simulations par éléments finis en hydrodynamique implémentées dans le logiciel openTelemac qui est largement utilisé pour des applications industrielles et scientifiques. Nous identifions et analysons les sources de cette non-reproductibilité. Nous définissons et implementons comment récupérer la reproductibilité numérique de deux modules d'openTelemac. Nous mesurons que le sur-coût en terme de temps de calcul de la version reproductible est tout à fait raisonnable en pratique. / HPC simulations in various scientific domains suffer from failures of numerical reproducibility because of floating-point arithmetic peculiarities. Different distributions of a parallel computation may yield different numerical results. Numerical reproducibility is a requested feature to facilitate the debug, the validation and the test of industrial or large software. In this thesis, we focus on the openTelemac software that implements finite element simulation for industrial and scientific hydrodynamics. We identify and analyze the sources of this reproducibility failure. We define and implement how to recover numerical reproducibility in two openTelemac modules. We also measure that the running time extra-cost of the reproducible version is reasonable enough in practice. Arithmétique flottante Reproductibilité Éléments finis Décomposition de domaine Simulation hydrodynamique Compensation OpenTelemac Floating-point arithmetic Reproducibility Finite element Domain decomposition Hydrodynamics simulation Compensation OpenTelemac 004
85	Higher Radix Floating-Point Representations for FPGA-Based Arithmetic Catanzaro, Bryan Christopher 22 April 2005 (has links) (PDF) Field Programmable Gate Arrays (FPGAs) are increasingly being used for high-throughput floating-point computation. It is forecasted that by 2009, FPGAs will provide an order of magnitude greater sustained floating-point throughput than conventional processors. FPGA implementations of floating-point operators have historically been designed to use binary floating-point representations, as do general purpose processors. Binary representations were chosen as the standard over three decades ago because they provide maximal numerical accuracy per bit of floating-point data. However, the unique nature of FPGA-based computation makes numerical accuracy per unit of FPGA resources a more important measure of the usefulness of a given floating-point representation. From this viewpoint, higher radix floating-point representations are well suited to FPGA-based computations, especially high precision calculations which require the support of denormalized numbers. This work shows that higher radix representations lead to more efficient use of FPGA resources. For example, a hexadecimal floating-point adder provides a 30% lower Area-Time product than its binary counterpart, and a hexadecimal floating-point multiplier has a 13% lower Area-Time product than its binary counterpart. This savings occurs while still delivering equal worst-case and better average-case numerical accuracy. This work presents a family of higher radix floating-point representations that are designed specifically to interoperate with standard IEEE floating-point, allowing the creation of floating-point datapaths which operate on standard binary floating-point data, yet use higher radix representations internally. Such datapaths provide higher performance by any measure: they are more accurate numerically, consume less FPGA resources and have shorter latencies. When taking into consideration the unique nature of FPGA-based computing systems, this work shows that binary floating-point representations are not optimal for most FPGA-based arithmetic computations. Higher radix representations can therefore be a useful tool for building efficient custom floating-point datapaths on FPGAs. FPGA computer arithmetic floating-point fixed-point floating fixed point radix rounding add multiply numerical accuracy throughput latency binary hexadecimal denormalized Electrical and Computer Engineering
86	Balancing Performance and Usage Cost: A Comparative Study of Language Models for Scientific Text Classification / Balansera prestanda och användningskostnader: En jämförande undersökning av språkmodeller för klassificering av vetenskapliga texter Engel, Eva January 2023 (has links) The emergence of large language models, such as BERT and GPT-3, has revolutionized natural language processing tasks. However, the development and deployment of these models pose challenges, including concerns about computational resources and environmental impact. This study aims to compare discriminative language models for text classification based on their performance and usage cost. We evaluate the models using a hierarchical multi-label text classification task and assess their performance using primarly F1-score. Additionally, we analyze the usage cost by calculating the Floating Point Operations (FLOPs) required for inference. We compare a baseline model, which consists of a classifier chain with logistic regression models, with fine-tuned discriminative language models, including BERT with two different sequence lengths and DistilBERT, a distilled version of BERT. Results show that the DistilBERT model performs optimally in terms of performance, achieving an F1-score of 0.56 averaged on all classification layers. The baseline model and BERT with a maximal sequence length of 128 achieve F1-scores of 0.51. However, the baseline model outperforms the transformers at the most specific classification level with an F1-score of 0.33. Regarding usage cost, the baseline model significantly requires fewer FLOPs compared to the transformers. Furthermore, restricting BERT to a maximum sequence length of 128 tokens instead of 512 sacrifices some performance but offers substantial gains in usage cost. The code and dataset are available on GitHub. / Uppkomsten av stora språkmodeller, som BERT och GPT-3, har revolutionerat språkteknologi. Dock ger utvecklingen och implementeringen av dessa modeller upphov till utmaningar, bland annat gällande beräkningsresurser och miljöpåverkan. Denna studie syftar till att jämföra diskriminativa språkmodeller för textklassificering baserat på deras prestanda och användningskostnad. Vi utvärderar modellerna genom att använda en hierarkisk textklassificeringsuppgift och bedöma deras prestanda primärt genom F1-score. Dessutom analyserar vi användningskostnaden genom att beräkna antalet flyttalsoperationer (FLOPs) som krävs för inferens. Vi jämför en grundläggande modell, som består av en klassifikationskedja med logistisk regression, med finjusterande diskriminativa språkmodeller, inklusive BERT med två olika sekvenslängder och DistilBERT, en destillerad version av BERT. Resultaten visar att DistilBERT-modellen presterar optimalt i fråga om prestanda och uppnår en genomsnittlig F1-score på 0,56 för alla klassificeringsnivåer. Den grundläggande modellen och BERT med en maximal sekvenslängd på 128 uppnår ett F1-score på 0,51. Dock överträffar den grundläggande modellen transformermodellerna på den mest specifika klassificeringsnivån med en F1-score på 0,33. När det gäller användningskostnaden kräver den grundläggande modellen betydligt färre FLOPs jämfört med transformermodellerna. Att begränsa BERT till en maximal sekvenslängd av 128 tokens ger vissa prestandaförluster men erbjuder betydande besparingar i användningskostnaden. Koden och datamängden är tillgängliga på GitHub. Natural Language Processing BERT Comparative Study Floating Point Operations Språkteknologi Hierarkisk Textklassificering BERT Jämförande Studie Flyttalsoperationer Other Mathematics Annan matematik
87	Towards fast and certified multiple-precision librairies / Vers des bibliothèques multi-précision certifiées et performantes Popescu, Valentina 06 July 2017 (has links) De nombreux problèmes de calcul numérique demandent parfois à effectuer des calculs très précis. L'étude desystèmes dynamiques chaotiques fournit des exemples très connus: la stabilité du système solaire ou l’itération à longterme de l'attracteur de Lorenz qui constitue un des premiers modèles de prédiction de l'évolution météorologique. Ons'intéresse aussi aux problèmes d'optimisation semi-définie positive mal-posés qui apparaissent dans la chimie oul'informatique quantique.Pour tenter de résoudre ces problèmes avec des ordinateurs, chaque opération arithmétique de base (addition,multiplication, division, racine carrée) demande une plus grande précision que celle offerte par les systèmes usuels(binary32 and binary64). Il existe des logiciels «multi-précision» qui permettent de manipuler des nombres avec unetrès grande précision, mais leur généralité (ils sont capables de manipuler des nombres de millions de chiffres) empêched’atteindre de hautes performances. L’objectif majeur de cette thèse a été de développer un nouveau logiciel à la foissuffisamment précis, rapide et sûr : on calcule avec quelques dizaines de chiffres (quelques centaines de bits) deprécision, sur des architectures hautement parallèles comme les processeurs graphiques et on démontre des bornesd'erreur afin d'être capables d’obtenir des résultats certains. / Many numerical problems require some very accurate computations. Examples can be found in the field ofdynamical systems, like the long-term stability of the solar system or the long-term iteration of the Lorenz attractor thatis one of the first models used for meteorological predictions. We are also interested in ill-posed semi-definite positiveoptimization problems that appear in quantum chemistry or quantum information.In order to tackle these problems using computers, every basic arithmetic operation (addition, multiplication,division, square root) requires more precision than the ones offered by common processors (binary32 and binary64).There exist multiple-precision libraries that allow the manipulation of very high precision numbers, but their generality(they are able to handle numbers with millions of digits) is quite a heavy alternative when high performance is needed.The major objective of this thesis was to design and develop a new arithmetic library that offers sufficient precision, isfast and also certified. We offer accuracy up to a few tens of digits (a few hundred bits) on both common CPU processorsand on highly parallel architectures, such as graphical cards (GPUs). We ensure the results obtained by providing thealgorithms with correctness and error bound proofs. Arithmétique flottante Arithmétique multi-précision Calcul GPGPU Expansions virgule flottante Processeurs graphiques Systèmes dynamiques Attracteur de Hénon Programmation semi-définie mal-posée Floating-point arithmetic Multi-precision arithmetic GPGPU computing Floating-point expansions Graphics process unit Dynamical systems Henon map Ill-posed semidefinite programming
88	An Optimized Fixed-Point Synthetic Aperture Radar Back Projection Algorithm Implemented on a Field-Programmable Gate Array Hettiarachchi, Don Lahiru Nirmal Manikka January 2021 (has links) No description available. Electrical Engineering Synthetic Aperture Radar SAR, SAR image formation Back projection algorithm Fixed-point based design FxBP FxBP-SWI Floating-point based design Field Programmable Gate Array FPGA Stratix V Arria 10 Stratix 10 OpenCL Total energy consumption FPGA vs. GPU Hardened floating-point units FPGAperformance metric
89	Calcul flottant haute performance sur circuits reconfigurables / High-performance floating-point computing on reconfigurable circuits Pasca, Bogdan Mihai 21 September 2011 (has links) De plus en plus de constructeurs proposent des accélérateurs de calculs à base de circuits reconfigurables FPGA, cette technologie présentant bien plus de souplesse que le microprocesseur. Valoriser cette flexibilité dans le domaine de l'accélération de calcul flottant en utilisant les langages de description de circuits classiques (VHDL ou Verilog) reste toutefois très difficile, voire impossible parfois. Cette thèse a contribué au développement du logiciel FloPoCo, qui offre aux utilisateurs familiers avec VHDL un cadre C++ de description d'opérateurs arithmétiques génériques adapté au calcul reconfigurable. Ce cadre distingue explicitement la fonctionnalité combinatoire d'un opérateur, et la problématique de son pipeline pour une précision, une fréquence et un FPGA cible donnés. Afin de pouvoir utiliser FloPoCo pour concevoir des opérateurs haute performance en virgule flottante, il a fallu d'abord concevoir des blocs de bases optimisés. Nous avons d'abord développé des additionneurs pipelinés autour des lignes de propagation de retenue rapides, puis, à l'aide de techniques de pavages, nous avons conçu de gros multiplieurs, possiblement tronqués, utilisant des petits multiplieurs. L'évaluation de fonctions élémentaires en flottant implique souvent l'évaluation en virgule fixe d'une fonction. Nous présentons un opérateur générique de FloPoCo qui prend en entrée l'expression de la fonction à évaluer, avec ses précisions d'entrée et de sortie, et construit un évaluateur polynomial optimisé de cette fonction. Ce bloc de base a permis de développer des opérateurs en virgule flottante pour la racine carrée et l'exponentielle qui améliorent considérablement l'état de l'art. Nous avons aussi travaillé sur des techniques de compilation avancée pour adapter l'exécution d'un code C aux pipelines flexibles de nos opérateurs. FloPoCo a pu ainsi être utilisé pour implanter sur FPGA des applications complètes. / Due to their potential performance and unmatched flexibility, FPGA-based accelerators are part of more and more high-performance computing systems. However, exploiting this flexibility for accelerating floating-point computations by manually using classical circuit description languages (VHDL or Verilog) is very difficult, and sometimes impossible. This thesis has contributed to the development of the FloPoCo software, a C++ framework for describing flexible FPGA-specific arithmetic operators. This framework explicitly separates the description of the combinatorial functionality of an arithmetic operator, and its pipelining for a given precision, operating frequency and target FPGA.In order to be able to use FloPoCo for designing high performance floating-point operators, we first had to design the optimized basic blocks. We first developed pipelined addition architectures exploiting the fast-carry lines present in modern FPGAs. Next, we focused on multiplication architectures. Using tiling techniques, we proposed novel architectures for large multipliers, but also truncated multipliers, based on the multipliers found in modern FPGA DSP blocks. We also present a generic FloPoCo operator which inputs the expression of a function, its input and output precisions, and builds an optimized polynomial evaluator for the fixed-point evaluation of this function. Using this building block we have designed floating-point operators for the square-root and exponential functions which significantly outperform existing operators. Finally, we also made use of advanced compilation techniques for adapting the execution of a C program to the flexible pipelines of our operators. FPGA Virgule flottante FloPoCo Chemin de données arithmétique Pipeline pour une fréquence donnée Addition pipelinée Additionneur rapide Multiplication Karatsuba-Offman Carré Multiplieur tronqué Multiplication par pavage Virgule fixe Approximation polynomiale Racine carrée flottante Exponentielle flottante Accumulation flottante Schéma d'évaluation de Horner Somme de carrés flottante Synthèse de haut niveau Nid de boucles parfait Multiplication de matrices Jacobi Dilemme du fabricant de table Méthode des différences tabulées Communications pipelinées FPGA Floating-point FloPoCo Arithmetic datapath Frequency-driven pipelining Pipelined addition Short-latency adder Multiplication Karatsuba-Offman Squarer Truncated multiplier Multiplication tiling Fixed-point Polynomial approximation Floating-point square root Floating-point exponential Floating-point accumulation Horner datapath Floating-point sum-of-products High-level synthesis Perfect loop nests Matrix-matrix multiply Jacobi stencil Table maker's dilemma Pipelined communications Pipelined communications
90	Taking architecture and compiler into account in formal proofs of numerical programs / Preuves formelles de programmes numériques en prenant en compte l'architecture et le compilateur Nguyen, Thi Minh Tuyen 11 June 2012 (has links) Sur des architectures récentes, un programme numérique peut donner des réponses différentes en fonction du hardware et du compilateur. Ces incohérences des résultats viennent du fait que chaque calcul en virgule flottante est effectué avec des précisions différentes. Le but de cette thèse est de prouver formellement des propriétés des programmes opérant sur des nombres flottants en prenant en compte l’architecture et le compilateur. Pour le faire, nous avons proposé deux approches différentes. La première approche est de prouver des propriétés des programmes en virgule flottante qui sont vraies sur plusieurs architectures et compilateurs. Cette approche ne considère que les erreurs d’arrondi qui doivent être validées quels que soient l’environnement matériel et le choix du compilateur. Elle est implantée dans la plate-forme Frama-C pour l’analyse statique de code C. La deuxième approche consiste à prouver des propriétés des programmes en analysant leur code assembleur. Nous nous concentrons sur des problèmes et des pièges qui apparaissent sur des calculs en virgule flottante. L’analyse directe du code assembleur nous permet de considérer des caratéristiques dépendant de l’architecture ou du compilateur telle que l’utilisation des registres en précision étendue. Cette approche est implantée comme une sur-couche de la plate-forme Why pour la vérification déductive. / On some recently developed architectures, a numerical program may give different answers depending on the execution hardware and the compilation. These discrepancies of the results come from the fact that each floating-point computation is calculated with different precisions. The goal of this thesis is to formally prove properties about numerical programs while taking the architecture and the compiler into account. In order to do that, we propose two different approaches. The first approach is to prove properties of floating-point programs that are true for multiple architectures and compilers. This approach states the rounding error of each floating-point computation whatever the environment and the compiler choices. It is implemented in the Frama-C platform for static analysis of C code. The second approach is to prove behavioral properties of numerical programs by analyzing their compiled assembly code. We focus on the issues and traps that may arise on floating-point computations. Direct analysis of the assembly code allows us to take into account architecture- or compiler-dependent features such as the possible use of extended precision registers. It is implemented above the Why platform for deductive verification Arithmétique en virgule flottante Programmes numériques Analyse statique Optimisations à la compilation Plate-forme Why Plate-forme Frama-C Floating-point arithmetic Numerical programs Static analysis Compile-time optimizations The Why platform The Frama-C platform

Search results