Les systèmes distribués sont au coeur des technologies de l'information.Il est devenu classique de s'appuyer sur multiples unités distribuées pour améliorer la performance d'une application, la tolérance aux pannes, ou pour traiter problèmes dépassant les capacités d'une seule unité de traitement. La conception d'algorithmes adaptés au contexte distribué est particulièrement difficile en raison de l'asynchronisme et du non-déterminisme qui caractérisent ces systèmes. La simulation offre la possibilité d'étudier les performances des applications distribuées sans la complexité et le coût des plates-formes d'exécution réelles. Par ailleurs, le model checking permet d'évaluer la correction de ces systèmes de manière entièrement automatique. Dans cette thèse, nous explorons l'idée d'intégrer au sein d'un même outil un model checker et un simulateur de systèmes distribués. Nous souhaitons ainsi pouvoir évaluer la performance et la correction des applications distribuées. Pour faire face au problème de l'explosion combinatoire des états, nous présentons un algorithme de réduction dynamique par ordre partiel (DPOR), qui effectue une exploration basée sur un ensemble réduit de primitives de réseau. Cette approche permet de vérifier les programmes écrits avec n'importe laquelle des interfaces de communication proposées par le simulateur. Nous avons pour cela développé une spécification formelle complète de la sémantique de ces primitives réseau qui permet de raisonner sur l'indépendance des actions de communication nécessaire à la DPOR. Nous montrons au travers de résultats expérimentaux que notre approche est capable de traiter des programmes C non triviaux et non modifiés, écrits pour le simulateur SimGrid. Par ailleurs, nous proposons une solution au problème du passage à l'échelle des simulations limitées pour le CPU, ce qui permet d'envisager la simulation d'applications pair-à-pair comportant plusieurs millions de noeuds. Contrairement aux approches classiques de parallélisation, nous proposons une parallélisation des étapes internes de la simulation, tout en gardant l'ensemble du processus séquentiel. Nous présentons une analyse de la complexité de l'algorithme de simulation parallèle, et nous la comparons à l'algorithme classique séquentiel pour obtenir un critère qui caractérise les situations où un gain de performances peut être attendu avec notre approche. Un résultat important est l'observation de la relation entre la précision numérique des modèles utilisés pour simuler les ressources matérielles, avec le degré potentiel de parallélisation atteignables avec cette approche. Nous présentons plusieurs cas d'étude bénéficiant de la simulation parallèle, et nous détaillons les résultats d'une simulation à une échelle sans précédent du protocole pair-à-pair Chord avec deux millions de noeuds, exécutée sur une seule machine avec un modèle précis du réseau / Distributed systems are in the mainstream of information technology. It has become standard to rely on multiple distributed units to improve the performance of the application, help tolerate component failures, or handle problems too large to fit in a single processing unit. The design of algorithms adapted to the distributed context is particularly difficult due to the asynchrony and the nondeterminism that characterize distributed systems. Simulation offers the ability to study the performance of distributed applications without the complexity and cost of the real execution platforms. On the other hand, model checking allows to assess the correctness of such systems in a fully automatic manner. In this thesis, we explore the idea of integrating a model checker with a simulator for distributed systems in a single framework to gain performance and correctness assessment capabilities. To deal with the state explosion problem, we present a dynamic partial order reduction algorithm that performs the exploration based on a reduced set of networking primitives, that allows to verify programs written for any of the communication APIs offered by the simulator. This is only possible after the development of a full formal specification with the semantics of these networking primitives, that allows to reason about the independency of the communication actions as required by the DPOR algorithm. We show through experimental results that our approach is capable of dealing with non trivial unmodified C programs written for the SimGrid simulator. Moreover, we propose a solution to the problem of scalability for CPU bound simulations, envisioning the simulation of Peer-to-Peer applications with millions of participating nodes. Contrary to classical parallelization approaches, we propose parallelizing some internal steps of the simulation, while keeping the whole process sequential. We present a complexity analysis of the simulation algorithm, and we compare it to the classical sequential algorithm to obtain a criteria that describes in what situations a speed up can be expected. An important result is the observation of the relation between the precision of the models used to simulate the hardware resources, and the potential degree of parallelization attainable with this approach. We present several case studies that benefit from the parallel simulation, and we show the results of a simulation at unprecedented scale of the Chord Peer-to-Peer protocol with two millions nodes executed in a single machine

Comprendre les performances d'une application multi-thread est difficile. Les threads interfèrent quand ils accèdent à la même ressource, ce qui ralentit leur exécution. Malheureusement, les outils de profiling existants se focalisent sur l'identification des causes de l'interférence, et non pas sur ses effets.Le développeur ne peut donc pas conclure si l'optimisation d'une interférence identifiée par un outil de profiling peut mener à une meilleure performance. Dans cette thèse, on propose de compléter les outils existants par un outil orienté-effet capable de quantifier l'impact de l'interférence sur la performance, indépendamment de la cause de l'interférence. Avec une évaluation de 27 applications, on montre que notre outil réussit à identifier 12 bottlenecks causés par 6 types d'interférence différents / Understanding the performance of a multi-threaded application is difficult. The threads interfere when they access the same resource, which slows their execution down. Unfortunately, current profiling tools focus on identifying the interference causes, not their effects.The developer can thus not know if optimizing the interference reported by a profiling tool can lead to better performance. In this thesis, we propose to complete the profiling toolbox with an effect-oriented profiling tool able to indicate how much interference impacts performance, regardless of the interference cause. With an evaluation of 27 applications, we show that our tool successfully identifies 12 performance bottlenecks caused by 6 different kinds of interference

Les thèmes de recherche présentés s'articulent autour des architectures et des protocoles de communication et de coordination pour les logiciels distribués coopératifs. Dans le cas de la communication, nous avons étudié un contexte d'interaction synchrone point-à-point, et dans le cas de la coordination, différents types et modes d'interaction sont considérés : synchrones / asynchrones, point-à-points ou multi-points, par échange de messages ou par invocation de méthodes à distance. Nos contributions ont concerné la spécification, la modélisation, la conception, la validation, l'implémentation et l'expérimentation. L'adoption d'une démarche orientée modèle formel constitue une caractéristique partagée par les différents résultats de cette recherche. Cette démarche, orientée modèle, appliquée aux problèmes de conception et de validation des systèmes à architecture multi-composants peut être considérée comme un fil conducteur dont dérive l'ensemble de nos travaux. L'étude du comportement des composants d'une architecture, qui peut se définir comme l'ensemble des règles qui décrivent la dynamique de leurs interactions, a constitué nos travaux de recherche initiaux. Les travaux ultérieurs se sont ouverts pour couvrir les problèmes relatifs à la coordination d'ensembles de composants, laquelle inclut, en particulier, l'intégration et la distribution de ces composants sous différentes contraintes architecturales : interdépendance, dynamisme et distribution. Enfin, la gestion de la dynamique de l'architecture et de ses interactions distribuées ainsi que son application pour le support des activités génériques de coopération ont été deux axes majeurs dans les problèmes traités. L'édition en groupe a constitué pour nous une catégorie spécifique d'activité coopérative. La télé-ingénierie et la télé-formation ont constitué nos domaines d'expérimentation principaux.

No description available.

Les réseaux mobiles ad hoc (MANETs) se forment spontanément à partir de terminaux mobiles qui communiquent en utilisant des interfaces sans fil à faible portée (e.g. Wi-Fi, Bluetooth). Dans la plupart des réseaux ad hoc déployés dans des conditions réelles, ces terminaux mobiles peuvent être volatiles et distribués de manière clairsemée, et former par conséquent des îlots de connectivité qui évoluent continuellement. Dans cette thèse, je considère spécifiquement ce type de réseaux, qui sont appelés MANETs discontinus. Les communications dans les MANETs discontinus présentent un défi, parce que les protocoles de routage conçus pour les MANETs connexes ne fonctionnent pas dans de tels réseaux. L'approche storecarry- and-forward est proposée depuis quelques années pour palier les discontinuités du réseau. Elle permet à un nœud de stocker temporairement un message, afin de le transmettre plus tard quand les conditions deviennent favorables. La mobilité des nœuds devient alors un avantage, en facilitant la propagation des messages d'un îlot vers un autre. L'approche orientée services semble appropriée pour mettre en œuvre des applications dans les MANETs discontinus à cause de la nature découplée des entités qu'elle met en jeu. En effet, le découplage entre un client et un fournisseur de service est essentiel dans un environnement où la disponibilité des fournisseurs est fluctuante, et où les communications de bout en bout ne sont pas garanties. Malgré ce découplage, dans les systèmes orientés services existants les fournisseurs sont souvent supposés stables et toujours accessibles. Bien que l'approche orientée services semble appropriée dans les MANETs discontinus, la mise en œuvre de services distribués nécessite des communications dans l'ensemble du réseau, malgré la fragmentation de celui-ci. En outre, la mise en œuvre doit prendre en compte l'accessibilité non prévisible des fournisseurs, ainsi que les délais potentiels de la communication. Cette thèse propose une plate-forme de services pour les terminaux mobiles, qui supporte l'exécution d'applications orientées services dans les MANETs discontinus. La plate-forme consiste en un intergiciel structuré en deux couches : une couche de communication et une couche de services. La couche de communication permet le découplage entre deux entités en termes d'interactions dans le temps, de comportement synchrone, et de connaissance mutuelle. Pour cette couche de communication (DoDWAN), un protocole opportuniste et basé contenu est utilisé. La couche de services (DiSWAN) permet le découplage entre les fournisseurs de services et les clients en termes d'interopérabilité et de contrat de service. Pour cette couche, des solutions de découverte et d'invocation de services sont proposées. Les éléments du protocole de découverte sont la description et la publication du coté fournisseur, et la collecte et la sélection du coté client. La description inclut des propriétés fonctionnelles et nonfonctionnelles du service, ainsi que des propriétés contextuelles. La découverte est basée sur le modèle pair à pair, où un client ne collecte que les services intéressants. Les invocations sont basées contenu pour bénéficier de la réplication de services, dans le cas où plusieurs fournisseurs peuvent fournir le même service métier. Le client crée sa requête en connaissant un fournisseur déjà découvert, mais il publie cette requête afin qu'elle soit reçue par tous les fournisseurs compatibles. L'exploitation de la multiplicité des fournisseurs pouvant engendrer des communications superflus, plusieurs mécanismes de "guérison" du réseau ont été mis en place pour éliminer les requêtes et réponses d'invocation redondantes. Des simulations dans un MANET discontinu ont été effectuées. Les simulations montrent que la performance de la découverte étant directement liée à celle du protocole de communication et que l'utilisation des invocations basées contenu permet de meilleurs temps de réponses et une meilleure satisfaction du client. Les simulations montrent aussi que les mécanismes de "guérison" du réseau sont efficaces.

Alors que l'informatique est devenue omniprésente dans notre société actuelle, assurer la qualité d'un logiciel revêt une importance grandissante. Pour accroître cette qualité, l'une des conditions à respecter est la correction du système. Dans cette thèse, nous nous intéressons plus particulièrement aux systèmes distribués mettant en œuvre un ou plusieurs programmes exécutés sur plusieurs machines qui communiquent entre elles à travers le réseau. Dans ce contexte, assurer leur correction est rendu plus difficile par leur hétérogénéité mais également par leurs spécificités communes. Les algorithmes correspondants sont parfois complexes et la prédiction de leur comportement difficilement réalisable sans une étude avancée. Les travaux réalisés au cours de cette thèse mettent en œuvre la vérification dynamique formelle de propriétés temporelles sur des applications distribuées. Cette approche consiste à vérifier l'implémentation réelle d'une application à travers son exécution. L'enjeu majeur est de réussir à appliquer les techniques associées au Model checking dans le cadre d'une vérification sur des implémentations réelles d'applications distribuées et non plus sur des modèles abstraits. Pour cela, nous proposons dans un premier temps une analyse sémantique dynamique par introspection mémoire d'un état système permettant de détecter des états sémantiquement identiques. Puis, nous mettons en œuvre la vérification dynamique formelle de certaines propriétés temporelles : les propriétés de vivacité, formulées à l'aide de la logique LTL_X, et le déterminisme des communications dans les applications MPI. Une évaluation de chacune de ces contributions est réalisée à travers plusieurs expériences / While computers have become ubiquitous in our current society, ensuring the software quality takes on an increasing importance. One of the requirements to enhance this quality is the system correctness. In this thesis, we are particularly interested in distributed systems implementing one or more programs executed on several machines which communicate with each other through a network. Ensuring the system correctness is more difficult in this context, due to their heterogeneity but also their common characteristics. Corresponding algorithms are sometimes complex and the prediction of their behavior may be difficult to realize without an advanced study. The work done during this thesis implement the dynamic formal verification of some temporal properties on legacy distributed applications. This approach consists of checking the real implementation of an application by its systematic execution. The challenge in this approach is how to apply the methods derived from Model checking in the context of the verification of legacy distributed applications (without access to source code) and no longer on abstract models. For that, we propose in a first step a dynamic semantic analysis of a system state permitting the detection of identical states. Then, we implement the dynamic formal verification of some temporal properties: liveness properties, specified with the LTL_X logic, and the communications determinism in MPI applications. These contributions are experimentaly validated and evaluated with different series of experiments

L émergence des environnements omniprésents pose un nouveau défi aux systèmes informatiques. Les intergiciels asynchrones (Message-Oriented Middleware, MOM) sont reconnus comme étant la solution la plus apte à répondre aux besoins de passage à grande échelle, de flexibilité, et d' hétérogénéité des nouvelles applications distribuées. Mais l'implémentation des intergiciels asynchrones actuels reste souvent figée quels que soient les sites d'exécution et l'application (les applications) l'utilisant et sont peu voire pas configurables. Cette thèse s'intéresse à la configuration et au déploiement des intergiciels asynchrones sur système hétérogène à grande échelle. Elle vise la définition d'un modèle d'intergiciel asynchrone configurable permettant une configuration statique et à l'exécution. Elle a pour objectif d'associer les nombreux travaux dans le domaine de l'asynchrone qui ont mené à la définition des modèles de communication asynchrones et les réflexions menées dans les intergiciels synchrones autour des nouveaux besoins de configuration et d'adaptabilité. La synthèse de tous nos travaux nous a mené à la création de DREAM (Dynamic REflective Asynchronous Middleware), un intergiciel asynchrone adaptable. Les mécanismes de contrôles fournis par Dream ainsi que son architecture permettent de réaliser une configuration en se basant sur les besoins applicatifs et les contraintes imposées par le système. Nous validons notre prototype par l'implémentation d'un service à évènement à base d'agents dans lequel nous utilisons les capacités d'adaptation de DREAM pour ajouter de nouvelles fonctionnalités.

L'évolution des réseaux de communication rend aujourd'hui possible l'apparition de nouvelles applications distribuées. Néanmoins, l'émergence du multimédia renforce les besoins de bande passante élevée et de garantie des délais, qui devront être pris en considération tant au niveau du réseau que des machines. Cette thèse propose l'architecture d'un système de communication complet, basé sur ATM, permettant de satisfaire les besoins des applications distribuées temps réel. En particulier, il est nécessaire d'intégrer de manière efficace les flux audio et vidéo, qui devront cohabiter avec d'autres trafics comme les alarmes ou les données traditionnelles. L'état de l'art sur l'architecture des machines pour les hauts débits permet de mieux cerner les problèmes posés par l'emploi des nouvelles technologies de communication, et montre que les nombreuses études dans ce domaine ne fournissent que des réponses partielles au problème posé. L'architecture du système de communication proposée permet de supporter plusieurs équipements audio/vidéo sur une même station, de construire des topologies de réseau variées, et d'assurer la redondance de chemins. L'introduction d'un micro-contrôleur sur la carte d'interface au réseau offre des services temps réel de haut niveau grâce au concept de télé-DMA, et fait ainsi profiter les applications des avantages d'ATM. D'autre part, une organisation protocolaire particulière permet de faire cohabiter efficacement les services temps réel et les services télé-informatique classiques. Pour les communications entre les équipements, un mécanisme de contrôle de flux à la source pour garantir un délai d'acheminement borné des messages temps réel est proposé. Les problèmes de récupération des applications existantes, de signalisation, d'administration et de gestion du basculement en cas de défaillance du réseau sont aussi abordés. Enfin, les performances globales du système de communication, puis celles d'un service de transfert périodique de variables temps réel implanté sur le micro-contrôleur sont évaluées.

Depuis 2001 j'ai développé au sein de l'équipe Oasis des travaux de recherche sur la sémantique des applications à base d'objets distribués, appliquant dans le contexte d'un vrai langage, et d'applications de taille réelle, mes recherches précédentes dans le domaine des algèbres de processus. Les différents aspects de ce travail touchent naturellement à la sémantique comportementale, et à la définition de procédures de génération de modèles prenant en compte les différentes facettes de la programmation d'applications distribuées, mais aussi, en amont, à l'analyse statique de code et aux techniques d'abstraction de modèles, et en aval aux outils de vérification de propriétés comportementales. Je montre dans ce mémoire la complexité de ces recherches et la grande variété des techniques requises. Nous avons mis en place une méthode cohérente basée sur un modèle sémantique très flexible, le modèle pNets (parameterized Networks of automata), qui nous offre un bon compromis entre décidabilité, complexité, et utilisabilité. Cette approche nous a permis de définir une sémantique comportementale pour différents aspects des applications à base d'objets ou de composants distribués, mais aussi une notion d'abstraction vers des modèles abstraits finis, permettant d'utiliser des outils de vérification de type " model-checking ". L'ensemble de ces aspects a donné lieu à la réalisation de prototypes, dans la plateforme VerCors, et à des cas d'étude de grande taille.

La complexité croissante des systèmes d'information modernes a motivé l'apparition de nouveaux paradigmes (objets, composants, services, etc), permettant de mieux appréhender et maîtriser la masse critique de leurs fonctionnalités. Ces systèmes sont construits de façon modulaire et adaptable afin de minimiser les temps d'arrêts dus aux évolutions ou à la maintenance de ceux-ci. Afin de garantir des propriétés non fonctionnelles (par ex. maintien du temps de réponse malgré un nombre croissant de requêtes), ces systèmes sont également amenés à être distribués sur différentes ressources de calcul (grilles). Outre l'apport en puissance de calcul, la distribution peut également intervenir pour distribuer une tâche sur des nœuds aux propriétés spécifiques. C'est le cas dans le cas des terminaux mobiles proches des utilisateurs ou encore des objets et capteurs connectés proches physiquement du contexte de mesure. L'adaptation d'un système et de ses ressources nécessite cependant une connaissance de son état courant afin d'adapter son architecture et sa topologie aux nouveaux besoins. Un nouvel état doit ensuite être propagé à l'ensemble des nœuds de calcul. Le maintien de la cohérence et le partage de cet état est rendu particulièrement difficile à cause des connexions sporadiques inhérentes à la distribution, pouvant amener des sous-systèmes à diverger. En réponse à ces défi scientifiques, cette thèse propose une abstraction de conception et de déploiement pour systèmes distribués dynamiquement adaptables, grâce au principe du Model@Runtime. Cette approche propose la construction d'une couche de réflexion distribuée qui permet la manipulation abstraite de systèmes répartis sur des nœuds hétérogènes. En outre, cette contribution introduit dans la modélisation des systèmes adaptables la notion de cohérence variable, permettant ainsi de capturer la divergence des nœuds de calcul dans leur propre conception. Cette couche de réflexion, désormais cohérente "à terme", permet d'envisager la construction de systèmes adaptatifs hétérogènes, regroupant des nœuds mobiles et embarqués dont la connectivité peut être intermittente. Cette contribution a été concrétisée par un projet nommé ''Kevoree'' dont la validation démontre l'applicabilité de l'approche proposée pour des cas d'usages aussi hétérogènes qu'un réseau de capteurs ou une flotte de terminaux mobiles. / The growing complexity of modern IT systems has motivated the development of new paradigms (objects, components, services,...) to better cope with the critical size of their functionalities. Such systems are then built as a modular and dynamically adaptable compositions, allowing them to minimise their down-times while performing evolutions or fixes. In order to ensure non-functional properties (i.e. request latency) such systems are distributed across different computation nodes. Besides the added value in term of computational power (cloud), this distribution can also target nodes with dedicated properties such as mobile nodes and sensors (internet of things), physically close to users for interactions. Adapting a system requires knowledge about its current state in order to adapt its architecture to its evolving needs. A new state must be then disseminated to other nodes to synchronise them. Maintaining its consistency and sharing this state is a difficult task especially in case of sporadic connexions which lead to divergent state between sub-systems. To tackle these scientific problems, this thesis proposes an abstraction to design and deploy distributed adaptive systems following the Model@Runtime paradigm. From this abstraction, the proposed approach allows defining a distributed reflexive layer to manipulate heterogeneous distributed nodes. In particular, this contribution introduces variable consistencies in model definition and divergence in system conception. This reflexive layer, eventually consistent allows the construction of distributed adapted systems even on mobile nodes with intermittent connectivity. This work has been realized in an open source project named Kevoree, and validated on various distributed systems ranging from sensor networks to “cloud” computing.