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 these presente un ensemble de techniques qui permettent l'optimisation des performances des systèmes reseaux modernes. Ces techniques reposent sur l'analyse et la transformation des programmes impliquées dans la mise en oeuvre des protocoles reseaux. La première de ces techniques fait appel à la spécialisation de programmes pour optimiser des piles de protocoles réseaux. La deuxième, que nous avons nommée spécialisation distante, permet à des systèmes embarqués limités en ressources de bénéficier de la spécialisation de programmes en déportant à travers le réseau les opérations de spécialisation à une machine distante moins limitée. La troisième propose un nouvel allocateur de mémoire qui optimise l'utilisation des caches matériels faite par un serveur réseau. Enfin, la quatrième technique utilise l'analyse de programmes statiques pour intégrer l'allocateur proposé dans un serveur réseau existant. On appelle ces techniques optimisations compilateur parce qu'elles opèrent sur le flot des données et du contrôle dans des programmes en les transformant pour qu'ils fonctionnent plus efficacement. Les programmes réseaux possèdent une propriété fondamentale qui les rend faciles à manipuler de cette manière : ils sont basés sur une conception qui les organise en différentes couches, chacune englobant une fonctionalité bien définie. Cette propriété introduit dans le code des bloques fonctionnelles bien définis qui sont ´equivalents aux procédures et aux fonctions d'un langage généraliste. Dans la première partie de cette thèse, la spécialisation de programmes est utilisée pour créer différentes configurations de ces bloques qui correspondent à différents contextes d'utilisation. Au départ, chacun de ces bloques fonctionnels, tels que ceux utilisés dans le protocole TCP et dans le routage des trames, est conçu et développé pour fonctionner dans des conditions variées. Cependant, dans certaines situations spécifiques (comme dans le cas d'un réseaux haut-performance sans aucune congestion), certaines caractéristiques (comme les algorithmes du control de congestion de TCP) n'ont pas d'utilité. La spécialisation peut donc instancier ces bloques de code en éliminant les parties non-necessaires et en appliquant des transformations du flot des données et du contrôle pour rendre plus efficace leur fonctionnement. Une fois que ces bloques individuels sont rendus spécialisables, on bénéficie de l'encapsulation propre d'une pile de protocole en couches. Chacune de ces couches peut être spécialisée pour obtenir une pile de protocole spécialisée. Car cette façon d'utiliser la spécialisation de programmes est nouvelle et nécessite un style de programmation bien différent par rapport à ce qu'il existe : il faut de l'assistance pour les développeurs d'applications sous forme de bibliothèques et d'interfaces de programmation. De plus, la spécialisation a un inconvénient : il est très gourmand comme processus et donc ne peut pas être invoqué arbitrairement. Ces besoins sont traités dans la deuxième contribution de cette thèse, La spécialisation distante. La spécialisation distante est un ensemble de méchanismes et d'interfaces développées comme des extensions du noyau d'un système d'exploitation. Ces extensions permettent de déporter le processus de la spécialisation `à travers le réseau sur un système distant. La spécialisation distante fournit les avantages de la spécialisation dynamique de programmes à des systèmes qui en bénéficie potentiellement le plus, c'est `à dire, les systèmes embarqués. Traditionnellement, ces systèmes ont utilisé du code optimisé à la main. Cependant, produire ce code implique une procédure lente et produit des erreurs dans le code résultant. De plus, cette procédure n'arrive pas à exploiter des opportunités d'optimisation sophistiquées qui peuvent être identifiiés facilement par les outils automatisés. La spécialisation distante permet d'obtenir un tel code optimisé automatiquement à l'exécution, une fois que le système est préparé et rendu spécialisable. Une application peut dans ce cas demander des versions spécialisées des composant OS correspondant à des contextes particuliers à travers le réseau. En suite, on considère les serveurs réseaux. La spécialisation optimise effectivement du code qui est limité en performance par l'exécution des instructions sur le processeur, en éliminant des instructions non nécessaires et en rendant plus efficaces les instructions restantes. Mais pour les applications qui ont des inefficacités plus importantes, la spécialisation est inefficace, car malgré des améliorations importantes au niveau des instructions, la partie améliorée étant petite, les gains globaux sont insignifiants. Le facteur traditionnel qui limite les systèmes réseaux en performance est celui des opérations I/O. Par contre, les systèmes réseaux modernes sont maintenant équipés de suffisamment de mémoire. Donc, les op´erations I/O ne constituent plus le goulot d'´étranglement. A l'inverse, l'accès à la mémoire occupe maintenant cette position. Aujourd'hui, les accès à la mémoire cûutent jusqu'à 100 fois plus que d'autres opérations notamment la manipulation des registres. Cette thèse propose un nouvel allocateur de mémoire qui s'appelle Stingy Allocator pour minimiser le nombre de défauts cache dans un serveur orienté événement. La notion de bloques facilite, à nouveau, l'application de notre stratégie d'optimisation. Les bloques d'exécution dans un serveur orienté événement s'appelle des étapes et peuvent être identifiées et analysées par un outil automatisé une fois déclaré par un programmeur sous forme d'annotation pour le code. L'allocateur Stingy dépend du fait que ces étapes peuvent s'exécuter dans des ordres différents sans avoir un effet important sur la sémantique globale de l'application. Combiné à une nouvelle approche d'ordonnancement qui arrange différentes étapes pour limiter l'utilisation de la mémoire, Stingy Allocator assure que toute la mémoire allouée par le serveur soit bornée et qu'il reste dans les caches du système. Un ensemble d'outils a été développé pour intégrer Stingy Allocator dans des programmes existants. Ces outils ont été utilisés pour optimiser des applications existantes. Avec l'aide de ces outils, un programmeur peut modifier un serveur réseau pour qu'il se serve de Stingy Allocator sans comprendre intimement le fonctionnement de celui-ci. Chacune des parties d´ecrites au-dessus a été évaluée dans le contexte des programmes existants. La spécialisation des piles de protocole a été évaluée rigoureusement sur la pile TCP/IP du noyau de Linux. Celle-ci a aussi été ´etudiée dans le contexte de la pile TCP/IP de FreeBSD. La spécialisation distante a été utilisée pour spécialiser dynamiquement la pile TCP/IP de Linux ainsi que le serveur web TUX. Nos expériences ont démontré des réductions importantes dans la taille du code résultant (amélioré d'un facteur de 2 à 20) et des améliorations appréciables en terme de performance, les gains ´etant entre un facteur de 1.12 et 1.4.

Le système de communication décrit est construit dans et avec l'architecture du système d'exploitation CHORUS, fondé sur la communication par message entre des "acteurs". Le modèle ISO sert de base à notre modèle, dans la mesure ou il permet de construire des couches distinctes pour organiser la communication dans chorus.