Définitions et résultats fondamentaux sur les polyèdres convexes. Opérations sur les polyèdres convexes. contextes abstraits. Système d'équations en avant associe à un programme. Analyse approchée en avant des programmes. Analyse approchée en arrière des programmes. Primitives évoluées. Application de la méthode. Note sur l'implémentation et les performances. comparaison avec des travaux voisins.

Ce travail porte sur la production de code séquentiel à partir du langage flot de données synchrone Lustre. La difficulté essentielle provient de l'aspect déclaratif du langage. En effet, il n'y a pas d'instruction de contrôle dans le langage Lustre ; toute la structure de contrôle du code objet doit donc être synthétisée par le compilateur. Cette synthèse consiste à construire un automate fini en simulant exhaustivement le comportement des variables booléennes du programme. Le code produit est particulièrement rapide ; en effet, la plupart des calculs booléens sont effectués une fois pour toute dès la compilation. En contrepartie, l'aspect exhaustif de cette démarche provoque parfois une véritable explosion de la taille du code. Ce problème peut être dû à la complexité intrinsèque du programme source ; il faut dans ce cas chercher un compromis entre rapidité et taille mémoire. Mais l'explosion peut être causée par la méthode de construction, qui produit très souvent des automates non minimaux ; nous avons donc étudié et développé un algorithme original qui construit à coup sûr des automates minimaux. Cet algorithme fait appel à de nombreuses manipulations symboliques de fonctions booléennes, que nous avons pu implémenter efficacement grâce à une représentation basée sur les graphes binaires de décision.

Le besoin de solutions de test en-ligne intégré est de plus en plus important. Malgré la complexité croissante de systèmes numériques, ces solutions doivent garantir un surcoût raisonnable en temps de conception, en ressources impliquées et en performance. Cela nécessite le développement de nouvelles méthodes de synthèse de haut niveau qui doivent garantir deux contraintes. La première est la possibilité de traiter des systèmes complexes à un coût raisonnable. La deuxième est la prise en compte des contraintes de test en-ligne dans les premières tâches du flot de la synthèse de haut niveau. Pour s'accommoder à ce besoin, la présente étude propose deux axes de travail. Le premier axe consiste à proposer deux méthodes de test en-ligne, non-concurrent et semi-concurrent, présentées comme solutions intégrées (BIST). Le deuxième axe consiste à proposer une nouvelle méthode de synthèse de haut niveau (HLS) qui tient compte de la testabilité en-ligne. La prise en compte des contraintes de test en-ligne est effectuée au niveau de la compilation de la description comportementale en graphe de flot de données (DFG). Selon les contraintes imposées au système, une des méthodes de test en-ligne développées dans le premier axe est intégrée au système au niveau ordonnancement. Un système numérique donné par sa description comportementale forme l'entrée de la méthode. Dans un premier temps, une optimisation orientée testabilité adresse les équations arithmétiques dans la description comportementale du système. Outre l'amélioration de la testabilité, cette optimisation peut permettre d'améliorer les performances du design final. La description optimisée est compilée en graphe de flot de données ordonnancé. La tâche de la compilation et de l'ordonnancement est résolue par une exploration de l'espace de solutions. Dans cette exploration nous introduisons le développement d'un algorithme génétique (AG) adapté à ce type de problèmes. Les contraintes de test en-ligne, de surface et de délai sont considérées à cette étape pour produire une solution satisfaisante. Une fois que le graphe de flot de données ordonnancé est obtenu, la méthode qui répond le mieux aux contraintes de test en-ligne est insérée dans l'ordonnancement nominal du système. L'allocation de ressource et l'assignation permettent la génération d'une architecture testable en-ligne au niveau RTL. Mots clés : synthèse de haut niveau, compilation, ordonnancement, testabilité en-ligne, DFG, BIST, AG.

La plate-forme .NET est un environnement d'exécution moderne et répandu, reposant sur une machine virtuelle qui interprète du code-octet typé. Elle prétend être parfaitement adaptée à l'exécution de composants écrits dans une grande variété de langages de programmation et faciliter leur interopération.<br /> En tant que langage fonctionnel statiquement typé avec polymorphisme paramétrique, Objective Caml présente des caractéristiques qui défient l'environnement d'exécution .NET et son système de types. Nous expérimentons ces difficultés dans un cadre pratique, par la conception et l'implantation de OCamIL, un compilateur complet pour Objective Caml qui produit du code-octet .NET vérifiable. Ses objectifs principaux sont la compatibilité et la possibilité d'interopérer.<br /> Ce travail met à l'épreuve les capacités de la plate-forme .NET autant que l'adéquation de l'implantation officielle de Objective Caml dans un tel projet (celle-ci est conçue pour un environnement d'exécution dénué de types ce qui explique qu'elle élimine les informations de types assez tôt dans la chaîne de compilation). Nous examinons la représentation des valeurs Caml et comparons deux stratégies : la reconstruction et la propagation de l'information de typage manquante. D'autres choix de conception décrits ici illustrent le compromis entre efficacité d'une part et lisibilité/interopérabilité de l'autre.<br /> Nous réalisons l'interopérabilité à l'aide d'un langage de description d'interface IDL qui construit un pont entre les deux systèmes de classes distincts utilisés par Objective Caml et l'environnement typé de .NET. Les bénéfices de l'interopération sont illustrés par des exemples non-triviaux.<br /> Au chapitre des performances, OCamIL occupe une place respectable au sein des compilateurs de langages fonctionnels sur .NET. Nous comparons également les exécutables .NET avec les programmes Objective Caml originaux.

Reproduction de : Thèse de doctorat : informatique : Grenoble, INPG : 1987. / Titre provenant de l'écran-titre. Bibliogr. p. 157-164.

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 de Kahn qui peuvent être écrits, de telle sorte que ces trois questions se traitent séparément. Pour mieux comprendre le lien entre ces éléments, nous revenons aux réseaux de Kahn. Notre principal résultat est la définition de la sous-classe des réseaux ordonnés réactifs. Ceux-ci sont les seuls pour lesquels nous pouvons décrire modulairement le comportement avec des horloges, sans restreindre les contextes d'appels. Ces réseaux ont une signature d'horloge en forme normale, qui maximise la granularité. Pour l'exprimer, nous introduisons les horloges entières, décrivant la communication de plusieurs valeurs en un seul instant. Nous appliquons ensuite nos résultats pour voir sous un nouveau jour Heptagon, Signal, les politiques des objets de Lucid Synchrone, mais aussi proposer une analyse pleinement modulaire de Lucy-n langage synchrone le plus fidèle aux réseaux de Kahn.

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.

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 the Java Memory Model (JMM) is complex, and unfortunately formally flawed. Targetting x86 architectures, we identify a subset of the JMM that is intuitive and tractable in formal proofs. We characterize the reorderings it allows, and factor out a proof common to the IRs of a compiler.

Cette thèse propose une nouvelle approche du parallélisme et de la concurrence, posant les bases d'un langage de programmation à la fois sûr et "secure" (garantissant la sécurité des données), fondé sur une sémantique formelle claire et simple, tout en étant adapté aux architectures multi-cœur. Nous avons adopté le paradigme synchrone, dans sa variante réactive, qui fournit une alternative simple à la programmation concurrente standard en limitant l'impact des erreurs dépendant du temps ("data-races"). Dans un premier temps, nous avons considéré un langage réactif d'orchestration, DSL, dans lequel on fait abstraction de la mémoire (Partie 1). Dans le but de pouvoir traiter la mémoire et la sécurité, nous avons ensuite étudié (Partie 2) un noyau réactif, CRL, qui utilise un opérateur de parallélisme déterministe. Nous avons prouvé la réactivité bornée des programmes de CRL. Nous avons ensuite équipé CRL de mécanismes pour contrôler le flux d'information (Partie 3). Pour cela, nous avons d'abord étendu CRL avec des niveaux de sécurité pour les données, puis nous avons défini dans le langage étendu, SSL, un système de types permettant d'éviter les fuites d'information. Parallèlement (Partie 4), nous avons ajouté la mémoire à CRL, en proposant le modèle DSLM. En utilisant une notion d'agent, nous avons structuré la mémoire de telle sorte qu'il ne puisse y avoir de "data-races". Nous avons également étudié l'implémentation de DSLM sur les architectures multi-cœur, fondée sur la notion de site et de migration d'un agent entre les sites. L'unification de SSL et de DSLM est une piste pour un travail futur.

Thèse diffusée initialement dans le cadre d'un projet pilote des Presses de l'Université de Montréal/Centre d'édition numérique UdeM (1997-2008) avec l'autorisation de l'auteur.