Le protocole Pastry réalise une table de hachage distribué sur un réseau pair à pair organisé en un anneau virtuel de noeuds. Alors qu'il existe plusieurs implémentations de Pastry, il n'y a pas encore eu de travaux pour décrire formellement l'algorithme ou vérifier son bon fonctionnement. Intégrant des structures de données complexes et de la communication asynchrone entre des noeuds qui peuvent rejoindre ou quitter le réseau, ce protocole représente un intérêt certain pour la vérification formelle. La thèse se focalise sur le protocole Join de Pastry qui permet à un noeud de rejoindre le réseau. Les noeuds ayant intégré le réseau doivent avoir une vue du voisinage cohérente entre eux. La propriété principale de correction, appelée CorrectDelivery, assure qu'à tout moment il y a au plus un noeud capable de répondre à une requête pour une clé, et que ce noeud est le noeud le plus proche numériquement à ladite clé. Il n'est pas trivial de maintenir cette propriété en présence de churn. Ce travail nous a permis de découvrir des violations inattendues de la propriété dans les versions publiées de l'algorithme. Sur la base de cette analyse, le protocole IdealPastry est conçu et vérifié en utilisant l'assistant interactif à la preuve TLAPS pour TLA+. Le protocole LuPastry est obtenu en assouplissant certaines hypothèses de IdealPastry. Il est montré formellement que LuPastry vérifie CorrectDelivery sous l'hypothèse qu'aucun noeud ne quitte le réseau. Cette hypothèse ne peut être relâchée à cause du risque de perte de connexion du réseau dans le cas où plusieurs noeuds quittent le réseau en même temps / Pastry is a structured P2P algorithm realizing a Distributed Hash Table over an underlying virtual ring of nodes. Several implementations of Pastry are available, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines complex data structures, asynchronous communication, and concurrency in the presence of spontaneous join and departure of nodes, it makes an interesting target for verification. This thesis focuses on the Join protocol of Pastry that integrates new nodes into the ring. All member nodes must have a consistent key mapping among each other. The main correctness property, named CorrectDelivery, states that there is always at most one node that can deliver an answer to a lookup request for a key and this node is the numerically closest member node to that key. This property is non-trivial to preserve in the presence of churn. In this thesis, unexpected violations of CorrectDelivery in the published versions of Pastry are discovered and analyzed using the TLA+ model checker TLC. Based on the analysis, the protocol IdealPastry is designed and verified using the interactive theorem prover TLAPS for TLA+. By relaxing certain hypotheses, IdealPastry is further improved to LuPastry, which is again formally proved correct under the assumption that no nodes leave the network. This hypothesis cannot be relaxed in general due to possible network separation when particular nodes simultaneously leave the network

Cette thèse traite l’utilisation des agents mobiles dans le domaine des algo- rithmes distribués en les déplaçant de manière aléatoire dans le réseau. Initialement k agents mobiles ayant les identités uniques sont placés dans le réseau. On décrit un algorithme distribué pour calculer un arbre couvrant dans les réseaux dynamiques en utilisant les agents mobiles. Les agents marquent les noeuds sur les quelles ils arrivent. Ils utilisent deux techniques di?érentes : le clonage dans lequel un agent crée son propre clone pour faire quelques tâches et le marquage sur la tableau de bord (un espace mémoire sur les noeuds). Ces techniques sont utilisés dans les applications comme l’arbre couvrant, le rassemblement et la collecte d’information. Chacun des agents détient une information partielle. Quand deux ou plusieurs agents se rencontrent sur un noeud, ils fusionnent en un seul agent. On s’intéresse alors au temps nécessaire ou tous les k agents fusionnent en un seul et unique agent. On présent une chaîne de Markov pour le comportement des agents, et on montre comment on peut utiliser cette technique pour calculer la bourne supérieur. On étudie le même problème quand les agents mobile commencent la marche aléatoire sous un régime stationnaire. On a aussi étudié le problème de Handshake et on l’a analysé en utilisant les agents mobiles. / This thesis deals with the use of mobile agents in distributed algorithms by performing random walks in the network. k mobile agents having unique identities are placed initially in a network. We describe a distributed algorithm for computing spanning trees in dynamic networks by using mobile agents. The agents mark the nodes on which they arrive. They use two di?erent techniques. In one problem they use the cloning in which an agent creates its own clone to do some task assigned. In the second, the mobile agents mark on the whiteboard (a memory location on the nodes). These techniques are used in applications such as spanning tree, gathering and collecting information. The mobile agents have limited knowledge and hence, they are not intelligent and do not have computational capabilities. When two or more agents meet at a node of the underlying graph, they merge into a single agent. The parameter of interest is the expected time for all the agents to merge into a single agent. We present a Markov chain, modelling the agents behavior, and show how this can be used to upper bound the expected time for all the k agents to merge into a single agent. We study the same problem when the mobile agents start their walk directly under stationary regime. Handshake problem is also studied and analyzed using mobile agents.

Les réseaux ad hoc sont des réseaux distribués, auto-organisés ne nécessitant pas d'infrastructure. Les entités formant un tel réseau doivent collaborer afin d'assurer le bon fonctionnement des services réseaux, tel que le routage. Dans un tel environnement, de nombreux algorithmes développés pour le monde filaire ne peuvent être adaptés de façon naïve sans entraîner une congestion importante du réseau qui va réduire son efficacité. Notre travail de thèse se penche sur l'étude de la gestion de services. En effet, sans application, le développement d'une architecture comme les réseaux ad hoc est inutile. La gestion de services consiste à fournir tout les moyens possibles pour faciliter et rendre fiable l'utilisation d'applications distribuées. Nos travaux contribuent à l'étude de deux points précis de la gestion de services. Premièrement, nous fournissons un algorithme permettant de répartir efficacement une information dans le réseau en sélectionnant certains objets du réseau pour être des réplicats de l'information. Cet algorithme peut alors être utilisé pour publier les informations relatives à un service afin de permettre sa recherche. Deuxièmement, nous avons étudié la prédiction de déconnexion entrainée par la mobilité des noeuds. Nous proposons trois solutions basées sur la recherche d'ensemble de chemins disjoints, la recherche de liens critiques et la recherche de noeuds critiques. Les recherches que nous proposons sont entièrement réalisées à partir d'informations locales. Les résultats obtenus fournissent une base au développement d'un gestionnaire de services distribués. De plus, certains de nos algorithmes (comme la recherche d'ensembles de chemins disjoints) peuvent être réutilisés dans d'autres applications, comme le routage QoS multi-chemins.

Nous présentons dans ce mémoire de thèse d'habilitation une étude sur des algorithmes distribués asynchrones de contrôle et d'ordonnancement. Un algorithme de contrôle établit une structure virtuelle sur un réseau de sites communicants. Nous faisons le choix %délibéré de faire un minimum d'hypothèses sur les connaissances de chaque site. De même, nous évitons autant que possible d'utiliser des mécanismes conduisant à des attentes qui peuvent être pénalisantes comme, par exemple, l'utilisation de synchroniseurs. Ces choix conduisent à privilégier les modes de fonctionnement essentiellement locaux. %dépendant le moins possible de l'état du reste du réseau. Nous introduisons toutefois une limite à cette démarche, dans ce travail, nous ne considérons que des algorithmes déterministes. Dans ces circonstances, un problème essentiel de l'algorithmique distribuée est l'établissement d'une structure de contrôle couvrant la totalité du réseau, dans laquelle chaque site distingue certains de ses voisins de façon spécifique. Après avoir rappelé des notions fondamentales en partie I, nous présentons dans la première partie, trois de nos algorithmes de construction d'arbre couvrant avec contraintes, ces dernières apportant une plus grande efficacité à la structure de contrôle établie. En particulier, nous considérons la contrainte de poids total minimum qui caractérise plutôt une recherche économique, celle de diamètre minimum qui concerne l'efficacité à la fois en temps mais aussi évidemment en messages et la contrainte de degré minimal qui permet par exemple d'utiliser des équipements d'interconnection moins coûteux. Dans la troisième partie nous présentons deux de nos heuristiques pour la résolution du problème de l'ordonnancement distribué en ligne, avec arrivées sporadiques, d'abord de tâches indépendantes puis de tâches avec dépendances non cycliques. Nous montrons que là encore, la structure d'arbre peut être utilisée de façon bénéfique. En particulier, dans des réseaux de taille arbitrairement grande, des arbres de plus courts chemins limités aux voisins relativement proches peuvent être utilisés pour définir un concept nouveau et prometteur ,: la Sphère de Calcul. Cette Sphère de Calcul limite le nombre de messages échangés et le temps de calcul. Tout au long de ce mémoire nous présentons des algorithmes nouveaux, voire pionniers dans leurs domaine. De nombreux développements sont possibles, certains déjà réalisés par nous-même ou par d'autres auteurs, d'autres sont des problèmes ouverts (recherche d'algorithmes optimaux par exemple).

L'émergence des systèmes pair-à-pair et la possibilité de réaliser des calculs et d'échanger des données par des services web conduit à des systèmes d'intégration de données à large échelle où l'évaluation de requêtes et d'autres traitements complexes sont réalisés par composition de services. Un problème important dans ce type de systèmes est l'absence de connaissances globales. Il est difficile par exemple de choisir le meilleur pair pour le routage des requêtes, le meilleur service lors de la composition de services ou de décider parmi les données locales à un pair celles à rafraîchir, à mettre en cache, etc. La notion de choix implique celle de classement. Bien qu'il soit possible de comparer et classer des entités d'après leur contenu ou d'autres métadonnées associées, ces techniques sont généralement basées sur des descriptions homogènes et sémantiquement riches. Une alternative intéressante dans le contexte d'un système à large échelle est le classement basé sur les liens qui exploite les relations entre les différentes entités et permet de faire des choix fondés sur des informations globales. Cette thèse présente un nouveau modèle générique de classement de services fondé sur leurs liens de collaboration. Nous définissons une importance globale de service en exploitant des connaissances spécifiques sur sa contribution aux autres services à travers les appels reçus et les données échangées. L'importance peut être calculée efficacement par un algorithme asynchrone sans génération de messages supplémentaires. La notion de contribution est abstraite et nous avons étudié son instanciation dans le cadre de trois applications: (i) le classement de services basé sur les appels où la contribution reflète la sémantique des services ainsi que leur utilisation avec le temps; (ii) le classement de services par l'utilisation des données où la contribution des services est fondée sur l'utilisation de leurs données pendant l'évaluation des requêtes dans un entrepôt distribué; (iii) la définition des stratégies de cache distribuées qui sont basées sur la contribution d'une mise en cache des données à réduire la charge du système.

Nous proposons dans ces travaux une étude des marches aléatoires dans l'algorithmique distribuée pour les réseaux dynamiques. Nous montrons dans un premier temps que les marches aléatoires sont un outil viable pour la conception d'algorithmes distribués. Ces <br />algorithmes reposent principalement sur les trois propriétés fondamentales des marches aléatoires (Percussion, Couverture, Rencontre). Nous fournissons une méthode qui évalue <br />le temps ́ecoulé avant que ces trois propriétés soient vérifiées. Cela nous permet d'évaluer de la complexité de nos algorithmes. Dans un second temps, nous proposons l'utilisation d'un jeton circulant aléatoirement sous forme de mot circulant afin de collecter sur ce jeton des informations topologiques. Ces informations permettent la construction et la maintenance d'une structure couvrante du réseau de communication. Ensuite, nous <br />avons utilisé cette structure pour concevoir un algorithme de circulation de jeton tolérant aux pannes pour les environnements dynamiques. Cet algorithme a la particularité d'être complètement décentralisé. Nous proposons dans un dernier temps d'adapter notre circulation de jeton pour proposer une solution au problème d'allocation de ressources dans les réseaux ad-hoc.

Les automates distribués sont des machines à états finis qui opèrent sur des graphes orientés finis. Fonctionnant comme des algorithmes distribués synchrones, ils utilisent leur graphe d'entrée comme un réseau dans lequel des processeurs identiques communiquent entre eux pendant un certain nombre (éventuellement infini) de rondes synchrones. Pour la variante locale de ces automates, où le nombre de rondes est borné par une constante, Hella et al. (2012, 2015) ont établi une caractérisation logique par des formules de la logique modale de base. Dans le cadre de cette thèse, nous présentons des caractérisations logiques similaires pour deux classes d'automates distribués plus expressives.La première classe étend les automates locaux avec une condition d'acceptation globale et la capacité d'alterner entre des modes de calcul non-déterministes et parallèles. Nous montrons qu'elle est équivalente à la logique monadique du second ordre sur les graphes.En nous restreignant à des transitions non-déterministes ou déterministes, nous obtenons également deux variantes d'automates strictement plus faibles pour lesquelles le problème du vide est décidable.Notre seconde classe adapte la notion standard d'algorithme asynchrone au cadre des automates distribués non-locaux. Les machines résultantes sont prouvées équivalentes à un petit fragment de la logique de point fixe, et plus précisément, à une variante restreinte du μ-calcul modal qui autorise les plus petits points fixes mais interdit les plus grands points fixes. Profitant du lien avec la logique, nous montrons aussi que la puissance expressive de ces automates asynchrones est indépendante du fait que des messages puissent être perdus ou non.Nous étudions ensuite la décidabilité du problème du vide pour plusieurs classes d'automates non-locaux. Nous montrons que le problème est indécidable en général, en simulant une machine de Turing par un automate distribué qui échange les rôles de l'espace et du temps. En revanche, le problème s'avère décidable en LOGSPACE pour une classe d'automates oublieux, où les nœuds voient les messages reçus de leurs voisins, mais ne se souviennent pas de leur propre état. Finalement, à titre de contribution mineure, nous donnons également de nouvelles preuves de séparation pour plusieurs hiérarchies d'alternance de quantificateurs basées sur la logique modale. / Distributed automata are finite-state machines that operate on finitedirected graphs. Acting as synchronous distributed algorithms, they use their input graph as a network in which identical processors communicate for a possibly infinite number of synchronous rounds. For the local variant of those automata, where the number of rounds is bounded by a constant, Hella et al. (2012, 2015) have established a logical characterization in terms of basic modal logic. In this thesis, we provide similar logical characterizations for two more expressive classes of distributed automata.The first class extends local automata with a global acceptance condition and the ability to alternate between non deterministic and parallel computations. We show that it is equivalent to monadic second-order logic on graphs. By restricting transitions to be non deterministic or deterministic, we also obtain two strictly weaker variants for which the emptiness problem is decidable.Our second class transfers the standard notion of asynchronous algorithm to the setting of non local distributed automata. There sulting machines are shown to be equivalent to a small fragment of least fixpoint logic, and more specifically, to a restricted variantof the modal μ -calculus that allows least fixpoints but forbids greatest fixpoints. Exploiting the connection with logic, we additionally prove that the expressive power of those asynchronous automata is independent of whether or not messages can be lost.We then investigate the decidability of the emptiness problem forseveral classes of nonlocal automata. We show that the problem isundecidable in general, by simulating a Turing machine with adistributed automaton that exchanges the roles of space and time. Onthe other hand, the problem is found to be decidable in logspace for a class of forgetful automata, where the nodes see the messages received from their neighbors but cannot remember their own state. As a minor contribution, we also give new proofs of the strictness of several set quantifier alternation hierarchies that are based on modallogic.

La réalité mixe, les jeux en ligne massivement multijoueur (MMOGs), les mondes virtuels et le cyberespace sont des concepts extrêmement attractifs. Mais leur déploiement à large échelle reste difficile et il est en conséquence souvent évité.La contribution principale de la thèse réside dans le système distribué Kiwano, qui permet à un nombre illimité d'avatars de peupler et d'interagir simultanément dans un même monde contigu. Dans Kiwano nous utilisons la triangulation de Delaunay pour fournir à chaque avatar un nombre constant de voisins en moyenne, indépendamment de leur densité ou distribution géographique. Le nombre d'interactions entre les avatars et les calculs inhérents sont bornés, ce qui permet le passage à l'échelle du système.La charge est repartie sur plusieurs machines qui regroupent sur un même nœud les avatars voisins de façon contiguë dans le graphe de Delaunay. L'équilibrage de la charge se fait de manière contiguë et dynamique, en suivant la philosophie des réseaux pair-à-pair (peer-to-peer overlays). Cependant ce principe est adapté au contexte de l'informatique dématérialisée (cloud computing).Le nombre optimal d'avatars par CPU et les performances de notre système ont été évalués en simulant des dizaines de milliers d'avatars connectés à la même instance de Kiwano tournant à travers plusieurs centres de traitement de données.Nous proposons également trois applications concrètes qui utilisent Kiwano : Manycraft est une architecture distribuée capable de supporter un nombre arbitrairement grand d'utilisateurs cohabitant dans le même espace Minecraft, OneSim, qui permet à un nombre illimité d'usagers d'être ensemble dans la même région de Second Life et HybridEarth, un monde en réalité mixte où avatars et personnes physiques sont présents et interagissent dans un même espace: la Terre. / Virtual worlds attract millions of users and these popular applications --supported by gigantic data centers with myriads of processors-- are routinely accessed. However, surprisingly, virtual worlds are still unable to host simultaneously more than a few hundred users in the same contiguous space.The main contribution of the thesis is Kiwano, a distributed system enabling an unlimited number of avatars to simultaneously evolve and interact in a contiguous virtual space. In Kiwano we employ the Delaunay triangulation to provide each avatar with a constant number of neighbors independently of their density or distribution. The avatar-to-avatar interactions and related computations are then bounded, allowing the system to scale. The load is constantly balanced among Kiwano's nodes which adapt and take in charge sets of avatars according to their geographic proximity. The optimal number of avatars per CPU and the performances of our system have been evaluated simulating tens of thousands of avatars connecting to a Kiwano instance running across several data centers, with results well beyond the current state-of-the-art.We also propose Kwery, a distributed spatial index capable to scale dynamic objects of virtual worlds. Kwery performs efficient reverse geolocation queries on large numbers of moving objects updating their position at arbitrary high frequencies. We use a distributed spatial index on top of a self-adaptive tree structure. Each node of the system hosts and answers queries on a group of objects in a zone, which is the minimal axis-aligned rectangle. They are chosen based on their proximity and the load of the node. Spatial queries are then answered only by the nodes with meaningful zones, that is, where the node's zone intersects the query zone.Kiwano has been successfully implemented for HybridEarth, a mixed reality world, Manycraft, our scalable multiplayer Minecraft map, and discussed for OneSim, a distributed Second Life architecture. By handling avatars separately, we show interoperability between these virtual worlds.With Kiwano and Kwery we provide the first massively distributed and self-adaptive solutions for virtual worlds suitable to run in the cloud. The results, in terms of number of avatars per CPU, exceed by orders of magnitude the performances of current state-of-the-art implementations. This indicates Kiwano to be a cost effective solution for the industry. The open API for our first implementation is available at \url{http://kiwano.li}.

La croissance des terminaux et des services de réseau mobile pose aujourd'hui une question sur la méthode de distribuer efficacement des données aux utilisateurs. Plusieurs applications de réseau ont besoin de télécharger des données afin de fournir des informations aux utilisateurs. En conséquence, l'explosion du trafic de données exercé par les clients qui cherchent des contenus en ligne provoque la saturation du réseau cellulaire des opérateurs mobiles. Similaire aux problèmes du réseau Internet, les utilisateurs mobiles ont désormais fait face à la congestion au niveau des passerelles de réseau. En raison de l'imprévisibilité de la mobilité humaine, les fournisseurs de services mobiles ne peuvent pas installer suffisamment des infrastructures pour leurs clients. La réplication de contenu dans ce contexte a été prouvée comme une bonne solution pour améliorer la performance et l'extensibilité du réseau. Dans cette thèse, nous abordons les problèmes de la réplication du contenu dans des réseaux hétérogènes mobiles. Nous étudions deux questions fondamentales: où et combien de répliques doivent être placées dans le système. Nous modélisons le problème à l'aide de la théorie de "facility location" et nous concevons un mécanisme distribué qui est capable de réduire la latence d'accès au contenu et d'éviter la congestion au niveau des passerelles mobiles. En outre, nous examinons les contraintes de ressources des équipements mobiles et proposons des mécanismes P2P pour transférer les répliques afin de parvenir l'équilibrage de charge parmi les utilisateurs. Nous évaluons nos mécanismes en utilisant des modèles de mobilité humaine. Enfin, pour résoudre le problème causé par les utilisateurs rationnels qui se comportent égoïstement lors de la réplication du contenu dans les réseaux hétérogènes mobiles, nous dérivons un modèle de coût et utilisons la théorie des jeux pour étudier les équilibres du système. Particulièrement, nous étudions le facteur de réplication dans un scénario "flash-crowd" avec de différents débits de réseau sans fil. A partir des résultats théoriques, nos futurs travaux sont d'élaborer des stratégies à mettre en œuvre dans les réseaux en pratique.

La conception d'algorithmes pour les systèmes concurrents et répartis est subtile et difficile. Ces systèmes sont enclins à des blocages et à des conditions de course qui peuvent se produire dans des entrelacements particuliers d'actions de processus et sont par conséquent difficiles à reproduire. Il est souvent non-trivial d'énoncer précisément les propriétés attendues d'un algorithme et les hypothèses que l'environnement est supposé de satisfaire pour que l'algorithme se comporte correctement. La vérification formelle est une technique essentielle pour modéliser le système et ses propriétés et s'assurer de sa correction au moyen du model checking. Des langages formels tels TLA+ permettent de décrire des algorithmes compliqués de manière assez concise, mais les concepteurs d'algorithmes trouvent souvent difficile de modéliser un algorithme par un ensemble de formules. Dans ce mémoire nous présentons le langage PlusCal-2 qui vise à allier la simplicité de pseudo-code à la capacité d'être vérifié formellement. PlusCal-2 améliore le langage algorithmique PlusCal conçu par Lamport en levant certaines restrictions de ce langage et en y ajoutant de nouvelles constructions. Notre langage est destiné à la description d'algorithmes à un niveau élevé d'abstraction. Sa syntaxe ressemble à du pseudo-code mais il est tout à fait expressif et doté d'une sémantique formelle. Des instances finies d'algorithmes écrits en PlusCal-2 peuvent être vérifiées à l'aide du model checker tlc. La deuxième contribution de cette thèse porte sur l'étude de méthodes de réduction par ordre partiel à l'aide de relations de dépendance conditionnelle et constante. Pour calculer la dépendance conditionnelle pour les algorithmes en PlusCal-2 nous exploitons des informations sur la localité des actions et nous générons des prédicats d'indépendance. Nous proposons également une adaptation d'un algorithme de réduction par ordre partiel dynamique pour une variante du model checker tlc. Enfin, nous proposons une variante d'un algorithme de réduction par ordre partiel statique (comme alternative à l'algorithme dynamique), s'appuyant sur une relation de dépendance constante, et son implantation au sein de tlc. Nous présentons nos résultats expérimentaux et une preuve de correction.