Regulation dynamique du partitionnement de donnees irregulieres sur machines paralleles a memoire distribuee.

  • By: Thibault Duboux
  • Number: PhD1996-01
  • Date: January 1996
  • Abstract:

    This document deals with load balancing. We start with an overview of existing works. Balancing is studied at every implementation step on distributed memory parallel computers, from design to execution. Then, we propose a strategy to maintain the data partitioning balanced for dynamic and irregular problems. This strategy was applied on synchronous and asynchronous parallel computers. A VLSI dictionary machine was extended to become scalable thanks to this balancing strategy. A dictionary machine was also implemented on an asynchronous computer. This implementation was used to start the design of database applications. At last, implementing the arrangement of line segments in the plane has validated this strategy for highly irregular applications.
  • Abstract (in french):

    Le fil conducteur de cette thèse est l'équilibrage de charge : après un état de l'art sur l'équilibrage à toutes les étapes, de l'élaboration à l'exécution, des implantations sur ordinateurs parallèles à mémoire distribuée, nous proposons une stratégie pour maintenir équilibré le partitionnement des données pour des problèmes dynamiques et irréguliers. Cette stratégie est particulièrement adaptée dans des applications gérant des données complexes soumises à des requêtes de mise à jour et de consultation. Elle se caractérise par sa trés faible influence sur le comportement de l'application. Cette stratégie a été appliquée sur des machines synchrones et asynchrones. Une machine dictionnaire synchrone a ainsi été rendue modulaire grâce à l'ajout de l'équilibrage. Une machine dictionnaire a également pu être implantée sur un ordinateur asynchrone, cela servant de point de départ pour des applications en bases de données. Enfin, le problème de l'arrangement d'un ensemble de segments dans le plan a permis de valider la stratégie d'équilibrage pour des applications complexes.
  • Keywords:

    Load Balancing, Parallel Data Structure, Computational Geometry.
  • Keywords (in french):

    Equilibrage de charge, structures de données parallèles, géométrie algorithmique.
  • Availability: Paper copy available.
  • Size: 104p
  • Format: Compressed PostScript
  • Get it

Contributions a l'arithmetique des ordinateurs : vers une maitrise de la precision.

  • By: Marc Daumas
  • Number: PhD1996-02
  • Date: January 1996
  • Abstract:

    Since the apparition of the first computer, floating point arithmetic have drastically changed. The IEEE standard of implementation has been successful in settling the specifications of modern computer arithmetic, but the scientists are loosing rapidly the control and the validation of their computations. In spite of the huge amount of work associated to the definition of the standard operations, the numerical validation of a program cannot always be left to the arithmetic implemented on the computer. I am presenting in the first part of these studies two extensions to offer to the user a higher chance of validity : a new rounding mode adapted to the elementary functions and an efficient coding for the intervals that could be used easily by end users. I present in the first part of my work a detailled definition of the unit in the last place function and the probability of absorption or propagation of round-off errors in a stream of multiplications. This work, added to the former work of many research groups and the proposal contained in my master thesis clearly show the benefits that could be drawn from the proposed extensions. It is possible with on-line arithmetic to adapt at each step the precision of computation, but the basic operators are not adapted to modern 32 bit or 64 bit architectures. An efficient implementation of on-line operators will necessarily involve a description of a low level circuit. The Field Programmable Gate Array, are electronic component in which each logic part can be configured. By using FPGAs, we are able to lower the cost of production of a new circuit since we do not need a prototype. We have implemented with these technologies the common on-line operators : addition, normalization and so on... The kernel for on-line arithmetic (in French, Nacel) defined in this dissertation has been used to implement more evolved arithmetic operators as the multiplication, the division, the extraction of square root and the elementary functions through a polynomial approximation. Data-flow architectures are not sensitive to the difficulties that arise in the design of modern computers : memory access, communication latency, partial use of the instruction pipeline. I shall describe in this work the functionnal model for a small on-line arithmetic virtual unit (in French, Puce). By implementing a token mechanism equivalent to the process implemented on the Manchester Data-Flow Machine, Puce is able to reproduce the behavior of a small data-flow machine. We have added to the model the basics for on-line arithmetic, and Puce is able to evaluate on-line any numerical expression. We shall present towards the end of this work the result of a software simulation of Puce on a Fast Fourier Transform to validate the model of evaluation.
  • Abstract (in french):

    Depuis l'apparition des premiers ordinateurs, l'arithmétique flottante a énormément évolué. La norme IEEE 754 a permis de fixer les caractéristiques de l'arithmétique des ordinateurs modernes, mais les scientifiques perdent de plus en plus vite le contrôle de la validité de leurs calculs. Malgré l'énorme travail associé à la définition des opérations, la validation des calculs ne peut toujours pas être assurée de façon certaine par l'arithmétique implantée sur les ordinateurs. Je présente dans la première partie de cette étude deux prolongements qui visent à augmenter la marge de validité des opérations : un nouveau mode d'arrondi pour les fonctions trigonométriques et un codage efficace des intervalles accessible facilement à l'utilisateur. Je présente aussi dans cette partie une étude détaillée de la fonction unit in the last place et la probabilité d'absorption ou de propagation des erreurs dans une chaîne de multiplication. Ces travaux, qui viennent s'ajouter aux travaux antérieurs d'autres équipes de recherche et aux solutions que j'ai proposées dans ma thèse de master montrent les bénéfices que l'on pourra tirer des deux extensions présentées. L'arithmétique en-ligne permet de gérer efficacement les problèmes de précision, mais les opérateurs élémentaires utilisés sont peu adaptés aux architectures modernes de 32 ou 64 bits. L'implantation efficace d'un opérateur en-ligne ne peut que passer par la description d'un circuit de bas niveau. Les prédiffusés actifs, terme français utilisé pour Field Programmable Gate Array, sont des composants spéciaux programmables au niveau des portes logiques. Ils permettent d'abaisser les coûts de production en évitant de fabriquer un prototype. Nous avons implanté grâce à ces technologies les opérateurs simples de calcul en-ligne : addition, normalisation, etc...Le Noyau Arithmétique de Calcul En-Ligne (Nacel) décrit dans ce mémoire permet d'implanter les opérations arithmétiques usuelles telles que la multiplication, la division, l'extraction de racine carrée et les fonctions élémentaires trigonométriques et hyperboliques par une approximation polynômiale. Les architectures à flots de données sont insensibles aux difficultés sur lesquelles butent les concepteurs des ordinateurs modernes : temps d'accès à la mémoire, latence de communication, occupation partielle du pipeline d'instructions. Je décris dans ce document le mode de fonctionnement d'une machine virtuelle appelée Petite Unité de Calcul En-ligne (Puce). Par une gestion adaptée des étiquettes inspirée pour le contrôle des données de celle utilisée par la Manchester Data Flow Machine, Puce reproduit le comportement complet d'une machine à flot de données. Elle comprend de plus les opérations en-ligne de calcul scientifique. Nous présentons afin de valider le modèle d'évaluation de Puce les résultats de simulations logicielles pour une ou plusieurs unités fonctionnelles.
  • Keywords:

    Computer Arithmetic, Floating Point Numbers, Precision Control, Field Programmable Gate Arrays, Computer Architecture, Data Flow Machines.
  • Keywords (in french):

    Arithmétique des ordinateurs, nombres à virgule flottante, contrôle de la précision, FPGA, architecture des ordinateurs, machines à flot de données.
  • Availability: Paper copy available.
  • Size: 126p
  • Format: Compressed PostScript
  • Get it

Outils pour la parallelisation automatique.

  • By: Pierre Boulet
  • Number: PhD1996-03
  • Date: January 1996
  • Abstract:

    Automatic parallelization is one of the approaches aimed at a better and easier use of parallel computers. It consists in taking a program written for a sequential computer (which has only one processor) and to adapt it to a parallel computer. The interest to have a program, named a parallelizer, do this parallelization automatically is that we could reuse all the code already written in fortran for sequential machines, after parallelization, on parallel machines. We are not there yet, but we are getting closer. My work fits in this framework. Approximately half of my thesis focuses on the realization of a software that automatically parallelizes a reduced class of programs (the uniform loop nests that use translations as data array accesses) into HPF (High Performance Fortran). I mainly discuss the HPF code generation which is the most innovative part of this program. Besides the realization of Bouclettes, my contribution to the domain is also theoretical with a study of a data partitioning technique called tiling and a study of the optimization of the evaluation of array expressions in HPF. Tiling is a technique aimed at optimizing the size of the distributed tasks to reduce the communication time overhead. Array expression evaluation is an optimization step of the parallel compiler (the program that translates the parallel code written in a high level language as HPF into directly executable machine code for the parallel computer).
  • Abstract (in french):

    La parallélisation automatique est une des approches visant à une plus grande facilité d'utilisation des ordinateurs parallèles. La parallélisation consiste à prendre un programme écrit pour une machine séquentielle (qui n'a qu'un processeur) et de l'adapter à une machine parallèle. L'intérêt de faire faire cette parallélisation automatiquement par un programme appelé paralléliseur est qu'on pourrait alors réutiliser tout le code déjà écrit en fortran pour machine séquentielles, après parallélisation, sur des machines parallèles. Nous n'y sommes pas encore, mais on s'en approche. C'est dans ce cadre que se situe mon travail. Une moitié approximativement de ma thèse est consacré à la réalisation d'un logiciel qui parallélise automatiquement une classe réduite de programmes (les nids de boucles uniformes qui utilisent des translations comme accès aux tableaux de données) en HPF (High Performance Fortran). J'insiste surtout sur la partie génération de code HPF, qui est la partie la plus novatrice de ce programme. Outre la réalisation de Bouclettes, ma contribution au domaine est aussi théorique avec une étude sur un partitionnement des données appelé pavage par des parallélépipèdes et une étude de l'optimisation des calculs d' << expressions de tableaux >> dans le langage HPF. Le pavage est une technique permettant d'optimiser la taille des tâches qu'on répartit sur les processeurs pour diminuer le temps passé en communications. L'évaluation d'expressions de tableaux est une étape d'optimisation du compilateur parallèle (le programme qui traduit le code parallèle écrit dans un langage de haut niveau comme HPF en code machine directement exécutable par l'ordinateur parallèle).
  • Keywords:

    Automatic Parallelization, Data Parallelism, High Performance Fortran, Loop Nests, Compilation, Optimization.
  • Keywords (in french):

    Parallélisation automatique, data-parallélisme, high performance fortran, nids de boucles, compilation, optimisation.
  • Availability: Paper copy available.
  • Size: 127p
  • Format: Compressed PostScript
  • Get it

Alignement et distribution en parallelisation automatique.

  • By: Michele Dion
  • Number: PhD1996-04
  • Date: January 1996
  • Abstract:

    Automatic parallelization, whose objective is to compute suitable time transformations (scheduling problem) and space transformations (allocation problem), can allow to automatically parallelize a sequential program. Alignment and distribution constitute the major contribution of this thesis. Minimizing time spent on communications when mapping affine loop nests onto distributed memory parallel computers (DMPCs) is a key problem with regard to performance. All communications are not equivalent. Local communications (translations), simple communications (horizontal or vertical ones) or structured communications (broadcasts, gathers, scatters, or reductions) are performed much faster than general affine communications onto DMPCs. We present heuristics based on the following strategy : (1) zero out as many nonlocal communications as possible, (2) as it is generally impossible to obtain a communication local mapping, try to optimize residual communications (try to find mappings such that residual communications are structured communications or can be decomposed into more simple data movements). Besides, we deal with a problem of partitioning and with a new type of space-time transformations, modular transformations.
  • Abstract (in french):

    La parallélisation automatique, dont l'objectif est de trouver le placement des calculs dans le temps (problème d'ordonnancement) et sur les différents processeurs de la machine (problème d'allocation), permet de générer automatiquement un programme parallèle à partir d'un programme séquentiel. L'alignement et la distribution des données et des instructions sur les processeurs constituent le point central de cette thèse. Lors du placement d'un nid de boucles affine sur un espace de processeurs, la minimisation du temps dû aux communications est un problème décisif en ce qui concerne les performances. Toutes les communications ne sont pas équivalentes. Les communications locales (translations), les communications structurées (diffusions, distributions, rassemblements, réductions, ...) ou les communications simples (suivant un des axes de l'espace des processeurs) s'effectuent beaucoup plus rapidement que les communications affines générales. Nous présentons donc des heuristiques basées sur la stratégie suivante : (1) minimisation du nombre de communications non bornées, (2) puisqu'il est en général impossible d'obtenir un placement n'aboutissant qu'à des communications locales, optimisation des communications résiduelles en essayant d'avoir des communications structurées ou des communications simples. Par ailleurs, nous nous intéressons à un problème de partitionnement et à une ouverture vers de nouvelles transformations, les transformations modulaires.
  • Keywords:

    Automatic Parallelization, Affine Loop Nests, Data-parallelism, HPF, Alignment and Distribution.
  • Keywords (in french):

    Parallélisation automatique, nids de boucles affines, parallélisme de données, HPF, alignement et distribution.
  • Availability: Paper copy available.
  • Size: 138p
  • Format: Compressed PostScript
  • Get it

Complexite memoire du routage dans les reseaux distribues.

  • By: Cyril Gavoille
  • Number: PhD1996-05
  • Date: January 1996
  • Abstract:

    Routing consists in locally decide routes of messages traveling trough intermediary nodes of a distributed network of processors in a parallel computer, or, more generally, in a computer's network. We study local characteristics of the ``router'' (coprocessor that computes routing) in comparison with the globality of the communication network. Precisely, we measure the minimum memory requirement of each router to ensure fast communications on arbitrary networks.
  • Abstract (in french):

    Au plus bas niveau des communications, le routage consiste à décider localement de la route des messages transitant par les noeuds intermédiaires d'un réseau distribué de processeurs dans un ordinateur parallèle, ou, plus généralement, dans un réseau distribué d'ordinateurs. Nous étudions les caractéristiques locales du ``routeur'' (coprocesseur effectuant le routage) par rapport à la globalité du réseau communiquant. Précisemment, nous mesurons la quantité minimale d'information nécessaire par chacun des routeurs pour assurer des communications rapides sur n'importe quel type de réseau.
  • Keywords:

    Interval Routing, Routing Tables, Compact Routing, Parallelism, Distributed Networks, Complexity.
  • Keywords (in french):

    Routage par intervalles, tables de routage, routage compact, parallélisme, réseaux distribués, complexité.
  • Availability: Electronic copy only.
  • Size: 114p
  • Format: Compressed PostScript
  • Get it

Analyse distribuee de traces d'execution de programmes paralleles.

  • By: Xavier-Francois Vigouroux
  • Number: PhD1996-06
  • Date: January 1996
  • Abstract:

    Monitoring consists in generating trace information during a parallel program execution. The goal is to detect performances problems. The amount of data generated by large parallel machines makes classical tools impossible to use. This thesis solves this problem by distributing the information among different storage sites (for exemple, the different disks of a parallel machine). This way, trace files may be read concurently. In order to obtain a consistent information, we built a client-server software to handle these files. Clients ask the software to return already filtered pieces of trace. This client-server architecture is extensible : user may add his own clients. Moreover, we have designed several innovating clients : hierarchical client, acoustic client, client with automatic problems detection, client consisting in a filtering interface to classical tools, clients integrating 3D tools, ...
  • Abstract (in french):

    Le monitoring consiste à générer des informations de trace durant une exécution d'un programme parallèle pour détecter les problèmes de performances. La quantité d'information générée par de très grosses machines parallèles rend les outils d'analyse classiques inutilisables. Cette thèse résout ce problème en distribuant l'information de trace sur plusieurs fichiers contenus sur plusieurs sites, les fichiers pouvant être lus en parallèle. La manipulation de ces fichiers afin d'obtenir une information cohérente est la base d'un logiciel client-serveur grâce auquel des clients demandent de l'information déjà filtrée sur une exécution. Cette architecture client serveur est extensible (l'utilisateur peut créer ses propres clients) et modulable. Nous avons, d'autre part, crée déjà plusieurs clients novateurs : client hiérarchique, sonore, recherche automatique de problèmes, interface filtrante aux outils classique, intégration d'outil 3D, ...
  • Keywords:

    Parallelism, Performance Analysis, Monitoring, Distributed Files.
  • Keywords (in french):

    Informatique parallèle, analyse de performances, monitoring, fichiers distribués.
  • Availability: Paper copy available.
  • Size: 184p
  • Format: Compressed PostScript
  • Get it

Equilibrage de charge dirigé par les données : applications à la synthèse d'images.

  • By: Jean-Marc Pierson
  • Number: PhD1996-07
  • Date: October 1996
  • Abstract:

    Load balancing is a key point in parallel computing. In this thesis, we study more especially rectilinear partitioning, which gives a solution to data driven load balancing, where locality constraints apply to data items (the computation associated with an item is a function of its neighborhood). We are more particularly interested in quantifying the quality of the balance produced by two partitioning heuristics. We also illustrate the usefulness of these approaches in the framework of dynamic load balancing. Some applications in the image synthesis domain are detailed (particle systems, animation) who outline the adequacy of our approach for irregular data structures. We then exhibit the work accomplished in the development of a portable parallel library and its extension to a distributed graphic environment.
  • Abstract (in french):

    L'équilibrage de charge est un point crucial dans l'utilisation des machines parallèles. Nous étudions dans cette thèse le partitionnement rectilinéaire qui constitue une solution à l'équilibrage des charges quand les données sont soumises à des contraintes de localité (le calcul associé à une donnée fait intervenir des données voisines). Nous nous attachons en particulier à apprécier la qualité de l'équilibrage de deux heuristiques de partitionnement. Nous montrons également la pertinence de ces approches à un équilibrage dynamique de la charge. Des applications dans le domaine de la synthèse d'images (système de particules, calculs d'animations) montrent l'adéquation de notre approche aux problèmes posés par des structures de données irrégulières. Nous exposons également le travail fourni dans le développement d'une bibliothèque parallèle portable et son extension à un environnement graphique distribué.
  • Keywords:

    Parallel Computing, Dynamic Load Balancing, Rectilinear Partitioning, Particle Systems, Animation, Zbuffer, Image Coherence, Programming Environment, Distributed Visualization.
  • Keywords (in french):

    Algorithmique parallèle, Equilibrage de charge dynamique, Partitionnement rectilinéaire, Système de particules, Animation, Zbuffer, Cohérence entre images, Environnements de programmation, Visualisation distribuée.
  • Availability: Paper copy available.
  • Size: 111p
  • Format: Compressed PostScript
  • Get it

Communications, routage et architectures des machines a memoire distribuee -- Autour du routage wormhole.

  • By: Eric Fleury
  • Number: PhD1996-08
  • Date: October 1996
  • Abstract:

    This thesis deals with several problems related to communication networks in multicomputers architectures. The first chapter provides a survey of the different technics of communication used in parallel computers. This study point out the main parameters involved in the delay of a communication : topology, routing and flow control. The wormhole routing which has become the switching technic of choice in modern distributed-memory multiprocessors is presented in details. The second chapter presents a methodology for building an architecture for a distributed-memory multiprocessor. We use this methodology to design the architecture of a massively parallel machine based on T9000 and C104. In chapter 3, we study the problem of deadlock-free wormhole routing in parallel and distributed architectures. We provide a necessary and sufficient condition for deadlock-free routing for wormhole routed interconnection networks for a large class of routing functions. Chapter 4 provides a survey of global communications with wormhole routing. Several articles deal with global communications but a careful reading shows that several hypotheses are used and therefore comparisons are impossible. Our aim is to give a survey and propose general models of communications. The last chapter study the path-based wormhole multicast problem. We give new path-based wormhole multicasting algorithms in meshes.
  • Abstract (in french):

    En moins de dix ans, le calcul parallèle a émergé comme une solution possible aux besoins sans cesse croissants de puissance de calcul. Cette accélération dans le développement et les besoins en calcul a vu l'avènement des architectures dites massivement parallèles. Les travaux réalisés dans cette thèse portent sur l'étude des différents paramètres liés au temps nécessaire à une communication entre deux processeurs. Un premier chapitre établit un état de l'art des techniques de commutation mises en oeuvre dans les machines massivement parallèles. Un consensus s'étant établi autour du mode wormhole, nous présentons en détail les caractéristiques et la mise en oeuvre de ce mode de commutation. Le deuxième chapitre présente une méthodologie de conception de l'architecture d'une machine parallèle à mémoire distribuée. Nous illustrons cette méthodologie dans le cadre de la conception du réseau d'interconnexion d'une machine parallèle à base de routeur C104 et de transputer T9000. Le troisième chapitre traite du problème spécifique de l'interblocage relatif à une fonction de routage. Nous donnons une définition générale de la notion de fonction de routage. Pour cette grande classe de fonction de routage, nous donnons une condition nécessaire et suffisante pour qu'une fonction de routage \rR\ soit sans interblocage sur un graphe $G$. Nous effectuons, dans le quatrième chapitre, une synthèse des divers articles traitant de la diffusion, de l'échange total et de l'échange total personnalisé en mode commutation wormhole. Notre but est de passer en revue ces différents résultats et de proposer un cadre général permettant de les comparer. Dans le cinquième chapitre nous étudions la diffusion partielle en mode de commutation wormhole en supposant que les routeurs offrent la facilité de copie-retransmission. Nous présentons de nouveaux algorithmes de diffusion partielle dans les grilles en mode commutation wormhole.
  • Keywords:

    Parallel Architectures, Routing, Adaptive Routing, Wormhole, Multiprocessor, Performance Evaluation, Deadlock, Collective Communications, Massively Parallel Computers, Multicast, Interconnection Networks.
  • Keywords (in french):

    Architectures parallèles, Routage, Routage adaptatif, Wormhole, Machines parallèles, Evaluation des performances, Interblocage, Communications globales, Ordinateurs massivement parallèles, Diffusion partielle, Réseaux d'interconnexion.
  • Availability: Paper copy available.
  • Size: 8+168p
  • Format: Compressed PostScript
  • Get it

Construction et exécution de graphes de t\^{a}ches acycliques à gros grain.

  • By: Michel Loi
  • Number: PhD1996-09
  • Date: October 1996
  • Availability: Out of print. Not available by FTP.
  • Format: Compressed PostScript
  • Get it

Techniques évolutionnaires pour l'apprentissage des réseaux récurrents à coefficients réels.

  • By: Cedric Gegout
  • Number: PhD1996-10
  • Date: December 1996
  • Abstract:

    Searching an optimization algorithm adapted to a given problem cannot be done within the only framework of genetic algorithms. One has to use a wider class of algorithms containing all the algorithms based upon the natural selection mechanism : the class of evolutionary algorithms. Three groups of algorithms belong to it : the evolution strategies, evolutionary programming and the genetic algorithms. The evolutionary algorithms which do not belong to one of these groups are called unconventional. The search of an evolutionary algorithm adapted to a certain problem lead naturally to the development of an unconventional algorithm. In this report, by solving a particular case we show the interests of unconventional algorithms, and how to improve them. The most important goal is to establish their properties and their functionalities for neural network learning procedures. Firstly, we introduce the principal characteristics of an efficient coding and especially the concepts of minimal coding and non-redundancy. This allows us to solve the difficult problem of initializing gradient descent based algorithms for training acyclic neural networks. This problem is first modelized as a multi-objective optimization problem : each net is evaluated by using the output function computed by the net and its derivatives. Recurrent network learning is also studied, but this problem is much more complex. We restrict our attention on convergent networks : the dynamic governing the network is asymptotically convergent. In this framework, evolutionary algorithms prove to be efficient tools for approximation of nonlinear functions.
  • Abstract (in french):

    La recherche d'un algorithme d'optimisation adapté à un problème donné ne peut pas se faire dans le seul cadre des algorithmes génétiques, il est nécessaire de considérer une classe d'algorithmes plus grande qui contient tous les algorithmes inspirés des mécanismes génétiques : les algorithmes évolutionnaires. Cette classe comprend trois grands groupes : les stratégies d'évolution (ou évolutives), les techniques de programmation évolutionnaire et les algorithmes génétiques. Les algorithmes qui n'appartiennent pas à l'un de ces groupes sont dits non conventionnels. Comme le montre ce rapport la recherche d'un algorithme évolutionnaire adapté à un problème donné amène naturellement à la conception d'un algorithme non conventionnel. On tâchera de montrer par l'agencement d'algorithmes évolutionnaires non conventionnels les attraits de chacuns, et les moyens de les renforcer. Le principal objectif étant d'appréhender les propriétés et les fonctionnalités les plus intéressantes de ces algorithmes pour l'apprentissage de réseaux de neurones, l'essentiel des travaux exposés sera élaboré au profit des réseaux de neurones. On introduira les principales caractéristiques d'un codage efficace et on développera en particulier les notions de minimalité et de redondance. Ceci nous permettra de résoudre le problème de l'initialisation des réseaux de neurones pour les algorithmes basés sur une descente de gradient. Ce problème est considéré comme un problème d'optimisation réelle, il peut être étudié comme un problème multicritère où l'évaluation d'un bon réseau d'initialisation s'effectue avec la fonction de sortie calculée par le réseau et sa différentielle. On étudie ensuite le problème de l'apprentissage des réseaux de neurones récurrents. Ce problème est plus complexe que celui des réseaux de neurones non récurrents. On choisit d'étudier le comportement asymptotique de ces réseaux. Dans ce cadre, les algorithmes évolutionnaires sont des outils puissants permettant d'entrainer un réseau pour qu'il approche une fonction donnée.
  • Keywords:

    Genetic Algorithms, Evolutionary Algorithms, Neural Networks, Learning, Recurrent Networks, Continuous Optimization, Antenna Arrays.
  • Keywords (in french):

    Algorithmes génétiques, Algorithmes évolutionnaires, Réseaux de neurones, Apprentissage, Réseaux récurrents, Optimisation réelle, Réseaux d'antennes.
  • Availability: Paper copy available.
  • Size: 127p
  • Format: Compressed PostScript
  • Get it

Une calcul de constructions infinies et son application à la vérification de systèmes communicants.

  • By: Eduardo Gimenez
  • Number: PhD1996-11
  • Date: December 1996
  • Abstract:

    Computer programs can be conceptually classified into transformational programs and reactive programs. Transformational programs are programs whose goal it is to compute an output value from certain input data. Termination is a key property for transformational programs, since it is a necessary condition to actually obtain the result we expect from it a value. On the contrary, a reactive program is a program whose role is to maintain an ongoing interaction with its environment, for example to control the execution of some process external to the program. For reactive programs, termination is no longer essential. When studying communicating systems, we are frequently faced with reasoning about different kind of infinite objects (interactive loops, infinite inputs, infinite spaces of states, etc.). This motivated us in the idea that the verification of reactive systems could be more easily developed into a logical framework capable of talking and expressing reasoning about infinite objects. During the last 15 years, some type theories like the Calculus of Constructions have arisen as a very interesting logical framework for program verification. However, these theories does not provide the description of infinite objects in a simple and direct way. In this thesis we develop an extension of the Calculus of Constructions with types that may contain infinite objects (the so-called co-inductive types). Our calculus is based on the guarded recursive definition schemes proposed by Thierry Coquand in the framework of Martin-L"of's type theory. The idea underlying this extension is to pursue the analogy ``proofs as functional programs''offered by pure lambda calculus to the notion of datatype provided by functional programming languages. In this way, infinite structures may be described in the same way as they are in some lazy programming languages, like Haskell. Opposite to Coquand's proposal, our extension preserves normalization, which is a crucial property for its implementation. This extension has been implemented in the version V6.1 of the Coq proof environment. Using this prototype, we have tested its potentialities as logical framework for the verification of reactive programs : we have study a simple communication protocol through an unreliable channel (the alternating bit protocol) and developped a certified interpreter for a CCS-like calculus of processes starting from a constructive proof of its specification.
  • Abstract (in french):

    Conceptuellement, on distingue deux sortes de programmes : les programmes séquentiels et les programmes réactifs. Dans les programmes séquentiels, le but est de calculer une donnée de sortie à partir de certaines données d'entrée. Pour cela, la terminaison du calcul joue un rôle crucial. En revanche, les programmes réactifs doivent contrôler ou maintenir une certaine interaction avec leur environnement, par exemple, pour contrôler un certain processus physique externe à l'ordinateur. Pour ce type d'activité, la terminaison du programme n'est plus essentielle. Dans les programmes réactifs, la considération de calculs qui ne finissent pas nous amène très vite à considérer également des types de structures infinies (listes de données infinies, espaces d'états infinis, etc.). Cette constatation motive l'idée que la vérification de programmes réactifs nécessite un cadre logique dans lequel on est capable de décrire et de raisonner sur des objets infinis. Pendant les 15 dernières années, des théories de types très expressives comme le Calcul des Constructions se sont révélées être un cadre particulièrement adapté à la vérification de programmes. Néanmoins, ces théories ne permettent pas de décrire des objets avec une structure non-bornée de manière simple. Dans cette thèse, nous développons une extension du Calcul des Constructions avec des types qui peuvent contenir des objets infinis (dits types co-inductifs). Notre calcul se base sur les schémas de définition récurrente gardée développés par Thierry Coquand dans le cadre de la théorie des types de Martin-L"of TC93. L'idée de base dans cette extension est de de poursuivre l'analogie ``preuves comme programmes fonctionnels'' du lambda calcul à la notion de type de donnée utilisée dans le langages de programmation fonctionnelle. Ainsi, des structures infinies peuvent être décrites de manière semblable à comme cela est fait dans les langages fonctionnels paresseux, tels que Haskell. A la différence de celle proposée par T. Coquand, notre extension préserve la propriété de normalisation forte, indispensable pour son implantation. Elle a été intégrée à la version V6.1 de l'éditeur de preuves Coq. Avec ce prototype, nous avons testé les potentialités de ce cadre logique pour la vérification de systèmes réactifs : nous avons étudié un protocole de communication de données à travers un canal de communication non-sûre, et la génération d'un simulateur interactif de processus à partir d'une preuve constructive de sa spécification.
  • Keywords:

    Constructive Type Theory, Co-inductive Types, Program Verification, Communicating Systems.
  • Keywords (in french):

    Théorie constructive des types, Types co_inductifs, Vérification de programmes, systèmes communicants.
  • Availability: Out of print.
  • Size: 186p
  • Format: Compressed PostScript
  • Get it