<p>As parallel and distributed systems scale to hundreds of thousands of cores and beyond, fault tolerance becomes increasingly important -- particularly on systems with limited I/O capacity and bandwidth. Error correcting codes (ECCs) are used in communication systems where errors arise when bits are corrupted silently in a message. Error correcting codes can detect and correct erroneous bits. Erasure codes, an instance of error correcting codes that deal with data erasures, are widely used in storage systems. An erasure code addsredundancy to the data to tolerate erasures. </p> <p><br> </p> <p>In this thesis, erasure coded computations are proposed as a novel approach to dealing with processor faults in parallel and distributed systems. We first give a brief review of traditional fault tolerance methods, error correcting codes, and erasure coded storage. The benefits and challenges of erasure coded computations with respect to coding scheme, fault models and system support are also presented.</p> <p><br> </p> <p>In the first part of my thesis, I demonstrate the novel concept of erasure coded computations for linear system solvers. Erasure coding augments a given problem instance with redundant data. This augmented problem is executed in a fault oblivious manner in a faulty parallel environment. In the event of faults, we show how we can compute the true solution from potentially fault-prone solutions using a computationally inexpensive procedure. The results on diverse linear systems show that our technique has several important advantages: (i) as the hardware platform scales in size and in number of faults, our scheme yields increasing improvement in resource utilization, compared to traditional schemes; (ii) the proposed scheme is easy to code as the core algorithm remains the same; (iii) the general scheme is flexible to accommodate a range of computation and communication trade-offs. </p> <p><br> </p> <p>We propose a new coding scheme for augmenting the input matrix that satisfies the recovery equations of erasure coding with high probability in the event of random failures. This coding scheme also minimizes fill (non-zero elements introduced by the coding block), while being amenable to efficient partitioning across processing nodes. Our experimental results show that the scheme adds minimal overhead for fault tolerance, yields excellent parallel efficiency and scalability, and is robust to different fault arrival models and fault rates.</p> <p><br> </p> <p>Building on these results, we show how we can minimize, to optimality, the overhead associated with our problem augmentation techniques for linear system solvers. Specifically, we present a technique that adaptively augments the problem only when faults are detected. At any point during execution, we only solve a system with the same size as the original input system. This has several advantages in terms of maintaining the size and conditioning of the system, as well as in only adding the minimal amount of computation needed to tolerate the observed faults. We present, in details, the augmentation process, the parallel formulation, and the performance of our method. Specifically, we show that the proposed adaptive fault tolerance mechanism has minimal overhead in terms of FLOP counts with respect to the original solver executing in a non-faulty environment, has good convergence properties, and yields excellent parallel performance.</p> <p><br> </p> <p>Based on the promising results for linear system solvers, we apply the concept of erasure coded computation to eigenvalue problems, which arise in many applications including machine learning and scientific simulations. Erasure coded computation is used to design a fault tolerant eigenvalue solver. The original eigenvalue problem is reformulated into a generalized eigenvalue problem defined on appropriate augmented matrices. We present the augmentation scheme, the necessary conditions for augmentation blocks, and the proofs of equivalence of the original eigenvalue problem and the reformulated generalized eigenvalue problem. Finally, we show how the eigenvalues can be derived from the augmented system in the event of faults. </p> <p><br> </p> <p>We present detailed experiments, which demonstrate the excellent convergence properties of our fault tolerant TraceMin eigensolver in the average case. In the worst case where the row-column pairs that have the most impact on eigenvalues are erased, we present a novel scheme that computes the augmentation blocks as the computation proceeds, using the estimates of leverage scores of row-column pairs as they are computed by the iterative process. We demonstrate low overhead, excellent scalability in terms of the number of faults, and the robustness to different fault arrival models and fault rates for our method.</p> <p><br> </p> <p>In summary, this thesis presents a novel approach to fault tolerance based on erasure coded computations, demonstrates it in the context of important linear algebra kernels, and validates its performance on a diverse set of problems on scalable parallel computing platforms. As parallel systems scale to hundreds of thousands of processing cores and beyond, these techniques present the most scalable fault tolerant mechanisms currently available.</p><br>

This project is concerned with the development and implementation of a novel preconditioning method for the iterative solution of linear systems that arise in the finite element discretisation of the incompressible Navier-Stokes equations with weakly imposed boundary conditions. In this context we studied an augmented approach where the Schur complement associated with the momentum block of the Navier-Stokes equations has special sparse structure. We follow the standard inf-sup stable method of discretising the Navier-Stokes equations by the Taylor-Hood elements with the Lagrange multiplier constraints discretised using the same order approximation on matching grids. The resulting system of nonlinear equations is solved iteratively by Newton's method. The spectrum of the linearised Oseen's problem, preconditioned by the exact augmentation preconditioner was analysed. Then we developed inexact versions of the preconditioner aimed at achieving optimal scaling of the algorithm in terms of computational resources and wall-clock times. The experimental evaluation of the methodology involve a number of benchmark problems in two and three spatial dimensions. The obtained results demonstrate efficiency, robustness and almost optimal scaling of the solution algorithm with respect to the discrete problem size. We used OOMPH-LIB as a testbed for our experiments. The preconditioning strategies were implemented using OOMPH-LIB's Parallel Block Preconditioning Framework. The initial version of the software was significantly upgraded during the course of this project with newly implemented functionalities to facilitate the rapid development of sophisticated hierarchical design of parallel block preconditioners. Parallel performance analysis of the newly introduced functionalities demonstrate negligible overhead in terms of wall-clock time and the framework demonstrate good weak and strong parallel scaling.

A high resolution spectrally accurate three-dimensional flow solver is developed in order to simulate convection dominated fluid flows. The governing incompressible Navier Stokes equations along with the energy equation for temperature are discretized using a second-order accurate projection method which utilizes Adams Bashforth and Backward Differentiation formula for temporal discretization of the non-linear convective and linear viscous terms, respectively. Spatial discretization is performed using a Fourier/Chebyshev spectral method. Extensive tests on three-dimensional Taylor Couette flow are performed and it is shown that the method successfully captures the different states ranging from formation of Taylor vortices to wavy vortex regime. Next, the code is validated for convection dominated flows through a comprehensive comparison of the results for two dimensional Rayleigh Benard convection with the theoretical and experimental results from the literature. Finally, fully parallel simulations, with efficient utilization of computational resources and memory, are performed on a model three-dimensional axially homogeneous Rayleigh Benard convection problem in order to explore the high Rayleigh number flows and to test the scaling of global properties.

No description available.

Quoique très difficile à résoudre, le problème de satisfiabilité Booléenne (SAT) est fréquemment utilisé lors de la modélisation d’applications industrielles. À cet effet, les deux dernières décennies ont vu une progression fulgurante des outils conçus pour trouver des solutions à ce problème NP-complet. Deux grandes avenues générales ont été explorées afin de produire ces outils, notamment l’approche logicielle et matérielle. Afin de raffiner et améliorer ces solveurs, de nombreuses techniques et heuristiques ont été proposées par la communauté de recherche. Le but final de ces outils a été de résoudre des problèmes de taille industrielle, ce qui a été plus ou moins accompli par les solveurs de nature logicielle. Initialement, le but de l’utilisation du matériel reconfigurable a été de produire des solveurs pouvant trouver des solutions plus rapidement que leurs homologues logiciels. Cependant, le niveau de sophistication de ces derniers a augmenté de telle manière qu’ils restent le meilleur choix pour résoudre SAT. Toutefois, les solveurs modernes logiciels n’arrivent toujours pas a trouver des solutions de manière efficace à certaines instances SAT. Le but principal de ce mémoire est d’explorer la résolution du problème SAT dans le contexte du matériel reconfigurable en vue de caractériser les ingrédients nécessaires d’un solveur SAT efficace qui puise sa puissance de calcul dans le parallélisme conféré par une plateforme FPGA. Le prototype parallèle implémenté dans ce travail est capable de se mesurer, en termes de vitesse d’exécution à d’autres solveurs (matériels et logiciels), et ce sans utiliser aucune heuristique. Nous montrons donc que notre approche matérielle présente une option prometteuse vers la résolution d’instances industrielles larges qui sont difficilement abordées par une approche logicielle. / Though very difficult to solve, the Boolean satisfiability problem (SAT) is extensively used to model various real-world applications and problems. Over the past two decades, researchers have tried to provide tools that are used, to a certain degree, to find solutions to the Boolean satisfiability problem. The nature of these tools is broadly divided in software and reconfigurable hardware solvers. In addition, the main algorithms used to solve this problem have also been complemented with heuristics of various levels of sophistication to help overcome some of the NP-hardness of the problem. The end goal of these tools has been to provide solutions to industrial-sized problems of enormous size. Initially, reconfigurable hardware tools provided a promising avenue to accelerating SAT solving over traditional software based solutions. However, the level of sophistication of software solvers overcame their hardware counterparts, which remained limited to smaller problem instances. Even so, modern state-of-the-art software solvers still fail unpredictably on some instances. The main focus of this thesis is to explore solving SAT on reconfigurable hardware in order to gain an understanding of what would be essential ingredients to add (and discard) to a very efficient hardware SAT solver that obtains its processing power from the raw parallelism of an FPGA platform. The parallel prototype solver that was implemented in this work has been found to be comparable with other hardware and software solvers in terms of execution speed even though no heuristics or other helping techniques were implemented. We thus show that our approach provides a very promising avenue to solving large, industrial SAT instances that might be difficult to handle by software solvers.

Le présent travail est consacré à l’approximation numérique des solutions du modèle aux moments M1 pour le transfert radiatif. Il s’agit, ici, de développer des solveurs numériques performants et précis capables de prédire avec précision et robustesse des écoulements où le transfert radiatif joue un rôle essentiel. Dans ce sens, plusieurs méthodes numériques ont été envisagées pour la dérivation des schémas numériques de type solveur de Godunov. Une attention particulière a été portée sur les solveurs préservant les ondes de contact stationnaires. En particulier, un schéma de relaxation et un solveur HLLC sont présentés dans ce travail. Pour chacun de ces solveurs, la robustesse de la méthode a été établie (positivité de l’énergie radiative et limitation du flux radiatif). La validation et l’intérêt des méthodes abordées sont exhibés à travers de nombreuses expériences numériques mono et multidimensionelles. / The present work is dedicated to the numerical approximation of the M1 moments model solutions for radiative transfer. The objective is to develop efficient and accurate numerical solvers, able to provide with precise and robust computations of flows where radiative transfer effects are important. With this aim, several numerical methods have been considered in order to derive numerical schemes based on Godunov type solvers. A particular attention has been paid to solvers preserving the stationary contact waves. Namely, a relaxation scheme and a HLLC solver are presented in this thesis. The robustness of each of these solvers has been established (radiative energy positivity and radiative flux limitation). Several numerical experiments in one and two space dimensions validate the developed methods and outline their interest.

An axisymmetric, Navier-Stokes finite volume flow solver, which uses Harten, Lax and van Leer (HLL) and Harten, Lax and van Leer&ndash / Contact (HLLC) upwind flux differencing scheme for spatial and uses Runge-Kutta explicit multi-stage time stepping scheme for temporal discretization on unstructured meshe is developed. Developed solver can solve the compressible axisymmetric flow. The spatial accuracy of the solver can be first or second order accurate. Second order accuracy is achieved by piecewise linear reconstruction. Gradients of flow variables required for piecewise linear reconstruction are calculated by Green-Gauss theorem. Baldwin-Lomax turbulent model is used to compute the turbulent viscosity. Approximate Riemann solver of HLL and HLLC implemented in solver are validated by solving a cylindrical explosion case. Also the solver&rsquo / s capability of solving unstructured, multi-zone domain is investigated by this problem. First and second order results of solver are compared by solving the flow over a circular bump. Axisymmetric flow in solid propellant rocket motor is solved in order to validate the axisymmetric feature of solver. Laminar flow over flat plate is solved for viscous terms validation. Turbulent model is studied in the flow over flat plate and flow with mass injection test cases.

Quoique très difficile à résoudre, le problème de satisfiabilité Booléenne (SAT) est fréquemment utilisé lors de la modélisation d’applications industrielles. À cet effet, les deux dernières décennies ont vu une progression fulgurante des outils conçus pour trouver des solutions à ce problème NP-complet. Deux grandes avenues générales ont été explorées afin de produire ces outils, notamment l’approche logicielle et matérielle. Afin de raffiner et améliorer ces solveurs, de nombreuses techniques et heuristiques ont été proposées par la communauté de recherche. Le but final de ces outils a été de résoudre des problèmes de taille industrielle, ce qui a été plus ou moins accompli par les solveurs de nature logicielle. Initialement, le but de l’utilisation du matériel reconfigurable a été de produire des solveurs pouvant trouver des solutions plus rapidement que leurs homologues logiciels. Cependant, le niveau de sophistication de ces derniers a augmenté de telle manière qu’ils restent le meilleur choix pour résoudre SAT. Toutefois, les solveurs modernes logiciels n’arrivent toujours pas a trouver des solutions de manière efficace à certaines instances SAT. Le but principal de ce mémoire est d’explorer la résolution du problème SAT dans le contexte du matériel reconfigurable en vue de caractériser les ingrédients nécessaires d’un solveur SAT efficace qui puise sa puissance de calcul dans le parallélisme conféré par une plateforme FPGA. Le prototype parallèle implémenté dans ce travail est capable de se mesurer, en termes de vitesse d’exécution à d’autres solveurs (matériels et logiciels), et ce sans utiliser aucune heuristique. Nous montrons donc que notre approche matérielle présente une option prometteuse vers la résolution d’instances industrielles larges qui sont difficilement abordées par une approche logicielle. / Though very difficult to solve, the Boolean satisfiability problem (SAT) is extensively used to model various real-world applications and problems. Over the past two decades, researchers have tried to provide tools that are used, to a certain degree, to find solutions to the Boolean satisfiability problem. The nature of these tools is broadly divided in software and reconfigurable hardware solvers. In addition, the main algorithms used to solve this problem have also been complemented with heuristics of various levels of sophistication to help overcome some of the NP-hardness of the problem. The end goal of these tools has been to provide solutions to industrial-sized problems of enormous size. Initially, reconfigurable hardware tools provided a promising avenue to accelerating SAT solving over traditional software based solutions. However, the level of sophistication of software solvers overcame their hardware counterparts, which remained limited to smaller problem instances. Even so, modern state-of-the-art software solvers still fail unpredictably on some instances. The main focus of this thesis is to explore solving SAT on reconfigurable hardware in order to gain an understanding of what would be essential ingredients to add (and discard) to a very efficient hardware SAT solver that obtains its processing power from the raw parallelism of an FPGA platform. The parallel prototype solver that was implemented in this work has been found to be comparable with other hardware and software solvers in terms of execution speed even though no heuristics or other helping techniques were implemented. We thus show that our approach provides a very promising avenue to solving large, industrial SAT instances that might be difficult to handle by software solvers.

Made available in DSpace on 2016-08-17T13:45:25Z (GMT). No. of bitstreams: 1 Leandro da Silva Pinheiro.pdf: 12011503 bytes, checksum: cfb85a56c46d3b7b25de578ead063b72 (MD5) Previous issue date: 2016-06-16 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Linear Programming problems will be broach in this work together with some ways to find their solutions. Graphically, using geometric figures such as Geogebra, algebraic solutions and, at least, it will be described the use of the tool "Solver"of the Cal spreedsheet of the LibreOffice, that it is easy tool and application in larger problems, relating to the matter worked in high school content, making analogies with situations of applications of this theory in eveyday life of the student without live of highlight the presentation of the great tool that this theory can display and be of geat importance in other areas of knowledge, providing the student with a greater and more "tangible" view of mathmatics as a tool for implementing. / Os problemas de Programação Linear serão abordados neste trabalho juntamente com algumas maneiras de encontrar suas soluções. Graficamente utilizando recursos geométricos como o Geogebra, soluções algébricas e por último será descrita a utilização da ferramenta "Solver" da planilha Calc do LibreOffice, que se trata de uma ferramenta de fácil utilização e aplicação em problemas de dimensões maiores, relacionando com assuntos trabalhados nos conteúdos do Ensino Médio, fazendo analogias com situações de aplicações dessa teoria na vida cotidiana do aluno sem deixar de destacar a apresentação da grandiosa ferramenta que essa teoria pode exibir e ser de grande importância em outras áreas de conhecimento, proporcionando ao aluno uma visão maior e mais "palpável" da Matemática como instrumento de aplicação.

[pt] Garantir que uma base de conhecimento com atos da administração pública contenha apenas fatos em conformidade com sua legislação torna-se um desafio para qualquer gestor público. Para isso, dado o grande volume de dados gerados por empresas públicas, faz-se necessário o emprego de recursos tecnológicos que auxiliem o processo de análise de conformidade destes atos. Este trabalho apresenta uma arquitetura computacional capaz de extrair informações publicados dos diários oficiais e então serializá-los em duas bases de conhecimento: triplas RDF/XML de fatos e triplas de RDF/XML de regras formalizadas em lógica iALC, uma lógica de descrição intuicionista. Para garantir a consistência desta base de conhecimento, foi desenvolvido um SAT Solver para iALC em forma de tableau semântico intuicionista. Uma extensão do tableau intuicionista de primeira ordem apresentado por Fitting (1969). Este SAT Solver faz parte de um módulo que além de gerar modelos e contra-exemplos para as regras formalizadas em iALC, também gera um código preliminar de consultas em SPARQL. Esta abordagem permite inferir e certificar a qualidade dos dados disponíveis na base de conhecimento RDF/XML de fatos. Para garantir a qualidade do nosso SAT Solver, fizemos a prova de soundness das suas regras. Para garantir a qualidade da nossa abordagem lógica, construímos um conjunto de 21 Questões de Competência e aplicamos à nossa ferramenta. Os resultados deste estudo de caso mostraram a eficácia e eficiência da nossa abordagem. / [en] Ensuring that a knowledge base with public administration acts contains only facts in accordance with its legislation becomes a challenge for any public manager. To achieve this, given the large volume of data generated by public companies, it is necessary to apply technological resources that assist in the process of analyzing the compliance of these acts. This work presents a computational architecture capable of extracting information published in official gazettes and then serializing it into two knowledge bases, RDF/XML triples of facts and RDF/XML triples of rules formalized in iALC logic, an intuitionistic description logic. To ensure the consistency of this knowledge base, a SAT Solver for iALC was developed in the form of an intuitionistic semantic tableau. An extension of the first-order intuitionist tableau presented by Fitting (1960). This SAT Solver is part of a module that generates models and counter-examples for rules formalized in iALC and generates a preliminary query code in SPARQL. This approach allows infer and certify the quality of the data available in the RDF/XML knowledge base of facts. To guarantee the quality of our SAT Solver, we carry out the soundness proof of its rules. To ensure the quality of our logical approach, we built a set of 21 Competency Questions and applied our tool. The results of this case study showed our approach s effectiveness and efficiency.