Validation formelle des langages à parallélisme de données.

  • By: David Cachera
  • Number: PhD1998-01
  • Date: January 1997
  • Abstract:

    In this thesis, we address the problem of formal validation for data parallel languages. The idea is to exploit the relative simplicity of this programming model to develop some methods, resembling those already in use for classical scalar languages. The first part of this work deals with a simple data parallel imperative language. We have shown that it was possible to define for this language a complete proof system, inspired from Hoare logic. This theoretical study has also be the key to define a practical methodology of proof by annotations, similar to the methodology used for scalar languages. We then worked on the Alpha language, that is a language of recurrence equations. It appeared that it was necessary to define a formal validation framework for this language, since the existing rewriting system allows only proofs of equivalence between programs. We have defined an execution model by means of an operational semantics, and a proof methodology. This methodology is based on invariants, that are refined from a translation of the program into a logical language to the final desired property.
  • Abstract (in french):

    Dans cette thèse, nous nous sommes intéressé à la validation formelle des langages à parallélisme de données. L'idée est de tirer parti de la relative simplicité de ce modèle de programmation pour développer des méthodes semblables à celles déjà éprouvées dans le cadre des langages scalaires classiques. La première partie du travail effectué concerne un langage data-parallèle simple, de type impératif. Nous avons montré qu'il était possible de définir un système de preuve complet pour ce langage, inpiré de la logique de Hoare. L'étude théorique nous a permis en outre de définir une méthodologie pratique de preuve par annotations, semblable à celle utilisée pour les langages scalaires. Nous nous sommes ensuite tourné vers le langage d'équations récurrentes Alpha. Il s'avérait nécessaire de définir pour ce langage un cadre formel de validation, plus riche que le système de transformations existant ne permettant que des preuves par équivalence. Nous avons défini un modèle d'exécution par l'intermédiaire d'une sémantique opérationnelle, et une méthodologie de preuve. Celle-ci utilise des invariants qui sont raffinés à partir d'une traduction du programme dans un langage logique jusqu'à l'obtention de la propriété voulue.
  • Keywords:

    Parallel Programming, Specifying and Verifying and Reasoning about Programs, Semantics of Programming Langages, Data-Parallel Languages, Recurrence Equations, Proof Methods, Hoare Logic, Weakest Preconditions, Invariants.
  • Keywords (in french):

    Programmation Parallèle, Spécification et Validation de Programmes, Sémantique des Langages de Programmation, Langages Data-Parallèles, Equations Récurrentes, Méthode de Preuve, Logique de Hoare, Plus Faibles Préconditions, Invariants.
  • Availability: Paper copy available.
  • Size: 160p
  • Format: Compressed PostScript
  • Get it

Réseaux et systèmes de communication - Etude de logiciels de base.

  • By: Loic Prylli
  • Number: PhD1998-02
  • Date: January 1998
  • Abstract:

    This thesis present a research work on networks and their communication software, for parallel computers with distributed memory. It deals with user issues, as well as with the communication implementation design. This work begins with an algorithmic problem: data redistribution, this problem is important in the field of regular numerical applications. Then I have studied how to simulate the behavior of an application running on a given parallel architecture. I have dealt with the parallelization of the simulation itself. I have proposed a model to evaluate the maximum parallelism in such simulations. In a third part, we use the previous experience to study the implementation of the message-passing implementation on several parallel architectures. We developed on two such architectures the basic communication software layer. Using some original protocols (eliminating all memory copies, minimizing the communication between the network interface card and the processor), we have been able to propose a system providing to the end-user the peak performance of the hardware.
  • Abstract (in french):

    Cette thèse présente un travail de recherche sur les réseaux et les systèmes de communication des machines parallèles à mémoires distribuées. Elle aborde à la fois des problèmes liés à l'utilisateur, et des problèmes liés à l'implémentation des communications. Ce travail commence par l'étude d'un problème algorithmique: la redistribution de données pour des tableaux distribuées cycliquement par blocs, ce problème est important pour les applications numériques régulières. Dans un deuxième temps, je me suis préoccupé du problème de simulation d'une machine parallèle pour une application donnée. Je me suis attaché au problème de parallélisation d'une telle simulation. J'ai proposé un modèle permettant d'évaluer le degré de parallélisme maximal exploitable pour la simulation. Dans une troisième partie, j'ai utilisé l'expérience acquise précédemment, pour l'étude de l'implémentation des systèmes de communication sur plusieurs plateformes parallèles. J'ai réalisé sur deux de ces plateformes un tel système. La mise en oeuvre d'une conception originale des protocoles (avec absence totale de recopies mémoires, et minimisation des échanges entre carte d'interface et processeur), m'a permis de proposer un système fournissant à l'utilisateur les performances crêtes du matériel.
  • Keywords:

    Distributed Memory Computers, Message-Passing Systems, High-Speed Networks, Parallel Computing, Clusters, Myrinet, ATM, Data Redistribution.
  • Keywords (in french):

    Ordinateurs à Mémoire Distribuée, Systèmes d'Echanges de Messages, Réseaux à Haut-Débits, Calcul Parallèle, Myrinet, ATM, Redistribution de Données.
  • Availability: Not available by FTP.
  • Size: 123p
  • Format: Compressed PostScript
  • Get it

MC : Un calcul de modules pour les systèmes de types purs.

  • By: Judicael Courant
  • Number: PhD1998-03
  • Date: February 1997
  • Abstract:

    We are concerned with the development of large proofs in provers based on the Curry-Howard isomorphism between proofs and functional programs. In this framework, it is natural to try to borrow ideas to the functional programming community. Therefore, the SML module system seems to be a good candidate in this respect. Indeed, SML-like module systems seem to be the right tool for the development of large programs ; moreover it seems they apply to many programming languages. Moreover, as for mathematical proofs, the notions of structures are quite similar to the notion of structures and theories as defined by the Bourbaki group in the 60's. Functors correspond to parameterized theories, which is an essential notion when developing large proofs. However, existing modules systems didn't seem suitable yet in a logical framework. Indeed, they lacked some desirable properties such as subject-reduction. Therefore we give a variant of existing systems (translucent sums/manifest types) based on the general framework of Pure Type Systems, allowing type abstraction and true separate type-checking. Results are much more satisfying from a theoretical point of view, and this extension of PTS can also be seen as an extension of the Curry-Howard isomorphism up to the level of theories and modules. We state and prove the expected theoretical results: Subject-Reduction, Church-Rosser property --- this system is therefore a true calculus --- Strong Normalization, Principal Typing, and decidability of Type Inference As a consequence, we also have the conservativity of the module extension over the considered PTS (and therefore the relative consistency of this extension).
  • Abstract (in french):

    Un des problèmes soulevés par la formalisation de mathématiques dans un assistant de preuve est la lourdeur de toute preuve, et de toute formalisation. Une approche pour pallier cette seconde difficulté consiste à établir des environnements de développements de preuves plus flexibles et expressifs fondés sur des formalismes aussi puissants que possible. Ces formalismes sont souvent fondés sur les paradigmes de la programmation fonctionnelle. Or il existe dans ce domaine des systèmes de modules qui facilitent la gestion de gros développements, tel le système de modules de SML, qui s'intègre bien dans une large classe de langages de programmation. En ce qui concerne la preuve mathématique, les notions de structures sont comparables à celles définies par Bourbaki. La notion de foncteur correspond ainsi à la paramétrisation d'une théorie, notion essentielle dans la formalisation mathématique car elle permet d'établir des théories sur des structures abstraites qui sont comparables à des bibliothèques de programmes que l'on peut instancier sur toute instance concrète de la structure considérée. Cependant, les systèmes de modules existants présentaient des défauts les rendant inutilisables dans la perspective d'un formalisme logique. Nous en proposons donc une variante corrigeant ces défauts. Nous montrons qu'elle s'adapte à la classe des Systèmes de Types Purs. Les résultats sont beaucoup plus satisfaisants sur le plan théorique, car le formalisme logique obtenu n'est pas seulement une extension du système initial mais est aussi une extension de la correspondance de Curry-Howard entre programmation et raisonnement. Nous montrons les résultats métathéoriques qu'on peut attendre d'un tel système : auto-réduction, confluence, normalisation forte, conservativité logique de l'extension par modules, consistance logique de l'extension. En outre, cette étude apporte de nouveaux éléments pour la compréhension des notions de classes et d'héritage des langages orientés objets.
  • Keywords:

    Type Theory, Module Systems, Curry-Howard Isomorphism.
  • Keywords (in french):

    Théorie des Types, Systèmes de Modules, Correspondance de Curry-Howard.
  • Availability: Paper copy available.
  • Size: 170p
  • Format: Compressed PostScript
  • Get it

Calculs parallèles pour le traitement des images satellites.

  • By: Sylvain Contassot-Vivier
  • Number: PhD1998-04
  • Date: February 1997
  • Abstract:

    The study presented in this Phd thesis puts in relation two a priori distinct scientific domains that are geology and computer science. Indeed, the context of this work is to design a complete processing line of parallel tools about satellite images, going from the three dimensional reconstruction to the visualization of the retrieved grounds.
  • Abstract (in french):

    L'étude réalisée dans cette thèse met en relation deux domaines scientifiques, a priori distincts, que sont la géologie et l'informatique. En effet, le contexte de ce travail est de concevoir une chaîne complète de traitements parallèles sur les images satellites allant de la reconstruction tridimensionnelle à la visualisation des terrains ainsi reconstitués.
  • Keywords:

    Parallel Algorithm, Stereo Vision, Load Balancing, Image Analysis and Processing, Rectilinear Partitioning, Image Synthesis.
  • Keywords (in french):

    Algorithmique Parallèle, Vision Stéréoscopique, Equilibrage de Charge, Analyse et Traitement d'Image, Partitionnement Rectilinéaire, Synthèse d'Image.
  • Availability: Paper copy available.
  • Size: 148p
  • Format: Compressed PostScript
  • Get it

Inducing an order on cellular automata by a grouping operation.

  • By: Ivan Rapaport
  • Number: PhD1998-05
  • Date: June 1997
  • Abstract:

    In this work we introduce an order relation on cellular automata. We prove that this order admits a minimum and that immediately above it very natural simple classes are located: nilpotents, additives, etc. We exhibit bounded infinite chaines and, on the other hand, we prove that the order does not admit a maximum. Undecidability results concerning cellular automata and periodic tilings of the plane are also proved.
  • Abstract (in french):

    Dans ce travail nous introduisons une relation d'ordre sur les automates cellulaires et commençons son étude. Nous montrons qu'elle admet un minimum et que les deux premières classes de Wolfram ainsi que les automates additifs se trouvent immédiatement au dessus du minimum. Nos exhibons des chaînes infinies avec une borne commune et nos montrons aussi que l'ordre n'admet pas de maximum. Quelques résultats d'indecidabilité concernant les automates cellulaires et les pavages périodiques du plan sont prouvés a la fin.
  • Keywords:

    Cellular Automata, Tilings.
  • Keywords (in french):

    Automates Cellulaires, Pavages.
  • Availability: Paper copy available.
  • Size: 83p
  • Comment: Introduction written in French. Everything else written in
  • Format: Compressed PostScript
  • Get it

Contribution à l'écriture et à l'extension d'une bibliothèque d'algèbre linéaire parallèle.

  • By: Stephane Domas
  • Number: PhD1998-06
  • Date: October 1998
  • Abstract:

    This thesis contains several works dealing with the scientific computations library, ScaLAPACK. The first part shows how to optimize several calls to the BLAS 3 routines executed on different processors, using pipelining and computation/communication overlap. We give a theoretical model of the execution time of these routines, in order to compute the optimal blocking for the pipeline. The second part presents a study on $LU$ factorization in ScaLAPACK (parallel block method). A theoretical model of the execution time is given to compute the optimal block size for the matrix distribution. We also propose an optimization based on pipelining and computation/communication overlap. The third part deals with the redistribution generation between ScaLAPACK calls in a Fortran 77 code. First, we give an execution time model of the redistribution of block cyclic distributed matrices. To achieve this, we present an algorithm that schedules the messages needed to redistribute. Then, we use the execution time model of ScaLAPACK routines to determine the set of the redistributions that minimize the total execution time of the code. The fourth part presents the parallelization of two methods to compute eigenvalues, using the routines proposed in ScaLAPACK.
  • Abstract (in french):

    Cette thèse est constituée de plusieurs travaux autour de la bibliothèque de calcul scientifique ScaLAPACK et de ses composants. La première partie montre comment optimiser une chaîne d'appel aux routines BLAS de niveau 3, en utilisant le pipeline et le recouvrement calcul/communication. Nous donnons un modèle théorique du temps d'exécution de ces routines afin de calculer le découpage optimal pour le pipeline. La deuxième partie est une étude de la factorisation $LU$ de ScaLAPACK (méthode par bloc en parallèle). Un modèle théorique du temps d'exécution est donné afin de calculer la taille de bloc optimale pour la distribution de la matrice à factoriser. Ensuite, nous proposons une optimisation basée sur le pipeline et le recouvrement calcul/communication. La troisième partie concerne la génération des redistributions entre des appels à ScaLAPACK dans un programme Fortran 77. Nous donnons d'abord un modèle du temps d'exécution de la redistribution de matrices distribuées par blocs cycliques. Pour cela, nous présentons un algorithme d'ordonnancement des messages nécessaires pour redistribuer. Ensuite, avec l'aide du modèle théorique des routines de ScaLAPACK, nous déterminons l'ensemble des redistributions qui minimise le temps d'exécution total du programme. La dernière partie est consacrée à la parallélisation de deux méthodes pour le calcul de valeurs propres, en utilisant les routines de ScaLAPACK.
  • Keywords:

    Parallelism, Parallel Linear Algebra, Libraries, Optimisations, Pipeline, Computation/Communication Overlap, Redistribution.
  • Keywords (in french):

    Parallélisme, Algèbre Linéaire Parallèle, Bibliothèque, Optimisations, Pipeline, Recouvrement Calcul/Communication, Redistribution.
  • Availability: Paper copy available.
  • Size: 130p
  • Format: Compressed PostScript
  • Get it

Cellular automata and chaos: from topology to Kolmogorv complexity.

  • By: Enrico Formenti
  • Number: PhD1998-07
  • Date: October 1998
  • Keywords:

    Cellular Automata, Dynamical Systems, Chaos, Kolmogorov Complexity.
  • Keywords (in french):

    Automates Cellulaires, Systemes Dynamiques, Chaos, Complexite de Komogorov.
  • Availability: Paper copy available.
  • Size: p
  • Format: Compressed PostScript
  • Get it