▼ 

Les systèmes embarqués et objets connectés sont aujourd'hui de plus en plus répandus. Contrairement à d'autres systèmes accessibles uniquement par le réseau, les systèmes embarqués sont accessibles physiquement par un attaquant. Celui ci peut alors exploiter cette proximité physique pour monter des attaques par canaux auxiliaires afin de compromettre ces systèmes ou leurs données. Ces attaques non intrusives ont ainsi montré une grande efficacité pour récupérer les clés cryptographiques utilisées dans de tels systèmes. Il est alors primordial de protéger les systèmes embarqués contre cette menace sérieuse. Les contre-mesures logicielles sont la plupart du temps appliquées manuellement par des experts. Dans cette thèse, nous proposons d'appliquer automatiquement ces contre-mesures au sein du processus de compilation. Nous proposons deux approches, l'une pour appliquer une contre-mesure de masquage booléen de premier ordre, l'autre pour appliquer une contre-mesure de polymorphisme de code. Nous apportons des réponses à plusieurs problèmes liés à la génération dynamique de code pour permettre l'utilisation du polymorphisme de code sur des systèmes contraints. Enfin, nous adaptons les contre-mesures choisies afin d'obtenir de meilleurs compromis entre les performances et la sécurité.

Embedded systems and connected objects are increasingly used nowadays. Unlike some other systems accessible only through the network, embedded systems are physically accessible by an attacker. The latter can then exploit this physical proximity to mount side-channel attacks to compromise these systems or their data. These non-intrusive attacks have shown great effectiveness in recovering cryptographic keys used in such systems. Embedded systems must therefore be secured against this severe threat. Software countermeasures are most often applied manually by experts. In this thesis, we propose to automatically apply these countermeasures within the compilation process. We propose two approaches, one to apply a first-order Boolean masking countermeasure, the other to apply a code polymorphism countermeasure. We address several problems related to dynamic code generation to enable the use of code polymorphism on constrained systems. Finally, we adapt the chosen countermeasures to obtain a better trade-off between performance and security.

Advisors/Committee Members: Charles, Henri-Pierre (thesis director), Heydemann, Karine (thesis director), Couroussé, Damien (thesis director), Heydemann, Karine (thesis director).

▼ 

Les compilateurs optimisants pour les langages de programmation sont devenus des logiciels complexes et donc une source de bugs. Ceci peut être dangereux dans le contexte de systèmes critiques comme l'avionique ou la médecine. Cette thèse s'inscrit dans le cadre de la compilation vérifiée optimisante dont l'objectif est d'assurer l'absence de tels bugs. Plus précisément, nous étudions sémantiquement une représentation intermédiaire SSA (Single Static Assignment) particulière, Sea of Nodes, utilisée notamment dans le compilateur optimisant HotSpot pour Java. La propriété SSA a déjà été étudiée d'un point de vue sémantique sur des représentations simples sous forme de graphe de flot de contrôle, mais le sujet des dépendances entre instructions a seulement été effleuré depuis une perspective formelle. Cette thèse apporte une étude sémantique de transformations de programmes sous forme Sea of Nodes, intégrant la flexibilité en termes de dépendances de données entre instructions. En particulier, élimination de zero-checks redondants, propagation de constantes, retour au bloc de base séquentiel et destruction de SSA sont étudiés. Certains des sujets abordés, dont la formalisation d'une sémantique pour Sea of Nodes, sont accompagnés d'une vérification à l'aide de l'assistant de preuve Coq.

Optimizing compilers for programming languages have become complex software, and they are hence subject to bugs. This can be dangerous in the context of critical systems such as avionics or health care. This thesis is part of research work on verified optimizing compilers, whose objective is to ensure the absence of such bugs. More precisely, we semantically study a particular SSA intermediate representation, Sea of Nodes, which is notably used in the optimizing compiler HotSpot for Java. The SSA property has already been studied from a semantic point of view on simple intermediate representations in control flow graph form, but the subject of dependencies between instructions has just been skimmed from a formal perspective. This thesis brings a semantic study of transformations of programs in Sea of Nodes form, integrating the flexibility regarding data dependencies between instructions. In particular, redundant zero-check elimination, constant propagation, transformation back to sequential basic block, and SSA destruction are studied. Some of the approached topics, including the formalization of a semantics for Sea of Nodes, are accompanied by a verification using the Coq proof assistant.

Advisors/Committee Members: Pichardie, David (thesis director), Demange, Delphine (thesis director).

▼ 

La compilation est une étape indispensable dans la création d'applications performantes.Cette étape autorise l'utilisation de langages de haut niveau et indépendants de la cible tout en permettant d'obtenir de bonnes performances.Cependant, de nombreux freins empêchent les compilateurs d'optimiser au mieux les applications.Pour les compilateurs statiques, le frein majeur est la faible connaissance du contexte d'exécution, notamment sur l'architecture et les données utilisées.Cette connaissance du contexte se fait progressivement pendant le cycle de vie de l'application.Pour tenter d'utiliser au mieux les connaissances du contexte d'exécution, les compilateurs ont progressivement intégré des techniques de génération de code dynamique.Cependant ces techniques ne se focalisent que sur l'utilisation optimale du matériel et n'utilisent que très peu les données.Dans cette thèse, nous nous intéressons à l'utilisation des données dans le processus d'optimisation d'applications pour GPU Nvidia.Nous proposons une méthode utilisant différents moments pour créer des bibliothèques adaptatives capables de prendre en compte la taille des données.Ces bibliothèques peuvent alors fournir les noyaux de calcul les plus adapté au contexte.Sur l'algorithme de la GEMM, la méthode permet d'obtenir des gains pouvant atteindre 100~% tout en évitant une explosion de la taille du code.La thèse s'intéresse également aux gains et coûts de la génération de code lors de l'exécution, et ce du point de vue de la vitesse d'exécution, de l'empreinte mémoire et de la consommation énergétique.Nous proposons et étudions 2 approches de génération de code à l'exécution permettant la spécialisation de code avec un faible surcoût.Nous montrons que ces 2 approches permettent d'obtenir des gains en vitesse et en consommation comparables, voire supérieurs, à LLVM mais avec un coût moindre.

Compilation is an essential step to create efficient applications.This step allows the use of high-level and target independent languages while maintaining good performances.However, many obstacle prevent compilers to fully optimize applications.For static compilers, the major obstacle is the poor knowledge of the execution context, particularly knowledge on the architecture and data.This knowledge is progressively known during the application life cycle.Compilers progressively integrated dynamic code generation techniques to be able to use this knowledge.However, those techniques usually focuses on improvement of hardware capabilities usage but don't take data into account.In this thesis, we investigate data usage in applications optimization process on Nvidia GPU.We present a method that uses different moments in the application life cycle to create adaptive libraries able to take into account data size.Those libraries can therefore provide more adapted kernels.With the GEMM algorithm, the method is able to provide gains up to 100~% while avoiding code size explosion.The thesis also investigate runtime code generation gains and costs from the execution speed, memory…

Advisors/Committee Members: Charles, Henri-Pierre (thesis director).

▼ 

Les processeurs multi-coeurs sont maintenant largement utilisés presque partout en informatique: ordinateurs de bureau, ordinateurs portables et accélérateurs tels que les GPGPU (General Purpose Graphics Processing Units). La difficulté de la programmation des systèmes parallèles est considérée comme un problème majeur qui va empêcher l'exploitation de leurs capacités dans le futur. Pour exploiter la puissance des processeurs multi-coeurs et les hiérarchies complexes de mémoire, il y a une grande nécessité pour utiliser des outils de parallélisation et d'optimisation automatique de code. L'optimisation polyédrique est un axe de recherche qui a comme but de résoudre ces problèmes. C'est est une représentation algébrique du programme et un ensemble d'analyses, de transformations et d'algorithmes de génération de code qui permettent à un compilateur de raisonner sur des transformations avancées de nids de boucle. Dans cette thèse, nous abordons certaines des limites du modèle polyédrique. Nous nous intéréssons particulièrement à trois problèmes et nous proposons des solutions pratiques à ces trois problèmes. Le premier problème est lié à la capacité d'appliquer l'optimisation de tuilage sur un code qui contient des fausses dépendances. Nous proposons une téchnique qui permet d'ignorer certaines fausses dépendences et donc qui permet d'appliquer l'optimisation de tuilage qui n'est pas possible sinon. Le second problème est lié au temps de compilation qui peut être trés long pour certains programmes. Nous proposons une téchnique qui transforme la représentation originale du programme à une nouvelle representation dans laquelle il y a moins d'instructions. L'optimisation de cette nouvelle représentation du programme est moins couteuse en terme de temps de compilation en comparaison avec l'optimisation de la représentation originale du programme. Le troisième problème est lié à deux limites: la première limite concerne la possibilité d'utiliser la compilation polyédrique sur des programmes qui ne resepectent pas les restrictions classiques du modèle polyédrique (un programme peut être représenté de façon précise dans le modèle polyédrique s'il ne contient pas des conditionnelles non-affines, des bornes de boucles non-affines et des accés non-affines). La seconde limite est liée à l'aptitude des outils à générer un code performant dans les performances se rapprochent des performances du code écrit à la main. Pour éviter ces deux limites, nous proposons un language de programmation que l'on appelle PENCIL, c'est un sous-ensemble de GNU C99 avec des règles de programmation spécifiques et quelques extensions. L'utilisation de ce sous-ensemble et l'utilisation de ces extensions permettent aux compilateurs de mieux exploiter le parallélisme et de mieux optimiser le code.

Multi-core processors are now in widespread use in almost all areas of computing: desktops, laptops and accelerators such as GPGPUs (General Purpose Graphics Processing Units). To harness the power of multi-core processors and complex memory hierarchies, the…

Advisors/Committee Members: Cohen, Albert Henri (thesis director), Verdoolaege, Sven (thesis director).

▼ 

In this dissertation we present a simple and scalable system for validating the correctness of low-level program transformations. Proving that program transformations are correct is crucial to the development of security critical software tools. We achieve a simple and scalable design by compiling sequential low-level programs to synchronous data-flow programs. Theses data-flow programs are a denotation of the original programs, representing all of the relevant aspects of the program semantics. We then check that the two denotations are equivalent, which implies that the program transformation is semantics preserving. Our denotations are computed by means of symbolic analysis. In order to achieve our design, we have extended symbolic analysis to arbitrary control-flow graphs. To this end, we have designed an intermediate language called Synchronous Value Graphs (SVG), which is capable of representing our denotations for arbitrary control-flow graphs, we have built an algorithm for computing SVG from normal assembly language, and we have given a formal model of SVG which allows us to simplify and compare denotations. Finally, we report on our experiments with LLVM M.D., a prototype denotational translation validator for the LLVM optimization framework.

Engineering and Applied Sciences

Advisors/Committee Members: Morrisett, John Gregory (advisor), Smith, Michael (committee member), Chong, Stephen (committee member).

▼ 

L'évolution du calcul haute performance est aujourd'hui dirigée par les besoins des applications de simulation numérique.Ces applications sont exécutées sur des supercalculateurs qui peuvent proposer plusieurs milliers de cœurs, et qui sont découpés en un très grand nombre de nœuds de calcul ayant eux un nombre de cœurs beaucoup plus faible.Chacun de ces nœuds de calcul repose sur une architecture à mémoire partagée, dont la mémoire est découpée en plusieurs blocs physiques différents : cela implique un temps d'accès dépendant à la fois de la donnée accédée ainsi que du processeur y accédant.On appelle ce genre d'architectures NUMA (pour emph{Non Uniform Memory Access}).La manière actuelle de les exploiter tend vers l'utilisation d'un modèle de programmation à base de tâches, qui permet de traiter des programmes irréguliers au delà du simple parallélisme de boucle.L'exploitation efficace des machines NUMA est critique pour l'amélioration globale des performances des supercalculateurs.Cette thèse a été axée sur l'amélioration des techniques usuelles pour leur exploitation : elle propose une réponse au compromis qu'il faut faire entre localité des données et équilibrage de charge, qui sont deux points critiques dans l'ordonnancement d'applications.Les contributions de cette thèse peuvent se découper en deux parties : une partie dédiée à fournir au programmeur les moyens de comprendre, analyser, et mieux spécifier le comportement des parties critiques de son application, et une autre partie dédiée à différentes améliorations du support exécutif.Cette seconde partie a été évaluée sur différentes applications, ce qui a permis de montrer des gains de performances significatifs.

Nowadays the evolution of High Performance Computing follows the needs of numerical simulations.These applications are executed on supercomputers which can offer several thousands of cores, split into a large number of computing nodes, which possess a relatively low number of cores.Each of these nodes consists of a shared memory architecture, in which the memory is physically split into several distinct blocks: this implies that the memory access time depends both on which data is accessed, and on which core tries to access it.These architectures are named NUMA (for Non Uniform Memory Access).The current way to exploit them tends to be through a tasks-based programming model, which can handle irregular applications beyond a simple loop-based parallelism.Efficient use of NUMA architectures is critical for the overall performance improvements of supercomputers.This thesis has been targetted at improving common techniques for their exploitation: it proposes an answer to the tradeoff that has to be made between data locality and load balancing, that are two critical aspects of applications scheduling.Contributions of this thesis can be split into two parts: the first part is dedicated to providing the programmer with means to understand, analyze, and better characterize the behavior of their applications' critical parts, and the second part is…

Advisors/Committee Members: Rastello, Fabrice (thesis director).

▼ 

Cette thèse porte sur la sécurité des programmes et particulièrement en utilisant la compilation pour parvenir à ses fins. La compilation correspond à la traduction des programmes sources écrits par des humains vers du code machine lisible par nos systèmes. Nous explorons les deux manières possible de faire de la compilation sécurisée : la sécurisation et la préservation. Premièrement, nous avons développé CompCertSFI, un compilateur qui sécurise des modules en les isolant dans des zones mémoires restreintes appelées bac à sable. Ces modules sont ensuite incapables d'accéder à des zones mémoires hors de leur bac à sable, ce qui empêche un module malveillant de corrompre d'autres entités du système. Sur le sujet de la préservation, nous avons défini une notion de Préservation de Flot d'Information qui s'applique aux transformations de programme. Cette propriété, lorsqu'elle est appliquée, permet de s'assurer qu'un programme ne devienne moins sécurité durant sa compilation. Notre propriété de préservation est spécifiquement conçus pour préserver les protections contre les attaques de type canaux cachés. Cette nouvelle catégorie d'attaque utilise des médiums physique comme le temps ou la consommation d'énergie qui ne sont pas pris en compte par les compilateurs actuels.

Our society has been growingly dependent on computer systems and this tendency will not slow down in the incoming years. Similarly, interests over cybersecurity have been increasing alongside the possible consequences brought by successful attacks on these systems. This thesis tackles the issue of security of systems and especially focuses on compilation to achieve its goal. Compilation is the process of translating source programs written by humans to machine code readable by our systems. We explore the two possible behaviours of a secure compiler which are enforcement and preservation. First, we have developed CompCertSFI, a compiler which enforces the isolation of modules into closed memory areas called sandboxes. These modules are then unable to access memory regions outside of their sandbox which prevents any malicious module from corrupting other entities of the system. On the topic of security preservation, we defined a notion of Information Flow Preserving transformation to make sure that a program does get less secure during compilation. Our property is designed to preserve security against side-channel attacks. This new category of attacks uses physical mediums such as time or power consumption which are taken into account by current compilers.

Advisors/Committee Members: Jensen, Thomas (thesis director).

▼ This thesis studies how we can facilitate combined Haskell/Agda developments. As foundation for our research we have created the Agda UHC backend, targeting the intermediate Core language of the Utrecht Haskell Compiler. We will present a formal description of our translation scheme, which now powers all major Agda backends. Building upon our new backend, we introduce a Contract framework specifically aimed at the Foreign Function Interface (FFI). As with most FFI implementations, a major challenge are the different type systems of the languages involved. Our contract library provides a concise and powerful way to translate data between Agda foreign languages like Haskell. We also provide a formal specification of our contract framework, making it feasible to implement a similar scheme in other languages. Furthermore, we provide an improved Agda FFI interface for function calls which combines well with our Contract framework. Our contributions make Agda a more viable choice for applied dependently-typed programming and provide an elegant and novel solution for the FFI problem in a dependently typed setting. Advisors/Committee Members: Swierstra, W. S., Dijkstra, A..

▼ 

Cette thèse traite deux problèmes importants dans le domaine du raisonnement et de la décision dans l'incertain. En premier lieu, nous développons des méthodes d'inférence basées sur la compilation pour les réseaux possibilistes. En effet, nous commençons par adapter au cadre possibiliste l'approche de base proposée, initialement, pour les réseaux Bayésiens et nous la raffinons, ensuite en utilisant la notion de structure locale. Nous proposons aussi une nouvelle stratégie de codage appelée structure locale possibiliste appropriée dans le cadre qualitatif. Nous implémentons, par ailleurs, une méthode purement possibiliste basée sur la transformation des réseaux possibilistes en bases de connaissances possibilistes. Notre deuxième contribution consiste à étendre nos approches d'inférence dans le cadre des réseaux causaux afin de calculer l'effet des observations et des interventions d'une manière efficace. Nous confrontons, en particulier, des approches basées sur la mutilation et celles basées sur l'augmentation. Finalement, nous étudionsl'aspect décisionnel sous compilation en étendant nos résultats portant sur la compilation des réseaux possibilistes afin d'évaluer les diagrammes d'influence possibilistes. Une étude expérimentale évaluant les différentes approches étudiées dans cette thèse est également présentée.

This thesis addresses two important issues in reasoning and decision making under uncertainty. At first, we have developed compilation-based inference methods dedicated to possibilistic networks. In fact, we have adapted the standard approach initially proposed for Bayesian networks into a possibilistic framework and we have refined it using local structure. We havealso proposed a new encoding strategy, called possibilistic local structure, exclusively useful in a qualitative framework. Moreover, we have implemented a purely possibilistic approach based on transforming possibilistic networks into possibilistic knowledge bases. Our second contribution consists in extending our inference approaches to possibilistic causal networks in order to efficiently compute the impact of both observations and interventions. We have confronted, in particular, mutilated-based approaches and augmented-based ones. Finally, we have explored the decision-making aspect under compilation by extending our results on compiling possibilistic networks to efficiently evaluate possibilistic influence diagrams. An experimental study evaluating the different approaches studied in this thesis is also presented.

Advisors/Committee Members: Benferhat, Salem (thesis director), Ben Amor, Nahla (thesis director).

▼ Shannon’s and Chomsky’s attempts to model natural language with Markov chains showed differing gauges of language complexity. These were codified with the Chomsky Hierarchy with four types of languages, each with an accepting type of grammar and au- tomaton. Though still foundationally important, this fails to identify remarkable proper subsets of the types including recursive languages among recursively enumerable languages. In general, with Rice’s theorem, it is undecidable whether a Turing machine’s language is re- cursive. But specifically, Hopcroft & Ullman show that the languages of space bound Turing machines are recursive. We show the converse also to be true. The space hierarchy theorem shows that there is a continuum of proper subsets within the recursive languages. With Myhill’s description of a linear bounded automata, Landweber showed that they accept a subset of the type 1 languages including the type 2 languages. Kuroda expanded the definition making the automata nondeterministic and showed that nondeterministic linear space is the set of type 1 languages. That only one direction was proven deterministically but both nondeterministically, would suggest that nondeterminism increases expressiveness. This is further supported by Savitch’s theorem. However, it is not without precedent for predictions in computability theory to be wrong. Turing showed that Hilbert’s Entschei- dungsproblem is unsolvable and Immerman disproved Landweber’s belief that type 1 lan- guages are not closed under complementation. Currently, a major use of language theory is computer language processing including compilation. We will show that for the Java programming language, compilability can be computed in nondeterministic linear space by the existence of a (nondeterministic) linear bounded automaton which abstractly computes compilability. The automaton uses the tra- ditional pipeline architecture to transform the input in phases. The devised compiler will attempt to build a parse tree and then check its semantic properties. The first two phases, lexical and syntactical analysis are classic language theory tasks. Lexical analysis greedily finds matches to a regular language. Each match is converted to a token and printed to the next stream. With this, linearity is preserved. With a Lisp format, a parse tree can be stored as a character string which is still linear. Since the tree string preserves structural information from the program source, the tree itself serves as a symbol table, which normally would be separately stored in a readable efficient manner. Though more difficult than the previous step, this will also be shown to be linear. Lastly, semantic analysis, including typechecking, and reachability are performed by traversing the tree and annotating nodes. This implies that there must exist a context-sensitive grammar that accepts compilable Java. Therefore even though the execution of Java programs is Turing complete, their compilation is not. Advisors/Committee Members: Torben Amtoft.

▼ The modular design methodology has been widely adopted to harness the complexity of large FPGA-based systems. As a result, a number of commercial and academic tool flows emerged to support modular design including Hierarchical Design Flow and Partial Reconfiguration Flow, OpenPR, HMFlow, PARBIT, REPLICA, GoAhead and QFlow frameworks. As all of these projects have shown, a modular approach raises the abstraction level, provides clear boundaries for incremental design, reduces placement complexity, and improves productivity. At the physical layer, modules can be compiled into rectangular regions, suitable for placement on the FPGA fabric. Creating a design then becomes the process of placing all of the modules on the FPGA, followed by inter-module routing. FPGAs, however, are not homogenous, and the shape of individual modules could greatly impact overall device utilization. Prior work in modular assembly utilize modules with a single shape and aspect ratio in the assembly process. Due to the increasing size and heterogeneity of contemporary FPGAs, the placement flexibility of such a module is becoming increasingly limited. This thesis introduces a process that exploits offline shape generation and exploration, enabling the selection of shapes using criterias such as resource usage efficiency, placement flexibility, and device utilization. Module shapes can be generated with these criterias in mind while still taking advantage of the reduced placement complexity of modular design and assembly Advisors/Committee Members: Athanas, Peter M. (committeechair), Plassmann, Paul E. (committee member), McGwier, Robert W. (committee member).

▼ 

Le développement des systèmes massivement parallèles de type manycores permet d'obtenir une très grande puissance de calcul à bas coût énergétique. Cependant, l'exploitation des performances de ces architectures dépend de l'efficacité de programmation des applications. Parmi les différents paradigmes de programmation existants, celui à mémoire partagée est caractérisé par une approche intuitive dans laquelle tous les acteurs disposent d'un accès à un espace d'adressage global. Ce modèle repose sur l'efficacité du système à gérer les accès aux données partagées. Le système définit les règles de gestion des synchronisations et de stockage de données qui sont prises en charge par les protocoles de cohérence. Dans le cadre de cette thèse nous avons montré qu'il n'y a pas un unique protocole adapté aux différents contextes d'application et d'exécution. Nous considérons que le choix d'un protocole adapté doit prendre en compte les caractéristiques de l'application ainsi que des objectifs donnés pour une exécution. Nous nous intéressons dans ces travaux de thèse au choix des protocoles de cohérence en vue d'améliorer les performances du système. Nous proposons une plate-forme de compilation pour le choix et le paramétrage d'une combinaison de protocoles de cohérence pour une même application. Cette plate- forme est constituée de plusieurs briques. La principale brique développée dans cette thèse offre un moteur d'optimisation pour la configuration des protocoles de cohérence. Le moteur d'optimisation, inspiré d'une approche évolutionniste multi-objectifs (i.e. Fast Pareto Genetic Algorithm), permet d'instancier les protocoles de cohérence affectés à une application. L'avantage de cette technique est un coût de configuration faible permettant d'adopter une granularité très fine de gestion de la cohérence, qui peut aller jusqu'à associer un protocole par accès. La prise de décision sur les protocoles adaptés à une application est orientée par le mode de performance choisi par l'utilisateur (par exemple, l'économie d'énergie). Le modèle de décision proposé est basé sur la caractérisation des accès aux données partagées selon différentes métriques (par exemple: la fréquence d'accès, les motifs d'accès à la mémoire, etc). Les travaux de thèse traitent également des techniques de gestion de données dans la mémoire sur puce. Nous proposons deux protocoles basés sur le principe de coopération entre les caches répartis du système: Un protocole de glissement des données ainsi qu'un protocole inspiré du modèle physique du masse-ressort.

Manycores architectures consist of hundreds to thousands of embedded cores, distributed memories and a dedicated network on a single chip. In this context, and because of the scale of the processor, providing a shared memory system has to rely on efficient hardware and software mechanisms and data consistency protocols. Numerous works explored consistency mechanisms designed for highly parallel architectures. They lead to the conclusion that there won't exist one protocol that fits to all…

Advisors/Committee Members: Gogniat, Guy (thesis director).

▼ 

Depuis le début des années 2000, la performance brute des cœurs des processeurs a cessé son augmentation exponentielle. Les circuits graphiques (GPUs) modernes ont été conçus comme des circuits composés d'une véritable grille de plusieurs centaines voir milliers d'unités de calcul. Leur capacité de calcul les a amenés à être rapidement détournés de leur fonction première d'affichage pour être exploités comme accélérateurs de calculs généralistes. Toutefois programmer un GPU efficacement en dehors du rendu de scènes 3D reste un défi.La jungle qui règne dans l'écosystème du matériel se reflète dans le monde du logiciel, avec de plus en plus de modèles de programmation, langages, ou API, sans laisser émerger de solution universelle.Cette thèse propose une solution de compilation pour répondre partiellement aux trois "P" propriétés : Performance, Portabilité, et Programmabilité. Le but est de transformer automatiquement un programme séquentiel en un programme équivalent accéléré à l'aide d'un GPU. Un prototype, Par4All, est implémenté et validé par de nombreuses expériences. La programmabilité et la portabilité sont assurées par définition, et si la performance n'est pas toujours au niveau de ce qu'obtiendrait un développeur expert, elle reste excellente sur une large gamme de noyaux et d'applications.Une étude des architectures des GPUs et les tendances dans la conception des langages et cadres de programmation est présentée. Le placement des données entre l'hôte et l'accélérateur est réalisé sans impliquer le développeur. Un algorithme d'optimisation des communications est proposé pour envoyer les données sur le GPU dès que possible et les y conserver aussi longtemps qu'elle ne sont pas requises sur l'hôte. Des techniques de transformations de boucles pour la génération de code noyau sont utilisées, et même certaines connues et éprouvées doivent être adaptées aux contraintes posées par les GPUs. Elles sont assemblées de manière cohérente, et ordonnancées dans le flot d'un compilateur interprocédural. Des travaux préliminaires sont présentés au sujet de l'extension de l'approche pour cibler de multiples GPUs.

Since the beginning of the 2000s, the raw performance of processors stopped its exponential increase. The modern graphic processing units (GPUs) have been designed as array of hundreds or thousands of compute units. The GPUs' compute capacity quickly leads them to be diverted from their original target to be used as accelerators for general purpose computation. However programming a GPU efficiently to perform other computations than 3D rendering remains challenging.The current jungle in the hardware ecosystem is mirrored by the software world, with more and more programming models, new languages, different APIs, etc. But no one-fits-all solution has emerged.This thesis proposes a compiler-based solution to partially answer the three "P" properties: Performance, Portability, and Programmability. The goal is to transform automatically a sequential program into an equivalent program accelerated with a GPU. A…

Advisors/Committee Members: Irigoin, François (thesis director).

▼ 

Les applications informatiques sont de plus en plus présentes dans nos vies. Pour les applications critiques (médecine, transport, . . .), les conséquences d’une erreur informatique ont un coût inacceptable, que ce soit sur le plan humain ou financier. Une des méthodes pour éviter la présence d’erreurs dans les programmes est la vérification déductive. Celle-ci s’applique à des programmes écrits dans des langages de haut-niveau transformés, par des compilateurs, en programmes écrits en langage machine. Les compilateurs doivent être corrects pour ne pas propager d’erreurs au langage machine. Depuis 2005, les processeurs multi-coeurs se sont répandus dans l’ensemble des systèmes informatiques. Ces architectures nécessitent des compilateurs et des preuves de correction adaptées. Notre contribution est l’extension modulaire d’un compilateur vérifié pour un langage parallèle ciblant des architectures parallèles multi-coeurs. Les spécifications des langages (et leurs sémantiques opérationnelles) présents aux divers niveaux du compilateur ainsi que les preuves de la correction du compilateur sont paramétrées par des modules spécifiant des éléments de parallélisme tels qu’un modèle mémoire faible et des notions de synchronisation et d’ordonnancement entre processus légers. Ce travail ouvre la voie à la conception d’un compilateur certifié pour des langages parallèles de haut-niveau tels que les langages à squelettes algorithmiques.

Nowadays, we are using an increasing number of computer applications. Errors in critical applications (medicine, transport, . . .) may carry serious health or financial issues. Avoiding errors in programs is a challenge and may be achieved by deductive verification. Deductive verification applies to program written in a high-level languages, which are transformed into machine language by compilers. These compilers must be correct to ensure the nonpropagation of errors to machine code. Since 2005, multicore processors have spread in all electronic devices. So, these architectures need adapted compilers and proofs of correctness. Our work is the modular extension of a verified compiler for parallel languages targeting multicore architectures. Specifications of these languages (and their operational semantics) needed at all levels of the compiler and proofs of correctness of this compiler are parameterized by modules specifying elements of parallelism such as a relaxed memory model and notions of synchronization and scheduling between threads. This work is the first step in the conception of a certified compiler for high-level parallel languages such as algorithmic skeletons.

Advisors/Committee Members: Loulergue, Frédéric (thesis director).

▼ 

La vérification formelle de programme n'apporte pas de garantie complète si l'outil de vérification est incorrect. Et, si un programme est vérifié au niveau source, le compilateur pourrait introduire des bugs. Les compilateurs et vérifieurs actuels sont complexes. Pour simplifier l'analyse et la transformation de code, ils utilisent des représentations intermédiaires (IR) de programme, qui ont de fortes propriétés structurelles et sémantiques. Cette thèse étudie d'un point de vue sémantique et formel les IRs, afin de faciliter la preuve de ces outils. Nous étudions d'abord une IR basée registre du bytecode Java. Nous prouvons un théorème sur sa génération, explicitant ce que la transformation préserve (l'initialisation d'objet, les exceptions) et ce qu'elle modifie et comment (l'ordre d'allocation). Nous implantons l'IR dans Sawja, un outil de développement d'analyses statiques de Java. Nous étudions aussi la forme SSA, une IR au coeur des compilateurs et vérifieurs modernes. Nous implantons et prouvons en Coq un middle-end SSA pour le compilateur C CompCert. Pour la preuve des optimisations, nous prouvons un invariant sémantique de SSA clé pour le raisonnement équationnel. Enfin, nous étudions la sémantique des IRs de Java concurrent. La définition actuelle du Java Memory Model (JMM) autorise les optimisations aggressives des compilateurs et des architectures parallèles. Complexe, elle est formellement cassée. Ciblant les architectures x86, nous proposons un sous-ensemble du JMM intuitif et adapté à la preuve formelle. Nous le caractérisons par ses réordonnancements, et factorisons cette preuve sur les IRs d'un compilateur.

An end-to-end guarantee of software correctness by formal verification must consider two sources of bugs. First, the verification tool must be correct. Second, programs are often verified at the source level, before being compiled. Hence, compilers should also be trustworthy. Verifiers and compilers' complexity is increasing. To simplify code analysis and manipulation, these tools rely on intermediate representations (IR) of programs, that provide structural and semantic properties. This thesis gives a formal, semantic account on IRs, so that they can also be leveraged in the formal proof of such tools. We first study a register-based IR of Java bytecode used in compilers and verifiers. We specify the IR generation by a semantic theorem stating what the transformation preserves, e.g. object initialization or exceptions, but also what it modifies and how, e.g. object allocation. We implement this IR in Sawja, a Java static analysis toolbench. Then, we study the Static Single Assignment (SSA) form, an IR widely used in modern compilers and verifiers. We implement and prove in Coq an SSA middle-end for the CompCert C compiler. For the proof of SSA optimizations, we identify a key semantic property of SSA, allowing for equational reasoning. Finally, we study the semantics of concurrent Java IRs. Due to instruction reorderings performed by the compiler and the hardware, the current definition of…

Advisors/Committee Members: Jensen, Thomas (thesis director).

▼ 

OCaml est un langage fonctionnel statiquement typé, qui génère après inférence de types un arbre de syntaxe abstraite dans lequel chacun des noeuds est annoté avec un ensemble d’informations issues de cette inférence. Ces informations, en particulier les types inférés, constituent une preuve de typage de l’expression annotée.Ce manuscrit de thèse s’intéresse à la vérification de ces arbres annotés en les considérant comme des preuves de typages du programme, et décrit un ensemble de règles permettant d’en vérifier la cohérence. La formalisation de ces règles de vérification de preuves de types peut être vue comme une représensation du système de types du langage étudié.Cette thèse présente plusieurs aspects de la vérification d’arbres de syntaxe annotés. Le premier cas étudié est la formalisation d’un dérivé de MiniML où toutes les expressions sont annotées de manière théoriquement parfaite, et montre qu’il est possible d’écrire des règles de vérification de manière algorithmique, rendant directe la preuve de correction vis-à-vis de la spécification. La seconde partie s’intéresse à la formalisation de règles de vérification pour un sous-ensemble du premier langage intermédiaire d’OCaml, le TypedTree, accompagné d’un vérificateur implémentant ces règles. Ces règles constituent alors une représentation du système de types d’OCaml, document jusqu’alors inexistant, au mieux disséminé dans diverses publications.

OCaml is a statically typed programming language that generates typed annotated abstract syntax trees after type inference. Each of their nodes contains information derived from the inference like the inferred type and the environment used to find this information. These annotated trees can then be seen as typing proofs of the program.In this thesis, we introduce a consistency checking of type-annotated trees, considering them as typing proof, and we describe a set of rules that defines the consistency property.Such consistency checking rules can then be seen as a formalized representation of the type system, since consistency ensures the typing invariants of the language.This thesis introduces multiple aspects of checking type-annotated trees. First of all, it considers a simplified and ideal version of MiniML and formalizes a set of rules to check consistency. In this formalism, we consider ideally type-annotated trees, which might not be the case for OCaml typed trees. Such type checking rules are presented in an algorithmic form, reducing as much as possible the gap from formalism to implementation. As such, they ease the correction proof between the implementation of the type checker and the specification of the type system. The second part of this thesis is dedicated to the formalization of a set of rules for a subset of the OCaml annotated trees: the TypedTree. The formalism described in these chapters is implemented as a type checker working on large subset of the language, leaving the formalization of some aspects for a further work. These rules constitute a formalized representation of the OCaml type…

Advisors/Committee Members: Mauny, Michel (thesis director).

▼ 

De nos jours, l'optimisation des compilateurs est de plus en plus mise à l'épreuve par la diversité des langages de programmation et l'hétérogénéité des architectures. Le modèle polyédrique est un puissant cadre mathématique permettant aux programmes d’exploiter la parallélisation automatique et l’optimisation de la localité, jouant un rôle important dans le domaine de l’optimisation des compilateurs. Une limite de longue date du modèle réside dans sa restriction aux programmes affines à contrôle statique, ce qui a entraîné une demande émergente de prise en charge d'extensions non affines. Cela est particulièrement aigu dans le contexte d'architectures hétérogènes où une variété de noyaux de calcul doivent être analysés et transformés pour répondre aux contraintes des accélérateurs matériels et pour gérer les transferts de données à travers des espaces mémoire. Nous explorons plusieurs extensions non affines du modèle polyhédral, dans le contexte d'un langage intermédiaire bien défini combinant des éléments affines et syntaxiques. D'un côté, nous expliquons comment les transformations et la génération de code pour des boucles avec des limites de boucle dynamiques non dépendantes des données et dynamiques sont intégrées dans un cadre polyédrique, élargissant ainsi le domaine applicable de la compilation polyédrique dans le domaine des applications non affines. D'autre part, nous décrivons l'intégration du pavage en recouvrement pour les calculs de pochoir dans un cadre polyhédral général, en automatisant les transformations non affines dans la compilation polyhédrique. Nous évaluons nos techniques sur des architectures de CPU et de GPU, en validant l'efficacité des optimisations en effectuant une comparaison approfondie des performances avec des frameworks et des librairies écrites à la pointe de la technologie.

Nowadays, optimizing compilers are increasingly challenged by the diversity of programming languages and heterogeneity of architectures. The polyhedral model is a powerful mathematical framework for programs to exploit automatic parallelization and locality optimization, playing an important role in the field of optimizing compilers. A long standing limitation of the model has been its restriction to static control affine programs, resulting in an emergent demand for the support of non-affine extensions. This is particularly acute in the context of heterogeneous architectures where a variety of computation kernels need to be analyzed and transformed to match the constraints of hardware accelerators and to manage data transfers across memory spaces. We explore multiple non-affine extensions of the polyhedral model, in the context of a welldefined intermediate language combining affine and syntactic elements. On the one hand, we explain how transformations and code generation for loops with non-affine, data-dependent and dynamic loop bounds are integrated into a polyhedral framework, extending the applicable domain of polyhedral compilation in the realm of non-affine applications. On the other hand, we…

Advisors/Committee Members: Cohen, Albert Henri (thesis director).

▼ 

Les systèmes temps-réel devenaient omniprésents, et jouent un rôle important dans notre vie quotidienne. Pour les systèmes temps-réel dur, calculer des résultats corrects n’est pas la seule exigence, il doivent de surcroît être produits dans un intervalle de temps borné. Connaître le pire cas de temps d’exécution (WCET - Worst Case Execution Time) est nécessaire, et garantit que le système répond à ses contraintes de temps. Pour obtenir des estimations de WCET précises, des annotations sont nécessaires. Ces annotations sont généralement ajoutées au niveau du code source, tandis que l’analyse de WCET est effectuée au niveau du code binaire. L’optimisation du compilateur est entre ces deux niveaux et a un effet sur la structure du code et annotations. Nous proposons dans cette thèse une infrastructure logicielle de transformation, qui pour chaque optimisation transforme les annotations du code source au code binaire. Cette infrastructure est capable de transformer les annotations sans perte d’information de flot. Nous avons choisi LLVM comme compilateur pour mettre en œuvre notre infrastructure. Et nous avons utilisé les jeux de test Mälardalen, TSVC et gcc-loop pour démontrer l’impact de notre infrastructure sur les optimisations du compilateur et la transformation d’annotations. Les résultats expérimentaux montrent que de nombreuses optimisations peuvent être activées avec notre système. Le nouveau WCET estimé est meilleur (plus faible) que l’original. Nous montrons également que les optimisations du compilateur sont bénéfiques pour les systèmes temps-réel.

Real-time systems have become ubiquitous, and play an important role in our everyday life. For hard real-time systems, computing correct results is not the only requirement. In addition, the worst-case execution times (WCET) are needed, and guarantee that they meet the required timing constraints. For tight WCET estimation, annotations are required. Annotations are usually added at source code level but WCET analysis is performed at binary code level. Compiler optimization is between these two levels and has an effect on the structure of the code and annotations.We propose a transformation framework for each optimization to trace the annotation information from source code level to binary code level. The framework can transform the annotations without loss of flow information. We choose LLVM as the compiler to implement our framework. And we use the Mälardalen, TSVC and gcc-loops benchmarks to demonstrate the impact of our framework on compiler optimizations and annotation transformation. The experimental results show that with our framework, many optimizations can be turned on, and we can still estimate WCET safely. The estimated WCET is better than the original one. We also show that compiler optimizations are beneficial for real-time systems.

Advisors/Committee Members: Puaut, Isabelle (thesis director), Rohou, Erven (thesis director).

▼ 

Les architectures parallèles hybrides constituées d'un grand nombre de noeuds de calcul multi-coeurs/GPU connectés en réseau offrent des performances théoriques très élevées, de l'ordre de quelque dizaines de TeraFlops. Mais la programmation efficace de ces machines reste un défi à cause de la complexité de l'architecture et de la multiplication des modèles de programmation utilisés. L'objectif de cette thèse est d'améliorer la programmation des applications scientifiques denses sur les architectures parallèles hybrides selon trois axes: réduction des temps d'exécution, traitement de données de très grande taille et facilité de programmation. Nous avons pour cela proposé un modèle de programmation à base de directives appelé DSTEP pour exprimer à la fois la distribution des données et des calculs. Dans ce modèle, plusieurs types de distribution de données sont exprimables de façon unifiée à l'aide d'une directive "dstep distribute" et une réplication de certains éléments distribués peut être exprimée par un "halo". La directive "dstep gridify" exprime à la fois la distribution des calculs ainsi que leurs contraintes d'ordonnancement. Nous avons ensuite défini un modèle de distribution et montré la correction de la transformation de code du domaine séquentiel au domaine distribué. À partir du modèle de distribution, nous avons dérivé un schéma de compilation pour la transformation de programmes annotés de directives DSTEP en des programmes parallèles hybrides. Nous avons implémenté notre solution sous la forme d'un compilateur intégré à la plateforme de compilation PIPS ainsi qu'une bibliothèque fournissant les fonctionnalités du support d'exécution, notamment les communications. Notre solution a été validée sur des programmes de calcul scientifiques standards tirés des NAS Parallel Benchmarks et des Polybenchs ainsi que sur une application industrielle.

Clusters of multicore/GPU nodes connected with a fast network offer very high therotical peak performances, reaching tens of TeraFlops. Unfortunately, the efficient programing of such architectures remains challenging because of their complexity and the diversity of the existing programming models. The purpose of this thesis is to improve the programmability of dense scientific applications on hybrid architectures in three ways: reducing the execution times, processing larger data sets and reducing the programming effort. We propose DSTEP, a directive-based programming model expressing both data and computation distribution. A large set of distribution types are unified in a "dstep distribute" directive and the replication of some distributed elements can be expressed using a "halo". The "dstep gridify" directive expresses both the computation distribution and the schedule constraints of loop iterations. We define a distribution model and demonstrate the correctness of the code transformation from the sequential domain to the parallel domain. From the distribution model, we derive a generic compilation scheme transforming DSTEP annotated input programs into…

Advisors/Committee Members: Irigoin, François (thesis director).

▼ Les langages synchrones ont été fondés pour modéliser et implémenter les systèmes réactifs temps-réels critiques. Avec la complexité toujours croissante des systèmes contrôlés, la vitesse d'exécution devient un critère important. Nous sommes donc à la recherche d'une exécution parallèle, combinant efficacité et sûreté.Les langages synchrones ont toujours intégré la notion de parallélisme, mais ce, pour l'expressivité de la modélisation. Leurs compilations visent principalement les circuits ou la génération de code séquentiel. Tous ont une sémantique formelle, qui rend possible la distribution correcte du code. Mais la préservation de cette sémantique peut être un obstacle à l'efficacité du code généré, particulièrement s'il est nécessaire de préserver une notion d'instant global au système.Le modèle sémantique qui nous intéresse est celui des réseaux de Kahn. Ces réseaux modélisent des calculateurs distribués, communiquant au travers de files de taille non bornée. Dans ce cadre, la distribution ne demande aucune communication ni synchronisation supplémentaire. En considérant l'histoire des files de communication, la sémantique de Kahn permet de s'abstraire de l'exécution effective, tout en garantissant le déterminisme du calcul. Pour cela, chaque nœud du réseau doit avoir une sémantique fonctionnelle continue.Le langage que nous développons est Heptagon, un langage synchrone fonctionnel du premier ordre, déscendant de Lustre. Son compilateur est un prototype universitaire, apparenté à l'outil industriel Scade. Grâce à sa sémantique de Kahn, la distribution d'un programme Heptagon ne pose pas de question, son efficacité beaucoup plus.L'efficacité requiert de minimiser les synchronisations. Cela revêt deux aspects non indépendants. Avoir un découplage suffisant des calculs : il y a des délais dans les dépendances entre calculs. Avoir une granularité importante des calculs : un fort ratio temps de calcul sur fréquence de communication. Or la sémantique synchrone et les horloges d'un programme Heptagon reflètent exactement l'inverse. Elles permettent au programmeur de se contenter d'un découplage d'un instant et à chaque instant, au maximum une valeur est calculée. De plus, les instants sont typiquement courts, pour assurer que le système réagit rapidement.Des précédents travaux sur le sujet, nous tirons deux constats.Le premier est que nous souhaitons le contrôle du parallélisme par le programmeur, directement dans le code source. Il doit pouvoir maîtriser à quels instants il y a communication ou synchronisation. La solution que nous proposons dans ce manuscrit est l'utilisation des futures dans Heptagon. Ils fournissent ce pouvoir au programmeur, tout en restant des annotations qui peuvent être supprimées sans changer la sémantique dénotationnelle du programme.Le deuxième constat est que la question de la granularité des calculs est une question profonde, touchant en particulier aux questions de dépendance de données, de choix des horloges et de compilation modulaire. Heptagon, comme ses parents, restreint les réseaux… Advisors/Committee Members: Pouzet, Marc (thesis director).

▼ 

Cette thèse traite de la compilation efficace des langages à objets en héritage multiple. La programmation objet est caractérisée par un mécanisme fondamental, emph{la liaison tardive}  – la méthode appelée dépend du type dynamique d'un paramètre distingué, le emph{receveur}. L'efficacité de ce mécanisme nécessite une implémentation adéquate qui est conditionnée par le schéma de compilation utilisé  – compilation séparée avec chargement dynamique, compilation globale, etc. Cependant la programmation par objets présente une apparente incompatibilité entre trois termes : l'héritage multiple, l'efficacité et l'owa  – en particulier, le chargement dynamique. Nous avons étudié les techniques d'implémentation compatibles avec l'héritage multiple couramment utilisées ainsi qu'une alternative prometteuse, le ph. Nous nous plaçons dans le cadre du typage statique, donc nos conclusions peuvent valoir pour des langages comme cpp, eiffel, java, csharp, etc. Différents schémas de compilation sont considérés, de l'owa à l'cwa. Ces techniques et ces schémas ont été mis en uvre dans le compilateur auto-gène du langage prm. L'influence sur l'efficacité de tous ces éléments a été testée dans un protocole expérimental rigoureux de méta-compilation et les tests ont été réalisés sur une variété de processeurs différents. Les résultats des ces expérimentations sont discutés et comparés aux évaluations a priori effectuées sur les techniques d'implémentation. Ils confirment aussi que le ph est une technique d'implémentation intéressante pour le sous-typage multiple à la java.

His thesis is about efficient compilation of object oriented language with multiple inheritance.Object oriented programing is characterized by a main mechanism, emph{late binding}  – invoked method only depends on the dynamic type of one special parameter, the emph{receiver}.In order to be efficient this mechanism needs an implementation which depends on some compilation scheme  – separate compilation with dynamic loading, global compilation, etc.However object oriented programming present akin of incompatibility between three terms: multiple inheritance, efficiency and open world assumption  – especially with dynamic loading.In this thesis, we have studied common implementation techniques compatible with multiple inheritance and a promising alternative, perfect class hashing.The context of this study is static typing, our conclusion holds for languages like cpp, eiffel, java, csharp, etc.Different compilation schemes are considered, from open world assumption to closed world assumption.These techniques and schemes are implemented in the prm bootstraped compiler.Efficiency influence of all this artifacts has been tested with a rigorous meta-compilation experimental protocol and these tests have been performed on a variety of different processors.Results of these experiments are discuss and compared to an a priori evaluations of implementations techniquesThey mainly confirm perfect class hashing as an interesting implementation for multiple subtyping, a la…

Advisors/Committee Members: Ducournau, Roland (thesis director).

▼ 

Dans le domaine du calcul haute performance, de nombreux programmes étalons ou benchmarks sont utilisés pour mesurer l’efficacité des calculateurs,des compilateurs et des optimisations de performance. Les benchmarks de référence regroupent souvent des programmes de calcul issus de l’industrie et peuvent être très longs. Le processus d’´étalonnage d’une nouvelle architecture de calcul ou d’une optimisation est donc coûteux.La plupart des benchmarks sont constitués d’un ensemble de noyaux de calcul indépendants. Souvent l’´étalonneur n’est intéressé que par un sous ensemble de ces noyaux, il serait donc intéressant de pouvoir les exécuter séparément. Ainsi, il devient plus facile et rapide d’appliquer des optimisations locales sur les benchmarks. De plus, les benchmarks contiennent de nombreux noyaux de calcul redondants. Certaines opérations, bien que mesurées plusieurs fois, n’apportent pas d’informations supplémentaires sur le système à étudier. En détectant les similarités entre eux et en éliminant les noyaux redondants, on diminue le coût des benchmarks sans perte d’information.Cette thèse propose une méthode permettant de décomposer automatiquement une application en un ensemble de noyaux de performance, que nous appelons codelets. La méthode proposée permet de rejouer les codelets,de manière isolée, dans différentes conditions expérimentales pour pouvoir étalonner leur performance. Cette thèse étudie dans quelle mesure la décomposition en noyaux permet de diminuer le coût du processus de benchmarking et d’optimisation. Elle évalue aussi l’avantage d’optimisations locales par rapport à une approche globale.De nombreux travaux ont été réalisés afin d’améliorer le processus de benchmarking. Dans ce domaine, on remarquera l’utilisation de techniques d’apprentissage machine ou d’´echantillonnage. L’idée de décomposer les benchmarks en morceaux indépendants n’est pas nouvelle. Ce concept a été aappliqué avec succès sur les programmes séquentiels et nous le portons à maturité sur les programmes parallèles.Evaluer des nouvelles micro-architectures ou la scalabilité est 25× fois plus rapide avec des codelets que avec des exécutions d’applications. Les codelets prédisent le temps d’exécution avec une précision de 94% et permettent de trouver des optimisations locales jusqu’`a 1.06× fois plus efficaces que la meilleure approche globale.

In high performance computing, benchmarks evaluate architectures, compilers and optimizations. Standard benchmarks are mostly issued from the industrial world and may have a very long execution time. So, evaluating a new architecture or an optimization is costly. Most of the benchmarks are composed of independent kernels. Usually, users are only interested by a small subset of these kernels. To get faster and easier local optimizations, we should find ways to extract kernels as standalone executables. Also, benchmarks have redundant computational kernels. Some calculations do not bring new informations about the system that we want to study, despite that we measure them many times. By…

Advisors/Committee Members: Jalby, William (thesis director).

▼ 

Dans la deuxième moitié du XVe siècle, les Croniques et conquestes de Charlemaine de David Aubert, l’Histoire de Charlemagne de Jean Bagnyon et l’anonyme Cronique associee ont cherché à rassembler et compiler les récits associés à Charlemagne. Composées dans des milieux différents à un moment où tant la réécriture en prose que le personnage de l’empereur étaient en vogue, ces compilations ont recyclé des chansons de geste et des chroniques des siècles précédents pour (re)constituer une histoire cohérente du personnage. Leur résultat est tantôt une biographie princière, tantôt un fragment cyclique qui s’arrête à la mort de l’empereur. La prose donne une forme nouvelle à ces récits inédits par leur organisation et leur extension, mais banals par leur matériau, recyclé de compilation en compilation. Par l’étude du contexte historique, et surtout la comparaison des versions proposées, dans leur récit, leurs articulations et leur présentation, nous souhaitons montrer comment la compilation est le reflet d’une lecture critique et organisée propre aux nouvelles habitudes de la fin du Moyen Âge. Le remaniement oriente sa propre lecture en fonction d’un public familier de la tradition littéraire : les morceaux de bravoure sont réécrits, comme l’épisode de Roncevaux, d’autres sont triés et oubliés en fonction du projet propre à chacune des œuvres. La compilation oscille entre la reconnaissance des textes et la déprise introduite par le nouvel ensemble. Au cœur de notre questionnement se trouve la double dynamique de fixation et de malléabilité de la mémoire, érigée au Moyen Âge comme modalité de l’activité littéraire. Nous proposons en annexe la transcription de la Cronique associee (ms Paris, Arsenal 3324) pour rendre ce texte plus facilement accessible.

In the second half of the fifteenth century, David Aubert’s Croniques et conquestes de Charlemaine, Jean Bagnyon’s Histoire de Charlemagne and the anonymous Cronique associee tried to collect and compile the stories linked to Charlemagne. Composed in various circles, when both rewriting in prose and Charlemagne himself were popular, these compilations recycled epic songs and chronicles written in the previous centuries to piece together a coherent story of this character. What results is either a princely biography or a cyclic fragment that is interrupted when the emperor dies. The prose form revives these stories whose structure and scope were novel but whose material had become trite after being compiled again and again. By studying the historical context, and especially by comparing the composition, narrative structure and presentation of different versions, I wish to show how the compilation reflects a critical and organized reading which epitomizes the new practices of the late Middle Ages. The rewriting process bears its own guidelines, depending on a reading public who is familiar with literary tradition: the purple patches, such as the Roncesvalles episode, are rewritten, while other passages are sorted away or forgotten, in keeping with the objective of each…

Advisors/Committee Members: Szkilnik, Michelle (thesis director).

▼ 

Cette thèse présente une extension du compilateur CompCert permettant de fournir des garanties formelles de préservation sémantique à des programmes auxquels CompCert n'en donne pas. CompCert est un compilateur pour le langage C vers différentes architectures qui fournit, en plus d'un exécutable compilé, des garanties formelles concernant le comportement du programme assembleur généré. En particulier, tout programme C ayant une sémantique définie selon le standard C est compilé en un programme assembleur équivalent, c'est-à-dire qui a la même sémantique. En revanche, ce théorème n'assure aucune garantie lorsque le programme source n'a pas de sémantique définie : on parle en C de comportement indéfini. Toutefois, des programmes C issus de réels projets largement utilisés contiennent des comportements indéfinis. Cette thèse détaille dans un premier temps un certain nombre d'exemples de programmes C qui déclenchent des comportements indéfinis. Nous argumentons que ces programmes devraient tout de même bénéficier du théorème de préservation sémantique de CompCert, d'abord parce qu'ils apparaissent dans de vrais projets et parce que leur utilisation des comportements indéfinis semble légitime. Dans ce but, nous proposons d'abord un modèle mémoire pour CompCert qui définit l'arithmétique arbitraire de pointeurs et la manipulation de données non initialisées, à l'aide d'un formalisme de valeurs symboliques qui capturent la sémantique d'opérations non définies dans le standard. Nous adaptons l'intégralité du modèle mémoire de CompCert avec ces valeurs symboliques, puis nous adaptons les sémantiques formelles de chacun des langages intermédiaires de CompCert. Nous montrons que ces sémantiques symboliques sont un raffinement des sémantiques existantes dans CompCert, et nous montrons par ailleurs que ces sémantiques capturent effectivement le comportement des programmes sus-cités. Enfin, afin d'obtenir des garanties similaires à celles que CompCert fournit, nous devons adapter les preuves de préservation sémantique à notre nouveau modèle. Pour ce faire, nous généralisons d'importantes techniques de preuves comme les injections mémoire, ce qui nous permet de transporter les preuves de CompCert sur nos nouvelles sémantiques. Nous obtenons ainsi un théorème de préservation sémantique qui traite plus de programmes C.

This thesis presents an extension of the CompCert compiler that aims at providing formal guarantees about the compilation of more programs than CompCert does. The CompCert compiler compiles C code into assembly code for various architectures and provides formal guarantees about the behaviour of the compiled assembly program. It states that whenever the C program has a defined semantics, the generated assembly program behaves similarly. However, the theorem does not provide any guarantee when the source program has undefined semantics, or, in C parlance, when it exhibits undefined behaviour, even though those behaviours actually happen in real-world code. This thesis exhibits a number of C idioms, that occur in…

Advisors/Committee Members: Blazy, Sandrine (thesis director), Besson, Frédéric (thesis director).

▼ 

Les systèmes informatiques critiques - tels que les commandes de vol électroniques et le contrôle des centrales nucléaires - doivent répondre à des exigences strictes en termes de sûreté de fonctionnement. Nous nous intéressons ici à l'application de méthodes formelles - ancrées sur de solides bases mathématiques - pour la vérification du comportement des logiciels critiques. Plus particulièrement, nous spécifions formellement nos algorithmes et nous les prouvons corrects, à l'aide de l'assistant à la preuve Coq - un logiciel qui vérifie mécaniquement la correction des preuves effectuées et qui apporte un degré de confiance très élevé. Nous appliquons ici des méthodes formelles à l'estimation du Temps d'Exécution au Pire Cas (plus connu par son abréviation en anglais, WCET) de programmes C. Le WCET est une propriété importante pour la sûreté de fonctionnement des systèmes critiques, mais son estimation exige des analyses sophistiquées. Pour garantir l'absence d'erreurs lors de ces analyses, nous avons formellement vérifié une méthode d'estimation du WCET fondée sur la combinaison de deux techniques principales: une estimation de bornes de boucles et une estimation du WCET via la méthode IPET (Implicit Path Enumeration Technique). L'estimation de bornes de boucles est elle-même décomposée en trois étapes : un découpage de programmes, une analyse de valeurs opérant par interprétation abstraite, et une méthode de calcul de bornes. Chacune de ces étapes est formellement vérifiée dans un chapitre qui lui est dédiée. Le développement a été intégré au compilateur C formellement vérifié CompCert. Nous prouvons que le résultat de l'estimation est correct et nous évaluons ses performances dans des ensembles de benchmarks de référence dans le domaine. Les contributions de cette thèse incluent la formalisation des techniques utilisées pour estimer le WCET, l'outil d'estimation lui-même (obtenu à partir de la formalisation), et l'évaluation expérimentale des résultats. Nous concluons que le développement fondé sur les méthodes formelles permet d'obtenir des résultats intéressants en termes de précision, mais il exige des précautions particulières pour s'assurer que l'effort de preuve reste maîtrisable. Le développement en parallèle des spécifications et des preuves est essentiel à cette fin. Les travaux futurs incluent la formalisation de modèles de coût matériel, ainsi que le développement d'analyses plus sophistiquées pour augmenter la précision du WCET estimé.

Safety-critical systems - such as electronic flight control systems and nuclear reactor controls - must satisfy strict safety requirements. We are interested here in the application of formal methods - built upon solid mathematical bases - to verify the behavior of safety-critical systems. More specifically, we formally specify our algorithms and then prove them correct using the Coq proof assistant - a program capable of mechanically checking the correctness of our proofs, providing a very high degree of confidence. In this thesis, we apply formal methods to obtain…

Advisors/Committee Members: Blazy, Sandrine (thesis director), Puaut, Isabelle (thesis director).

▼ 

Cette thèse porte premièrement sur la reconfiguration dynamique et la simulation hétérogène dans les Réseaux des Capteurs sans Fil. Ces réseaux sont constitués d’une multitude de systèmes électroniques communicants par radio-fréquence, très contraints en énergie. La partie de communication radio entre ces nœuds est la plus consommatrice. C’est pourquoi la minimisation du temps effectif est désirée. On a implémenté une solution qui consiste à envoyer au nœud un fichier de reconfiguration codé utilisant un langage de programmation haut niveau (MinTax). Le nœud sera capable de compiler ce fichier et générer le code object associé à son architecture, in-situ. Grâce au caractère abstrait du MinTax, plusieurs architectures matérielles et systèmes d’exploitation sont visés. Dans un deuxième temps, ce travail de thèse est lié au simulateur de réseaux de capteurs IDEA1TLM.IDEA1TLM permet de prédire quels circuits et configurations sont les plus adéquats à une application sans fil donnée. Ce simulateur a été amélioré pour permettre la simulation rapide des systèmes électroniques matériellement différents dans le même réseau ainsi que le logiciel présent sur les nœuds.

This PhD thesis concerns the dynamic reconfiguration and simulation of heterogeneous Wireless Sensor Networks. These networks consist of a multitude of electronic units called ?nodes ?, which communicate through a radio interface. The radio interface is the most power-consuming on the node. This is why the minimisation of the radio-time would lead to improved energy efficiency. We have implemented a software solution which consists in sending an update to a node which is coded in a high-level language (MinTax). This file is compiled by the node and machine code is generated for the target hardware architecture. Owing to the abstract nature of MinTax, multiple hardware architectures. as well as operating systems are supported. As a second part of this PhD, work has been focused on a network simulator called IDEATLM.IDEA1TLM allows us to predict which circuits and configurations are the most appropriate for a given task. This solution has been improved to allow a faster simulation of electronic systems which are different from a hardware standpoint, yet part of the same network, as well as to model the actual software running on them.

Advisors/Committee Members: Mieyeville, Fabien (thesis director).

▼ 

La modélisation géométrique est utilisée dans de nombreux domaines pour la construction d’objets 3D, l’animation ou les simulations. Chaque domaine est soumis à ses propres contraintes et nécessiterait un outil dédié. En pratique, un même outil est utilisé pour plusieurs domaines, en factorisant les caractéristiques communes. Ces modeleurs fournissent un ensemble d'opérations types, que l'utilisateur compose pour construire ses objets. Pour des opérations plus spécifiques, les outils actuels offrent des API.La plate-forme Jerboa propose un outil de génération d'opérations géométriques personnalisées. Elles sont définies graphiquement par des règles de transformations de graphes. Des vérifications automatiques de préservation de la cohérence des objets sont faites lors de l’édition qui peuvent être enrichies par des propriétés métiers. Notre contribution a consisté à étendre le langage par des scripts, pour composer les règles et réaliser des opérations complexes. Nous avons étendu les vérifications automatiques, en particulier pour assurer la cohérence géométrique. Enfin, nous avons modifié le processus d'application des opérations pour augmenter les possibilités de contrôle.Pour valider cette approche, nous avons développé un modeleur dédié à la géologie, pour la représentation du sous-sol, en collaboration avec l'entreprise Géosiris. Nous avons défini un flux d'activité avec Géosiris en suivant des contraintes spécifiques à la géologie. Grâce à la rapidité de développement des opérations dans Jerboa, nous avons pu prototyper et tester rapidement plusieurs algorithmes de reconstruction du sous-sol, pour les appliquer sur des données réelles fournies par l'entreprise.

Geometric modeling is used in various scopes for 3D object construction, animation or simulations. Each domain must cope with its constraints and should have its dedicated tool. In fact, several common characteristics of different domains are factored in a single tool. These modelers contain sets of basic operations that the user composes to build his objects. For more specific operations, current common tools offer API.Jerboa’s platform allows to generate personalized geometrical operations. These are defined by graph transformation rules. During their design, many automated verifications are done for the preserving of object consistency. They also be enriched with additional properties. Our contribution consists in extending the Jerboa language with scripts to compose rules and define complex operations. We also extended automated verifications, in particular to ensure geometric consistaency. Finally, we modified operations application process, in order to increase user control possibilities.To validate this approach, we have implemented a geological dedicated modeler for subsoil modeling, in collaboration with Geosiris Company. We defined a workflow with Geosiris that follows specific geological reconstruction constraints. Thanks to the Jerboa rapid prototyping mecanism, we developped and quickly tested several subsoil reconstruction algorithms,…

Advisors/Committee Members: Lienhardt, Pascal (thesis director), Belhaouari, Hakim (thesis director).

▼ 

LNT est un langage formel de spécification récent, basé sur les algèbres de processus, où plusieurs processus concurrents et asynchrones peuvent interagir par rendez-vous multiple, c'est-à-dire à deux ou plus, avec échange de données. La boite à outils CADP (Construction and Analysis of Distributed Processes) offre plusieurs techniques relatives à l'exploration d'espace d'états, comme le model checking, pour vérifier formellement une spécification LNT. Cette thèse présente une méthode de génération d'implémentation distribuée à partir d'un modèle formel LNT décrivant une composition parallèle de processus. En s'appuyant sur CADP, nous avons mis au point le nouvel outil DLC (Distributed LNT Compiler), capable de générer, à partir d'une spécification LNT, une implémentation distribuée en C qui peut ensuite être déployée sur plusieurs machines distinctes reliées par un réseau. Pour implémenter de manière correcte et efficace les rendez-vous multiples avec échange de données entre processus distants, nous avons élaboré un protocole de synchronisation qui regroupe différentes approches proposées par le passé. Nous avons mis au point une méthode de vérification de ce type de protocole qui, en utilisant LNT et CADP, permet de détecter des boucles infinies ou des interblocages dus au protocole, et de vérifier que le protocole réalise des rendez-vous cohérents par rapport à une spécification donnée. Cette méthode nous a permis d'identifier de possibles interblocages dans un protocole de la littérature, et de vérifier le bon comportement de notre propre protocole. Nous avons aussi développé un mécanisme qui permet, en embarquant au sein d'une implémentation des procédures C librement définies par l'utilisateur, de mettre en place des interactions entre une implémentation générée et d'autres systèmes de son environnement. Enfin, nous avons appliqué DLC au nouvel algorithme de consensus Raft, qui nous sert de cas d'étude, notamment pour mesurer les performances d'une implémentation générée par DLC.

LNT is a recent formal specification language, based on process algebras, where several concurrent asynchronous processes can interact by multiway rendezvous (i.e., involving two or more processes), with data exchange. The CADP (Construction and Analysis of Distributed Processes) toolbox offers several techniques related to state space exploration, like model checking, to formally verify an LNT specification. This thesis introduces a distributed implementation generation method, starting from an LNT formal model of a parallel composition of processes. Taking advantage of CADP, we developed the new DLC (Distributed LNT Compiler) tool, which is able to generate, from an LNT specification, a distributed implementation in C that can be deployed on several distinct machines linked by a network. In order to handle multiway rendezvous with data exchange between distant processes in a correct and efficient manner, we designed a synchronization protocol that gathers different approaches suggested in the past. We set up a verification method…

Advisors/Committee Members: Salaün, Gwen (thesis director), Lang, Frédéric (thesis director).

▼ 

Dans cette thèse nous proposons une interface de programmation pour aider les développeurs dans leur tâche d'optimisation de programme par calcul approché. Cette interface prend la forme d'extensions aux langages de programmation pour indiquer au compilateur quelles parties du programme peuvent utiliser ce type de calcul. Le compilateur se charge alors de transformer les parties du programme visées pour rendre l'application adaptative, allouant plus de ressources aux endroits où une précision importante est requise et utilisant des approximations où la précision peut être moindre. Nous avons automatisé la découverte des paramètres d'optimisation que devrait fournir l'utilisateur pour les codes à stencil, qui sont souvent rencontrés dans des applications de traitement du signal, traitement d'image ou simulation numérique. Nous avons exploré des techniques de compression automatique de données pour compléter la génération de code adaptatif. Nous utilisons la transformée en ondelettes pour compresser les données et obtenir d'autres informations qui peuvent être utilisées pour trouver les zones avec des besoins en précision plus importantes.

In this thesis we introduce a new application programming interface to help developers to optimize an application with approximate computing techniques. This interface is provided as a language extension to advise the compiler about the parts of the program that may be optimized with approximate computing and what can be done about them. The code transformations of the targeted regions are entirely handled by the compiler to produce an adaptive software. The produced adaptive application allocates more computing power to the locations where more precision is required, and may use approximations where the precision is secondary. We automate the discovery of the optimization parameters for the special class of stencil programs which are common in signal/image processing and numerical simulations. Finally, we explore the possibility of compressing the application data using the wavelet transform and we use information found in this basis to locate the areas where more precision may be needed.

Advisors/Committee Members: Bastoul, Cédric (thesis director), Helluy, Philippe (thesis director).

▼ 

Cette thèse traite des langages à objets en héritage multiple et typage statique exécutés avec des machines virtuelles. Des analogies sont à faire avec Java bien que ce langage ne soit pas en héritage multiple.Une machine virtuelle est un système d'exécution d'un programme qui se différencie des classiques compilateurs et interpréteurs par une caractéristique fondamentale : le chargement dynamique. Les classes sont alors découvertes au fil de l'exécution.Le but de la thèse est d'étudier et de spécifier une machine virtuelle pour un langage à objets en héritage multiple, pour ensuite spécifier et implémenter des protocoles de compilation/recompilation. Ces derniers devront mettre en place les optimisations et les inévitables mécanismes de réparations associés.Nous présenterons d'abord l'architecture et les choix réalisés pour implémenter la machine virtuelle : ceux-ci utilisent le langage Nit en tant que langage source ainsi que le hachage parfait, une technique d'implémentation de l'héritage multiple.Ensuite nous présenterons les spécifications pour implémenter des protocoles de compilation/recompilation ainsi que les expérimentations associées.Dans ce cadre, nous avons présenté une extension des analyses de préexistence et de types concrets, pour augmenter les opportunités d'optimisations sans risque. Cette contribution dépasse la problématique de l'héritage multiple.

This thesis is about object-oriented languages in multiple inheritance and static typing executed by virtual machines.We are in the context of a Java-like language and system but in multiple inheritance.A virtual machine is an execution system which is different from static compilers and interpreters since they are in dynamic loading.This characteristic makes classes to be discovered during the execution.The thesis' goal is to study, specify and implement a virtual machine for an object-oriented language in multiple inheritance and then in a second step to specify and implement compilation/recompilation protocols.These protocols are in charge of optimizations and unavoidable repairing.We will present the architecture of the virtual machine : the used language is Nit, and perfect hashing as the multiple inheritance implementation technique. Then we will present the protocols and the experiments.In this thesis, we have presented an extension of preexistence and concrete types analysis to increase optimization opportunities. This contribution is not limited to multiple inheritance object-oriented languages.

Advisors/Committee Members: Ducournau, Roland (thesis director).