La compilation traditionnelle est confrontée à de nombreux défis face aux besoins d'optimisations de programmes pour architectures parallèles. Un défi particulier est la conception de langages et représentations intermédiaires (RIs) appropriés.Bien que différentes RIs aient été proposées pour repousser les limites de la compilation traditionnelle, la plupart ne sont toujours pas adaptées pour appliquer des transformations de programmes pertinentes.Différentes alternatives sont donc de plus en plus exploitées, telles que l'autotuning ou la compilation interactive. Ces dernières nécessitent l'usage de langages intermédiaires fondamentalement différents, par exemple, les méta-langages pour la transformation de programmes. Dans cette thèse, centrée sur les besoins en applications numériques, nous étudions ce type de meta-langages; nous adressons particulièrement quatre questions:(i) Comment introduire une expressivité spécifique à un domaine?(ii) Comment repenser leur conception pour améliorer leur flexibilité dans la composition de transformations et la génération de plusieurs variantes de programme?(iii) Jusqu'où pouvons-nous introduire du support pour le NUMA (Non-Uniform Memory Access)?(iv) En tant que nouvelle classe de méta-langages, comment formaliser leur sémantique? Nous répondons à ces questions au travers de la conception et la sémantique de TeML, un méta-langage pour l'optimisation d'applications tensorielles. / Traditional compilation faces numerous challenges with program optimizations for parallel architectures. A particular challenge is the design of proper intermediate languages and representations to enable the application of relevant optimization techniques.Various parallel intermediate representations and languages have been proposed.To overcome this issue, different alternatives are more and more exploitedsuch as empirical autotuning or interactive compilation. Such alernatives require fondamentally different typesof intermediates languages such as transformation meta-languages. In this thesis, we study transformation meta-languages for numerical applications: wa particularly address four questions:(i) How do we introduce domain-specific expressiveness?(ii) How do we rethink their design to enhance their flexibility in composing optimizations paths and generating multiple program variants?(iii) How far can we introduce NUMA (Non-Uniform Memory Access) awareness?(iv) As a new class of meta-languages, how do we formalize their semantics? We answer these questions through the design and semantics of TeML, a tensor optimizations meta-language.

Le calcul massivement parallèle a connu durant ces deux dernières décennies un fort développement. Les efforts dans ce domaine ont d'abord surtout été orientés vers les machines, plutôt qu'à la définition de langages adaptés au parallélisme massif. Par la suite, deux principaux modèles de programmation ont émergé : le parallélisme de contrôle et le parallélisme de données. Le premier a connu un vif succès. Dans ce modèle cependant, les applications massivement parallèles s'avèrent difficiles à concevoir et peu fiables, compte tenu du grand nombre de processus envisagés. En revanche, le parallélisme de données paraît aujourd'hui être un bon compromis entre les besoins des utilisateurs et les contraintes imposées par les architectures parallèles. 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.

Cette these decrit la definition et la mise en oeuvre dun langage de programmation pour bases de donnees : le langage a objets Peplom (PErsistent Programming Language for Object Management). Lapproche adoptee a pour but doffrir une su^rete importante du langage, une implementation efficace et de la flexibilite pour le schema des definitions (types, modules, etc...). Le langage propose nest pas totalement nouveau puisquil est syntaxiquement base sur le langage C/C++ ce qui lui confere une conformite avec les standards. La these presente dans un premier temps un etat de lart en deux parties. La premiere partie sattache a etudier les systemes de types sous langle des modeles de memoire necessaires a leur implantation. La deuxieme partie analyse les SGBD a objets existants et les compare suivant un certain nombre de criteres. Le langage Peplom est ensuite decrit en insistant surtout sur leffort dintegration de concepts. Un typage fort et lintroduction orthogonale des concepts bases de donnees dans le langage de programmation lui confere une grande su^rete. Par ailleurs, Peplom apporte une solution interessante au probleme de structuration des programmes qui seffectue a deux niveaux : les types abstraits structurent les definitions des entites modelisees alors que les modules structurent les donnees manipulees. La production de programmes avec le langage Peplom seffectue en deux phases. La premiere phase consiste a saisir les definitions composant lapplication. Celles-ci sont memorisees de maniere incrementale dans un dictionnaire gere par le compilateur. Le dictionnaire autorise les incoherences transitoires de la description des programmes, offrant ainsi une grande flexibilite pour le programmeur et une bonne base pour levolution de schemas. La deuxieme phase realise la generation dapplications executables. Le generateur produit du code supportant le modele structurel et semantique des donnees. Il sappuie sur la couche systeme consistant simplement en un gestionnaire de memoire (persistante et temporaire). Les performances du prototype implante sont comparables a celles des systemes C++ persistants offrant moins de fonctionnalites.

RDF est un langage de représentation des connaissances dédié à l'annotation des ressources dans le Web Sémantique. Bien que RDF peut être lui-même utilisé comme un langage de requêtes pour interroger une base de connaissances RDF (utilisant la conséquence RDF), la nécessité d'ajouter plus d'expressivité dans les requêtes a conduit à définir le langage de requêtes SPARQL. Les requêtes SPARQL sont définies à partir des patrons de graphes qui sont fondamentalement des graphes RDF avec des variables. Les requêtes SPARQL restent limitées car elles ne permettent pas d'exprimer des requêtes avec une séquence non-bornée de relations (par exemple, Existe-t-il un itinéraire d'une ville A à une ville B qui n'utilise que les trains ou les bus?"). Nous montrons qu'il est possible d'étendre la syntaxe et la sémantique de RDF, définissant le langage PRDF (pour Path RDF) afin que SPARQL puisse surmonter cette limitation en remplaçant simplement les patrons de graphes basiques par des graphes PRDF. Nous étendons aussi PRDF à CPRDF (pour Constrained Path RDF) permettant d'exprimer des contraintes sur les sommets des chemins traversés (par exemple, "En outre, l'une des correspondances doit fournir une connexion sans fil."). Nous avons fourni des algorithmes corrects et complets pour répondre aux requêtes (la requête est un graphe PRDF ou CPRDF, la base de connaissances est un graphe RDF) basés sur un homomorphisme particulier, ainsi qu'une analyse détaillée de la complexité. Enfin, nous utilisons les graphes PRDF ou CPRDF pour généraliser les requêtes SPARQL, définissant les extensions PSPARQL et CPSPARQL, et fournissons des tests expérimentaux en utilisant une implémentation complète de ces deux langages.

Cette thèse concerne la modélisation des Systèmes d'Information Coopératifs (SICo). Les techniques de modélisation proposées par les langages actuels ne donnent pas de réponses directes aux différents problèmes posés par la modélisation des SICo. Pour mieux contrôler la complexité de ces derniers, il est nécessaire d'avoir un niveau d'abstraction élevé et de disposer de modèles qui s'approchent du modèle de raisonnement du développeur. Nous avons choisi la solution des architectures logicielles pour organiser l'ingénierie des SICo. Une telle approche offre au concepteur des techniques et des langages de modélisation permettant d'exprimer les propriétés des systèmes composants et de leurs interactions. La solution que nous proposons repose sur un guide méthodologique permettant de capitaliser, organiser et réutiliser des modèles d'architectures logicielles adaptés aux SICo. Ce guide méthodologique traite quatre aspects complémentaires. Premièrement, il propose des patrons produit capitalisant des familles d'architectures de coopération. Deuxièmement, il offre une représentation graphique et textuelle des solutions modèles en utilisant respectivement un langage semi-formel et un langage formel. Ensuite, il facilite la classification des SICo en se basant sur différents modes de coopération entre des systèmes composants. Enfin, il propose des patrons processus formalisant la démarche méthodologique. Patrons produits et patrons processus constituent le système de Patrons pour les Architectures COopératives (PACO).

Les analogies auxquelles nous nous intéressons mettent quatre chaînes de symboles en proportion, par exemple, fable : fabuleux :: miracle : miraculeux ou abc : aabbcc :: a^n.b^n.c^n : a^n+1.b^n+1.c^n+1. Une étude historique de l'analogie en linguistique nous a permis de dégager les deux articulations (conformité et rapport) et les notions constitutives (similarité et contiguïté) de ce type d'analogie. De postulats généraux nous avons tiré une caractérisation formelle (encore partielle) rendant compte de la commutation entre chaînes de symboles. Une application directe est la conjugaison automatique par analogie. Nous avons proposé de définir certains langages formels à l'aide de ce type d'analogie. La grammaticalité, c'est-à-dire l'appartenance à un langage, est testée par égalité avec certaines chaînes attestées après réduction selon des modèles analogiques, eux aussi attestés. L'absence de non-terminaux fait de ce type de grammaires des grammaires par l'exemple. Nous examinons la possible place de tels langages dans le débat sur l'adéquation des langages formels à la description des langues. En forçant la conservation des analogies entre deux langages de chaînes analogiques, on obtient une méthode générale applicable à divers problèmes du traitement automatique des langues, par exemple, l'analyse structurale ou la traduction automatique de phrases.

Thesis (Ph. D.)--University of Sussex, 1990. / Includes bibliographical references (p. 265-271) and index.

Cette thèse traite de la conception et implémentationd’un langage de programmation pour les systèmes detraitement de flux en temps réel, comme l’encodagevidéo. Le modèle des réseaux de Kahn est bien adaptéà ce domaine et y est couramment utilisé. Dans cemodèle, un programme consiste en un ensemble deprocessus parallèles communicant à travers des filesmono-producteur, mono-consommateur. La force dumodèle réside en son déterminisme.Les langages synchrones fonctionnels comme Lustresont dédiés aux systèmes embarqués critiques. Un programmeLustre définit un réseau de Kahn synchronequi peut être exécuté avec des files bornées et sans blocage.Cette propriété est garantie par un système detypes dédié, le calcul d’horloge, qui établit une échellede temps globale à un programme. Cette échelle detemps globale est utilisée pour définir les horloges, sé-quences booléennes indiquant pour chaque file, et àchaque pas de temps, si un processus produit ou consommeune donnée. Cette information sert non seulementà assurer la synchronie mais également à générerdu logiciel ou matériel à état fini.Nous proposons et étudions les horloges entières, unegénéralisation des horloges booléennes autorisant desentiers naturels arbitrairement grands. Les horlogesentières décrivent la production ou consommation deplusieurs valeurs depuis une même file au cours d’uninstant. Nous les utilisons pour définir la constructiond’échelle de temps locale, qui peut masquer despas de temps cachés par un sous-programme au contexteenglobant.Ces principes sont intégrés à un calcul d’horloge pourun langage fonctionnel d’ordre supérieur. Nous étudionsses propriétés et prouvons en particulier que lesprogrammes bien typés ne bloquent pas. Nous compilonsles programmes typés vers des circuits numériquessynchrones en adaptant le schéma de générationde code dirigé par les horloges de Lustre. L’informationde typage contrôle certains compromis entre temps etespace dans les circuits générés. / This thesis addresses the design and implementationof a programming language for real-time streaming applications,such as video decoding. The model of Kahnprocess networks is a natural fit for this area and hasbeen used extensively. In this model, a program consistsin a set of parallel processes communicating via singlereader, single writer queues. The strength of the modellies in its determinism.Synchronous functional languages such as Lustre arededicated to critical embedded systems. A Lustre programdefines a synchronous Kahn process network, thatis, which can be executed using finite queues and withoutdeadlocks. This is enforced by a dedicated type system,the clock calculus, which establishes a global timescale throughout a program. The global time scale isused to define clocks: per-queue boolean sequences indicating,for each time step, whether a process producesor consumes a token in the queue. This information isused both for enforcing synchrony and for generatingfinite-state software or hardware.We propose and study integer clocks, a generalizationof boolean clocks featuring arbitrarily big natural numbers.Integer clocks model the production or consumptionof several values from the same queue in the courseof a time step. We then rely on integer clocks to definethe local time scale construction, which may hide timesteps performed by a sub-program from the surroundingcontext.These principles are integrated into a clock calculus fora higher-order functional language. We study its properties,proving among other results that well-typed programsdo not deadlock. We adjust the clock-directedcode generation scheme of Lustre to generate finite-statedigital synchronous circuits from typed programs. Thetyping information controls certain trade-offs betweentime and space in the generated circuits.

Cette thèse adresse les problèmes d'universalité et de complétude computationelle pour plusieurs modèles de calcul inspirés par la biologie. Il s'agit principalement des systèmes d'insertion/effacement, réseaux de processeurs évolutionnaires, ainsi que des systèmes de réécriture de multi-ensembles. Les résultats décrits se classent dans deux catégories majeures : l'étude de la puissance de calcul des opérations d'insertion et d'effacement avec ou sans mécanismes de contrôle, et la construction des systèmes de réécriture de multi-ensembles universels de petite taille. Les opérations d'insertion et d'effacement consistent à rajouter ou supprimer une sous-chaîne dans une chaîne de caractères dans un contexte donné. La motivation pour l'étude de ces opérations vient de la biologie, ainsi que de la linguistique et de la théorie des langages formels. Dans la première partie de ce manuscrit nous examinons des systèmes d'insertion/effacement correspondant à l'édition de l'ARN, un processus qui insère ou supprime des fragments de ces molécules. Une particularité importante de l'édition de l'ARN est que le endroit auquel se font les modifications est déterminé par des séquences de nucléotides se trouvant toujours du même côté du site de modification. En termes d'insertion et d'effacement, ce phénomène se modéliserait par des règles possédant le contexte uniquement d'un seul côté. Nous montrons qu'avec un contexte gauche de deux caractères il est possible d'engendrer tous les langages rationnels. D'autre part, nous prouvons que des contextes plus longs n'augmentent pas la puissance de calcul du modèle. Nous examinons aussi les systèmes d’insertion/effacement utilisant des mécanismes de contrôle d’application des règles et nous montrons l'augmentation de la puissance d'expression. Les opérations d'insertion et d'effacement apparaissent naturellement dans le domaine de la sécurité informatique. Comme exemple on peut donner le modèle des grammaires gauchistes (leftist grammar), qui ont été introduites pour l'étude des systèmes critiques. Dans cette thèse nous proposons un nouvel instrument graphique d'analyse du comportement dynamique de ces grammaires. La deuxième partie du manuscrit s'intéresse au problème d'universalité qui consiste à trouver un élément concret capable de simuler le travail de n'importe quel autre dispositif de calcul. Nous commençons par le modèle de réseaux de processeurs évolutionnaires, qui abstrait le traitement de l'information génétique. Nous construisons des réseaux universels ayant un petit nombre de règles. Nous nous concentrons ensuite sur les systèmes de réécriture des multi-ensembles, un modèle qui peut être vu comme une abstraction des réactions biochimiques. Pour des raisons historiques, nous formulons nos résultats en termes de réseaux de Petri. Nous construisons des réseaux de Petri universels et décrivons des techniques de réduction du nombre de places, de transitions et d'arcs inhibiteurs, ainsi que du degré maximal des transitions. Une bonne partie de ces techniques repose sur une généralisation des machines à registres introduite dans cette thèse et qui permet d'effectuer plusieurs tests et opérations en un seul changement d'état / The present thesis considers the problems of computational completeness and universality for several biologically-inspired models of computation: insertion-deletion systems, networks of evolutionary processors, and multiset rewriting systems. The presented results fall into two major categories: study of expressive power of the operations of insertion and deletion with and without control, and construction of universal multiset rewriting systems of low descriptional complexity. Insertion and deletion operations consist in adding or removing a subword from a given string if this subword is surrounded by some given contexts. The motivation for studying these operations comes from biology, as well as from linguistics and the theory of formal languages. In the first part of the present work we focus on insertion-deletion systems closely related to RNA editing, which essentially consists in inserting or deleting fragments of RNA molecules. An important feature of RNA editing is the fact that the locus the operations are carried at is determined by certain sequences of nucleotides, which are always situated to the same side of the editing site. In terms of formal insertion and deletion, this phenomenon is modelled by rules which can only check their context on one side and not on the other. We show that allowing one-symbol insertion and deletion rules to check a two-symbol left context enables them to generate all regular languages. Moreover, we prove that allowing longer insertion and deletion contexts does not increase the computational power. We further consider insertion-deletion systems with additional control over rule applications and show that the computational completeness can be achieved by systems with very small rules. The motivation for studying insertion-deletion systems also comes from the domain of computer security, for the purposes of which a special kind of insertion-deletion systems called leftist grammars was introduced. In this work we propose a novel graphical instrument for visual analysis of the dynamics of such systems. The second part of the present thesis is concerned with the universality problem, which consists in finding a fixed element able to simulate the work any other computing device. We start by considering networks of evolutionary processors (NEPs), a computational model inspired by the way genetic information is processed in the living cell, and construct universal NEPs with very few rules. We then focus on multiset rewriting systems, which model the chemical processes running in the biological cell. For historical reasons, we formulate our results in terms of Petri nets. We construct a series of universal Petri nets and give several techniques for reducing the numbers of places, transitions, inhibitor arcs, and the maximal transition degree. Some of these techniques rely on a generalisation of conventional register machines, proposed in this thesis, which allows multiple register checks and operations to be performed in a single state transition

Cette thèse traite des ensembles rationnels de mots indexés par des ordres linéaires et en particulier du problème de la fermeture par complémentation. Dans un papier fondateur de 1956, Kleene initie la théorie des langages en montrant que les automates sur les mots finis et les expressions rationnelles ont le même pouvoir d'expression. Depuis, ce résultat a été étendu à de nombreuses structures telles que les mots infinis (Büchi, Muller), bi-infinis (Beauquier, Nivat, Perrin), les mots indexés par des ordinaux (Büchi, Bedon), les traces, les arbres... Plus récemment, Bruyère et Carton ont introduit des automates acceptant des mots indexés par des ordres linéaires et des expressions rationnelles correspondantes. Ces structures linéaires comprennent les mots infinis, les mots indexés par des ordinaux et leurs miroirs. Le théorème de Kleene a été généralisé aux mots indexés par les ordres linéaires dénombrables et dispersés, c'est-à-dire les ordres ne contenant pas de sous-ordre isomorphe à Q. Pour la plupart des structures, la classe des ensembles rationnels forme une algèbre de Boole. Cette propriété est nécessaire pour traduire une logique en automates. La fermeture par complémentation restait un problème ouvert. Dans cette thèse, on résout ce problème de façon positive: on montre que le complément d'un ensemble rationnel de mots indexés par des ordres linéaires dispersés est rationnel. La méthode classique pour obtenir un automate acceptant le complémentaire d'un ensemble rationnel se fait par déterminisation. Nous montrons que cette méthode ne peut-être appliquée dans notre cas: tout automate n'est pas nécessairement équivalent à un automate déterministe. Nous avons utilisé d'autres approches. Dans un premier temps, nous généralisons la preuve de Büchi, basée sur une congruence de mots, et obtenons ainsi la fermeture par complémentation dans le cas des ordres linéaires de rang fini. Pour obtenir le résultat dans le cas général, nous utilisons l'approche algébrique. Nous développons une structure algébrique qui étend la reconnaissance classique par semigroupes finis : les semigroupes sont remplacés par les diamant-semigroupes qui possèdent un produit généralisé. Nous prouvons qu'un ensemble est rationnel si et seulement s'il est reconnu par un diamant-semigroupe fini. Nous montrons aussi qu'un diamant-semigroupe canonique, appelé diamant-semigroupe syntaxique, peut être associé à chaque ensemble rationnel. Notre preuve de la complémentation est effective. Le théorème de Schützenberger établit qu'un ensemble de mots finis est sans étoile si et seulement si son semigroupe syntaxique est fini et apériodique. Pour finir, nous étendons partiellement ce résultat au cas des ordres de rang fini.