L'étude des principaux domaines d'application et des techniques essentielles du traitement d'images permet de dégager des interrogations directes pour le concepteur d'architectures d'ordinateurs. Quelques unes des voies possibles pour leurs solutions matérielles sont ensuite présentées dans leurs principes et a l'aide d'exemples. Présentation de deux études : la machine ROMULARD (multi-microprocesseur) pour la saisie et le traitement d'images et le systeme KIDS, architecture plus ambitieuse alliant les aspects logiciels et matériels.

XML (eXtensible Markup Language) est un format standard pour l'échange de données semi-structurées, qui est utilisé dans services web, les bases de données, et comme format de sérialisation pour échanger des données entre applications. Afin d'avoir un meilleur traitement de données XML, plusieurs langages statiquement typés pour XML ont été récemment définis, tels XDuce, CDuce, XJ, XTatic, XACT, XHaskell, OCamlDuce. Ces langages peuvent vérifier si un programme n'engendra d'erreurs de types à l'exécution. Mais la plupart de ces langages n'incluent pas le polymorphisme paramétrique ou l'incluent sous un forme très limitée. Cependant, le traitement de données XML nécessite du polymorphisme paramétrique, c'est pourquoi il a été demandé et discuté à plusieurs reprises dans diverses groupes de travail de standardisation (par example, RELAX-NG et XQuery). Nous étudions dans cette thèse les techniques pour étendre par le polymorphisme paramétrique les langages de traitement XML. Notre solution se deroule sur deux étapes: (i) nous définissons et étudions une relation de sous-typage polymorphe sémantique pour un système de type avec types récursifs, types des produits, types des flèches, et types des ensemblistes (c'est-à-dire, l'union, l'intersection et la négation); et (ii) nous concevons et étudions un langage fonctionnel d'ordre supérieur qui tire pleinement parti des nouvelles fonctionnalités du système de type. La solution que nous proposons dans cette thèse est générale. Ainsi elle a des domaines d'application autres que les langages pour le traitement de données XML.

Les Web Services sont aujourd'hui à la base de nombreuses applications de commerce électronique. Aujourd'hui les solutions de sécurité qui sont proposées pour les Web-Services permettent de protéger en confidentialité et en intégrité les communications entre les Web-Services et de contrôler l'accès aux Web-Services. Cependant, le plus souvent, les clients utilisent ces applications sans en connaître le fonctionnement interne. De ce fait, ils n'ont aucune connaissance sur l'usage de leurs données qui est effectué à l'intérieur d'une application. BPEL (Business Process Execution Language) est un langage de programmation permettant d'orchestrer des Web-Services au sein d'une architecture orientée services. Une des fonctionnalités des architectures orientées services est la découverte dynamique des services effectivement utilisés au cours de l'exécution d'une orchestration. De ce fait, l'utilisateur d'un programme BPEL ne peut connaitre avant l'exécution comment et par qui les données qu'il va fournir seront utilisées. Dans le cadre de cette thèse, nous proposons un modèle de politique de contrôle de flux d'information adapté aux architectures orientées services et en particulier aux orchestrations de services. Ce modèle offre aux utilisateurs la possibilité de spécifier des contraintes sur l'usage qui est fait de leurs données personnelles. Les politiques de contrôle de flux d'information définies suivant ce modèle sont définies au cours de l'exécution par l'utilisateur d'une orchestration de services. Les aspects dynamiques des Web-Services conduisent, en effet, à des situations où la politique peut empêcher l'exécution nominale de l'orchestration (par exemple lorsqu'il est fait usage d'un service que l'utilisateur ne connaissait pas avant l'exécution). A cet effet, nous proposons à l'utilisateur d'autoriser dynamiquement des modifications de la politique de contrôle de flux d'information. Afin de lui permettre d'effectuer cette modification, nous proposons dans le cadre de cette thèse un mécanisme permettant à l'utilisateur de disposer d'un maximum d'informations sur l'usage qui est fait de ses données et qui conduit à une violation de la politique de contrôle de flux d'information. Nous avons ensuite appliqué cette approche au langage d'orchestration BPEL. Nous avons en particulier présenté les principaux flux d'information qui interviennent dans ce langage. Nous avons enfin proposé une implémentation de ces mécanismes de contrôle de flux d'information en modifiant un orchestrateur BPEL existant.

Certains environnements ont besoin de plusieurs compilateurs, par exemple un pour le système d'exploitation, supportant la norme C/C++ complète, et l'autre pour les applications, qui supporte éventuellement un sous-ensemble de la norme, mais capable de fournir plus de performance. Le maintien de plusieurs compilateurs pour une plateforme cible représente un effort considérable. Il est donc plus facile d'implémenter et de maintenir un seul outil responsable des optimisations particulières au processeur ciblé. Il nous faut alors un moyen de relier ces compilateurs à l'optimiseur, de préférence, en gardant au passage certaines structures de données internes aux compilateurs qui, soit prendraient du temps, soit seraient impossible à reconstruire à partir du code assembleur par exemple. Dans cette thèse, nous introduisons Tirex, une représentation textuelle intermédiaire pour échanger des informations de bas niveau, déjà dépendantes de la cible, entre les compilateurs, les optimiseurs et les autres outils de la chaîne de compilation. Notre représentation contient un flot d'instructions du processeur cible, mais garde également la structure explicite du programme et supporte la forme SSA (Static Single Assignment). Elle est facilement extensible et très flexible, ce qui permet de transmettre toute donnée jugée importante à l'optimiseur. Nous construisons Tirex par extension de MinIR, une représentation intermédiaire elle-même basée sur un encodage YAML des structures du compilateur. Nos extensions de Tirex comprennent: l'abaissement de la représentation au niveau du processeur cible, la conservation du flot de données du programme, ainsi que l'ajout d'informations sur les structures de boucles et les dépendances de données. Nous montrons que Tirex est polyvalent et peut être utilisé dans une variété d'applications différentes, comme par exemple un environnement d'exécution virtuel (VEE),et fournit une base forte pour un environnement d'analyse du programme. Dans le cadre d'un VEE, nous présentons un interprèteur de la forme SSA et un compilateur just-in-time (JIT). Nous montrons comment l'interprétation d'une représentation au niveau du processeur cible élimine la plupart des problèmes liés à l'exécution en mode mixte. Nous explorons également les questions liées à l'interprétation efficace d'une représentation de programme sous la forme SSA.

La vérification déductive de programmes consiste à annoter des programmes par une spécification, c'est-à-dire un ensemble de formules logiques décrivant le comportement du programme, et à prouver que les programmes vérifient bien leur spécification. Des outils tels que la plate-forme Why prennent en entrée un programme et sa spécification et calculent des formules logiques telles que, si elles sont prouvées, le programme vérifie sa spécification. Ces formules logiques peuvent être prouvées automatiquement ou à l'aide d'assistants de preuve.Lorsqu'un programme est écrit dans un langage supportant les alias de pointeurs, c'est-à-dire si plusieurs variables peuvent désigner la même case mémoire, alors le raisonnement sur le programme devient particulièrement ardu. Il est nécessaire de spécifier quels pointeurs peuvent être égaux ou non. Les invariants des structures de données, en particulier, sont plus difficiles à vérifier.Cette thèse propose un système de type permettant de structurer la mémoire de façon modulaire afin de contrôler les alias de pointeurs et les invariants de données. Il est basé sur les notions de région et de permission. Les programmes sont ensuite interprétés vers Why de telle façon que les pointeurs soient séparés au mieux, facilitant ainsi le raisonnement. Cette thèse propose aussi un mécanisme d'inférence permettant d'alléger le travail d'annotation des opérations de régions introduites par le langage. Un modèle est introduit pour décrire la sémantique du langage et prouver sa sûreté. En particulier, il est prouvé que si le type d'un pointeur affirme que celui-ci vérifie son invariant, alors cet invariant est effectivement vérifié dans le modèle. Cette thèse a fait l'objet d'une implémentation sous la forme d'un outil nommé Capucine. Plusieurs exemples ont été écrits pour illustrer le langage, et ont été vérifié à l'aide de Capucine.

En ajoutant au lambda-calcul des structures de données algébriques, des types dépendants et un système de modules, on obtient un langage de programmation avec peu de primitives mais une très grande expressivité. L'assistant de preuve Coq s'appuie sur un tel langage (le CIC) à la sémantique particulièrement claire. L'utilisateur n'écrit pas directement de programme en CIC car cela est ardu et fastidieux. Coq propose un environnement de programmation qui facilite la tâche en permettant d'écrire des programmes incrémentalement grâce à des constructions de haut niveau plus concises. Typiquement, les types dépendants imposent des contraintes fortes sur les données. Une analyse de cas peut n'avoir à traiter qu'un sous-ensemble des constructeurs d'un type algébrique, les autres étant impossibles par typage. Le type attendu dans chacun des cas varie en fonction du constructeur considéré. L'impossibilité de cas et les transformations de type doivent être explicitement écrites dans les termes de Coq. Pourtant, ce traitement est mécanisable et cette thèse décrit un algorithme pour réaliser cette automatisation. Par ailleurs, il est nécessaire à l'interaction avec l'utilisateur de calculer des programmes du CIC sans faire exploser la taille syntaxique de la forme réduite. Cette thèse présente une machine abstraite conçu dans ce but. Enfin, les points fixes permettent une manipulation aisée des structure de données récursives. En contrepartie, il faut s'assurer que leur exécution termine systématiquement. Cette question sensible fait l'objet du dernier chapitre de cette thèse.

Mémoire (M.Eng.)-- Université du Québec ;a Chicoutimi, 1993. / Résumé disponible sur Internet. CaQCU Document électronique également accessible en format PDF. CaQCU

Les travaux de cette thèse s'inscrivent dans le contexte général des réseaux logiciels, dits "Software-Defined Networking" (SDN). Ce paradigme récent est l'une des initiatives les plus notables pour rendre les réseaux actuels programmables ou, en d'autres termes, plus simple à configurer, à tester, à corriger et à faire évoluer. Dans un écosystème SDN, l'interface nord (Northbound API) est utilisée par l'administrateur réseaux pour définir ses politiques et programmer le plan de contrôle, elle représente donc un enjeu majeur. Idéalement, cette interface nord devrait permettre aux administrateurs de décrire, le plus simplement possible, des services réseaux et leurs interactions, plutôt que de spécifier comment et sur quels équipements physiques ils doivent être déployés. Des travaux existants montrent que cela peut être notamment réalisé grâce à des solutions de virtualisation de réseaux et des langages de programmation dédiés de haut niveau. L'objectif de ce travail de thèse est de proposer une nouvelle interface nord qui, d'une part, exploiterait la virtualisation de réseau et, d'autre part, exposerait ses services sous la forme d'un langage de programmation dédié. Actuellement, plusieurs langages intégrant des solutions de virtualisation de réseau existent. Néanmoins, nous pensons que les modèles d'abstraction qu'ils utilisent pour construire des réseaux virtuels restent inappropriés pour assurer des critères de simplicité, modularité et flexibilité des topologies virtuelles et des programmes de contrôle. Dans ce contexte, nous proposons un nouveau langage de contrôle de réseaux nommé AirNet. Ce dernier intègre un modèle d'abstraction dont la principale caractéristique est d'offrir une séparation nette entre les équipements de bordure (Edge) et de cœur de réseau (Fabric). Cette idée est bien connue et acceptée dans le domaine des architectures réseaux. L'originalité de notre contribution étant de faire remonter ce concept au niveau du plan de contrôle virtuel et non de le restreindre au seul plan physique. Ainsi, des frontières logiques entre les différents types de politiques existeront (fonctions de contrôle et de données vs. fonctions de transport), garantissant ainsi la modularité et la réutilisabilité de tout ou partie du programme de contrôle. De plus, dans l'approche proposée, la définition du réseau virtuel et des politiques peut être totalement dissociée de l'infrastructure physique cible, favorisant ainsi la portabilité des applications de contrôle. Une implémentation du langage AirNet a également été réalisée. Ce prototype inclut en particulier une bibliothèque des primitives et opérateurs du langage, ainsi qu'un hyperviseur qui assure la composition des politiques de contrôle sur un réseau virtuel, et leur transposition (mapping) sur l'infrastructure physique. Afin de s'appuyer sur des contrôleurs SDN existants, l'hyperviseur inclut des modules d'intégration des contrôleurs POX et RYU. Une validation expérimentale a été menée sur différents cas d'étude (filtrage, répartition de charge, authentification dynamique, limitation de bande passante, etc.) dont les résultats attestent de la faisabilité de la solution. Enfin, des mesures de performances ont montré que le surcoût apporté par cette nouvelle couche d'abstraction est parfaitement acceptable. / The work of this thesis falls within the general context of software-defined networking (SDN). This new paradigm is one of the most significant initiatives to enable networks programmability or, in other words, to make current networks easier to configure, test, debug and evolve. Within an SDN ecosystem, the Northbound interface is used by network administrators to define policies and to program the control plane, it thus represents a major challenge. Ideally, this northbound interface should allow administrators to describe, as simply as possible, network services and their interactions, rather than specifying how and on what physical device they need to be deployed. Current related works show that this can be partly achieved through virtualization solutions and high-level domain specific languages (DSL). The objective of this thesis is to propose a new Northbound interface which will, on the one hand, rely on network virtualization and, on the other hand, expose its services as a domain specific programming language. Currently, several languages that include network virtualization solutions exist. Nevertheless, we believe that the abstract models they are using to build virtual networks remain inadequate to ensure simplicity, modularity and flexibility of virtual topologies and control programs. In this context, we propose a new network control language named AirNet. Our language is built on top of an abstraction model whose main feature is to provide a clear separation between edge and core network devices. This concept is a well-known and accepted idea within the network designer community. The originality of our contribution is to lift up this concept at the virtual control plane, not limiting it solely at the physical plane. Thus, logical boundaries between different types of policies will exist (control and data functions vs. transport functions), ensuring modularity and reusability of the control program. Moreover, in the proposed approach, the definition of the virtual network and policies is totally dissociated from the target physical infrastructure, promoting the portability of control applications. An implementation of the AirNet language has also been done. This prototype includes in particular a library that implements the primitives and operators of the language, and a hypervisor that achieves the composition of the control policies on the virtual network, and their mapping on the physical infrastructure. In order to rely on existing SDN controllers, the hypervisor includes integration modules for the POX and RYU controllers. An experimental validation has been also conducted on different use cases (filtering, load balancing, dynamic authentication, bandwidth throttling, etc.), whose results demonstrate the feasibility of our solution. Finally, performance measurements have shown that the additional cost brought by this new abstraction layer is perfectly acceptable.

Les architectures parallèles sont de plus en plus présentes dans notre environnement, que ce soit dans les ordinateurs personnels disposant des dizaines d’unités de calculs jusqu’aux super-calculateurs comptant des millions d’unités. Les architectures haute performance modernes sont généralement constituées de grappes de multiprocesseurs, elles même constituées de multi-cœurs, et sont qualifiées d’architecture hiérarchiques. La conception de langages pour de telles architectures est un sujet de recherche actif car il s’agit de simplifier la programmation tout en garantissant l’efficacité des programmes. En effet, écrire des programmes parallèles est, en général, plus complexe tant au point de vue algorithmique qu’au niveau de l’implémentation. Afin de répondre à cette problématique, plusieurs modèles structurés ont été proposés. Le modèle logico-materiel BSP définit une vision structurée pour les architectures parallèles dites plates. Afin d’exploiter les architectures actuelles, une extension adaptée aux architectures hiérarchiques a été proposée : Multi-BSP. Tout en préservant la philosophie BSP, ce modèle garanti efficacité, sécurité d’exécution, passage à l’échelle et prédiction de coût.Cette thèse s’articule donc autour de cette idée et propose de définir Multi-ML, un langage basé sur le modèle logico-materiel Multi-BSP, garantissant les propriétés énoncées ci-dessus. Afin de pouvoir garantir la sécurité d’exécution des programmes Multi-ML, nous proposons une sémantique formelle ainsi qu’un système de type afin d’accepter uniquement des programmes bien formés. De plus, nous proposons une machine abstraite permettant de décrire formellement l’évaluation d’un programme Multi-ML sur une machine Multi-BSP. Une implantation du langage, développé dans le cadre de cette thèse, permet de générer un code exécutable. Il est donc possible d’exécuter, efficacement, des algorithmes Multi-BSP écrits à l’aide de Multi-ML sur diverses machines hiérarchiques / From personal computers using an increasing number of cores, to supercomputers having millions of computing units, parallel architectures are the current standard. The high performance architectures are usually referenced to as hierarchical, as they are composed from clusters of multi-processors of multi-cores. Programming such architectures is known to be notoriously difficult. Writing parallel programs is, most of the time, difficult for both the algorithmic and the implementation phase. To answer those concerns, many structured models and languages were proposed in order to increase both expressiveness and efficiency. Among other models, Multi-BSP is a bridging model dedicated to hierarchical architecture that ensures efficiency, execution safety, scalability and cost prediction. It is an extension of the well known BSP model that handles flat architectures.In this thesis we introduce the Multi-ML language, which allows programming Multi-BSP algorithms “à la ML” and thus, guarantees the properties of the Multi-BSP model and the execution safety, thanks to a ML type system. To deal with the multi-level execution model of Multi-ML, we defined formal semantics which describe the valid evaluation of an expression. To ensure the execution safety of Multi-ML programs, we also propose a typing system that preserves replicated coherence. An abstract machine is defined to formally describe the evaluation of a Multi-ML program on a Multi-BSP architecture. An implementation of the language is available as a compilation toolchain. It is thus possible to generate an efficient parallel code from a program written in Multi-ML and execute it on any hierarchical machine

Cette thèse porte sur l'analyse statique de code par typage dans le but de détecter les erreurs dans les programmes avant leur exécution. Plus précisément, nous nous intéressons ici au domaine du sous-typage, dans lequel les propriétés du code sont représentées par des ensemble de contraintes de la forme (t1 <= t2). Nos mécanismes de vérification sont alors basés sur l'agrégation de contraintes de sous-typage et la vérification de leur compatibilité par saturation. Le langage de base sur lequel nous travaillons est un ML étendu, muni de variants et d'un mécanisme de filtrage de motifs. Nous commençons par définir un formalisme nous permettant d'exprimer nos systèmes de types sous forme de règles d'inférences. Ce formalisme présente l'avantage d'être suffisamment souple pour nous permettre de prouver les propriétés de validité et de terminaison de nos systèmes, et suffisamment précis pour nous permettre d'en dériver une implémentation de manière systématique. Après avoir défini un système de types de base pour notre langage, nous en présentons trois extensions originales : * Une amélioration du typage du filtrage de motifs basée en particulier sur l'ajout d'un opérateur de disjonction entre les contraintes de sous-typage. Cet opérateur permet alors d'exprimer, pour chaque cas de filtrage, le lien entre le filtre et les contraintes extraites du typage de l'expression correspondante. Ceci nous permet en particulier de représenter beaucoup plus finement le type de certaines fonctions et ainsi d'accepter plus de programmes valides. * Une alternative au mécanisme classique de généralisation permettant de distinguer les contraintes associées aux différents usages des paramètres des fonctions. Un tel mécanisme rend en particulier la construction de langage "let" de ML obsolète. Mixé avec la première extension, nous obtenons un système permettant d'encoder dans le langage lui même (c'est à dire sans ajouter de construction supplémentaire), un modèle objet intéressant. * Une formalisation des GADT basée sur une implantation originale des variables de type existentielles. En plus d'être compatible avec le sous-typage, cette variante des GADT présente une amélioration notable par rapport aux GADT standards par le fait qu'elle étend les possibilités d'inférence. Les annotations de type, habituellement obligatoires en présence de GADT, deviennent ici presque toutes facultatives. Bien qu'il soit possible de dériver directement une implémentation de ces systèmes, ce qui est principalement utile pour leur compréhension et leur prototypage, les performances des typeurs obtenus de la sorte ne sont pas suffisantes pour analyser des programmes de taille réelle. Ceci est principalement dû aux différentes extensions que nous apportons au langage des contraintes, en particulier les opérateurs de disjonction et de négation. Nous présentons alors les différentes techniques que nous avons mises en place pour l'implémentation de nos systèmes permettant à nos analyses de passer à l'échelle en pratique. / This PHD thesis focuses on static analysis of programs by type inference in order to detect program errors before their execution. More precisely, we focus hear in the field of sub-typing, where program properties are described by sets of constraints of the form (t1 <= t2). Our verification mechanisms are based on the aggregation of sub-typing constraints and checking of their compatibility by saturation. The base language on which we define our type systems is an ML-like language provided with variants and pattern matching. We starts by defining a formalism to express our type systems thanks to inference rules. This formalism has the advantage to be sufficiently flexible to allow proving validity and termination properties of our systems, and sufficiently precise to allow a systematic derivation of our inference rules into a runnable typer. After the definition of a base type system for our language, we present three novel extensions: * An improvement of type inference for the pattern matching based on the addition of the "or" operator between sub-typing constraints. This operator allow to express a link, in each cases of a match, between the pattern and the constraints generated at typing time of the case expression. This allows us to refine the type of some functions, and then to accept more valid programs. * A new implementation of the generalization mechanism. This allows to distinguish constraints associated to the different occurrences of a function parameter in its body. Thanks to this mechanism, the "let" construction from ML is in particular obsolete. By mixing this extension with the first one, we obtain a type system able to encode "objects" without any additional language construction. * A formalization of GADT based on an novel implementation of existential type variables. In addition to be compatible with the sub-typing context of this thesis, this alternative to GADT has the advantage to improve type inference. As a consequence, most of type annotations, usually required in the presence of GADT, are now optional. Despite the fact that it is possible to directly derive an implementation of our type systems from their rules, that is principally interesting for their comprehension and prototyping, the effectiveness of such typer is insufficient to analyze real world programs. This is principally due to the extensions we provide to the language of constraints, and in particular to the "or" and "not" operators. At then end, we present multiple techniques we used in our implementation to extend the scalability of our analysis.