Les problèmes d'allocation de ressources suscitent un intérêt croissant aussi bien en Économie qu'en Informatique. Ordinairement, ils sont résolus par des techniques centralisées, dans lesquelles une entité omnisciente détermine comment allouer les ressources de manière optimale. Cependant, ces approches font des hypothèses qui ne sont pas toujours réaliste. Or, il n'est souvent pas possible d'avoir une entité omnisciente. Certaines applications sont dynamiques et nécessitent une méthode de résolution adaptative qui puisse prendre en compte de nouvelles informations durant la résolution. Ces approches considèrent toujours que les communications entre les participants ne sont pas restreintes, ce qui n'est évidemment pas le cas dans la plupart des cas, comme dans les réseaux pair-à-pair par exemple où un pair ne peut communiquer qu'à un ensemble restreint du système.Dans cette thèse, nous nous focalisons sur les méthodes de ré-allocation distribuées, basée sur des systèmes multi-agents, qui transforment une allocation initiale par des séquences de transactions locales entre agents. Nous cherchons à concevoir des comportements d'agents menant un processus de négociation à une allocation socialement optimale. Cette allocation peut alors être vue comme un phénomène émergent. Nous voulons également identifier les paramètres favorisant l'efficacité des négociations ainsi que ceux qui la restreignent. Nous considérons différentes mesures de bien-être social et nous fournissons les comportements à implémenter pour négocier efficacement dans chaque cas. Nous proposons une méthode adaptative et ``anytime'' où n'importe quel type de réseau d'accointances peut être considéré. / Resource allocation problems have been widely studied according to various scenarios in the literature. They are usually solved by means of centralized techniques, where an omniscient entity determines how to optimally allocate resources. However, these solving methods are not well-adapted for applications where privacy is required. Moreover, several assumptions made are not always plausible, which may prevent their use in practice, especially in the context of agent societies. For instance, dynamic applications require adaptive solving processes, which can handle the evolution of initial data. Such techniques never consider restricted communication possibilities whereas many applications are based on. For instance, in peer-to-peer networks, a peer can only communicate to a small subset of the systems.In this thesis, we focus on distributed methods to solve resource allocation problems. Initial allocations evolves step by step thanks to local agent negotiations. We seek to provide agent behaviors leading negotiation processes to socially optimal allocations. In this work, resulting resource allocations can be viewed as emergent phenomena. We also identify parameters favoring the negotiation efficiency. We provide the agent behavior to implement when four different social welfare notions are considered. The original method proposed in thesis is adaptive, anytime and can handle any restriction on agent communication possibilities.

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal.

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal

Cette thèse s’intéresse au problème d’estimation et d’optimisation distribuée dans les réseaux asynchrones, c’est à dire en n’utilisant que des communication locales et asynchrones. A partir de multiples applications allant de l’apprentissage automatique aux réseaux de capteurs sans-fils, nous concevons et analysons théoriquement de nouveaux algorithmes résolvant trois problèmes de nature très différentes : la propagation de la plus grande des valeurs initiales, l’estimation de leur moyenne et enfin l’optimisation distribuée. / This thesis addresses the distributed estimation and optimization of a global value of interest over a network using only local and asynchronous (sometimes wireless) communications. Motivated by many different applications ranging from cloud computing to wireless sensor networks via machine learning, we design new algorithms and theoretically study three problems of very different nature : the propagation of the maximal initial value, the estimation of their average and finally distributed optimization.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Le calcul sur grille permet à un individu, une société, de disposer d’un ensemble d’unités de calcul fournies par des tiers. Dans ce type d’architecture, des problèmes de sécurité se posent : comment garantir à la fois la sécurité du matériel et de l’application. Pour ce qui concerne la sécurité de l’application, il s’agit principalement d’assurer la confidentialité du code et l’intégrité de son exécution. La sécurité du matériel consiste à protéger la machine contre tout code malveillant pouvant être contenu dans l’application. Aucun système ne permet aujourd’hui, de satisfaire ces contraintes fortes de sécurité. Notre objectif dans cette thèse est de proposer et de valider des solutions pour les problèmes de sécurité des grilles informatiques.Pour résoudre ces problèmes, nous proposons l’utilisation de la carte à puce comme support d’exécution hautement sécurisé à travers le déploiement de grilles de cartes à puce. Grâce aux mécanismes de sécurité qu’elles intègrent, les cartes à puce permettent en effet de protéger l’application et son code aussi bien que le support d’exécution. Le travail effectué dans cette thèse consiste à définir un environnement pour le calcul sécurisé sur grille de cartes à puce. / Abstract

La propension des systèmes informatiques à subir des défaillances matérielles est à l'origine d'une recherche abondante afin de concevoir des systèmes dits tolérants aux pannes. Le procédé couramment retenu consiste à procéder à des réplications, donnant alors naissance à ce que l'on nomme un système distribué. La question se pose alors de savoir si l'on peut garantir que les multiples copies sont cohérentes entre elles. Ainsi, la recherche d'un accord devient-elle un problème à résoudre, à portée paradigmatique : le Consensus. Or, la complexité des algorithmes de Consensus rend la tache ardue : il n'est donc pas rare que l'on commette des erreurs lors de leur conception. De là découle l'idée, développée depuis plus de trente ans, de recourir à des procédés de vérification mécanique des algorithmes et de leurs preuves de correction. Ces procédés prennent place parmi ce que l'on désigne usuellement comme étant des méthodes formelles. C'est à la croisée des recherches en algorithmique distribuée et en méthodes formelles que se situent nos travaux. Plus spécifiquement, il s'agit de faire usage d'un logiciel de certification formelle, Isabelle/HOL, afin de garantir l'exactitude des preuves de correction d'algorithmes de Consensus exprimés dans un cadre formel uniforme du nom de Heard-Of, proposé en 2009 par Charron-Bost et Schiper. Nous montrons que, du fait de leur expression dans un même cadre formel, et du fait de leur proximité, suivant les cas, soit de conception (nombre de rondes, recours à des mécanismes de vote, ...) soit de forme syntaxique, soit d'hypothèses de fonctionnement (synchronisme partiel, ...), ces algorithmes présentent des preuves dont une part conséquente d?arguments sont communs. Cela permet de copier certains d'entre eux d'une preuve à l'autre, afin de réduire l'effort de certification : ces arguments peuvent alors être automatiquement évalués par la machine pour chacun d'entre eux, l'utilisateur n'ayant à intervenir que là où celle-ci est en peine, c'est-à-dire lorsque les différences algorithmiques induisent qu'il faille réviser les détails de l'argumentation. L'exposé que nous faisons de la certification que nous avons effectuée pour six algorithmes distribués dédiés à la résolution du problème du Consensus illustre cette démarche. Par conséquent, nous présentons d'abord les portions communes des démonstrations, puis détaillons ce qui est propre à chacune, l'objectif n'étant pas de permettre une lecture linéaire de chaque démonstration mais de mettre en évidence notre proposition / Computer systems fail. Whatever the reason of these failures, it has been a widespread approach to try and increase the faults-tolerance of a computer system through its replication. The resulting system is said to be a distributed one, in which replicas have to be kept consistent with each others. Hence, reaching agreement, and Consensus in particular, becomes the problem to solve - indeed, the paradigm. Solving Consensus (under various assumptions) is a hard task : algorithms designed on this purpose are subtle and proving their being correct is error-prone - whenever they are, which occasionally appears not to be the case. For more that thirty years, researchers interested in what is called Formal Methods have been working on mechanizing the verification process, in order to increase confidence in the correctness of (distributed) algorithms. The work we present here is at the intersection of distributed algorithms and formal methods. We use the Isabelle/HOL software to certify the correctness proof of various Consensus algorithms expressed in a uniform framework based on the Heard-Of Model, introduced by Charron-Bost and Schiper in 2009. Expressed in a common model, these algorithms, which, depending on the case, share some common mecanisms (number of steps, intermediate votes, ...), some elements of syntax, or types of assumptions (partial synchronism...), can be proved using some common arguments. As a consequence, the certification effort can be reduced by copying some intermediate lemmas from one proof to another and let the computer automatically parse them until some manual adaptation is required. This lead to the idea of certifying the correctness of multiple algorithms all together, instead of proving them one after the other, as one would do on paper in a traditional way. The effort of translation in the formal language of the proof assistant is then possibly reduced. Of course, each proof will also contain specific arguments, which will have to be isolated and translated into the software. Here, we illustrate this proposition through the presentation of formal certificates of correctness for six Consensus algorithms. As a consequence, on should not expect to find here a comprehensive linear presentation of each proof : we first show the arguments shared by multiple proofs, followed by those which are specific to each o them

Bien que le développement actuel d'accélérateurs se concentre principalement sur la création de puces Multiprocesseurs (MPSoC) hétérogènes, c'est-à-dire composés de processeurs spécialisées, de nombreux acteurs de la microélectronique s'intéressent au développement d'un autre type de MPSoC, constitué d'une grille de processeurs identiques. Ces MPSoC homogènes, bien que composés de processeurs énergétiquement moins efficaces, possèdent une programmabilité et une flexibilité plus importante que les MPSoC hétérogènes, ce qui favorise notamment l'adaptation du système à la charge demandée, et offre un espace de solutions de configuration potentiellement plus vaste et plus simple à contrôler. C'est dans ce contexte que s'inscrit cette thèse, en exposant la création d'une architecture MPSoC homogène scalable (c'est-à-dire dont la mise à l'échelle des performances est linéaire), ainsi que le développement de différents systèmes d'adaptation et de programmation sur celle-ci.Cette architecture, constituée d'une grille de processeurs de type MicroBlaze, possédant chacun sa propre mémoire, au sein d'un Réseau sur Puce 2D, a été développée conjointement avec un système d'exploitation temps réel (RTOS) spécialisé et modulaire. Grâce à la création d'une pile de communication complexe, plusieurs mécanismes d'adaptation ont été mis en œuvre : une migration de tâche « avec redirection de données », permettant de diminuer l'impact de cette migration avec des applications de type flux de données, ainsi qu'un mécanisme dit « d'exécution distante ». Ce dernier consiste non plus à migrer le code instruction d'une mémoire à une autre, mais de conserver le code dans sa mémoire initiale et de le faire exécuter par un processeur distinct. Les différentes expériences réalisées avec ce mécanisme ont permis de souligner la meilleure réactivité de celui-ci face à la migration de tâche, tout en possédant des performances d'adaptation plus faible.Ce dernier mécanisme a conduit naturellement à la création d'un modèle de programmation de type « mémoire partagée » au sein de l'architecture. La mise en place de ce dernier nécessitait la création d'un mécanisme de cohérence mémoire, qui a été réalisé de façon matérielle/logicielle et scalable par l'intermédiaire du développement de la librairie PThread. Les performances ainsi obtenues mettent en évidence les avantages d'un MPSoC homogène tout en utilisant une programmation « classique » de type multiprocesseur. / Although the accelerators market is dominated by heterogeneous MultiProcessor Systems-on-Chip (MPSoC), i.e. with different specialized processors, a growing interest is put on another type of MPSoC, composed by an array of identical processors. Even if these processors achieved lower performance to power ratio, the better flexibility and programmability of these homogeneous MPSoC allow an easier adaptation to the load, and offer a wider space of configurations. In this context, this thesis exposes the development of a scalable homogeneous MPSoC – i.e. with linear performance scaling – and different kind of adaptive mechanisms and programming model on it.This architecture is based on an array of MicroBlaze-like processors, each having its own memory, and connected through a 2D NoC. A modular RTOS was build on top of it. Thanks to a complex communication stack, different adaptive mechanisms were made: a “redirected data” task migration mechanism, reducing the impact of the migration mechanism for data-flow applications, and a “remote execution” mechanism. Instead of migrate the instruction code from a memory to another, this last consists in only migrate the execution, keeping the code in its initial memory. The different experiments shows faster reactivity but lower performance of this mechanism compared to migration.This development naturally led to the creation of a shared memory programming model. To achieve this, a scalable hardware/software memory consistency and cache coherency mechanism has been made, through the PThread library development. Experiments show the advantage of using NoC based homogeneous MPSoC with a brand programming model.

L'objectif de cette thèse est l'étude de la synthèse de plans dans un contexte multi-agent. La problèmatique principale est de comprendre les mécanismes qui permettent à une société d'agents autonomes de construire collectivement un plan global. Contrairement aux approches classiques dans lesquelles la planification n'est qu'un outil parmi d'autres pour définir les activités des agents et la coordination une «surcouche» nécessaire à leur synchronisation, la contribution de nos travaux repose sur la conception d'un modèle de planification entièrement distribué dans lequel les agents raisonnent conjointement sur leurs activités respectives pour atteindre un but commun prédéfini en intégrant leurs compétences hétérogènes ainsi que leurs croyances partielles sur le monde. Dans cette perspective, nous proposons de considérer la synthèse de plans comme un raisonnement collectif et révisable fondé sur l'échange entre les agents de conjectures, i.e., des plans qui peuvent être exécutés si certaines conditions sont vérifiées et de réfutations, i.e., des objections quant à la réalisation du plan. Les intéractions entre agents peuvent se définir comme un processus dialectique d'investigation dans lequel les agents proposent leurs compétences pour démonter la validité de certaines hypothèses, réfuter les conjectures non réalisables, réparer lorsque cela est possible les conjectures précédemment réfutées et ainsi élaborer pas à pas un plan solution.

La thèse porte sur la structure argumentale des verbes parasynthétiques italiens. Elle s'intéresse En particulier à deux sous-groupes : les dénominaux dont la paraphrase est « faire devenir S », où S est le substantif de base (appelés BN); et les désadjectivaux dont la paraphrase est « faire quelque chose plus A », où A est l'adjective de base (appelés DPV). Les deux types de verbes posent des questions très différentes, mais liées à la question de la syntaxe lexicale : les premiers forment une construction seconde inattendue dans le domaine roman ; les deuxièmes peuvent générer deuxlectures aspectuelles (stative et événementiel) même en étant causatifs.La thèse s'ouvre avec des chapitres de caractère général. Le premier plaide pour une amélioration des méthodes de collecte de données dans le domaine génératif. Les deuxième et troisième chapitres décrivent les cadres formels pertinents ainsi que la parasynthèse.La première partie de la thèse porte sur les BN. Au moyen de tests conduits sur des locuteurs natifs de l'italien, elle affirme et analyse l'acceptabilité de la construction pseudo-résultative en italien. Cette enquête se poursuit par une comparaison avec les données du français, qui se comporte différemment. La deuxième partie s'ouvre avec une réflexion sur les diagnostics de la stativité, et se poursuit avec l'analyse des DPVs. En particulier, le concept de causalité stative est analysé et traduit dans la théorie de la causalité de force-dynamics.Enfin, une application au TALN des diagnostics de stativité est décrite dans le dernier chapitre. L'importance de l'identification précise de la stativité est éclaircie. / The present dissertation investigates the argument structure of two groups of Italian parasyntheticverbs: denominal verbs paraphrased as "make X become N", where N is the base noun (henceforth BN); adjectival verbs paraphrased as "make X more A", where A is the base adjective. The two groups present different issues linked to the lexical syntax, the former can participate in a secondary predication that is unexpected for Romance languages; the latter can receive two aspectual readings (stative and eventive) which are both causative.The dissertation starts with three chapters of general interest. The first one describes new experimental methods that can be employed in generative linguistics. The second and third one describe useful frameworks and the morphological process of parasynthesis.The first part of the dissertation analyses BNs. It is shown by means of several experiments that Italian native speakers accept the pseudo-resultative construction. Results of a comparative study with French are reported and show that French behaves differently to Italian in this respect.4The second part analyses stativity diagnostics and apply them in the study of DPVs. It gives account for the causal stativity in the force-dynamic framework.The last chapter applies stativity diagnostics in the natural language processing domain.