Christoph Weidenbach

Stephan Merz

have been the best mentors anyone could hope for-supportive in di cult times, hard on me when I needed it, and extremely informative when I had no clue. Uwe Waldmann's classes initiated me into the field, and he continued to o↵er me a helping hand throughout my master's and Ph.D. My o ce mates Daniel Wand and Mathias Fleury as well as the rest of the RG1 and VeriDis teams made the workplace a fun place to be. Special thanks to Tianxiang Lu, whose work is the basis of this dissertation, and Hernán Vanzetto, who dedicated a large portion of his busy schedule for me in my early days. I would not have been here without the Max Planck Institute's funding and support; a big, warm thanks to everyone who makes education possible. I would also not have been here but for my family; my warm, loud, bona fide Egyptian family where everyone takes a surprising interest in your proof of correctness of a P2P protocol. From my mom, also moonlighting as my rock, my dad, a.k.a. provider of all my comforts, my brilliant little sister, my lighthouse, who serves dutifully as my big sister when necessary, her husband and my new brother whose love for her makes her shine even brighter, to my aunt and grandmothers who are buckets of kindness and delight in the shape of human beings. Also belonging to this category, under the title "Brother from Another Mother", is my best friend Eman, who taught me more about myself than I could have ever learned on my own. I have been equally blessed in friends as in family: Nahla, a.k.a. "Partner in Crime" and "Most Selfless Human Being"; Rana, who has been there for me every day of a six-year journey of ups and big downs; Hagar, my role model and powerhouse; Areej, the genuine heart who sees me as I want to be seen and not as I really am, and her husband Eslam who has been there for me through thick and thin; My Powerpu↵ Girls Iva and Maha, Maha, you push me to be a better person and I want to make you proud; Iva, your friendship has been the most important pillar in my life the past years and I will not try to do it justice here; Yusra, you are a lesson on kindness and awesomeness; Dahlia, you're beautiful inside and out; and finally, to Mohammed and Walaa, my home, my conscience and my mirror. My final thanks goes to technology, to people who made the internet what it is and made all the things that make life and work easier, to people who support and donate to these things. Wikipedia, online open course-ware, my Spotify study playlist; these things remind me everyday why I am in tech and that ideas can change the world.

Résumé

Les réseaux pair-à-pair (P2P) constituent un modèle de plus en plus populaire pour la programmation d'applications Internet car ils favorisent la décentralisation, le passage à l'échelle, la tolérance aux pannes et l'auto-organisation. à la di↵érence du modèle traditionnel client-serveur, un réseau P2P est un système réparti décentralisé dans lequel tous les noeuds interagissent directement entre eux et jouent à la fois les rôles de fournisseur et d'utilisateur de services et de ressources. Une table de hachage distribuée (DHT) est réalisée par un réseau P2P et o↵re les mmes services qu'une table de hachage classique, hormis le fait que les di↵érents couples (clef, valeur) sont stockés dans di↵érents noeuds du réseau. La fonction principale d'une DHT est la recherche d'une valeur associée à une clef donnée. Parmi les protocoles réalisant une DHT on peut nommer Chord, Pastry, Kademlia et Tapestry. Ces protocoles promettent de garantir certaines propriétés de correction et de performance ; or, les tentatives de démontrer formellement de telles propriétés se heurtent invariablement à des cas limites dans lesquels certaines propriétés sont violées. Tianxiang Lu a ainsi décrit des problèmes de correction dans des versions publiées de Pastry. Il a conçu un modèle, appelé LuPastry, pour lequel il a fourni une preuve partielle, mécanisée dans l'assistant à la preuve TLA + Proof System, démontrant que les messages de recherche de clef sont acheminés au bon noeud du réseau dans le cas sans départ de noeuds. En analysant la preuve de Lu j'ai découvert qu'elle contenait beaucoup d'hypothèses pour lesquelles aucune preuve n'avait été fournie, et j'ai pu trouver des contreexemples à plusieurs de ces hypothèses. La présente thèse apporte trois contributions. Premièrement, je présente LuPastry + , une spécification TLA + révue de LuPastry. Au-delà des corrections nécessaires d'erreurs, LuPastry + améliore LuPastryen introduisant de nouveaux opérateurs et définitions, conduisant à une spécification plus modulaire et isolant la complexité de raisonnement à des parties circonscrites de la preuve, contribuant ainsi à automatiser davantage la preuve. Deuxièmement, je présente une preuve TLA + complète de l'acheminement correct dans LuPastry + . Enfin, je démontre que l'étape finale du processus d'intégration de noeuds dans LuPastry(et LuPastry + ) n'est pas nécessaire pour garantir la cohérence du protocole. Concrètement, j'exhibe une nouvelle spécification avec un processus simplifié d'intégration de noeuds, que j'appelle Simplified LuPastry + , et je démontre qu'elle garantit le bon acheminement de messages de recherche de clefs. La preuve de correction pour i Simplified LuPastry + est obtenue en réutilisant la preuve pour LuPastry + , et ceci représente un bon succès pour la réutilisation de preuves, en particulier considérant la taille de ces preuves. Chacune des deux preuves requiert plus de 30000 étapes interactives ; à ma connaissance, ces preuves constituent les preuves les plus longues écrites dans le langage TLA + à ce jour, et les seuls exemples d'application de preuves mécanisées de théorèmes pour la vérification de protocoles DHT.

Abstract

A distributed hash table (DHT) is a peer-to-peer network that o↵ers the function of a classic hash table, but where di↵erent key-value pairs are stored at di↵erent nodes on the network. Like a classic hash table, the main function provided by a DHT is key lookup, which retrieves the value stored at a given key. Examples of DHT protocols include Chord, Pastry, Kademlia and Tapestry. Such DHT protocols certain correctness and performance guarantees, but formal verification typically discovers border cases that violate those guarantees. In his PhD thesis, Tianxiang Lu reported correctness problems in published versions of Pastry and developed a model called LuPastry, for which he provided a partial proof of correct delivery of lookup messages assuming no node failure, mechanized in the TLA + Proof System. In analyzing Lu's proof, I discovered that it contained unproven assumptions, and found counterexamples to several of these assumptions. The contribution of this thesis is threefold. First, I present LuPastry + , a revised TLA + specification of LuPastry. Aside from needed bug fixes, LuPastry + contains new definitions that make the specification more modular and significantly improve proof automation. Second, I present a complete TLA + proof of correct delivery for LuPastry + . Third, I prove that the final step of the node join process of LuPastry/LuPastry + is not necessary to achieve consistency. In particular, I develop a new specification with a simpler node join process, which I denote by Simplified LuPastry + , and prove correct delivery of lookup messages for this new specification. The proof of correctness of Simplified LuPastry + is written by reusing the proof for LuPastry + , which represents a success story in proof reuse, especially for proofs of this size. Each of the two proofs amounts to over 32,000 proof steps; to my knowledge, they are currently the largest proofs written in the TLA + language, and-together with Lu's proof-the only examples of applying full theorem proving for the verification of DHT protocols.

iii

Zusammenfassung

Eine verteilte Hashtabelle (DHT) ist ein P2P Netzwerk, das die gleiche Funktion wie eine klassische Hashtabelle anbietet, wo aber verschiedene Schlüssel-Inhalt Paare an verschiedenen Knoten im Netzwerk gespeichert werden. Chord, Pastry, Kademlia und Tapestry sind einige bekannte Implementierungen von DHT. Solche Protokolle versprechen bestimmte Eigenschaften bezüglich Korrektheit und Leistung. Die formale Verifikation von diesen Protokollen führt jedoch normalerweise zu Widersprüchen dieser Eigenschaften. In seiner Doktorarbeit entdeckt Tianxiang Lu Gegenbeispiele zu verö↵entlichten Versionen von Pastry und entwickelt LuPastry, ein Pastry Model ausschließlich des Knotenausfalles. Zusätzlich bietet Lu einen Teilbeweis für korrekte Lieferung von Suchnachrichten in LuPastry in der Sprache TLA + an. Lus Beweis basiert auf unbewiesenen Annahmen. Beim Untersuchen des Beweises habe ich Gegenbeispiele zu mehreren dieser Annahmen entdeckt. Diese Doktorarbeit deckt drei Hauptthemen ab. Erstens, es wird LuPastry + entwickelt: eine revidierte TLA + Spezifikation zu LuPastry. Neben den benötigten Fehlerkorrekturen, bietet LuPastry + zusätzlich neue Definitionen an, welche die Spezifikation modularer machen, und die Automatisierung des Beweises signifikant verbessern. Zweitens, biete ich einen vollständigen TLA + korrektheitsbeweis für LuPastry + an. Drittens, zeige ich, dass der letzte Schritt des Beitrittsprotokolles in LuPastry/LuPastry + nicht notwendig für Korrektheit ist. Insbesondere, biete ich eine neue Spezifikation mit einem einfacheren Beitrittsprotokoll an, und einen Korrektheitsbeweis dafür. Nach bestem Wissen sind diese Beweise (2 Beweise je von über 32.000 Schritten) bis dato die größten in TLA + geschriebenen Beweise. v

Introduction

Les réseaux pair-à-pair (P2P) constituent un modèle qui est de plus en plus utilisé pour la programmation d'applications Internet modernes. à la di↵érence du modèle traditionnel client-serveur qui repose sur un serveur central fournissant des ressources aux clients, un réseau P2P est un système distribué et décentralisé dans lequel tous les noeuds (aussi appelés pairs) interagissent directement entre eux et jouent à la fois les rles de fournisseurs et d'utilisateurs de services et de ressources.

Le modèle P2P a connu sa première heure de gloire en 1999 avec la popularité du système Napster de partage de fichiers qui permettait à ses utilisateurs de chercher et de télécharger des fichiers mis à disposition par d'autres utilisateurs [START_REF] Johnson | The Evolution of the Peer-to-Peer File Sharing Industry and the Security Risks for Users[END_REF]. Cependant, Napster peut être considéré comme un réseau P2P de première génération qui nécessitait encore un serveur central d'indexe contenant des informations sur les utilisateurs et sur leurs contenus partagés. Ce serveur était responsable pour la recherche de fichiers, alors que l'échange de fichiers était réalisé directement entre deux utilisateurs. Plus tard, les services évoluaient vers un modèle tout à fait décentralisé, à la base d'applications comme Gnutella et Kazaa qui fonctionnaient en l'absence de tout serveur central. Ces applications sont souvent appelées des applications P2P de seconde génération.

Les réseaux P2P favorisent le passage à l'échelle et la robustesse car ils ne nécessitent pas de serveur central qui représente un point unique de défaillance ou encore un goulot d'étranglement pour la performance. Ils sont aussi moins coteux et plus faciles à déployer car ils s'auto-organisent et ne nécessitent pas d'équipements spécifiques concernant les serveurs ou les systèmes d'exploitation. Ceci étant dit, certaines applications P2P à large échelle optent pour une architecture semi-distribuée en utilisant un ou plusieurs noeuds spéciaux, parfois appelés super-noeuds, qui sont toujours en ligne et garantissent ainsi au réseau une connectivité et fiabilité accrues.

Aujourd'hui la technologie P2P se trouve dans des applications très diverses, allant du partage de fichiers au visionnage de contenus multi-média et à la téléphonie par Internet. Ainsi Skype, l'application populaire de téléphonie audio et vidéo, repose-t-il sur un réseau P2P entièrement décentralisé, ainsi qu'un certain nombre de super-noeuds. Le site Web o ciel indique que chaque nouveau noeud ajouté au réseau contribue à la puissance de traitement et à la bande passante. Ainsi, en décentralisant les ressources, les réseaux P2P de seconde génération ont réussi à quasiment éliminer les cots associés à une infrastructure centralisée importante [START_REF]What Are P2P Communications[END_REF]. Le site Web argumente aussi que le modèle P2P correspond au modèle prévu à l'origine pour le Web, dans lequel les utilisateurs contribuent de nouveaux contenus (des pages Web) et accèdent aux contenus créés par d'autres utilisateurs.

Un exemple supplémentaire d'une application P2P populaire est le flash player d'Adobe Systèmes, un des visionneurs de médias le plus utilisés sur Internet, qui repose désormais sur la technologie P2P pour visionner du contenu en temps réel et sur demande. Adobe indique qu'une page Web fournissant de l'audio et vidéo à votre ordinateur peut livrer le contenu avec une meilleure performance si les utilisateurs qui visionnent le même contenu partagent leur bande passante. De cette manière, l'audio ou vidéo peut être servie de manière plus lisse, sans coupures ou pauses dues à l'approvisionnement. Ceci est appelé du réseautage assisté par les pairs car les pairs sur le réseau assistent les uns les autres afin de fournir une meilleure expérience [START_REF]What Are Peer-Assisted Networking Settings?[END_REF]. D'autres applications reposaient sur la technologie P2P à un certain moment mais l'abandonnaient plus tard en faveur du modèle centralisé. Pendant un certain temps, la British Broadcasting Corporation (BBC) utilisait un protocole P2P pour soutenir son iPlayer BBC bien connu, une application qui permettait aux utilisateurs de visionner des vidéos de la BBC. Dans un entretien datant de 2008 avec Anthony Rose du groupe BBC Controller Vision and Online Media, celui-ci a rmait que deux ans auparavant l'utilisation de P2P o↵rait des bénéfices clairs et substantiels mais que l'abandon de cette technologie était justifié par les baisses dramatiques du prix de la bande passante qui rétablissaient la faisabilité du modèle client-serveur [START_REF] Rose | Evolution of the BBC iPlayer[END_REF]. Rose se réservait également la possibilité d'un retour ultérieur au P2P. Le service Spotify de streaming audio faisait aussi appel à la technologie P2P pour son client sur ordinateur jusqu'en 2014 quand il revenait à un modèle client-serveur, pour des raisons similaires [START_REF] Torrentfreak | Spotify Starts Shutting Down Its Massive P2P Network[END_REF]. Enfin, la plate-forme Livestation pour la distribution en temps réel de la télévision et de la radio utilisait également une technologie P2P rachetée à Microsoft Research.

L'application qui est probablement la plus fortement associée avec la technologie P2P dans l'opinion publique est BitTorrent, un protocole de communication pour l'échange P2P de fichiers par Internet. En e↵et, en date de 2013 le trafic BitTorrent à lui seul est responsable de 3,35% de la bande passante utilisée par toutes les applications Internet dans le monde [START_REF]Application Usage & Threat Report[END_REF]. Les utilisateurs installent un client BitTorrent au choix parmi plusieurs disponibles, alors qu'un tracker BitTorrent fournit une liste de fichiers disponibles pour l'échange et assiste le client établir une communication avec d'autres pairs qui possèdent le fichier. Il s'agit d'un modèle proche de celui de Napster dans lequel le tracker représente un serveur central qui initie la communication parmi les pairs mais o ceux-ci continuent à interagir de manière décentralisée sans l'aide du serveur. Cependant, de nombreux clients BitTorrent actuels utilisent un système sans tracker dans lequel chaque pair agit comme tracker, résultant en un modèle entièrement décentralisé. De nombreuses entreprises distribuant du logiciel ou du multi-média se servent de la technologie BitTorrent pour offrir des téléchargements. Cette méthode de distribution est particulièrement recommandée par d'importants projets du logiciel libre comme la distribution Linux Ubuntu 1 ou la suite bureautique LibreO ce 2 , afin d'améliorer la disponibilité des téléchargements et de réduire la charge des serveurs propres à ces projets.

Un problème majeur concernant les réseaux P2P à large échelle purs, c'est à dire entièrement décentralisés, réside dans la gestion e cace des ressources disponibles. Un réseau P2P non-structuré sans contrainte sur la topologie des noeuds participants est très ine cace : une fonction comme la recherche d'un fichier donné demanderait dans un tel réseau d'inonder le réseau avec une requête de recherche jusqu'à ce que cette requête atteigne un pair possédant le fichier demandé. Ceci donnerait lieu à une quantité importante de trafic réseau inutile, ainsi qu'à des charges importantes d'utilisation de la CPU et de la mémoire.

Une table de hachage distribuée (distributed hash table, DHT) o↵re un moyen de structurer un réseau P2P de manière à organiser les ressources disponibles, et de rendre les communications entre les pairs fiables et e caces. Une DHT est un réseau P2P qui sert de table de hachage, répartissant les couples (clef, valeur) parmi les di↵érents noeuds du réseau. Les noeuds qui forment la DHT se voient a↵ectés des identifiants uniques, et les messages entre les noeuds sont acheminés par une route impliquant des noeuds intermédiaires et déterminée en fonction de l'identifiant du noeud cible, plutt que par inondation du réseau. Comme une table de hachage classique, une DHT o↵re deux fonction principales : put(k , v ) associe la valeur v à la clef k , alors que get(k ) récupère la valeur associée à la clef k . En raison de l'absence de serveur central ayant une vue globale du réseau, les noeuds d'une DHT doivent collaborer pour déterminer l'ensemble de clefs stockées à chaque noeud, ainsi que pour acheminer les requêtes put et get au noeud concerné.

Les tables de hachage distribuées bénéficient des avantages combinés des réseaux P2P et des tables de hachage, de par une conception simple et élégante permettant la localisation d'une donnée demandée avec une très bonne e cacité, et ne nécessitant aucune information globale. Dans la plupart des applications pratiques, les réseaux P2P/DHT sont sujets à un taux important de churn, des noeuds rejoignant et quittant le réseau en permanence, ainsi qu'à des défaillances spontanées de noeuds qui partent sans en informer au préalable d'autres noeuds du réseau. L'implémentation d'une DHT doit être capable de gérer ces turbulences de manière e cace et gracieuse, assurant une reconfiguration du réseau vers un état stable qui garantit une connectivité entre les noeuds vivants et un consensus sur l'ensemble de clefs a↵ectées à chaque noeud.

La dernière décennie a vu de grands e↵orts de recherche dans le domaine des réseaux P2P, et en particulier des DHT. De nombreuses implémentations de DHT ont été proposées dans la littérature scientifique, et beaucoup de travaux ont été entrepris afin d'étudier les propriétés de ces implémentations et comment les améliorer. Parmi les protocoles DHT les plus connus figurent Pastry, Chord, Kademlia et CAN [START_REF] Rowstron | Pastry: Scalable, Decentralized Object Location and Routing for Large-Scale Peer-to-Peer Systems[END_REF][START_REF] Stoica | Chord: A Scalable Peer-to-peer Lookup Service for Internet Applications[END_REF][START_REF] Maymounkov | Kademlia: A Peer-to-Peer Information System Based on the XOR Metric[END_REF][START_REF] Ratnasamy | A Scalable Content-addressable Network[END_REF]. Ces protocoles sont similaires dans le sens qu'ils se focalisent sur la gestion e cace de données stockées de manière répartie parmi un grand nombre de noeuds. Cependant, ils di↵èrent par rapport à des caractéristiques telles que la topologie du réseau logique, la fonction pour calculer la distance entre deux noeuds du réseau, et le modèle de routage. Par exemple, Chord organise les noeuds dans un cercle virtuel appelé l'anneau Chord. Pastry repose sur une structure arborescente de noeuds, assistée par une structure annulaire similaire à celle de Chord et qui sert de base au routage quand la structure arborescente est incapable de déterminer la cible appropriée. Dans Chord, ainsi que dans d'autres protocoles, les noeuds exécutent périodiquement un algorithme de stabilisation, en échangeant des messages de ping afin de maintenir à jour leurs informations locales concernant le réseau. L'article [START_REF] Zhang | A Survey on Distributed Hash Table (DHT): Theory, Platforms, and Applications[END_REF] donne un excellent aperçu des di↵érentes variantes de DHT, leurs théories sous-jacentes, et leurs applications.

Alors que les entreprises optant pour la technologie P2P utilisent généralement des implémentations propriétaires, comme dans les exemples cités précédemment, ces implémentations reposent souvent sur des protocoles proposés dans la littérature scientifique. Un exemple bien connu d'applications fondées sur des DHT est le tracking réparti des systèmes BitTorrent sans trackers explicites mentionnés plus haut qui est implanté par de nombreux clients BitTorrent. Ainsi, l'implémentation Mainline DHT de tracking réparti pour BitTorrent, fondée sur Kademlia, est probablement l'implémentation la plus importante de DHT en pratique. Une étude menée en 2013 estimait le nombre d'utilisateurs de Mainline DHT entre 10 et 25 millions, avec un churn quotidien d'au moins 10 millions [START_REF] Wang | Measuring Large-Scale Distributed Systems: Case of BitTorrent Mainline DHT[END_REF]. Des implémentations propriétaires de DHT incluent Oracle Coherence, la grille de données résidant dans la mémoire vive d'Oracle implantée en Java et le service DynamoDB de bases de données proposé par Amazon.

Les publications concernant les protocoles DHT typiquement a rment certains taux de stabilité et de fiabilité de ces protocoles en fonction du churn. Cependant, ces a rmations ne sont généralement fondées que sur des démonstrations papier, au mieux. Observant les problèmes de connectivité de certaines applications P2P populaires soumises au churn, on s'est rendu compte au cours de ces dernières années que la technologie DHT actuelle ne peut pas garantir des niveaux de fiabilité tels qu'imaginés à l'origine. Par exemple, l'application Skype fondée sur une implantation P2P qui est très certainement une DHT, a subi deux coupures massives en 2007 et en décembre de 2010, cette dernière étant due à une défaillance spontanée d'un nombre important de super-noeuds. Dans quelques heures à peine, le nombre d'utilisateurs connectés à Skype tomba de 23,3 millions à environ 1,6 millions, et la coupure dura deux jours.

De telles coupures représentent bien évidemment une facture importante pour les entreprises. Ce risque, couplé à une utilisation en augmentation de la technologie P2P/DHT dans de nombreuses applications demandant de la tolérance aux pannes, a motivé des travaux de recherche s'intéressant à la vérification de protocoles P2P, et particulièrement DHT, en employant des méthodes formelles telles que la modélisation formelle, la simulation et la vérification automatique par model checking. Naturellement, l'analyse et la vérification de tels systèmes répartis de large échelle sont tout sauf triviales. En e↵et, en raison de la taille et de la complexité de tels systèmes, les e↵orts de vérification ont le plus souvent été limités à l'étude de certains fragments de ces protocoles -tels que la recherche de clefs dans un réseau statique sans arrivée ou départ de noeuds -et ils ont typiquement fait appel à des méthodes légères telles que la modélisation et la simulation.

La présente thèse s'insère dans cette ligne de recherche : elle propose une étude de la correction de Pastry sur la base de la preuve de théorèmes mécanisée. Plus précisément, je vérifie le protocole de la recherche de clefs (requêtes get) pour deux variantes de Pastry en donnant des preuves de correction complètes et rigoureuses dans l'assistant interactif à la preuve TLA + . Il a déjà été démontré dans [START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF] qu'aucune version publiée de Pastry ne garantit cette propriété de correction car des ajouts et départs de noeuds peuvent causer une séparation irréversible du réseau, conduisant à un acheminement erroné de messages de recherche de clefs. Dans cette thèse je démontre que le modèle de Pastry sans départ de noeuds garantit l'acheminement correct de messages de recherche de clefs. Je montre également que, toujours dans le modèle sans départ de noeuds, la correction est maintenue par un processus d'ajout de noeuds qui est plus simple que ceux proposés pour Pastry, par exemple dans les articles [START_REF] Haeberlen | Consistent Key Mapping in Structured Overlays[END_REF][START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF].

Dans ce qui suit, je discute certains travaux connexes traitant du sujet de la vérification formelle de protocoles P2P. Ensuite, je décris la contribution de cette thèse à ce domaine de recherche. Ceci est suivi d'une courte description des outils et techniques utilisés dans cette thèse, et en particulier de l'assistant à la preuve TLA + . Enfin, je donne un court résumé de la suite de la thèse.

Travaux connexes

Un grand nombre d'études scientifique a été dédié pendant ces dernières années au protocole de DHT Chord qui présente de fortes similarités à Pastry. Il implante une table de hachage distribuée de la manière suivante. Une fonction fixe de hachage associe à chaque clef et à chaque noeud vivant de Chord un identifiant de m bits (l'identifiant d'un noeud est calculé en appliquant la fonction de hachage à son adresse IP alors que l'identifiant d'une clef est déterminée en hachant la clef). L'espace d'identifiants est assimilé à un cercle appelé l'anneau Chord qui contient les 2 m identifiants possibles entre 0 et 2 m 1. La clef k est associée au premier noeud n dont l'identifiant est égal à celui de k ou qui le suit dans le sens de l'anneau ; n est appelé le noeud successeur de k . Chaque noeud n maintient une liste de ses successeurs dans l'anneau, ainsi qu'un tableau de doigts (finger table) pour un routage e cace, ce dernier contenant les adresses d'au plus m noeuds à di↵érents catégories de distance de n. Plus spécifiquement, la i -ème entrée dans cette table contient le premier noeud à une distance d'au moins 2 i 1 identifiants de n sur l'anneau. Les noeuds de Chord utilisent un algorithme périodique de stabilisation pour maintenir à jour leurs listes de successeurs et tableaux de doigts. Un routage correct des requêtes est garanti si chaque noeud connat son noeud successeur immédiat sur l'anneau. En présence de défaillances de noeuds, cette hypothèse ne peut être maintenue à tout moment, et l'e↵et de défaillances de noeuds est mitigé par la réplication, conduisant au maintien de listes de successeurs : plus grande la taille de la liste de successeurs et plus grande sera la probabilité que la requête d'une clef renvoie le noeud correct.

Bakhshi et al. [START_REF] Bakhshi | Verification of Peer-to-Peer Algorithms: A Case Study[END_REF] décrivent un modèle abstrait de réseaux P2P structurés en anneau dans le ⇡-calcul. Ils utilisent ce modèle pour vérifier l'algorithme de stabilisation de Chord en exhibant une bisimulation faible entre la spécification de Chord en tant que réseau en anneau et l'implémentation de l'algorithme de stabilisation. Cette étude est menée dans un modèle d'ajout pur de noeuds mais sans défaillances, et des entités comme les tableaux de doigts ou listes de successeurs ne sont pas prises en compte.

Zave a mené beaucoup de travaux au sujet de la vérification de Chord. Utilisant Alloy pour modéliser formellement et pour vérifier Chord, elle démontre que le modèle d'ajout pur -c'est à dire dans lequel aucun noeud ne part du réseau -est correct mais que le protocole complet n'assure pas forcément les invariants a rmés [START_REF] Zave | Using Lightweight Modeling to Understand Chord[END_REF]. Dans l'article [START_REF] Zave | How to Make Chord Correct (Using a Stable Base[END_REF] elle présente une version de Chord assortie d'une preuve partiellement mécanisée de correction.

DKS [START_REF] Onana Alima | A Family of Low Communication, Scalable and Fault-Tolerant Infrastructures for P2P Applications[END_REF] est une implémentation d'une table de hachage distribuée dont le nom est dérivée de recherche k -aire répartie. DKS(N , k , f ) décrit un protocole P2P pour un réseau de taille maximale N , une arité de recherche de k dans le réseau et un paramètre f de tolérance aux pannes. Brièvement, la recherche k -aire répartie garantit que n'importe quelle clef t peut être localisée dans au plus log k (N ) sauts. Initialement, l'espace de recherche est identique à l'espace entier de clefs dans la table de hachage. à chaque pas de la recherche distribuée, l'espace de recherche actuel est divisé en k parties de tailles égales, dont chacune est sous la responsabilité d'un noeud di↵érent. En répétant ces sous-divisions jusqu'à ce que chaque partie ne contienne qu'un élément, l'algorithme aboutit à la partie contenant la clef t qui correspond à la cible de la recherche.

DKS peut être vu comme une généralisation de systèmes comme Chord, Pastry ou Tapestry. Comme Chord, DKS repose sur une structure en anneau, bien que les auteurs a rment que cette structure soit arbitraire et que les algorithmes proposés fonctionnent également pour d'autres topologies de réseaux. Le point distinctif de DKS est que, contrairement à d'autres protocoles, il ne requiert pas de routine corrective pour maintenir à jour des tableaux de routage ou d'autres informations locales. En e↵et, les tableaux de routage sont corrigés à la volée pendant les opérations de recherche et d'insertion. Cette idée repose sur l'observation que, dans les systèmes P2P o le nombre de recherches et insertions est beaucoup plus grand que celui d'ajouts de noeuds, de départs ou de défaillances, la correction des tableaux de routage à la volée pendant que le protocole e↵ectue des opérations de recherche et d'insertion évite une consommation inutile de la bande passante due à un mécanisme périodique de correction.

DKS permet aux noeuds de rejoindre ou de quitter le réseau à n'importe quel moment. Comme dans le cas de Chord, un noeud rejoint un réseau DKS en envoyant une requête correspondante à son successeur sur l'anneau. Rejoindre l'anneau est un événement atomique dans le sens qu'un noeud i recevant plus d'une requête à rejoindre l'anneau ne peut en traiter plus d'une à la fois. Un noeud peut soit quitter l'anneau de manière gracieuse en informant d'autres noeuds de son intention de partir, soit il peut échouer abruptement. Il est a rmé que le système continue à fournir un service fiable de recherche de clefs pourvu que pas plus de f noeuds consécutifs n'échouent en même temps.

Les auteurs de DKS mènent des expériences par simulation afin de déterminer l'e↵et du churn sur l'e cacité du traitement des requêtes de clefs [START_REF] Onana Alima | A Family of Low Communication, Scalable and Fault-Tolerant Infrastructures for P2P Applications[END_REF]. Le protocole DKS est décrit en détail dans la thèse de Ghodsi [START_REF] Ghodsi | Distributed K-ary System: Algorithms for Distributed Hash Tables[END_REF]. Dans cette thèse, Ghodsi discute plusieurs problèmes tels que des demandes d'intégration à l'anneau concurrentes à des défaillances de noeuds, et il a rme qu'on ne peut pas garantir la correction en présence de défaillances arbitraires de noeuds, à cause d'une possible séparation du réseau. Toujours concernant DKS, citons le travail de Borgstrm et al. [START_REF] Borgström | Verifying a Structured Peer-to-Peer Overlay Network: The Static Case[END_REF] qui utilise CCS pour la vérification formelle du protocole de recherche de clefs dans le cas statique, c'est à dire sans la prise en compte de l'arrivée ou du départ de noeuds.

Le travail le plus proche, et qui constitue également le point de départ de cette thèse, a été mené par Lu [START_REF] Lu | Model Checking the Pastry Routing Protocol[END_REF][START_REF] Lu | Towards Verification of the Pastry Protocol Using TLA +[END_REF][START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF] concernant Pastry. Pastry [START_REF] Rowstron | Pastry: Scalable, Decentralized Object Location and Routing for Large-Scale Peer-to-Peer Systems[END_REF] est un réseau structuré en anneau, de manière similaire à Chord, et chaque noeud maintient des listes de successeurs et de prédecesseurs, appelées l'ensemble de feuilles (leaf set) du noeud. Au lieu du tableau de doigts de Chord, chaque noeud dispose d'un tableau de routage dont les entrées sont déterminées par la longueur du préfixe de bits commun entre les identifiants de l'entrée et du noeud. Comme dans le cas de Chord, l'acheminement correct de requêtes de clefs peut être garanti par Pastry si chaque noeud a un ensemble de feuilles correct, ou au moins connat ses successeur et prédecesseur sur l'anneau, indépendamment du contenu du tableau de routage.

Lu modélise Pastry en TLA + , et il utilise l'outil TLC de model checking, ainsi que l'assistant TLAPS à la preuve, pour vérifier formellement le bon acheminement de de requêtes de clefs (messages get) : à tout moment il existe au plus un noeud qui puisse répondre à une requête de recherche de clef, et ce noeud est le noeud vivant le plus proche à la clef. Comme dans le cas de Chord, Lu découvre plusieurs problèmes dans le protocole Pastry original, même après avoir pris en compte des améliorations proposées. Enfin il présente une variante de Pastry appelée LuPastryet ne prenant en compte que l'intégration de noeuds, et il vérifie l'acheminement correct sous l'hypothèse forte qu'aucun noeud ne fait défaillance. Il est à noter que la variante de Pastry proposée par Lu repose aussi sur des ajouts atomiques de noeuds dans le sens qu'un noeud vivant est seulement autorisé à assister un seul noeud à la fois à rejoindre l'anneau, comme dans le cas de DKS. Dans sa preuve, Lu réduit la propriété du bon acheminement à un ensemble d'environ 50 invariants que le protocole est a rmé vérifier, et ces invariants sont démontrés à l'aide de TLAPS. Dans ce sens, LuPastryreprésente un e↵ort majeur dans le domaine de la vérification formelle mécanisée d'algorithmes répartis.

Néanmoins, la preuve de Lu repose sur de nombreuses hypothèses présentées sans preuve concernant l'arithmétique et les structures de données spécifiques au protocole. En examinant la preuve, j'ai découvert des contre-exemples à plusieurs de ces hypothèses de base. Alors que j'ai pu démontrer des variantes plus fortes de plusieurs de ces hypothèses, ceci n'a pas été possible pour d'autres. En e↵et, j'ai pu trouver un contre-exemple à l'un des invariants a rmés par Lu, la preuve duquel n'a été possible grce à des hypothèses incorrectes. Cette observation m'a conduit à concevoir une nouvelle preuve de correction pour LuPastry, et ce faisant à améliorer la spécification TLA + du protocole dans plusieurs respects. Au cours de mon travail de preuve j'ai observé que le sousprotocole d'intégration de noeuds peut être simplifié de manière significative sans en a↵ecter la correction. Plus précisément, l'étape finale appelée échange de bail (lease exchange) que le nouveau noeud doit e↵ectuer avec ses noeuds voisins avant de participer activement au protocole n'est pas nécessaire pour démontrer la correction dans les scénarios o il n'y a que des ajouts de noeuds au réseau. En e↵et, cet échange de bail ne faisait pas partie du protocole d'origine publié dans [START_REF] Rowstron | Pastry: Scalable, Decentralized Object Location and Routing for Large-Scale Peer-to-Peer Systems[END_REF] mais a seulement été introduit par les auteurs dans un article ultérieur, parmi d'autres améliorations au protocole. Bien qu'aucune raison explicite n'ait été donnée, on peut considérer que la raison probable à l'ajout de cette étape était d'améliorer la justesse des ensembles de feuilles et, par conséquent, la fiabilité de la recherche de clefs. Comme démontré par Lu, le protocole entier dans lequel des noeuds peuvent arriver et partir librement ne garantit pas le bon acheminement de messages de recherche de clefs, même en présence d'échange de bail. Par contre, j'observe qu'en absence de départ de noeuds, le protocole est correct même sans cette étape. à la suite de cette observation, j'ai formalisé une variante plus simple de la spécification de Lu-Pastryqui s'a↵ranchit de l'étape d'échange de bail, et j'ai démontré que cette variante garantit le bon acheminement de messages.

Contributions de cette thèse

Cette thèse fait les contributions suivantes.

1. LuPastry + . Une version améliorée de la spécificaton TLA + de LuPastry [START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF] est proposée. Au-delà de la correction d'erreurs, la structure de la spécification est plus modulaire, en introduisant de nouveaux opérateurs qui permettent d'améliorer notablement le degré d'automatisation de la preuve de correction. Cette thèse présente une contribution originale dans les sens suivants. D'abord, elle représente une étude de deux variantes dynamiques de Pastry, sans se restreindre à une vue statique du réseau, en permettant à des noeuds d'intégrer le réseau de manière concurrente. Ensuite, la vérification du protocole repose sur la preuve mécanisée de théorèmes plutt que sur des méthodes moins rigoureuses comme la simulation ou le model checking d'instances finies. Enfin, la preuve de correction de LuPastry + simplifié, obtenue en adaptant celle de LuPastry + , représente une réussite unique en matière de réutilisation de preuves, spécialement pour une preuve de taille aussi importante contenant plus de 32000 interactions de preuve.

Outils et techniques

Vérification formelle

La vérification formelle d'un système informatique (matériel ou logiciel) est le fait de s'assurer de la correction du système, c'est à dire que le système fonctionne comme prévu en garantissant un ensemble d'exigences ou propriétés spécifiques, sur la base de méthodes mathématiques formelles.

Il existe di↵érentes approches à la vérification formelle qui varient de par leur rigueur, et par conséquent de par le temps et e↵ort nécessaires à leur application. Quelle que soit l'approche choisie, la première étape consiste en une spécification du système : un modèle du système décrivant son comportement attendu, rédigé dans une notation mathématique choisie, qu'elle soit fondée sur la logique, les automates, les réseaux de Petri, les algèbres de processus ou la théorie des ensembles. Une spécification doit être aussi précise, non-ambigue, concise et complète que possible. Cette thèse implique deux techniques de vérification formelle : le model checking et la preuve mécanisée.

Model checking. Par model checking, on entend un ensemble de techniques pour vérifier que toute exécution du système vérifie les propriétés énoncées. Pour des systèmes à nombre d'états fini, cette approche est rigoureuse. Il est également possible d'utiliser le model checking pour des modèles infinis, à condition que des ensembles infinis d'états puissent être représentés de manière finitaire. Pour des systèmes de taille arbitraire, le model checking su t pour vérifier des instances du système de taille fixe, et ceci aide à découvrir des erreurs et à gagner en confiance en la correction de la spécification du système entier, mais ne sert pas de preuve dans l'absolu. En d'autres termes, le model checking est utile pour démontrer la présence plutt que l'absence d'erreurs [START_REF] Beckert | Formal Specification and Verification[END_REF]. Model checking présente l'avantage d'être entièrement automatisé et de ne demander que peu d'interaction de la part de l'utilisateur. Cependant, un problème typique avec le model checking est l'explosion d'états car pour la plupart des systèmes pratiques l'espace d'états est soit infini soit crot de manière exponentielle avec le nombre de paramètres variables du système [START_REF] Baier | Principles of Model Checking[END_REF].

Preuve mécanisée. La vérification déductive dénote le processus de générer une collection d'obligations de preuve mathématiques dont la véracité implique la correction du système. Ces obligations sont alors déchargées, ou démontrées, à l'aide d'un outil dédié à la preuve mécanique. Un outil automatique de preuve de théorèmes essaie de démontrer ou d'infirmer une obligation de preuve donnée de manière entièrement automatisée, sans interférence de la part de l'utilisateur. De tels outils peuvent être généralistes tels que Spass [START_REF] Weidenbach | SPASS Version 3.5[END_REF] ou Zenon [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF], ainsi que des prouveurs SMT (satisfiabilité modulo théories) tels que CVC4 [START_REF] Barrett | CVC4[END_REF] ou Z3 [START_REF] De | Z3: An E cient SMT Solver[END_REF] qui se chargent d'obligations de preuve relatives à une certaine théorie comme l'arithmétique ou la théorie des ensembles. 3 Pour des systèmes de grande taille, un outil interactif de preuve, aussi appelé assistant à la preuve, est un outil logiciel qui assiste un utilisateur en la rédaction de preuves mathématiques dont les obligations de preuve élémentaires sont déléguées à un outil de preuve automatique. L'application de la preuve de théorèmes à la vérification de systèmes de grande taille peut être un processus long et coteux, et il demande une très fine compréhension du système, ainsi que de nombreuses interactions avec l'assistant à la preuve.

TLA + TLA + est un langage de spécification formelle dédié à la modélisation et la vérification de systèmes répartis. TLA + permet d'écrire une spécification du système, d'en énoncer les propriétés et enfin d'écrire des preuves de ces propriétés.

Le langage de spécification est fondé sur la logique temporelle des actions (temporal logic of actions, TLA), une variante de la logique temporelle de temps linéaire définie par Leslie Lamport en 1994, pour la spécification du comportement dynamique du système, et sur la théorie non-typée des ensembles due à Zermelo et Fraenkel pour décrire les structures de données. Les systèmes sont décrits en tant que machines à états opérant sur des n-uplets de variables d'états, en définissant un prédicat d'états Init et un prédicat de transitions Next qui contraignent respectivement les états initiaux possibles du système et sa relation de transition. Un prédicat de transition (appelé aussi action) est une formule de la logique du premier ordre contenant de variables non-primées et primées qui dénotent respectivement les valeurs de ces variables dans les états avant et après la transition.

Les propriétés énoncées d'une spécification TLA + sont elles aussi exprimées en tant que formules de la logique temporelle. Ces propriétés peuvent être vérifiées sur des instances finies de la spécification en faisant appel à TLC [START_REF] Yu | Model Checking TLA + Specifications[END_REF], le model checker par énumération explicite d'états associé à TLA + . Pour des instances de taille infinie ou arbitraire, les propriétés peuvent être démontrées en rédigeant une preuve qui peut être certifiée à l'aide de TLAPS (TLA + Proof System, [START_REF] Cousineau | TLA + Proofs[END_REF]), dont l'architecture est présentée à la figure 2.1. La base de TLAPS est un langage hiérarchique de preuves : l'utilisateur rédige une preuve TLA + formée d'une hiérarchie d'étapes de preuve. Chaque étape est interprétée par le gestionnaire de preuves qui génère des obligations de preuve correspondantes et les envoie à des outils automatiques de preuve incluant Zenon, Isabelle/TLA + et des solveurs SMT. Des étapes plus di ciles qui ne peuvent être démontrées immédiatement par les outils automatiques peuvent être décomposées en de multiples sous-étapes. à cause de la nature non-typée du langage, une partie de l'e↵ort de preuve consiste en la démonstration d'un invariant de typage qui fixe en particulier les domaines et co-domaines des fonctions et opérateurs.

TLA + et ses outils sont accessibles depuis l'interface TLA + toolbox. La toolbox est un environnement intégré de développement qui permet aux utilisateurs de rédiger des spécifications TLA + , d'exécuter le model checker TLC et de rédiger et certifier des preuves en faisant appel au gestionnaire de preuves. Les langages de spécification et de preuves TLA + sont brièvement expliqués au chapitre 3.

Méthodologie

Je démontre la propriété de sreté qui exprime le bon acheminement des requêtes pour deux variantes di↵érentes de Pastry. La propriété a rme qu'à tout moment d'une exécution il existe au plus un noeud qui puisse répondre à une requête de clef, et ce noeud est le noeud vivant le plus proche à cette clef [START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF].

Pour chaque variante de Pastry, la méthodologie empruntée pour trouver la preuve est illustrée à la figure 2.2. La variante de Pastry en question est décrite par une spécification TLA + et la propriété de bon acheminement est démontrée en la réduisant à des invariants inductifs de la spécification. Une propriété P est un invariant d'une spécification si elle est vraie à tous les états initiaux de la spécification, ainsi qu'à tous les états accessibles à partir des états initiaux. La propriété P est un invariant inductif si elle est vraie à tous les états initiaux de la spécification, et si sa véracité est préservée par toutes les transitions. D'après cette définition tout invariant inductif est un invariant car une propriété vraie à tous les états initiaux et préservée par toutes les transitions est nécessairement vraie à tous les états accessibles. Le plus grand défi dans l'élaboration de la preuve est de trouver les invariants inductifs qui sont su sants et corrects. Ce processus de découverte des invariants sous-jacents se déroule comme suit.

Je commence par exprimer une propriété P qui m'apparat à la fois comme utile pour la preuve du bon acheminement et comme invariant correct de la spécification. Je me sers du model checking pour vérifier s'il y a des contreexemples à cette propriété dans un réseau de petite taille, par exemple de quatre ou huit noeuds. Si TLC trouve un contre-exemple, alors P n'est pas un invariant de la spécification, et il est nécessaire de reformuler la propriété de manière appropriée. Si aucun contre-exemple n'est trouvé alors on peut avoir assez de confiance pour procéder à l'étape suivante en démontrant par induction, à l'aide de TLAPS, que P est un invariant inductif. Ce processus peut toujours révéler des contre-exemples à la propriété P qui n'ont pas pu être trouvés par model checking, et dans ce cas la propriété doit toujours être révisée. Si la démonstration établit P comme un invariant de la spécification, alors la propriété est ajoutée à la liste d'invariants qui peuvent être utilisés dans la preuve du bon acheminement. Cette dernière preuve se déroule en parallèle au processus de générer et de modifier des invariants : les invariants découverts sont motivés par la preuve du bon acheminement, et ils influent à leur tour sur cette preuve.

Organisation

Cette thèse est organisée comme suit. Le chapitre 3 contient des notions préliminaires sur les réseaux pair-à-pair, les tables de hachage distribuées, la vérification formelle et le langage et l'assistant à la preuve TLA + . Dans le chapitre 4 je présente le modèle LuPastry + ainsi que sa spécification en TLA + . Dans le chapitre 5 je décris les améliorations que ma nouvelle spécification LuPastry + apporte à la spécification originale de LuPastrypar Lu. Je résume également mon analyse de la preuve partielle de correction par Lu et décris des contre-exemples que j'ai pu découvrir à certaines de ses hypothèses, et à l'un des invariants a rmés dans la preuve. Enfin, j'explique la structure de ma nouvelle preuve rigoureuse de correction pour LuPastry + . Cette preuve elle-même est décrite au chapitre 6. Dans le chapitre 7 je présente le protocole LuPastry + simplifié dans lequel la phase d'échange de bail est éliminée du processus d'intégration de noeuds, et je montre comment j'adapte la preuve TLA + de LuPastry + pour obtenir une nouvelle preuve de correction du protocole simplifié. Enfin, le chapitre 8 contient des remarques de conclusion et une discussion des limitations de ce travail, ainsi que d'éventuels travaux futurs dans cette direction.

Introduction

Peer-to-peer (P2P) networks are an increasingly popular model for modern internet applications. In contrast to the traditional client/server model, which relies on a centralized server providing resources to clients, a P2P network is a distributed, decentralized system in which all nodes, or peers, communicate directly with each other and act as both providers and users of services and resources.

The P2P model came to popularity with the rise of the file sharing system Napster in 1999, which allowed users to search and download files found on other users' devices [START_REF] Johnson | The Evolution of the Peer-to-Peer File Sharing Industry and the Security Risks for Users[END_REF]. However, Napster can be seen as a first generation P2P network, which still relied on a central index server that indexed users and their shared content. Searching for files took place through the server, while file transfer took place directly between two users. Later on, the trend moved towards a completely decentralized model with applications like Gnutella, which could operate without any central servers. These applications are often termed second generation P2P applications.

P2P networks are favored for their scalability and robustness, since there is no central server representing a single point of failure or a performance bottleneck. They are also cheaper and easier to set up, since they are self-organized and there is no need for any special server equipment or operating system. That said, some large-scale P2P applications opt for a semi-distributed approach, making use of one or more special nodes, sometimes termed supernodes, that remain online to provide the network with better connectivity and reliability.

Today, P2P technology is used in a large variety of applications from file sharing to multimedia streaming and online telephony. Skype, the popular voice and video chatting application, relies on a completely decentralized P2P network with a number of supernodes. According to their o cial web site, "Each new node added to the network adds potential processing power and bandwidth to the network. Thus, by decentralizing resources, second generation (2G) P2P networks have been able to virtually eliminate costs associated with a large, centralized infrastructure" [START_REF]What Are P2P Communications[END_REF]. It is also argued on the web page that the P2P model was the original model envisioned for the world wide web 13 at the time of its creation, with users both creating new content (web pages) and accessing content created by other users.

Another example of a popular P2P application is Adobe System's flash player, which is one of the most widely-used media players on the internet, and now based on P2P technology for support of live and on-demand streaming. Adobe states that "A website that serves audio and video to your computer can deliver the content with better performance if users who are playing the same content share their bandwidth. Sharing bandwidth allows the audio or video to play more smoothly, without skips or pauses from bu↵ering. This is called peer-assisted networking, since peers on the network assist each other to provide a better experience" [START_REF]What Are Peer-Assisted Networking Settings?[END_REF].

Other applications relied on P2P technology at some point, but later abandoned it in favor of the centralized model. For some time, the British Broadcast Corporation (BBC) used P2P as the underlying model for its famous BBC iPlayer, a desktop application which allows users to stream BBC videos. In a 2008 interview with Anthony Rose, BBC Controller Vision and Online Media Group, he stated that "there were definite and substantial benefits from using P2P two years ago", but that the shift away from P2P was justified because of the dramatic decline in the price of bandwidth, making the client/server model feasible once more [START_REF] Rose | Evolution of the BBC iPlayer[END_REF]. Rose also expressed the possibility of a return to P2P in the future. Spotify, the music streaming service, also relied on P2P technology for music streaming on their desktop client until they moved back to a client/server model in 2014, citing similar reasons [START_REF] Torrentfreak | Spotify Starts Shutting Down Its Massive P2P Network[END_REF]. Livestation, a platform for distributing live television and radio online, also started out based on P2P technology acquired from Microsoft Research.

Perhaps the application that is most strongly associated in the minds of the public with P2P technology is BitTorrent, a communications protocol for P2P file sharing over the internet. In fact, as of 2013, BitTorrent tra c amounts to 3.35% of all internet application bandwidth worldwide [START_REF]Application Usage & Threat Report[END_REF]. Users install one of the several available BitTorrent clients, and a BitTorrent tracker provides a list of files available for transfer and helps the client communicate with other peers that have the file. This is a Napster-like model where the tracker represents a central server that initiates the communication between peers, but where peers continue to communicate in a decentralized way without the help of the server. However, many BitTorrent clients now use a trackerless system, where every peer acts as a tracker, resulting in a completely decentralized model. Many software and multimedia companies now o↵er some downloads using BitTorrent technology. It is particularly encouraged as a download method by major opensource and free software projects such as the Linux distribution Ubuntu1 , or the LibreO ce o ce suite2 , in order to improve download availability and reduce the load on the project's own servers.

A key problem with pure, completely decentralized P2P networks, and in particular large-scale networks, is how to e ciently manage the available re-sources. A completely unstructured P2P network where no topology is imposed on the participating nodes is highly ine cient, since in such a network, functions like search for a given file would have to resort to flooding the network with a search request until the request reaches a peer that has the required file. Flooding causes a very high amount of unnecessary network tra c and CPU/memory usage [START_REF] Zhou | On the Performance of P2P Network: An Assortment Method[END_REF][START_REF] George | Unstructured Peer-to-Peer Networks: Topological Properties and Search Performance[END_REF].

Distributed hash tables (DHT) are a way of structuring P2P networks so that the available resources are organized, and communication among peers is reliable and e cient. A DHT is a P2P network that acts as a hash table where di↵erent (key-value) pairs are stored at di↵erent nodes on the network. Nodes forming a DHT are assigned unique identifiers, and messages from one node to another-instead of being flooded through the network-are routed through a number of intermediate nodes, the route being determined by node identifiers. Like a classic hash table, a DHT o↵ers two main functions: put(k , v ) stores the value v at key k , and get(k ) retrieves the value associated with key k . Due to the lack of a central server with a global view of the network, nodes in a DHT must collaborate to decide on their respective key storage range, and to route put and get requests to the appropriate node.

Distributed hash tables tap the advantages of both P2P communication and hash tables, with a simple and elegant design that enables locating a required piece of data with high e ciency, and without the need for global information. In most practical applications, P2P/DHT networks are subject to a high level of churn; nodes are continuously joining and leaving the network, and may fail abruptly without giving notice to other nodes on the network. The DHT implementation should handle this turbulence e ciently and smoothly and ensure that the network always recovers into a stable state where connectivity among the live nodes is maintained and there is no confusion as to which node stores which portion of the key space.

The past decade has seen extensive research in the area of P2P networks, and especially DHT. Numerous implementations of DHT have been proposed in research publications, and a lot of work has been done to study the properties of these implementations and how to improve them. Among the most popular DHT protocols are Pastry, Chord, Kademlia and CAN [START_REF] Rowstron | Pastry: Scalable, Decentralized Object Location and Routing for Large-Scale Peer-to-Peer Systems[END_REF][START_REF] Stoica | Chord: A Scalable Peer-to-peer Lookup Service for Internet Applications[END_REF][START_REF] Maymounkov | Kademlia: A Peer-to-Peer Information System Based on the XOR Metric[END_REF][START_REF] Ratnasamy | A Scalable Content-addressable Network[END_REF]. These protocols are similar in that they focus on the e cient management of data stored in a distributed fashion over a large number of nodes, but they di↵er in some characteristics such as the topology of the overlay network, the distance function between nodes on the network, and the routing model. In Chord, for example, nodes are organized in a circle called the Chord ring. Pastry uses a tree-like structure of nodes, aided by a ring structure similar to that of Chord that is used for routing when the tree structure cannot find the proper target. In Chord and other protocols, nodes employ a periodic "stabilization algorithm" by exchanging ping messages to keep their local information about the network up to date. An excellent survey of the di↵erent variants of DHT, the underlying theory and applications can be found in [START_REF] Zhang | A Survey on Distributed Hash Table (DHT): Theory, Platforms, and Applications[END_REF].

While companies opting for P2P technology typically base their services on their own proprietary implementations as in the examples mentioned above, these implementations are often based on or similar to the implementations proposed in scientific publications. A prominent example of DHT-based applications is "distributed tracking" for trackerless BitTorrent systems mentioned above, supported by many popular BitTorrent clients. Arguably the largest practical implementation of DHT is the distributed BitTorrent tracking implementation Mainline DHT, based on Kademlia. In 2013, a study measured Mainline DHT users to range from 10 million to 25 million, with a daily churn of at least 10 million [START_REF] Wang | Measuring Large-Scale Distributed Systems: Case of BitTorrent Mainline DHT[END_REF]. Proprietary DHT implementations include Oracle Coherence, Oracle's Java-based in-memory data grid, and Amazon's DynamoDB database service [START_REF] Decandia | Dynamo: Amazon's Highly Available Key-Value Store[END_REF].

Published proposals of DHT protocols typically make claims regarding the reliability and stability of the given protocol under churn. However, these claims are usually supported by paper-and-pencil arguments at best. With popular P2P-based applications su↵ering from connectivity problems due to churn, it has become increasingly clear over the years that the reliability of current DHT technology cannot be guaranteed as was once believed. Skype, for example, which is based on a proprietary P2P implementation that is most likely a DHT, has su↵ered two major outages in 2007 and December of 2010, the latter being due to the abrupt failure of a large number of "supernodes". In just a few hours, the number of online Skype users dropped from 23.3 million users to around 1.6 million. The outage lasted for two days.

Such outages obviously come with a huge bill for business. This risk, along with the increasing usage of P2P/DHT technology in many applications where fault-tolerance is required, has motivated a line of research that looks into the verification of P2P protocols, and in particular DHT, using formal methods like formal modeling, simulation and model checking. Naturally, the analysis and verification of such large distributed systems is anything but trivial. In fact, due to the size and complexity of such systems, most verification e↵orts have been limited to studying only fragments of these protocols-such as lookups in a static network where nodes do not join or leave-typically using lightweight methods such as modeling and simulation.

This thesis is a work in this line of research that studies the correctness of Pastry using full theorem proving. I verify the correctness of lookups (get requests) for two variants of Pastry by giving a complete proof of correctness using the interactive proof assistant TLA + . It has already been shown in [START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF] that all published versions of Pastry violate this correctness property, since node leaves and failures may cause the network to separate irreversibly, leading to incorrect delivery of lookup messages. In this thesis, I prove that the purejoin model of Pastry is correct w.r.t. delivery of lookup messages. I also show that in the pure-join model, correctness still holds using a node join process that is simpler than the ones proposed for Pastry, for example in [START_REF] Haeberlen | Consistent Key Mapping in Structured Overlays[END_REF][START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF].

In what follows, I discuss some of the relevant literature on the subject of formal verification of P2P protocols. Next, I describe the contribution of this thesis to this research area. This is followed by a brief description of the tools and techniques used in this thesis, in particular the proof assistant TLA + . Finally, I give a short outline of the remainder of this thesis.

Related Work

Chord [START_REF] Stoica | Chord: A Scalable Peer-to-peer Lookup Service for Internet Applications[END_REF] has been one of the most studied DHT implementations in recent years, and operates in a way that is very similar to Pastry. It implements a distributed hash table as follows. A consistent hash function assigns each key and each live Chord node an m-bit identifier (a node's identifier is determined by hashing its IP address, while a key's identifier is determined by hashing the key). The identifier space is arranged as a "circle" called the Chord ring, containing the 2 m possible identifiers ranging from 0 to 2 m 1. A key k is assigned to the first node n whose identifier is equal to or follows that of k on the ring; n is called the successor of k . Each node n maintains a successor list of its successor nodes on the ring, and a finger table for e cient routing, which contains the addresses of up to m nodes at di↵erent "distance classes" from n. In particular, the i th entry is the first node at least 2 i 1 identifiers after n on the ring. Chord nodes employ a periodic "stabilization algorithm" to keep their successor lists and finger tables up to date. Correct lookups can be guaranteed if each node knows its immediate successor on the ring. Due to node failure, however, this may not be the case. The e↵ect of node failure is mitigated by replication, hence the successor lists; the bigger the size r of the successor list, the higher the probability that a lookup request for a key returns the correct node.

Bakhshi et al. describes an abstract model for structured P2P networks with a ring topology in ⇡-calculus, and uses this model to verify the stabilization algorithm of Chord by establishing weak bisimulation between the specification of Chord as a ring network and the implementation of the stabilization algorithm [START_REF] Bakhshi | Verification of Peer-to-Peer Algorithms: A Case Study[END_REF]. This is a pure-join model in which node failure is not taken into account, and features such as finger tables and successor lists are not modeled.

Zave has done a lot of work verifying Chord. Using Alloy to formally model and verify Chord, she shows that the pure-join protocol-i.e. where nodes do not leave the network-is correct, but that the full version of the protocol may not maintain the claimed invariants [START_REF] Zave | Using Lightweight Modeling to Understand Chord[END_REF]. In [START_REF] Zave | How to Make Chord Correct (Using a Stable Base[END_REF], she presents a full version of Chord (where both node joins and leaves are modeled) with a partiallyautomated proof of correctness. The correctness of this version of Chord relies on the assumption that there is a stable base of r + 1 permanent ring members, where r is the size of the successor list.

DKS [START_REF] Onana Alima | A Family of Low Communication, Scalable and Fault-Tolerant Infrastructures for P2P Applications[END_REF] is a distributed hash table implementation, where the name is short for distributed k -ary search. DKS(N , k , f ) describes a P2P protocol for a network of maximum size N , a search arity of k within the network, and a fault-tolerance parameter f . Briefly, distributed k -ary search performs a lookup for any key t in at most log k (N ) hops. Initially, the search space is the entire key space of the hash table. At each step of the distributed search, the current search space is divided into k equal parts, each part being the responsibility of a di↵erent node. This partitioning is repeated until each partition contains only one element, at which point the part containing key t is the lookup target.

DKS can be seen as a generalization of other systems like Chord, Pastry or Tapestry. Like Chord, DKS also has a ring structure, though, according to the authors, this structure is arbitrary and the algorithms provided work for other network topologies as well. The distinguishing feature of DKS is that unlike other protocols, it does not employ an active correction routine for the nodes' routing tables or other local information. Instead, routing tables are corrected on-the-fly while performing lookups and insertions. This idea is based on the observation that, in P2P systems where the number of lookups and insertions is significantly higher than the number of node joins, leaves and failures, correcting routing tables on the fly during lookup and insertion operations saves the unnecessary bandwidth consumption incurred by a periodical correction mechanism.

DKS allows nodes to join and leave the network freely. Like Chord, a node joins a DKS network by sending a join request to its successor on the ring. Joins are "atomic" in the sense that a node i receiving more than one join request at a time has to handle at most one at a time. A node may leave gracefully by informing other nodes of its leaving, or fail abruptly. It is claimed that the system can still provide reliable lookup if no more than f consecutive nodes fail simultaneously.

The authors of DKS conduct some experiments using simulation to observe how lookup e ciency is a↵ected by churn [START_REF] Onana Alima | A Family of Low Communication, Scalable and Fault-Tolerant Infrastructures for P2P Applications[END_REF]. DKS is also described in detail in the Ph.D. thesis of Ghodsi [START_REF] Ghodsi | Distributed K-ary System: Algorithms for Distributed Hash Tables[END_REF]. In this thesis, Ghodsi discusses several issues such as concurrent joins and node failure, and claims that it is impossible to guarantee correctness where node failure is possible, due to the possibility of network separation. Another work on DKS is by Borgström et al., who use CCS for the formal verification of lookups in the static case of the protocol, i.e. without taking node joins or failure into account [START_REF] Borgström | Verifying a Structured Peer-to-Peer Overlay Network: The Static Case[END_REF].

The most relevant work as well as the starting point of this thesis was done by Lu [START_REF] Lu | Model Checking the Pastry Routing Protocol[END_REF][START_REF] Lu | Towards Verification of the Pastry Protocol Using TLA +[END_REF][START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF] on Pastry. Pastry has a ring structure that is very similar to Chord, and employs successor as well as predecessor lists for each node, called the "leaf set" of that node. Instead of Chord's finger table, each node possesses a routing table, whose entries are determined by the length of the common prefix of bits between the entry's ID and the ID of the node. Like Chord, correct delivery of lookup messages can be guaranteed in Pastry if each node has a correct leaf set, or at least correct information about its direct successor/predecessor on the ring, regardless the content of the routing table.

Lu models Pastry in TLA + , and uses the accompanying TLC model checker and the TLAPS proof assistant to formally verify correct delivery of lookup (get) messages: at any point in time, there is at most one node that answers a lookup request for a key, and this node must be the closest live node to that key. As in the case of Chord, Lu discovers several problems in the original Pastry protocol. He also shows that the improvements proposed in later publications on Pastry, as in [START_REF] Haeberlen | Consistent Key Mapping in Structured Overlays[END_REF], still do not guarantee consistency. Finally, he presents a pure-join variant of Pastry, which he calls LuPastry, for which he verifies correct delivery under the strong assumption that nodes never fail. Notably, Lu's Pastry variant also enforces "atomic" joins where a live node may only facilitate the joining of one new node at a time, as in the case of DKS. Lu's proof reduces correct delivery to a set of around 50 claimed invariants, which are proven with the help of TLAPS. As such, LuPastry represents a major e↵ort in the area of computer-aided formal verification of distributed algorithms.

Still, Lu's proof relies on many unproven assumptions relating to arithmetic and to protocol-specific data structures. This is likely due to the sheer size of the proof and the lack of maturity of the TLA + proof assistant at the time. Upon examining Lu's proof, I discovered counterexamples to several of the underlying assumptions. While I was able to prove weaker variants of many assumptions, this was not possible for others. In fact, I was able to find a counterexample to one of Lu's claimed main invariants, for which the TLA + proof was only possible because of incorrect assumptions. This has led me to redesign the overall proof of correctness for LuPastry, and, in the process, improve the TLA + specification of the protocol in many ways.

While working on the new proof, I also realized that the node join process of the protocol can be made significantly simpler without impacting correctness. In particular, the final "lease exchange" step, a handshaking step between a new node and its neighbor nodes before it becomes an active participant, is unnecessary for correctness in the join-only scenario. In fact, this exchanging of leases was not part of the original Pastry protocol published in [START_REF] Rowstron | Pastry: Scalable, Decentralized Object Location and Routing for Large-Scale Peer-to-Peer Systems[END_REF], but introduced by the authors in a later paper, among other improvements to the protocol [START_REF] Haeberlen | Consistent Key Mapping in Structured Overlays[END_REF]. While not explicitly stated, the likely reason behind introducing this additional step was improving the accuracy of the leaf sets and, consequently, the consistency of lookups in the protocol. As Lu shows, however, this lease exchange step does not guarantee lookup consistency; the full dynamic protocol where nodes join and leave freely violates correct delivery of lookup messages, even with the implementation of lease exchange. I observe, on the other hand, that the pure-join model is correct without this step. As a result of this observation, I have formalized a simpler variant of the LuPastry specification where the lease exchange step is omitted, and proven correct delivery of messages for this simpler variant.

Contribution of This Thesis

The contributions of this thesis are as follows.

1. LuPastry + . An improved version of the TLA + specification of LuPastry [START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF]. Aside from fixing bugs, the specification is rewritten in a more modular way using new operators which greatly improve the level of automation in the correctness proof.

2. LuPastry + Correctness Proof. A complete, rigorous proof of correct delivery of lookup messages for LuPastry + in TLA + .

3. Simplified LuPastry + . A variant of LuPastry + with a simpler node join process in which the lease exchange step is omitted.

4. Simplified LuPastry + Correctness Proof. A complete, rigorous proof of correct delivery of lookup messages for Simplified LuPastry + in TLA + . This proof is adapted from the correctness proof for LuPastry + , and represents a success story in proof reuse.

This thesis presents a unique contribution in the following ways. First, it is a study of two dynamic variants of Pastry that is not only limited to the static view of the network, but also allows for nodes to join the network concurrently. Second, the form of verification used here is full theorem proving, instead of less rigorous methods such as simulation or model checking. Third, the proof of correctness for Simplified LuPastry + , which was adapted from the original proof for LuPastry + , presents a unique success story in proof reuse, particularly for such a large proof of over 32,000 proof interactions.

Tools and Techniques

Formal Verification

Formal verification of a (hardware or software) system is the act of checking the correctness of the system-i.e. that the system operates as intended by satisfying a set of specific requirements/properties-using formal methods of mathematics.

There are di↵erent approaches to formal verification that vary in rigor, and accordingly in the time and e↵ort required to apply them. Regardless the approach taken, one has to start with a specification of the system: a model of the system describing its desired behavior, written in the mathematical notation of choice, such as logic, automata, Petri nets, process algebra or set theory [START_REF] Benduhn | A Survey on Modeling Techniques for Formal Behavioral Verification of Software Product Lines[END_REF]. A specification should be as precise, unambiguous, concise and complete as possible. Two approaches of formal verification are relevant to this thesis: model checking and theorem proving.

Model checking. Model checking consists of checking that every possible state the system can reach from its initial state fulfills the desired properties. For finite-state systems, this approach is rigorous. It is also possible to apply model checking on infinite models where infinite sets of states can be e↵ectively represented finitely. In systems with arbitrary size, model checking can be used to verify instances of the system that have a fixed size, which helps find bugs and gain confidence in the correctness of the full system specification, but does not serve as proof. That is, model checking is helpful in proving the presence, rather than the absence, of bugs [START_REF] Beckert | Formal Specification and Verification[END_REF]. Model checking has the advantage of being fully automatic and requiring little interaction from the user. However, a typical problem with model checking is "state explosion", since for many practical systems, the state space is either infinite or increases exponentially with the number of variable parameters of the system [START_REF] Baier | Principles of Model Checking[END_REF].

Theorem proving. Deductive verification is the process of generating a collection of mathematical proof obligations, the truth of which implies the correctness of the system, which are then discharged or proven by a dedicated theorem prover. An automated theorem prover attempts to prove or disprove a given proof obligation in a completely automated manner, without interference from the user. Such provers can be general-purpose provers like Spass [START_REF] Weidenbach | SPASS Version 3.5[END_REF] or Zenon [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF], or SMT (Satisfiability Modulo Theory) provers like CVC4 [START_REF] Barrett | CVC4[END_REF] or Z3 [START_REF] De | Z3: An E cient SMT Solver[END_REF], which handle proof obligations relating to a certain theory such as the theory of arithmetic or set theory. 3 For large systems, an interactive theorem prover, also called a proof assistant, is a software tool that assists a user in writing large proofs, where the individual proof obligations are sent to a back-end automated theorem prover. Applying theorem proving to large systems can be a very lengthy and expensive process, and requires a very deep understanding of the system and many interactions with the proof assistant.

TLA + TLA + is a formal specification language for modeling and verifying distributed systems. In TLA + , one can write a specification of the system, assert properties of the system, and write proofs for these properties.

The specification language is based on Temporal Logic of Action (TLA), a variant of linear-time temporal logic designed by Leslie Lamport in 1994, for specifying system behavior, and untyped Zermelo-Fränkel set theory for describing data structures. Systems are specified as state machines over a tuple of state variables by defining a state predicate Init and a transition predicate Next that constrain the possible initial states and the next-state relation. Transition predicates (also called actions) are first-order formulas that contain unprimed and primed state variables for denoting the values of the variables in the state before and after the transition.

Asserted properties of TLA + specifications are also expressed as logic formulas. These properties can be verified for finite instances of the specification using TLC [START_REF] Yu | Model Checking TLA + Specifications[END_REF], TLA + 's explicit-state model checker. For instances of infinite or arbitrary size, the properties can be proven by writing proofs in the TLA + Proof System TLAPS [START_REF] Cousineau | TLA + Proofs[END_REF], shown in Figure 2.1. TLAPS is based on a hierarchical proof language; the user writes a TLA + proof in the form of a hierarchy of proof steps. Each step is interpreted by the proof manager, which generates corresponding proof obligations and passes them to automatic back-end provers, including Zenon, Isabelle/TLA + , and SMT solvers. Larger steps that cannot be proven directly by any of the back-end provers can be broken further into sub-steps. Because the language is untyped, part of the proof e↵ort consists in proving a typing invariant that expresses the shapes of functions and operators.

TLA + and tools can be used from within the TLA + toolbox. The toolbox is an all-in-one IDE that allows users to write TLA + specifications, run the TLC model checker, and write and verify proofs using the proof manager. The TLA + specification and proof language are briefly explained in Chapter 3.

TLA + Toolbox (IDE)
The TLA + Proof System

Proof Manager

Interpret proofs, compute proof obligations.

Coalesce modal / first-order expressions.

Call back-end provers to attempt proof.

Certify proof (optional, when possible).

SMT Solvers

Zenon Isabelle PTL (ls4)

. . .

Methodology

I prove the safety property "correct delivery" for two di↵erent variants of Pastry. The property states that at any point in time, there is at most one node that answers a lookup request for a key, and this node must be the closest live node to that key [START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF].

For each variant of Pastry, the methodology used for finding the proof is illustrated in Figure 2.2. The variant of Pastry in question is expressed as a TLA + specification, and the property correct delivery is proven by reducing it to a number of inductive invariants of the specification. A property P is an invariant of a given specification if it holds at every initial state of the specification, as well as all states reachable from the initial states. P is an inductive invariant if it holds at every initial state of the specification, and is preserved by all transitions. By this definition, every inductive invariant is an invariant, since properties valid at the initial state(s) and preserved by all transitions are valid at all reachable states.

The most challenging part of the proof process is coming up with the necessary and correct inductive invariants. The process of inferring the needed correctness invariants works as follows. First, I express a property P that seems both useful to the proof of correct delivery and also a correct inductive invariant of the specification. I use model checking to check if there are any counterexamples to this property in a small-size network of e.g. four or eight nodes. If TLC finds counterexamples, then P is not an invariant of the specification and needs to be reformulated accordingly. If no counterexamples are found, there is enough confidence to proceed to the next step of proving P to be an inductive invariant using TLAPS by induction. This process may still reveal counterexamples to P that could not be revealed by model checking, again requiring the property to be revised. If P can be proven as an invariant of the specification using TLAPS, it is added to the list of invariants that can be used to prove correct delivery. The proof of correct delivery itself is a process that runs in parallel to that of creating and modifying invariants; the invariants found are motivated by the proof of correct delivery, and, in turn, shape this proof.

Organization

This thesis is organized as follows. Preliminaries of peer-to-peer networks, distributed hash tables, and the TLA + language are presented in Chapter 3. In Chapter 4, I present LuPastry + and its specification in TLA + . In Chapter 5, I describe the improvements that my new specification LuPastry + introduces to Lu's original specification of LuPastry. I also summarize my analysis of Lu's partial proof of correctness and describe counterexamples I have discovered to some of the assumptions and one claimed invariant in the proof. Finally, I show the structure of my new, complete correctness proof for LuPastry + . The proof itself is described in Chapter 6. In Chapter 7, I present Simplified LuPastry + , in which the lease exchange phase of the node join process is eliminated, and show how I adapt the TLA + proof for LuPastry + into a new proof of correctness for the simplified protocol. Finally, Chapter 8 contains concluding remarks and a discussion of limitations as well as possible future work. In the traditional client/server architecture, which has been the de facto model for internet applications since the early days, a client makes a service request to a designated server, whose task is to receive and fulfill the request. This is a centralized network model where clients and servers are two distinct types of participants, with di↵erent capabilities and responsibilities, as shown in Figure 3.1a; clients are recipients of the service and do not share their own resources with other network participants, and servers are providers of the service and share their resources with the client. A typical example of the client/server architecture is the HyperText Transfer Protocol (HTTP), where the client initiates a request to retrieve a certain web page, and the server responds to the request. In this model, the centralized server holds most of the resources and therefore represents the most important part of the system, as well as the bottleneck.

In contrast to this model, peer-to-peer (P2P) is a decentralized application architecture in which all participant nodes, or peers, are both suppliers and consumers of the given service. Peers are considered to have equal capabilities, and tasks or work loads are distributed among all peers. Each peer makes a portion of its resources directly available to all other peers. Peers communicate with each other without the need for coordination by a central server (see Figure 3.1b). P2P came into popularity through Napster, the file sharing system released in 1999. Since then, it has become the underlying communications model for many internet applications in many domains such as content delivery, file sharing and multimedia streaming.

Participating nodes in a P2P network form a virtual overlay network on top of the physical network. Communication still happens directly over the underlying TCP/IP network, but at the application layer peers communicate directly with each other via logical links. Each "logical" path in the overlay network corresponds to an actual path in the underlying physical network. These logical overlay links make the P2P network independent from the topology of Because they utilize the resources of all peers, P2P networks have the characteristics of decentralized control, self-organization, adaptation and scalability.

However, all P2P networks were not created equal. P2P models can be classified as either pure or hybrid. Pure P2P networks are completely decentralized and server-free, and all nodes are seen as identical in responsibilities and capabilities. Pure P2P models can be further classified as either structured or unstructured. In their early days, pure P2P networks were unstructured. In an unstructured P2P network, there is no structure or topology that is globally imposed upon the di↵erent peers. Because of this lack of network topology, added to the lack of a central server, when a peer issues a search for certain piece of data in the network, the request is "flooded" through the network to find as many peers as possible that have the required data [START_REF] George | Unstructured Peer-to-Peer Networks: Topological Properties and Search Performance[END_REF]. While easy to implement, this lack of structure causes a very high amount of unnecessary network tra c and CPU/memory usage [START_REF] Zhou | On the Performance of P2P Network: An Assortment Method[END_REF][START_REF] George | Unstructured Peer-to-Peer Networks: Topological Properties and Search Performance[END_REF].

This lack of structure caused the trend to shift for a period of time towards a "hybrid" P2P architecture, which is a compromise between the client/server model and the pure P2P model. Hybrid networks are P2P networks that still employ some special servers (sometimes referred to as supernodes) for certain functions, for example to facilitate log-ins (joins), to coordinate part of the node-to-node communication, or to maintain network connectivity. Compared to pure unstructured P2P networks, hybrid models have the advantage in applications where certain functions like search benefit from a centralized structure while other functions benefit from the decentralized aggregation of the resources of all nodes [START_REF] Yang | Comparing Hybrid Peer-to-Peer Systems[END_REF].

A key problem with pure P2P networks, and in particular with large-scale networks, is how to e ciently manage the available resources. To compete with the hybrid model, a structure is needed to e ciently utilize the resources of all peers. This motivated the rise of what is called structured P2P networks. In a structured P2P network, a specific topology is enforced, and the protocol ensures that using this structure, any node can e ciently search the network for a particular piece of data and retrieve it. The most common structure for a structured P2P network is a distributed hash table. Pastry, the focus of this thesis, is a structured P2P protocol that implements a distributed hash table . Other examples include Chord, CAN, Tapestry, Kademlia and DKS, all mentioned in the previous chapter. Structured P2P networks like Chord and CAN have been shown to outperform unstructured P2P networks with respect to search functionality by several orders of magnitude [START_REF] George | Unstructured Peer-to-Peer Networks: Topological Properties and Search Performance[END_REF].

Distributed Hash Tables (DHT)

A distributed hash table (DHT) is a decentralized distributed system that provides a lookup service similar to that of a hash table, but where di↵erent nodes in the system are responsible for storing di↵erent (key, value) pairs (see Figure 3.2). Like a classic hash table, a DHT o↵ers two main functions: put(k , v ) stores the value v at key k , and get(k ) retrieves the value associated with key k . As with a regular hash table, any participating node should be able to e ciently retrieve the value associated with a given key. Most DHT implementations promise a lookup performance of O(log N ), where N is the number of active nodes. Due to the lack of a central server with a global view of the network, nodes in a DHT must collaborate to decide on their respective key storage range, and to route put and get requests to the appropriate node.

Nodes forming a DHT are assigned unique identifiers. These identifiers determine the topology of the network; messages from one node to another are routed through a number of intermediate nodes, the route being determined by node identifiers. Also, nodes determine their respective key storage range based on their own identifiers.

Distributed hash tables have a variety of potential applications. For example, they can be used to implement a distributed file-sharing system, where, instead of all files being stored on one central server, di↵erent files can be stored at di↵erent network nodes depending on the file's hash key. In order to retrieve a certain file, a node sends a lookup/get request with the hash key of the file. The underlying DHT protocol ensures that the lookup message arrives at the node storing the file in question.

From the perspective of this thesis, where correct delivery of messages is concerned, put requests can be seen as get requests where the node receiving the request performs the additional operation of storing a given value at a given key that it manages. Therefore, only lookup/get requests are modeled in the DHT protocols presented here.

Pastry

Pastry was first introduced in [START_REF] Rowstron | Pastry: Scalable, Decentralized Object Location and Routing for Large-Scale Peer-to-Peer Systems[END_REF] as a "completely decentralized, fault-resilient, scalable, and reliable" DHT with good locality properties. Each node in the Pastry network is assigned a unique identifier, which ranges from 0 to 2 128 1. This identifier is assigned randomly when the node joins the network, and it is assumed that the generated identifiers are uniformly distributed across the identifier space. For example, a node's ID may be generated as a cryptographic hash of the node's ID address or its public key. Because of this uniform distribution, nodes with adjacent identifiers are likely to be in di↵erent geographical locations.

As a DHT, the main function of Pastry is to e ciently route a given message with a given key to the node whose ID is numerically closest to that key among all live Pastry nodes. The expected performance of Pastry is O(log N ) routing steps, where N is the number of live Pastry nodes.

The distinguishing feature of Pastry as opposed to other protocols like Chord is that Pastry takes locality into account. It seeks to minimize not only the number of routing steps in the overlay network, but also the distance traveled by the message according to some proximity metric such as the number of IP routing hops. Two applications based on Pastry are the large-scale storage utility PAST [START_REF] Druschel | PAST: A Large-scale, Persistent Peer-to-Peer Storage Utility[END_REF] and the publish/subscribe platform Scribe [START_REF] Castro | Scribe: A Large-scale and Decentralized Application-level Multicast Infrastructure[END_REF].

Node State Each node maintains a routing table, a neighborhood set, and a leaf set. For the purpose of routing, node identifiers can be seen as numbers in base 2 b . The routing table of a node contains entries at various distances away from the node, based on the digits in the node's identifier. In particular, the entry at row r and column c of node i 's routing table should contain a node whose ID shares an r digit prefix with i 's ID, and where the (r + 1) st digit is c. This setup of the routing table achieves logarithmic-time routing in the number of nodes. A node's neighborhood set contains N nodes that are closest to the node in terms of the predefined proximity metric (representing, for example, the geographical location). This set is taken into account during routing to enhance locality. A node's leaf set, on the other hand, contains the 2L nodes with identifiers that are numerically closest to the node's identifier on both the left and right sides of the ring. A typical value for L is 2 b . The leaf set serves as the base case for routing, but its main function is to maintain the structure of the Pastry ring and improve fault-tolerance. The leaf set is the part of the Pastry node state that is most relevant to the correctness proof presented in this thesis.

Node Joins When a new node wishes to join the network, the Pastry algorithm assigns it a random identifier i . It is assumed that the node knows about some Pastry node j . Node i sends a join request to j , and j forwards the request through the network until it reaches the numerically closest node k to i . Each node along the route of the join request message updates its information to include i , and send i a message to "introduce itself", attaching to the message its own state (leaf set, routing table and neighborhood set). When node k receives i 's join request, it responds to it and sends i its own state. Node i builds its own leaf set, neighborhood set and routing table from the information it receives from k and other nodes. Finally, i contacts all nodes in its leaf set, neighborhood set and routing table, sending them a copy of its state. At this point, i is ready to fully participate in the Pastry network and route and receive messages.

Node Leaves/Failure Pastry nodes may fail or leave the network silently, without giving warning to other nodes. A Pastry node is considered failed when its neighbors in the ID space cannot communicate with it. In the event of node failure, the neighboring nodes lazily update their leaf sets as follows. If node i fails, and nodes j and k are its immediate left and right neighbors on the ID ring, then j contacts k and uses k 's right leaf set to repair its own right leaf set, and k uses j 's left leaf set to repair its own left leaf set. This procedure guarantees that nodes eventually repair their leaf sets if no more than L nodes with adjacent identifiers fail at the same time.

Since its introduction, Pastry has been the subject of several publications. In [START_REF] Castro | Exploiting Network Proximity in Peer-to-Peer Overlay Networks[END_REF], the authors of Pastry present a study of its locality properties. They also introduce some refinements to the node join and leave process, but these refinements are mainly concerned with how routing tables are updated while maintaining good locality properties. In [START_REF] Castro | One Ring to Rule Them All: Service Discovery and Binding in Structured Peer-to-Peer Overlay Networks[END_REF], the authors propose a design sketch of bootstrapping a Pastry network. In [START_REF] Castro | Secure Routing for Structured Peer-to-peer Overlay Networks[END_REF], the authors study attacks aimed at preventing correct message delivery in Pastry and similar structured P2P networks, and presents defenses to these attacks, describing techniques for secure node joining, routing table maintenance and message routing in the presence of malicious nodes. In [START_REF] Mahajan | Controlling the Cost of Reliability in Peer-to-Peer Overlays[END_REF], the authors discuss techniques to reduce overhead incurred by the stabilization mechanism, which nodes use to repair their state under continuous joins and leaves.

Lease Exchange

In a 2005 paper, the authors introduce a new leaf set stabilization protocol for Pastry nodes [START_REF] Haeberlen | Consistent Key Mapping in Structured Overlays[END_REF]. In a Pastry network, a node's responsibilities is mostly determined by the portion of the ID space that its ID is numerically closest to. Therefore, consistency in Pastry is determined first and foremost by the reliability of nodes' leaf sets. The authors introduce a new leaf set stabilization protocol that aims to guarantee that, with high probability, only one node considers itself responsible for a given key at any time, despite routing anomalies. Essentially, this is the same property of interest in this thesis.

Briefly, the new leaf set stabilization mechanism relies on the concept of key ownership, which I also denote in this thesis by key coverage, following the convention of Lu in [START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF]. A node may only accept lookup messages and join request messages for a key that it owns or covers. Ideally, a node should cover exactly the set of keys that its ID is numerically closest to among all Pastry nodes. The join process is modified so that at the end of the join process, a node must explicitly agree on its key ownership/coverage range with both its right and left neighbor nodes (according to its leaf set). Each neighbor releases part of its key ownership, and the new node claims it. This takes place by exchanging a series of messages, which are called leases in this thesis. While it is not explicitly stated in the paper exactly which inconsistent behavior this additional lease exchange step was designed to mitigate, it is claimed that using this new mechanism, lookup messages can be guaranteed to arrive at the correct node "with high probability". In his Ph.D. thesis, Lu shows that this lease exchange step does not guarantee correct delivery of lookups in all cases [START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF]. In this thesis, I show that correct delivery of lookups is guaranteed in the pure-join model of Pastry, even without lease exchange.

3.3

The TLA + Language I will illustrate the TLA + specification and proof language first using a concise summary taken from [START_REF] Lamport | A Summary of TLA +[END_REF], and then by aid of an example of a simple specification, taken from Leslie Lamport's "TLA + Hyperbook" [START_REF] Lamport | The TLA + Hyperbook[END_REF] with some slight modifications. The aim here is not to formally describe the TLA + syntax and semantics, but to give an intuitive understanding of the language that is sucient for understanding the TLA + specifications and proof fragments presented in the next chapters. For the interested reader, Merz presents a very clear and compact explanation of TLA + in [START_REF] Merz | The Specification Language TLA +[END_REF]. An in-depth explanation can be found in Lamport's 2002 textbook "Specifying Systems" [START_REF] Lamport | Specifying Systems: The TLA + Language and Tools for Hardware and Software Engineers[END_REF], or the more up-to-date "TLA + Hyperbook" [START_REF] Lamport | The TLA + Hyperbook[END_REF], available online as open-source and continuously being updated by Lamport.

A Summary of TLA +

A TLA + specification consists of three main types of statements: declarations of constant and variable parameters, definitions of functions and operators, and assertions of assumptions and theorems.

Constant parameters are parameters whose values may di↵er from one instance of the system to another, but that have fixed values during the entire execution of one system instance. Variable parameters are parameters whose values may change during system execution. The state of a system is defined by the values of its variable parameters.

Definitions of operators and functions as well as the assertions in the specification are expressed as logical formulas. TLA + distinguishes between two types of formulas: transition (or action) formulas and temporal formulas. Transition formulas describe states and state transitions. Temporal formulas describe behaviors, i.e. infinite sequences of states.

TLA + specifications are organized in modules. A module may incorporate declarations, definitions, assumptions and theorems from other modules M 1 , . . . , M n using the keyword extends.

extends M 1 , . . . , M n

Constants and variables are declared using the keywords constant and variable (alternatively constants and variables).

constants C 1 , . . . , C n variables V 1 , . . . , V m
Properties can be asserted as assumptions using the keyword assumption or the synonymous assume, as axioms using the keyword axiom, or as theorems using the keyword theorem or the synonymous lemma and corollary. Assumptions, axioms and theorems may be given optional identifiers by inserting id = after the keyword. assumption P theorem id = P Functions and operators are defined as follows. F (x 1 , . . . , x n ) = exp defines the operator F with arity n such that F (e 1 , . . . , e n ) equals exp with every occurrence of x i replaced by e i . f [x 1 2 S 1 , . . . , x n 2 S n ] = exp defines a function f with arity n and domain

S 1 ⇥ • • • ⇥ S n , such that f [x 1 , . . . , x n ] = exp for all x 1 2 S 1 , . . . , x n 2 S n . F (x 1 , . . . , x n ) = exp f [x 1 2 S 1 , . . . , x n 2 S n ] = exp
Functions are allowed to have recursive definitions, so the symbol f may occur in the expression exp.

TLA + expressions mainly inherit their syntax and semantics from both Zermelo-Fränkel set theory and first-order logic. In the examples above, I use P to denote expressions of assumptions and theorems, and exp for expressions of function and operator definitions, implying a distinction between logical formulas and general TLA + expressions which may or may not have a boolean type. However, TLA + is based on purely untyped set theory that does not even make a distinction between formulas and terms that exists in first-order logic. In TLA + , every value is a set. The following, for example, is a syntacticallycorrect statement of a lemma in TLA + .

lemma Strange = 3
Attempting to prove this lemma in TLA + , however, would fail using any of the available back-end provers, since basically it is asking to prove that 3 = true, which is not provable (or disprovable) given TLA + semantics.

Figure 3.3 shows the main constant operators of TLA + that are relevant for this thesis, extracted from Lamport's compact summary of TLA + syntax in [START_REF] Lamport | A Summary of TLA +[END_REF]. The first two parts of the table list operators from set theory and first-order logic.

The TLA + keyword choose is Hilbert's choice operator. The TLA + expression choose x : P (x ) (or choose x 2 S : P ) denotes some fixed but arbitrary element x (in the set S ) for which the property P holds, if some such x exists. If there is no such x , as in choose x 2 Nat : x ⇤ 0 = 1, the result of the choose expression is not specified.

The next part in the table describes syntax for functions, tuples and records. A tuple e = he 1 , . . . , e n i is a special kind of function whose domain is {1, . . . , n} for a natural number n, such that e[i ] = e i for i 2 {1, . . . , n}. A string is a tuple of characters where the string "abc" is the same as ha, b, ci. A record is a function whose domain is a finite set of strings. For a record e = [h

TLA + By Example

Consider two jugs, a big jug and a smaller jug. Initially, the two jugs are empty. The following are the possible actions: (1) empty the small jug, (2) empty the big jug, (3) fill the small jug from the faucet, (4) fill the big jug from the faucet, (5) fill the small jug by pouring from the big jug, and (6) fill the big jug by pouring from the small jug. The next two lines declare the constant and variable parameters of the specification. The constants BigCapacity and SmallCapacity denote the maximum capacities of the big and small jug, respectively. The variables big and small denote the amount of water in the big and small jugs at a specific point in time, respectively.

The first definition of the module defines an operator Min, where Min(x , y) returns the minimum of two numbers x and y. This operator will be useful for later definitions in the specification.

The next line defines vars to be the tuple of variables of the specification, vars = hbig, small i. At any point in time, the state of the system is defined by the values of the variables vars. Specifications are defined as state-transition systems, which means we need to define the initial state, and the next-state relation.

The initial state is described by a TLA + formula Init, which states that initially, big = 0 and small = 0. The next six definitions in the module specify the six possible actions of the system. In these formulas, unprimed occurrences of a variable name denote the value of this variable before the transition, and primed occurrences denote its value after the transition. The action FillSmall , for example, sets the next value of small to the maximum capacity of the small jug, keeping the other variable big unchanged. TLA + allows local declarations in the form of let-in statements, as can be seen in the definition of action SmallToBig.

The formula Next describes the next-state relation as a disjunction of all the possible actions. Note that disjunctions and conjunctions can be written in the form of "bulleted lists", where the indentation indicates the nesting level.

As mentioned above, TLA + distinguishes between two types of formulas: transition formulas and temporal formulas. Transition formulas describe states and state transitions, like the definitions of Init, Min, Next and the six action formulas in our example. Temporal formulas describe behaviors, i.e. infinite sequences of states. The system specification in our example is defined by the following temporal formula, using the box symbol as in classic temporal logic to mean "always".

Spec = Init ^2[Next] vars
The formula Spec is a conjunction of the initial state Init and the formula 2[Next] vars , which specifies that every transition either satisfies the action formula Next or leaves vars unchanged. 1Proving in TLA + Let us complete the module in Figure 3.4 with more definitions and a meaningful proof, shown in Figure 3.5. Properties to be verified are also specified in TLA + as logical formulas. The invariant we would like to prove is the type invariant of the specification variables. TypeInvariant = big 2 0 . . BigCapacity ^small 2 0 . . SmallCapacity Since practically nothing can be proven about constant parameters (there are no definitions), we must make assumptions about their types, as in the assumption ConstantTypes. Operators and functions have TLA + definitions from which the types can be inferred, as in the lemma MinType which states the type of the operator Min by expanding its definition (using the keyword def ).

We prove the type invariant by induction. The lemma InitTypeInvariant represents the induction base case, and proves that the type invariant holds initially by definition of the initial state and the type invariant itself. The lemma NextTypeInvariant represents the induction step and states that whenever the type invariant holds immediately before a transition in Next, it will hold immediately after the execution of that transition. The proof of this lemma is more involved, and proceeds by a case distinction on the possible actions in Next (part of the proof has been omitted for compactness). The proof consists of steps, each of which is processed by the proof manager into one or more proof obligations and sent to one or more of the back-end automated theorem provers to solve. It is possible to specify exactly which back-end prover to use on a particular step, as in the last step in the proof of this lemma which is sent to the SMT back-end. A step that is too big for the back-end prover to handle can be broken further into sub-steps; i. Finally, we prove the invariance of TypeInvariant in the specification Spec using the two previous lemmas. This last theorem is proven using the Propositional Temporal Logic prover LS4.

in ^big 0 = big + poured ^small 0 = small poured Next = _ FillSmall _ FillBig _ EmptySmall _ EmptyBig _ SmallToBig _ BigToSmall Spec = Init ^2[Next] vars

Chapter 4

LuPastry + This chapter presents LuPastry + and its specification in TLA + . LuPastry + is based on Lu's specification of Pastry, LuPastry [START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF]. Essentially, LuPastry + is an implementation of LuPastry with improved TLA + definitions of functions and operators and a number of bug fixes. As will be discussed in Chapter 5, the improvements introduced in LuPastry + are not only necessary for a rigorous proof (because of the bug fixes), but also result in a shorter, more modular and more readable proof of correctness.

An Overview of the LuPastry + Model

The Network Ring, Coverage and Leaf Sets In Pastry, the set of possible keys is the interval 0 . . 2 M 1 for some positive integer M . Every live Pastry node is randomly assigned a unique identifier from the same key space-i.e. node identifiers are also keys. The Pastry key space can therefore be visualized as a ring with size 2 M (see Figure 4.1a).

I use the convention that keys increase in a clockwise direction on the ring. I also use the notion of right and left sides of a key: 0 is directly on the left side of 1, while 2 is directly on its right side.

For the implementation of a distributed hash table, live nodes1 need to distribute among them the responsibility for storing (key, value) pairs. Each live node needs to determine its coverage: a contiguous range of keys, including the node's own ID, that the node is responsible for, or covers. If a node i covers key k , then i considers itself (1) the proper recipient of all lookup messages addressed to k , and (2) the node responsible for facilitating the joining of any new node that is assigned ID k . In the absence of a central server and shared memory, live nodes need to rely on message passing and local information to agree on a proper division of coverage.

An ideal distribution of coverage among live nodes is shown in between them (roughly) equally. For example, consider node 11 in the figure.

On one side of the node, there are four keys that lie between it and node 0, which are {12, 13, 14, 15}. Therefore, node 11 should cover the two keys closest to it, {12, 13}, while node 0 should cover the other two keys, {14, 15}. On the other side of node 11, there are three keys between itself and node 7. Because there is an odd number of keys, the tie is arbitrarily (but deterministically) broken in favor of the left side. Therefore, node 7 covers the two keys closest to it, namely {8, 9}, while node 11 covers the key 10. So the coverage of node 11 should be the keys {10, 11, 12, 13}.

A node i determines its coverage by maintaining a leaf set: a set containing what i believes to be its L live neighbor nodes on both the left and right sides, for a positive integer L. The left and right neighbors of a leaf set ls are the closest nodes to the leaf set owner among all leaf set members.

In Figure 4.1b, for example, assuming correct leaf sets and L = 2, the leaf set of node 11 would look like this.

Left

Node Right {4, 7} 11 {0, 4}

The left and right neighbors of node 11 on the ring are nodes 7 and 0, respectively. Note that the left and right parts of the leaf set may overlap, i.e. one node may be in both the right and left leaf sets. Also, in this example, the leaf set is complete or full, i.e. it contains the maximum number of members L on both sides.

Finally, the coverage end-points of a node are computed as the midpoints between the node and its leaf set neighbors, and so the coverage of node 11 in the example would be the interval [START_REF] Castro | Secure Routing for Structured Peer-to-peer Overlay Networks[END_REF][START_REF] Castro | Scribe: A Large-scale and Decentralized Application-level Multicast Infrastructure[END_REF].

Node 10233102 X X X X X X X X X X Prefix Digit 0 1 2 3 0 -0-2212102 1 -2-2301203 -3-1203203 1 0 1-1-301233 1-2-230203 1-3-021022 2

The Routing Table

Theoretically speaking, one could rely completely on the leaf set for the routing of messages among nodes. In order for node i to send a message to some other node j , i would look for j in its leaf set. If i does not find j , it forwards the message to some other leaf set member k 1 on the way to j . Node k 1 , in turn, becomes responsible for routing the message further on, either to j or some other node k 2 along the way, and so on. Because leaf sets only contain the closest few neighbors of a node, routing in this way would take linear time in the number of nodes. While su cient for correct routing, this method is highly ine cient.

Instead, it is possible to achieve logarithmic-time routing if each node maintains a routing table, which contains not only the closest neighbors to it, but nodes at di↵erent "distance classes" away from it. For example, each node i may keep the addresses of nodes that are roughly at distances 2, 4, 8, 16, . . . and so on away from i .

In Pastry, this is implemented as follows. The protocol takes as a parameter a positive number B . All keys on the ring are interpreted as numbers in base 2 B . Note that M has to be divisible by B . And so a key or node ID k will have M ÷ B digits in base 2 B , each digit in the range 0 . . 2 B 1.

The routing table of node i is essentially a matrix, with M ÷ B rows and 2 B columns. The value at row r and column c in the matrix is either NIL if no entry is present, or a node j that has the same r -digit prefix as i , and whose (r + 1) st digit is c.

Routing tables can be illustrated using the following example taken directly from [START_REF] Rowstron | Pastry: Scalable, Decentralized Object Location and Routing for Large-Scale Peer-to-Peer Systems[END_REF]. In this example, M = 16, B = 2 and therefore the base is 2 B = 4. A node ID is read as an 8-digit number in base 4. Shaded cells indicate the corresponding digit in the node's ID. Figure 4.2 shows an example routing table for a node with ID 10233102. Entries at row r have a shared prefix of exactly r digits with the node.

Node Failure

LuPastry + operates under the same assumption of LuPastry that nodes do not fail or leave the network.

Node Join

The node join process is illustrated in Figure 4.3. In LuPastry + , each node is either "Dead" (not shown), "Waiting" (white), "OK" (gray) or "Ready" (black). "Dead" nodes simply refer to keys in the key space that are not assigned as identifiers to some node on the network. Only "Ready" nodes facilitate the joining of new nodes into the network, and based on the join model in the original LuPastry, a "Ready" node may only help at most one new node join the network at a time.

Suppose some "Dead" node i that decides to join the network. It is assumed that node i has the means of obtaining the address of some "Ready" node j , for example through some dedicated server. Node i starts the join process by changing its status to "Waiting" and sending a join request to node j . Node j forwards the join request to the "Ready" node k that covers key i . We denote node k by the node responsible for i .

When node k receives the join request message, and when it is not handling the joining of any other node, it responds to i with a join reply message. Node k attaches its own leaf set and routing table to the join reply message, so that node i can use them to eventually build its own leaf set and routing table.

When node i receives k 's join reply message, containing k 's leaf set, it begins the probing phase: in order for node i to construct its proper leaf set (and routing table), i sends probe messages to the nodes in the leaf set received from k . More accurately, i only sends probe messages to the nodes that are close enough to it on the ring to be contained in its leaf set.

All non-dead nodes that receive the probe from i potentially add i to their leaf set, and respond to i with a probe reply message, attaching their own leaf set. Node i continues to receive probe replies and to probe more newlydiscovered nodes. This process continues until i has probed all nodes it has heard of that are close enough to i to be in i 's leaf set.

When i has received probe replies to all its probes, and no new nodes have been discovered, i finishes probing and changes its status to "OK". "OK" nodes can be viewed as semi-live nodes that have finished constructing their leaf sets and routing tables, but must await confirmation from their leaf set neighbors before becoming fully live, or "Ready". In order for i to become "Ready", i has to exchange leases with both its left and right leaf set neighbors. Note that one of those neighbors must be k , since k is the facilitator of i 's join process and therefore must be closest to i on the ring on either the right or the left side (this is also proven in the correctness proof).

Node i sends out lease request messages to both its leaf set neighbors. If i 's neighbor is "Ready" or "OK", and also considers i to be its neighbor, it grants i the lease in a lease reply message. When i has received lease replies from both its neighbors, it switches to "Ready", and grants its neighbors leases in turn by sending them lease reply messages. When k receives i 's lease reply message, it may help other new nodes join the ring.

Because i is joining through k , k must be Ready, and i and k must be in agreement that they are each other's leaf set neighbors. Therefore, k must grant i 's lease request. Let us assume k is i 's left neighbor, and i is k 's right neighbor, as in Figure 4.3. There is a possibility, however, that i 's other neighbor r does not see i as its left neighbor. Provably, this can only happen if there is another Waiting node u between i and r that has started a join process through r , and has become r 's left leaf set neighbor. In this case, i 's lease request to r is denied, and i cannot turn "Ready"; it must autonomously repeat the lease request again at a later time until it is granted. This scenario is not relevant for the safety property this thesis is interested in verifying. However, under fairness conditions, i will eventually hear from u and update its leaf set to have u as its right leaf set neighbor. Node i will repeat its lease request, this time to u, and u will grant this request. Eventually, i will be able to turn "Ready".

Communication

Communication is modeled as a set of messages that are "in transmission", i.e. pending messages that have been sent from the source node, but not yet received by the destination node. Nodes send messages by adding them to this set, and receive messages by removing them from this set. There is no guarantee as to the order in which sent messages are read by the destination node; the messages are not timestamped and message interleaving is fully allowed. However, as will be seen in the TLA + specification, a node may be prevented from "receiving" a certain message-i.e. removing it from the set of pending messages-until certain preconditions have been fulfilled. For example, a Waiting node may not pick up any probes addressed to it until its leaf set is non-empty. Message loss is simulated by arbitrarily dropping messages from the set of pending messages.

The TLA + Specification of LuPastry +

The complete picture of the TLA + specification of LuPastry + is shown in Figure 4.4. At the very bottom, the specification starts with the declaration of constant parameters. Then, the network ring and the accompanying distance functions are defined, followed by definitions of the necessary data structures or "types", like the leaf set, routing table and messages exchanged between nodes. The dynamic aspect of the specification is described as a state-transition system, where a state is defined by the values of the variables of the specification. The variables are declared, followed by the definition of the initial state, and a next-state relation given by a set of possible actions or events.

Data Structures

The leaf set, routing table, message, and other types.

Ring Description

Distance functions and other arithmetic definitions.

Specification Parameters

Constant Parameters

The LuPastry + specification takes the following constant parameters.

Definition 1 (LuPastry + Constants).

constants A, B , M , L, NIL These constants can be described as follows.

A

The set of nodes that are live in the initial state.

B

Keys are interpreted as numbers in base 2 B . M Decides the size of the Pastry ring 2 M . Keys and node identifiers are in the range 0 . . 2 M 1.

L

The size of the left (right) leaf set of a node.

NIL

Represents an empty slot in the routing table.

Ring Description and Distance Metrics

The ID interval and ring size are defined as follows. 2Definition 2 (Ring Interval and Size).

RingSize = 2 M I = 0 . . (RingSize 1)
Two main distance metrics are used in LuPastry + , the clockwise distance from one node to another, and absolute (shortest) distance between two nodes.

Leaf Sets and Routing Tables

The leaf set data structure is defined as the following set of records. The content of a leaf set ls is the set of all nodes contained in this leaf set, including its owner ls.node. The empty leaf set of a node i is a leaf set whose owner is i and which has no members in the left or right sides.

EmptyLS (i ) = [node 7 ! i , left 7 ! {}, right 7 ! {}]
A new leaf set may be obtained by adding nodes to, or removing nodes from, another leaf set. The two operations are almost identical; the only di↵erence is the pool of nodes from which the new leaf set members are selected. When adding a set of nodes a to a leaf set ls, the selection pool is the original members of ls and the new nodes in a. When removing a set of nodes a from a leaf set ls the selection pool is the original members of ls, excluding those in a. Members of the new leaf set are selected as the (right and left) closest nodes to the leaf set owner ls.node.

Definition 8 (Adding To Leaf Set).

AddToLS (a, ls)

= let i = ls.node C = (ls.right [ ls.left [ a) \ {i } NL = if Cardinality(C )  L then C else choose S 2 subset C : Cardinality(S ) = L ^8 x 2 (C \ S ), y 2 S : ClockwiseDistance(y, i ) < ClockwiseDistance(x , i ) NR = if Cardinality(C )  L then C else choose S 2 subset C : Cardinality(S ) = L ^8 x 2 (C \ S ), y 2 S : ClockwiseDistance(i , y) < ClockwiseDistance(i , x ) in [node 7 ! i , left 7 ! NL, right 7 ! NR]
Definition 9 (Removing From Leaf Set).

RemoveFromLS (a, ls)

= let i = ls.node C = (ls.right [ ls.left) \ ({i } [ a) NL = if Cardinality(C )  L then C else choose S 2 subset C : Cardinality(S ) = L ^8 x 2 (C \ S ), y 2 S : ClockwiseDistance(y, i ) < ClockwiseDistance(x , i ) NR = if Cardinality(C )  L then C else choose S 2 subset C : Cardinality(S ) = L ^8 x 2 (C \ S ), y 2 S : ClockwiseDistance(i , y) < ClockwiseDistance(i , x ) in [node 7 ! i , left 7 ! NL, right 7 ! NR]
Leaf set neighbors of a leaf set ls are defined to be the closest nodes to the leaf set owner ls.node among all leaf set members.

Because the routing table is irrelevant to the correctness proof presented here, most TLA + specifics are omitted for the sake of compactness and clarity. Analogously to the leaf set, the routing table data structure is defined by RoutingTable. EmptyRT denotes the empty routing table (i.e. where all entries are NIL), and RTContent(rt) is the set of nodes in routing table rt, excluding NIL entries. AddToRT (a, rt, i ) defines the operation of adding the set of nodes a to the routing table rt belonging to node i .

The TLA + formula NextHop(i , j ) determines the next node on the path from i to j , based on i 's leaf set and routing tables. If there is no route possible, e.g. if i 's leaf set and routing tables are empty, then NextHop(i , j ) = i . If j is a member of i 's leaf set or routing table, then NextHop(i , j ) = j . Otherwise, NextHop(i , j ) = k for some k 6 = i , k 6 = j such that k is closer to j than i is in terms of absolute distance on the ring.

Messages

Nodes can exchange messages of the following types: (1) a lookup message, "Lookup", (2) a routing error message, "IllegalRoute", (3) a join request, "Join-Request", (4) a join reply, "JoinReply", (5) a probe message, "Probe", (6) a probe reply message, "ProbeReply", (7) a lease request message, "LeaseRequest", and (8) a lease reply message, "LeaseReply". A message in TLA + is defined as a record with a destination and a content. The content of a message contains all relevant information, such as the message type, its sender, or any other attachments like a leaf set or a routing table.

Variable Parameters

The state of a LuPastry + network is represented as the tuple vars of variables.

Definition 14 (LuPastry + Variables).

vars = hMessagePool , Status, LeafSets, RoutingTables, Probing, Leases, Grants, ToJoin, Failed i

MessagePool represents the set of messages currently in transmission. Messages are added to this set by the sending node and removed when they are received by the destination node. Variables Status, LeafSets, and RoutingTables are arrays whose i th entries are the current status, leaf set, and routing table of node i . Similarly, Probing[i ] is the set of nodes that node i has probed but has not heard back from yet, Leases[i ] and Grants[i ] are the set of nodes i has acquired leases from, and granted leases to, respectively. Lastly, ToJoin[i ] designates the node that is currently joining through i , if any, otherwise ToJoin[i ] = i . Lastly, Failed [i ] is the set of nodes that i suspects to have died. Because of the restriction imposed in LuPastry + that nodes do not leave the network, failure recovery is not modeled in the protocol and therefore the set Failed [i ] is always provably empty.

The Initial State

The initial state of the LuPastry + network is given by the formula Init.

Definition 15 (Initial State).

Init = ^MessagePool = {} ^Status = [i 2 I 7 ! if i 2 A then "Ready" else "Dead"] ^ToJoin = [i 2 I 7 ! i ] ^Probing = [i 2 I 7 ! {}] ^Failed = [i 2 I 7 ! {}] ^Leases = [i 2 I 7 ! if i 2 A then A else {i }] ^Grants = [i 2 I 7 ! if i 2 A then A else {i }] ^LeafSets = [i 2 I 7 ! if i 2 A then AddToLS (A, EmptyLS (i )) else EmptyLS (i )] ^RoutingTables = [i 2 I 7 ! if i 2 A then AddToRT (A, EmptyRT , i ) else AddToRT ({i }, EmptyRT , i )]
Initially, there are no messages being exchanged, so MessagePool is empty. The status of each node i is Ready if i belongs to the set A of initially-live nodes. No nodes are in the process of joining, so ToJoin[i ] = i for all i . No node is probing other nodes, and no nodes are suspected as failed. An A-node is assumed to have granted leases to, and obtained leases from, all other Anodes. Also, A-nodes include each other in their leaf sets and routing tables, while Dead nodes have empty leaf sets and routing tables.

The Next-State Relation

The next-state relation defines the possible actions of the protocol and is given by the following TLA + formula Next.

Definition 16 (Next-State Relation).

Next = 9 i , j 2 I : _ Lookup(i , j ) _ RouteLookup(i , j ) _ DeliverLookup(i , j ) _ Join(i , j ) _ RouteJoinRequest(i , j ) _ ReceiveJoinRequest(i ) _ ReceiveJoinReply(i ) _ ReceiveProbe(i ) _ ReceiveProbeReply(i ) _ RequestLease(i ) _ ReceiveLeaseRequest(i ) _ ReceiveLeaseReply(i ) _ LoseMessage
The last action in the formula, LoseMessage models message loss by dropping an arbitrary message from the set MessagePool . This action is not relevant for proving the safety property of interest in this thesis, but is included in the specification since the underlying network is not assumed to be reliable. It can be seen from the definition of Next and the high-level description in Section 4.1 that, with the exception of action LoseMessage, the actions of LuPastry + can be divided into four main categories: lookups, join handling, probing and lease exchange. The next section describes these actions in more detail.

Actions In Detail

Lookups Lookups are modeled using three actions. A lookup message for some key j is issued to any non-dead destination i through the action Lookup(i , j ).

A node i that receives a lookup message for some key j that it does not cover has to forward this message to the closest node k to key j that it can find in its leaf set or routing table (possibly j itself). If no such k is found, an error message is returned. This is modeled in the action RouteLookup.

Of particular relevance to the correctness proof is the action DeliverLookup, where a node i receives a lookup request for a key j that it covers. Note that the actual response to the lookup message is irrelevant to correctness and therefore not modeled in the specification; the lookup message is simply received by i and discarded.

Definition 17 (Action Lookup).

Lookup(i , j ) = let msg = [destination 7 ! i , content 7 ! [type 7 ! "Lookup", node 7 ! j ]] in ^Status[i ] 6 = "Dead" ^i 6 = j ^MessagePool 0 =

Join Handling

The join handling phase of the protocol is modeled in four actions. The first action is Join, where a new node gets assigned the unused identifier j and wishes to join the network. The node changes its status to Waiting, and issues a join request message to some Ready node i . As can be seen in the definition, Join(j , i ) is an action executed by node j , but it refers to the local variable Status[i ] of a di↵erent node i . This is the only place in the specification where this is allowed; it is assumed that j has some means of obtaining the address of some Ready node on the network, for example through the designated server that is also responsible for assigning j its ID.

A node i that receives a join request from a node j that it does not cover has to forward this request to the next node k along the way. This is modeled by the action RouteJoinRequest.

If a Ready node i receives a join request message from a node j that it covers, it can only handle this join request if it is not handling any other join requests at the moment, i.e. if its to-join field is clear. In this case, i handles the join request by setting its to-join field to j , adding j to its leaf set, and responding to j with a join reply message. Node i attaches its leaf set to the join reply message. This is modeled by the action ReceiveJoinRequest.

Finally, in action ReceiveJoinReply, a Waiting node i receives a reply to its join request. Node i adds all content of the attached leaf set to its own leaf set. Note that, in case of an overflow, only the L closest nodes to i from the left and right sides will remain in i 's new leaf set. Node i now enters the probing phase by sending probe messages to those nodes that have been successfully added to its leaf set, i.e. those nodes that are su ciently close to it.

The TLA + expression ProbeSet(i , ls, a, b) is simply a set of probe messages from i to each node in a set of nodes b. Attached to each probe message is the leaf set ls and a set of nodes a suspected by i to be failed nodes.

Definition 20 (Action Join).

Join(j

, i ) = let msg = [destination 7 ! i , content 7
ReceiveJoinReply(i ) = Status[i ] = "Waiting" ^9 m 2 MessagePool : ^m.content.type = "JoinReply" ^m.destination = i ^let nrt = AddToRT (LeafSetContent(m.content.ls) [ RTContent(m.content.rt), RoutingTables[i ], i ) nls = AddToLS (LeafSetContent(m.content.ls), LeafSets[i ]) prb = LeafSetContent(nls) \ {i } msg = ProbeSet(i , nls, {}, prb) in ^RoutingTables 0 = [RoutingTables except ! [i ] = nrt] ^LeafSets 0 = [LeafSets except ! [i ] = nls] ^Probing 0 = [Probing except ! [i ] = prb] ^MessagePool 0 = (MessagePool \ {m})
[ msg ^unchanged hStatus, Leases, Grants, ToJoin, Failed i

Probing

As mentioned above, a node begins the probing phase as soon as it has received its join reply message. A node always attaches its own leaf set to any probe message that it sends out. Nodes that receive a probe message may also start probing new nodes that they discover in the attached leaf set of the message.

Therefore, two main actions describe the probing phase. In the action ReceiveProbe, a node i receives a probe message from a node j . Node i adds j to its leaf set and routing table, and looks in the attached leaf set for new nodes that are potential members of its own leaf set. That is, i looks for nodes that are close enough to it to be in its leaf set, but are not. Node i then sends probe messages to those new nodes.

Action ReceiveProbeReply describes what happens when a node i receives a reply to its probe from node j . Similarly to the action ReceiveProbe, node i adds node j to its leaf set and routing table, and then looks in the message attachment for new nodes to probe. Additionally, node i also removes j from the set of nodes it is probing. Node i then checks to see if it has finished its probing phase. If node i is a Waiting node and there are no more nodes left for i to probe, node i changes its status to OK and starts a new phase, which is the lease exchange phase. Node i sends lease request messages to its left and right leaf set neighbors.

Definition 24 (Action Receive Probe).

ReceiveProbe(i ) = ^Status[i ] = "Ready" _ LeafSets[i ] 6 = EmptyLS (i ) ^9 m 2 MessagePool : ^m.content.type = "Probe" ^m.destination = i ^let j = m.content.node nf = Failed [i ] \ {j } nls1 = AddToLS ({j }, LeafSets[i ]) nls2 = AddToLS ((LeafSetContent(m.content.ls) \ nf ), nls1) pm = LeafSetContent(nls2) prb1 = (LeafSetContent(nls1) \ m.content.failed ) \ {i } prb2 = pm \ LeafSetContent(nls1) prb3 = (prb1 [ prb2) \ (Probing[i ] [ nf [ {j }) cont = [type 7 ! "ProbeReply", node 7 ! i , ls 7 ! LeafSets[i ], failed 7 ! nf ] in ^Failed 0 = [Failed except ! [i ] = nf ] ^RoutingTables 0 = [RoutingTables except ! [i ] = AddToRT ({j }, @, i )] ^LeafSets 0 = [LeafSets except ! [i ] = nls1] ^Probing 0 = [Probing except ! [i ] = @ [ prb3] ^MessagePool 0 = (MessagePool [ {[destination 7 ! j , content 7 ! cont ]} [ ProbeSet(i , nls1, nf , prb3
ReceiveProbeReply(i ) = Status[i ] 6 = "Dead" ^9 m 2 MessagePool : ^m.content.type = "ProbeReply" ^m.destination = i ^let j = m.content.node ls = m.content.ls nf = Failed [i ] \ {j } nls1 = AddToLS ({j }, LeafSets[i ]) nls2 = AddToLS ((LeafSetContent(ls) \ nf ), nls1) pm = LeafSetContent(nls2) prb1 = (LeafSetContent(nls1) \ m.content.failed ) \ (Probing[i ] [ nf [ {i }) prb2 = pm \ (LeafSetContent(nls1) [ Probing[i ] [ nf [ prb1) prb3 = (Probing[i ] [ prb1 [ prb2) \ {j } fin = Status[i ] = "Waiting" ^prb3 = {} msg1 = [destination 7 ! LeftNeighbor (nls1), content 7 ! [type 7 ! "LeaseRequest", node 7 ! i ]] msg2 = [destination 7 ! RightNeighbor (nls2), content 7 ! [type 7 ! "LeaseRequest", node 7 ! i ]] in ^RoutingTables 0 = [RoutingTables except ! [i ] = AddToRT ({j }, @, i )] ^LeafSets 0 = [LeafSets except ! [i ] = nls1] ^Failed 0 = [Failed except ! [i ] = if fin then {} else nf ] ^Probing 0 = [Probing except ! [i ] = prb3] ^Status 0 = [Status except ! [i ] = if fin then "OK" else @] ^MessagePool 0 = (MessagePool [ ProbeSet(i , nls1, nf , prb1) [ ProbeSet(i , nls1, nf , prb2) [ if fin then {msg1, msg2} else {}) \ {m} ^unchanged hLeases, Grants, ToJoini

Lease Exchange

The lease exchange phase begins when a Waiting node i receives the last probe reply message, changes its status to OK, and sends lease request messages to its left and right leaf set neighbors.

A Ready/OK node i that receives a lease request grants the lease only if the request comes from a leaf set neighbor. This is described in the action ReceiveLeaseRequest.

There is a possibility that a node i issues a lease request to its leaf set neighbor j , but by the time the request arrives at j , i is no longer j 's leaf set neighbor. This can happen if a new node k between i and j on the ring starts the join process through node j , becoming its new leaf set neighbor. In this case, j does not grant i 's lease request, and i must autonomously repeat the request at a later time, when it may have updated its leaf set neighbor. This case is handled by the action RequestLease, where a node i autonomously requests a lease from one of its leaf set neighbors.

Finally, a node that receives a lease reply from its neighbor granting it the lease, responds by granting its neighbor a lease in return. If the node has been granted leases from both its neighbors, it switches from OK to Ready. This is described by the action ReceiveLeaseReply.

RequestLease(i ) = let ln = LeftNeighbor (LeafSets[i ]) rn = RightNeighbor (LeafSets[i ]) msg(d ) = [destination 7 ! d , content 7 ! [type 7 ! "LeaseRequest", node 7 ! i ]] in ^Status[i ] = "OK" ^¬(ln 2 Leases[i ] ^rn 2 Leases[i ]) ^MessagePool 0 = MessagePool [ if ln / 2
^Leases 0 = [Leases except ! [i ] = nl ] ^ToJoin 0 = [ToJoin except ! [i ] = if ToJoin[i ] = m.content.ls.node then i else @] ^Status 0 = [Status except ! [i ] = if fin then "Ready" else @] ^Grants 0 = [Grants except ! [i ] = if fin then @ [ {ln, rn} else @] ^MessagePool 0 = if Fin then (MessagePool \ {m})
[ {msg(ln), msg(rn)} else (MessagePool \ {m}) ^unchanged hLeafSets, RoutingTables, Probing, Failed i

As can be seen from the above definitions, a dead node has one capability, which is to turn Waiting and issue a request to join the network. All non-Dead nodes can initiate lookups and route lookup and join request messages. Only Ready nodes handle lookup and join request messages. All non-Dead nodes can exchange probe messages except Waiting nodes that have not received a reply to their join request. Even after finishing the probing phase, a Ready/OK node may still receive probes from other nodes, triggering a new probing phase; these additional probing phases do not a↵ect the Ready/OK status of a node but only the content of its leaf set. Only Ready/OK nodes exchange lease request and reply messages.

This concludes the TLA + specification of LuPastry + . In the next chapter, I present the key di↵erences between LuPastry + and the original specification and proof of LuPastry by Lu.

Chapter 5

Improvements in LuPastry + to LuPastry

LuPastry + is an improved version of the LuPastry specification in TLA + , accompanied with a complete proof of correct delivery of lookup messages. Section 5.1 starts with an analysis of Lu's partial proof of correct delivery for Lu-Pastry, pointing out several counterexamples to assumptions used in Lu's proof, and highlighting the need for the new, complete proof I present in this thesis. In Section 5.2, I describe the changes I introduce to Lu's TLA + specification of LuPastry that make both the specification and the final correctness proof more modular, readable and concise. Finally, Section 5.3 gives an overview of the structure of the new correctness proof. 1. At the bottom-most layer is Lu's TLA + specification of LuPastry.

Lu's Partial Proof of Correct Delivery

2. The Arithmetic and Theory layer consists of a large number of unproven mathematical assumptions, mostly stated as TLA + lemmas where the proof is omitted.

3. The Leaf Set Properties layer consists of a large number of unproven assumptions on the leaf set data structure, which is the main relevant data structure for proving correct delivery. formulated by Lu. The lemmas and theorems in this layer are proven in TLA + , but using the underlying unproven mathematical assumptions in the Arithmetic and Theory layer, as well as unproven assumptions about the leaf set data structure in the Leaf Set Properties layer.

The

5. The Type Lemmas and Invariant layer is concerned with the types of certain TLA + operators, as well as the types of all specification variables in vars which are given by the type invariant. This layer contains both unproven assumptions, and some lemmas proven relying on other unproven assumptions.

6. Finally, the Proof of Invariants layer contains a complete TLA + proof of the 50 claimed invariants of the protocol. Naturally, this layer of the proof relies heavily on the unproven assumptions about the leaf set data structure and ring arithmetic.

The fact that Lu's proof relied on a large number of unproven assumptions is due to the sheer size of the proof, and the lack of maturity of the TLA + proof assistant at that time. For example, a large part of Lu's proof was written before the SMT back-end of TLA + was developed, and therefore it was a sensible decision at the time to make a separation between lemmas about data structures, which often required theory reasoning and remained unproven, and proven invariants relating to the behavior of the system.

I have attempted to prove Lu's unproven assumptions, and found counterexamples to many of them, such as arithmetic assumptions ignoring border cases. Moreover, several assumptions were stated but not actually used later in the proof. My analysis of Lu's proof can be summarized in the following points.

1. Many assumptions in the Arithmetic and Theory layer were not used later in the proof. Also, many assumptions were stated in such a way that made them di cult to prove in TLA + using the available encodings from TLA + to the back-end provers (for example, by relying heavily on the division operator). Some assumptions ignored border cases, which means they had to be reformulated (i.e. weakened). I did not attempt to reformulate and prove all the lemmas in this layer, since it seemed more e cient to start from the top-level proof and go back to prove only as many arithmetic facts as needed. Moreover, as will be discussed in Section 5.2, I have changed some definitions in the LuPastry specification in order to make arithmetic reasoning much simpler, for example, by replacing division by multiplication whenever possible.

2. The Leaf Set Properties layer contains 112 unproven assumptions about the leaf set data structure. Upon examining these assumptions, I could prove only 21 directly. I discovered that 34 assumptions were unneeded later in the proof. The rest of the assumptions were incorrect. I attempted to reformulate and prove all incorrect assumptions in this layer.

For six of the assumptions, it was not possible to find a correct formulation; i.e. the assumption could not be weakened in such a way that would still make it useful for the proof. See Figure 5.2. As will be discussed later, the new, complete proof required a new layer of leaf set lemmas in which I include lemmas from Lu that could be reformulated and proven, as well as many new lemmas that were required in the top-level proof.

3. The theorems in the Reduction to Invariants layer rely heavily on the unproven arithmetic and leaf set assumptions, and reduce correct delivery to a set of 50 claimed invariants by Lu. As I will point out in what follows, I have discovered a counterexample to one of these claimed invariants. Therefore, my conclusion was that a new reduction proof was needed, reducing correct delivery to a set of proven correctness invariants, where both the reduction proof and the proof of the correctness invariants would rely only on proven facts about arithmetic and the leaf set data structure.

4. The Type Lemmas and Invariant layer also contains some unproven assumptions. More importantly, it contains only a few lemmas and is missing lemmas about the types of most operators and functions of the specification. Because TLA + is an untyped language, a significant part of the proof of any TLA + proof obligation is proving types for the TLA + expressions appearing in that obligation. Therefore, a rigorous, complete proof of correctness would require a much more comprehensive layer of type lemmas. Also, this layer would need to appear much earlier in the proof hierarchy, since it is also useful for proving leaf set properties and for the reduction proof.

5. The Proof of Invariants layer is the largest part of Lu's proof, and contains a complete TLA + proof of 50 claimed invariants, based largely on the Similarly, the following assumption states that the leaf set obtained by adding a node k to some leaf set ls, contains the same nodes in ls, and possibly also k . This is not true: if ls is full (complete), then adding a new node k to it will generally result in some other node being removed from the leaf set, invalidating the claimed equality. There is no obvious weaker alternative of this assumption that is useful to the proof.

Counterexample to Claimed Invariant

Using the TLC model checker, I discovered a counterexample to one of the 50 claimed correctness invariants in Lu's proof. 58 m 2 MessagePool : m.content.type = "JoinReply" )

let n = m.content.node in ^ClockwiseDistance(LeftNeighbor (LeafSets[n]), n)  ClockwiseDistance(LeftNeighbor (m.content.ls), n) ^ClockwiseDistance(n, RightNeighbor (LeafSets[n]))  ClockwiseDistance(n, RightNeighbor (m.content.ls))
The formula asserts that if some node n sends a JoinReply message, then n's current neighbors are closer to it than its neighbors were at the time when the message was sent. This is not true, however, if n's leaf set was empty at the time the message was sent. In case of an empty leaf set, the left and right neighbors of node n are n itself. Any new neighbors of n will be farther away from n than n itself.

Improvements to the LuPastry Specification

In analyzing Lu's proof, I was able to gain a better insight into the main complexity bottlenecks.

1. Many proof obligations in Lu's top-level proof are repetitive because they require the same reasoning about integer arithmetic, including division, exponentiation and the modulus operator. Many of these obligations fail due to the inability of the SMT back-end to deal with these obligations.

2. Most of Lu's assumptions about the leaf set data structure could only be proven by strengthening the assumptions to include more information about how leaf set members are distributed within the leaf set (left or right parts).

3. All proof obligations in Lu's proof that contain choose fail due to the lack of necessary lemmas, as I will show in what follows.

Exchanging Division for Multiplication

A small change that greatly simplified the task of proving necessary arithmetic assumptions was changing the definition of RingSize. In the original specification of LuPastry, the size of the Pastry ring was defined as, RingSize = 2 M . Reasoning about shortest (absolute) distance on the ring requires frequent mention to the value RingSize ÷ 2. However, the division operator is a rather di cult operator to reason about, especially given the current TLA + to SMT encoding. In LuPastry + , I define the operator HalfRingSize to denote half the size of the ring. RingSize is then defined as twice HalfRingSize.

HalfRingSize = 2 (M 1) RingSize = 2 ⇤ HalfRingSize
This change eliminates the division operator from many arithmetic assumptions, making them easier to prove automatically using the available SMT back-end.

Isolating Theory Reasoning Using New Operators

I rewrite some TLA + definitions in LuPastry using new operators that abstract away from arithmetic calculations and reduce the use of TLA + 's choose operator, which is di cult for back-end provers to reason about and hence restrains automation.

Arithmetic calculations, which mainly involve comparisons between distances between nodes on the ring, appeared so extensively in LuPastry that arithmetic reasoning was frequently needed at the top level of the original proof. For example, one of the most typical subformulas is the comparison,

ClockwiseDistance(i , j )  ClockwiseDistance(i , k ),
which appears extensively in LuPastry, as in the definitions of RightNeighbor , AddToLS , or Covers (see Definitions 10,8 and 12).

In these definitions, the exact distances between nodes are actually irrelevant; the definitions are only concerned with whether some key j lies on the clockwise path from key i to key k . However, reasoning about each such comparison still requires that the definition of ClockwiseDistance be unfolded.

The standard way of avoiding this problem and simplifying the proof is by renaming the repetitive parts in the definition using new predicates. I have relied on this idea to make the specification of LuPastry more modular, readable, and concise.

In LuPastry + , I introduce a new predicate called ClockwiseArc, where ClockwiseArc(i , j , k ) holds if j lies on the clockwise path from i to k . I replace all expressions of the form ClockwiseDistance(i , j )  ClockwiseDistance(i , k ) in definitions by ClockwiseArc(i , j , k ).

Definition 29 (Clockwise Arc).

ClockwiseArc(i , j , k ) = ClockwiseDistance(i , j )  ClockwiseDistance(i , k )
In the bottom-most Arithmetic and Theory layer of the proof, I then prove once and for all the necessary properties of this relation in TLAPS, using the SMT back-end for arithmetical reasoning. The following are some examples of proven arc properties.

Definition 30 (Examples of Arc Properties).

theorem ArcReflexivity = 8 x , y 2 I : ClockwiseArc(x , y, y) ^ClockwiseArc(x , x , y)

theorem ArcAntiSymmetry = 8 x , y, z 2 I : ^ClockwiseArc(x , y, z ) ^ClockwiseArc(x , z , y) ) y = z ^ClockwiseArc(x , y, z ) ^ClockwiseArc(y, x , z ) ) x = y theorem ArcRotation = 8 x , y, z 2 I : ^x 6 = y ^ClockwiseArc(x , y, z ) ) ClockwiseArc(y, z , x ) ^y 6 = z ^ClockwiseArc(x , y, z ) ) ClockwiseArc(z , x , y)
These theorems are now used heavily in the new proof so that unfolding of the definition of ClockwiseDistance (or ClockwiseArc) is no longer needed. It is clear that this abstraction helps automate the proof process, since now automatic back-ends like Zenon or Spass without native support for integer arithmetic are able to solve larger steps.

Similarly to ClockwiseArc, I define the following predicates for absolute distance. AbsoluteCloser (x , y, z ) holds if y is closer to x than z is, in terms of absolute distance. StrictlyAbsoluteCloser defines the same notion but in the strict sense.

Definition 31 ((Strictly) Absolute Closer).

AbsoluteCloser (x , y, z ) = AbsoluteDistance(y, x )  AbsoluteDistance(z , x ) StrictlyAbsoluteCloser (x , y, z ) = AbsoluteDistance(y, x ) < AbsoluteDistance(z , x )
A related issue is the extensive use of the choose operator of TLA + , which is Hilbert's "-operator for definite choice. As explained in Chapter 3, the TLA + expression choose x 2 S : P (x ) denotes some fixed but arbitrary element x in set S for which the property P holds, if some such x exists. If P holds for no x 2 S , as in choose x 2 Nat : x ⇤ 0 = 1, the result of the choose expression is not specified.

Many LuPastry operators are defined using the choose operator, such as the operator RightNeighbor (see Definition 10). It is unwieldy to reason about operator RightNeighbor by unfolding its definition because we would invariably have to show the existence of a node contained in ls.right, if ls.right is nonempty, whose distance to ls.node is minimal among all these nodes. Formally, we need the following lemma.

lemma ClosestExists = 8 x 2 I , S ✓ I : S 6 = {} ) 9 y 2 S : 8 z 2 S : ClockwiseDistance(x , y)  ClockwiseDistance(x , z )
The proof of this lemma requires induction, and set theory and arithmetic reasoning. Such a lemma does not appear at all in Lu's proof, which is why all proof obligations in Lu's proof that contain choose fail to be proven using any of the available back-end provers.

Therefore, similar to the operator ClockwiseArc, I isolate occurrences of the choose operator by introducing a new set of closeness operators.

Definition 32 (LuPastry + Closeness Operators). The expression ClosestFromTheLeft(x , a) evaluates to the closest node y in the set of nodes a to the node x from the left side. If a is empty, then y = x . ClosestFromTheRight is defined similarly for the right side. The expression ClosestNodesFromTheLeft(x , a, n) evaluates to the n closest nodes in a to x from the left side. If a contains no more than n elements, then the expression evaluates to a. ClosestNodesFromTheRight is defined similarly for the right side. Finally, AbsoluteClosest(x , a) returns the closest node y to x in a, in terms of absolute distance.

ClosestFromTheLeft(x , a) = if a = {} then x else choose y 2 a : 8 z 2 a : ClockwiseArc(z , y, x ) ClosestFromTheRight(x , a) = if a = {} then x else choose y 2 a : 8 z 2 a : ClockwiseArc(x , y, z ) ClosestNodesFromTheLeft(x , a, n) = if Cardinality(a)  n then a else choose sub 2 subset a : ^Cardinality(sub) = n ^8 in 2 sub, out 2 (a \ sub) : ClockwiseArc(out, in, x ) ClosestNodesFromTheRight(x , a, n) = if Cardinality(a)  n then a else choose sub 2 subset a : ^Cardinality(sub) = n ^8 in 2 sub, out 2 (a \ sub) : ClockwiseArc(x , in , out) AbsoluteClosest(x , a)
In LuPastry + , all LuPastry definitions that use choose are rewritten in terms of closeness operators instead, to abstract away from the choose expression. For example, the definition of RightNeighbor in LuPastry + is as follows.

RightNeighbor (ls) = ClosestFromTheRight(ls.node, ls.right)

For each closeness operator (all of which are defined using choose, I prove three lemmas.

1. A choice lemma, which proves the existence of a value satisfying the characteristic predicate of choose.

2. A type lemma, which proves the type of the operator.

3. An expansion lemma, which proves any other relevant properties of the operator, so that they can be used later in the proof without expanding the definition of the operator.

The following would be the choice, type and expansion lemmas for the operator ClosestFromTheRight.

lemma choose ClosestFromTheRight = 8 x 2 I , a 2 subset I : a 6 = {} ) 9 y 2 a : 8 z 2 a : ClockwiseArc(x , y, z ) lemma type ClosestFromTheRight = 8 x 2 I , a 2 subset I : ClosestFromTheRight(x , a) 2 I lemma def ClosestFromTheRight = 8 x 2 I , a 2 subset I : ^a = {} ) ClosestFromTheRight(x , a) = x ^a 6 = {} ) ClosestFromTheRight(x , a) 2 a ^8 y 2 a : ClockwiseArc(x , ClosestFromTheRight (x , a), y)
Of course, type and expansion lemmas are also a useful thing to have for other TLA + expressions. Type lemmas are crucial for all TLA + constants, variables, functions and operators. It is useful to have expansion lemmas for all TLA + functions and operators that occur heavily in the proof, to avoid constantly having to expand their definitions. The following are the type and expansion lemmas for operator RightNeighbor .

Defining Additional Leaf Set Properties

By observing Lu's assumptions on the leaf set data structure, I noticed that most of them require some additional properties that were not defined in Lu-Pastry.

Definition 33 (Balanced Leaf Set). A leaf set is balanced if its left and right parts contain the same number of nodes.

E↵ect of New Abstractions on Proof Automation

While the new operators make the TLA + specification more modular, concise and readable, the most significant gain lies in improving proof automation. Because all arithmetic comparisons and occurrences of the choose operator are grouped into only a few definitions, and with the help of a few lemmas on arc properties as well as choice, type and expansion lemmas, I claim that the final correctness proof is much more concise, and therefore more automated, than it would be without these operators. I illustrate this using a simple lemma about adding new nodes to the leaf set data structure, that I prove once with and once without the use of the new operators. lemma 8 ls 2 LeafSet, a 2 subset I : IsProper (AddToLS (a, ls))

Basically, the lemma says that the leaf set obtained by adding some new nodes to a leaf set is proper.

The proof of this lemma using the original definitions of LuPastry consists of 23 interactive proof steps that generate 64 proof obligations. With the new definitions of LuPastry + , the same proof consists of only 12 interactive proof steps (40 proof obligations). This significant di↵erence comes from the fact that the new operators allow back-end provers to succeed directly on some steps, which would otherwise have to be broken down into further substeps using the original definitions. Already for this simple example there is a 50% reduction in the number of steps, i.e. user interactions.

Other Changes

I introduce some additional changes to the specification that can be summarized as follows.

1. I simplify the definitions of clockwise and absolute distances, which, in turn, simplifies the Arithmetic and Theory layer of the proof. I also eliminate some LuPastry definitions of distance that are unnecessary for the proof. In particular, Lu defined a notion of vector distance or "displacement" from node x to node y; a value that is positive or negative depending on the direction (clockwise or counter-clockwise). Both clockwise and absolute distances were defined in terms of displacement. Instead, I remove the definition of displacement and flatten the definitions of clockwise and absolute distances, as seen in Definitions 3 and 4.

2. I fix some bugs in some of the definitions of the original specification. In particular, definitions relating to message routing and the routing table data structure were not well-defined; they ignored some border cases. This was not discovered by Lu during the proof process, since the proof is partial and is more dependent on the leaf set data structure than the routing process.

3. I modify the probing process so that the node does not attempt to probe itself, which is clearly unnecessary. This simplifies some parts of the proof.

4. Perhaps contrary to convention, I find it more natural to visualize node IDs as increasing in the clockwise direction on the ring, and not vice versa. Therefore, in the new specification, and in the explanation of LuPastry in Chapter 4, the definitions are changed from those of Lu so that the notions of "right" and "left" are reversed.

LuPastry + Proof Structure

I have written a new, complete proof of correct delivery for LuPastry. The new proof is based on the same assumptions as in Lu's original partial proof. Additionally, I impose the assumption that the node leaf set size L is at least three, L 3. The motivation behind this additional assumption is explained in Chapter 6. The structure of the new LuPastry + proof can be seen on the right side of Figure 5.3, in comparison to Lu's partial proof on the left side.

Proof of Invariants

50 Proven Invariants, 14,500 Lines Type Lemmas and Invariant Refined LuPastry Specification At the bottom layer is the new TLA + specification of LuPastry, including the improvements discussed in Section 5.2.

Arithmetic and Theory This is the bottom-most layer of the correctness proof, containing all lemmas on ring arithmetic and set theory. All the necessary properties of the distance and closeness operators are proven in this layer.

Abstraction Lemmas This layer of the proof contains all the necessary type lemmas for all TLA + variables, functions and operators, as well as choice and expansion lemmas, as discussed in Section 5.2. This layer also contains the proof of the overall type invariant of the LuPastry + variables.

Leaf Set Properties This layer contains a large number of proven lemmas about the leaf set data structure. The lemmas in this layer contain the lemmas reformulated from Lu's proof -as discussed in Section 5.1 -as well as many more I have added as necessary to a rigorous top-level proof.

Reduction to Invariants This layer contains the main theorems reducing the property of correct delivery to 80 correctness invariants I have formulated for LuPastry + .

Proof of Invariants This layer contains proofs for the 80 correctness invariants of LuPastry + .

Because the LuPastry + proof is rigorous, there was a need for a larger number of invariants than in Lu's proof. Naturally, there is an overlap between the invariants of LuPastry and those of LuPastry + . However, there is no oneto-one correspondence between the two sets of invariants. In particular, while Lu's original proof of correct delivery relies more on the lease exchange phase of the protocol, my own proof relies completely on the probing process. In fact, in Chapter 7, I adapt the correctness proof of LuPastry + to a simplified specification of LuPastry + , where the lease exchange phase is entirely omitted from the join process.

Currently, TLAPS requires that the enabled predicate be unfolded manually in the machine-checked proof. Therefore, my proof uses this stronger definition of correct delivery. The first occurrence of enabled at the left hand side of the implication is replaced by the preconditions of the action formula DeliverLookup. The second occurrence at the right hand side of the implication is replaced by only one of the preconditions relating to coverage, making the property StrongCorrectDelivery stronger than the original property CorrectDelivery.

Invariant 2 (Strong Correct Delivery).

StrongCorrectDelivery = 8 i , j , k 2 I : ^Status[i ] = "Ready" ^Status[j ] = "Ready" ^j 6 = i ^Covers(LeafSets[i ], k ) ^9 m 2 MessagePool : m.content.type = "Lookup" ^m.content.node = k ^m.destination = i ) ^AbsoluteDistance(i , k )  AbsoluteDistance(j , k ) ^¬Covers(LeafSets[j ], k )
Lu also eliminates the keyword enabled, but by replacing both of its occurrences with preconditions of action DeliverLookup. His partial proof aims at proving the following property which he calls CorrectCoverage. Proof. Assume that StrongCorrectDelivery holds. Consider i , j , k 2 I , where j 6 = i and DeliverLookup(i , k ) is enabled. Because DeliverLookup(i , k ) is enabled, i is Ready. It is required to show that (1) if j is Ready, then j is farther from k than i is in terms of absolute distance, and (2) DeliverLookup(j , k ) is not enabled. The first obligation can be readily discharged by definition of StrongCorrectDelivery. It is left to show that DeliverLookup(j , k ) is not enabled. If j is not Ready, then DeliverLookup(j , k ) is not enabled by definition of DeliverLookup. If j is Ready, then by StrongCorrectDelivery, j 's leaf set does not cover k . Therefore, DeliverLookup(j , k ) is not enabled. Therefore, CorrectDelivery holds. Figure 6.1 shows a more abstract view of the structure of the proof depicted in Figure 5.3b. At the very bottom are a few underlying assumptions and arithmetic axioms, which will be explained in Section 6.2. The middle layer consists of a large number of proven lemmas on arithmetic, set theory, types, the leaf set data structure and coverage among other things, as explained in Chapter 5. The top-level proof reduces (strong) correct delivery to a number of other correctness invariants (right side of the top layer), and proves these invariants with respect to the specification (left side of the top layer). The proof of the invariants alone, without the reduction proof of correct delivery, makes up over 80% of the total proof, and is over 24,000 lines long -it is one and a half times larger than the largest Harry Potter book. Therefore, instead of presenting the proof of the invariants in detail, I will focus on the two most important invariants for the reduction proof: network stability and exclusive coverage. In Section 6.1, I give the intuition behind these properties and how they are proven to be invariants of LuPastry + . In Section 6.2, I list the assumptions and arithmetic axioms that were necessary for the proof. The proof uses only three unproven arithmetic axioms relating to division, exponentiation and the modulus operator which cannot be proven by the current arithmetic back-ends in TLA + . In Section 6.3, I list all the invariants in the proof. 1 Finally, an outline of the reduction proof, reducing strong correct delivery to the correctness invariants, is given in Section 6.4.

Intuition

The idea behind the proof is very intuitive. The main task in proving correct delivery is proving that coverages of di↵erent Ready nodes are mutually exclusive; i.e. that no two Ready nodes i and j cover the same key k .

Proving Exclusive Coverage

Consider two Ready nodes i , j such that i 6 = j . Both i and j compute their coverage ranges with respect to the content of their leaf set. Figure 6.2 shows the di↵erent ways i and j may compute their coverage depending on their leaf sets. It su ces to only consider one side of coverage for each node, e.g. i 's right coverage range with j 's left coverage range. We can guarantee that the coverage ranges of i and j do not overlap if i and j "are aware of each other". Consider Figure 6.2a, for example, where node i 's right leaf set neighbor is k , but j is right-closer to i than k is. Node i is "unaware" of j , since the closest right leaf set member it knows about is farther than j . Node i computes its coverage to end at the midpoint between itself and k , thereby overstepping its boundary and overlapping with what should be j 's coverage range.

Figure 6.2b, on the other hand, shows the situation where i and j are each other's leaf set neighbors. In this case, both i and j compute their coverage ranges with respect to each other, and so the coverages cannot overlap.

Another situation is depicted in Figure 6.2c, where nodes i and j are not each other's leaf set neighbors, but their leaf set neighbors lie between them on the ring. Also in this case the coverages of nodes i and j cannot overlap; the midpoint between i and its right leaf set neighbor is before the midpoint between it and j . Similarly, the midpoint between j 's left leaf set neighbor and j is after the midpoint between i and j . This is another case where i and j are "aware" of each other, even without them being each other's leaf set neighbors.

Finally, it may be that i and j are aware of each other, but there is a node k between i and j that only node i is aware of, as in Figure 6.2d. For example, node k is i 's right leaf set neighbor, but j 's left leaf set neighbor is i , not k . In this case, j 's coverage starts from the midpoint between i and j , but i 's coverage extends only up to the midpoint between itself and k . The coverages of i and j do not overlap, but the coverages of j and k do. Because we want to guarantee non-overlapping coverage for all Ready nodes, this situation is benign only for a non-Ready k .

From these examples, it becomes clear that if each Ready node is aware of its right and left Ready neighbors on the ring, we can show non-overlapping coverage. In fact, I observe that it is possible to show non-overlapping coverage for all Ready and OK nodes. That is, I prove that in LuPastry + , a Ready/OK node always has its Ready/OK neighbors as members of its leaf set, and is therefore "aware" of them. This observation is the motivation behind the Simplified LuPastry + protocol I present in Chapter 7, where I show that correct delivery is still guaranteed even if the lease exchange phase of LuPastry + -which helps a node turn from OK to Ready-is eliminated entirely.

More formally, I define exclusive coverage for Ready/OK nodes as follows.

ExclusiveCoverage = 8 i , j 2 ReadyOKNodes, k 2 I : i 6 = j ^i 6 = k ^j 6 = k ) ¬Covers(LeafSets[i ], k ) _ ¬Covers(LeafSets[j ], k )
Let a node i be stable if its leaf set contains its Ready/OK neighbors on the ring. A LuPastry + network is a stable network if all Ready/OK nodes are stable.

Stable(i ) = ^ClosestFromTheRight(i , ReadyOKNodes \ {i }) 2 LeafSetContent(LeafSets[i ]) ^ClosestFromTheLeft(i , ReadyOKNodes \ {i }) 2 LeafSetContent(LeafSets[i ]) StableNetwork = 8 i 2 ReadyOKNodes : Stable(i )
For example, the ring in Figure 6.3a is stable if nodes 0, 2, 7, 11 are stable.

It is clear that if we show that StableNetwork is an invariant of LuPastry + , we can prove exclusive coverage between all Ready/OK nodes, thereby proving correct delivery.

Proving Network Stability

For a minimum leaf set size L = 3, it can be shown that StableNetwork is an invariant of LuPastry + as follows. First, I make the following (proven) remarks about LuPastry + .

1. Because LuPastry + excludes node failure, all protocol actions that modify a node's leaf set do so through the operation AddToLS , as can be seen from Section 4.2. Therefore, nodes are never purposely removed from a leaf set, but a node j may only be evicted from the leaf set of node i through an AddToLS operation that results in an overflow; i.e., if the leaf set of i becomes full and j is replaced by another node k that is closer to i than j is.

2.

A new node i joins the network through a Ready node r that initially covers it, and so i will remain the closest participating node to r on one side (right or left) until it finishes its join process. Only after i has finished joining and turned Ready can other nodes join the network between r and i . As a result, any Waiting participating node that lies between two Ready/OK neighbors i and j is either the to-join of i or the to-join of j .

3. Let i be a Waiting node, joining through a Ready node r . As soon as r receives i 's join request, i is a member of r 's leaf set. As soon as i receives r 's join reply, r is a member of i 's leaf set.

4. Let i and j be two consecutive Ready or OK nodes on the ring (see Figure 6.3b). There can be at most two participating nodes k 1 , k 2 between i and j : the to-join nodes of i and j . Any other non-Dead node between i and j must be a Waiting node whose join request has not been picked up by i or j (since they are busy facilitating the joins of k 1 and k 2 ). Therefore, any Ready/OK node cannot be separated from the Ready/OK node closest to it by more than two nodes.

5. If the leaf set size is three or more, we can ensure that stable i and j remain stable even if new nodes are added to their leaf sets.

From the previous remarks, it is clear that a stable node cannot be destabilized simply by adding new members to its leaf set, since the leaf set is always large enough to accommodate a node's Ready/OK neighbor. Therefore, the main task of proving network stability is to show that as soon as a node turns OK, it is stable, and by turning OK, does not destabilize any previously-stable Ready/OK nodes. This is the most involved and lengthy part of the proof of network stability. A node turns OK as soon as it has finished the probing process and received replies to all its outgoing probes. Let i be a Waiting node in the probing phase joining through some Ready node r , and let j be i 's Ready/OK neighbor at the time i turns OK. If we can prove that i has exchanged probes with j before it turned OK, then we can show that at the time when i turns OK, it is stable, and other Ready/OK nodes are aware of it and so remain stable.

There are three di↵erent possibilities for the relationship between node j and node i .

Case 1 Node j is the node responsible for i 's joining, j = r . In this case, it is guaranteed that j and i are members of each other's leaf sets. Therefore, i is stable when it turns OK, and previously-stable j is still stable when i turns OK.

Case 2 Node j was already a member of r 's leaf set when r responded to i 's join request. This means that j was in the leaf set which r attached to i in its join reply message. Therefore, i has issued a probe to j and cannot turn OK before it has received a probe reply from j . Therefore, i and j must have exchanged probes before i turned OK.

Case 3 Node j was not a member of r 's leaf set when r responded to i 's join request. Because r is a stable Ready node, it must be that j was Dead/Waiting. If j were Ready/OK, it would be a Ready/OK neighbor of r and a member of r 's leaf set. Therefore, j was a Dead/Waiting node at the time r responded to i 's join request, and not a member of r 's leaf set. It turned Ready/OK while i was in the probing phase. Let r 2 be the Ready node responsible for j 's joining. When j was Dead/Waiting, r and r 2 were each other's Ready/OK neighbors2 , and therefore, r 2 was in the leaf set attached to i 's join reply message. Therefore, it must be that i has probed and received a reply from r 2 before turning OK. There are two possibilities. responded to j 's join request. This means that i was in the leaf set that r 2 attached to j 's join reply. This means that j could not have turned OK before probing and receiving a reply from i .

Case 3b Node j 's join request reached r 2 before i 's probe did. In this case, j was already in r 2 's leaf set, which r 2 attached to the probe reply to i . Therefore, i could not have turned OK before probing and receiving a probe reply from j . This informal proof of correct delivery is a behavioral-style proof, which focuses mainly on events from a local point of view of a node, and the possible histories of execution leading up to these events. In contrast, the formal TLA + proof of correct delivery is an assertional-style or invariant-inductive proof, which focuses on global states and uses induction to prove a set of properties to be invariants, i.e. true at every reachable state of the system. Nevertheless, the behavioral argument presented above shows the motivation behind the invariants chosen for the proof and listed in Section 6.3.

Assumptions and Arithmetic Axioms

The starting point of the proof are assumptions that have to be made about the specification parameters. The proof relies on the following assumptions. In addition, the following are arithmetic facts that cannot be proven by any of the current back-ends in TLA + , and therefore have to be stated as TLA + axioms without proofs. These are axioms relating to the exponentiation, division and modulus operator respectively. Axiom 1. (Exponentiation Properties)

8 a, b 2 Int : ^a 6 = 0 ) a 1 = a ^a 6 = 0 ) 8 m, n 2 Int : a (m+n) = a m + a n ^b 6 = 0 ) 0 b = 0 ^0 < a ^0 < b ) 8 c 2 Int : a (b⇤c) = (a b ) c ^0 < a ^0 < b ) 8 c 2 Int : b  c ) a b  a c
Axiom 2. (Whole Integer Division) 8 x , y, q 2 Nat : 0 < y ^x = q ⇤ y ) q = x ÷ y Axiom 3. (Modulus Properties) 8 x , y 2 Nat : 0 < y ^x y ) (x %y) = (x y)%y

Correctness Invariants

This section contains a list of the proven correctness invariants of LuPastry + . In Section 6.4, it is proved that strong correct delivery follows from these correctness invariants. I denote by CorrectnessInvariants the TLA + conjunction of all the correctness invariants listed here.

The TLA + proof files reduce correct delivery to 80 correctness invariants. In this presentation, however, many of these invariants have been clustered together or formulated in a more compact way for readability, resulting in fewer formulas in total. In the TLA + files, it is sometimes much easier to prove a large number of small formulas than a smaller number of larger formulas. This is particularly true for Pastry, because of the symmetry between the "left" and "right" components of the proof. Many invariants consist of a right and left component; for example, the same invariant may need to be proven for both the right and left Ready/OK neighbor of a node. These two components are easier to prove separately in TLA + , since the proof for one side is simpler, and can later be directly reused for the other side. Here, I group right and left components of the same property in one big formula.

To relate this list of invariants to the intuitive proof discussed in Section 6.1 and make the presentation more meaningful, the invariants can be (very roughly) grouped into the following categories: basic invariants, invariants relating to the joining and probing phases, and invariants relating to coverage and stability.

Basic Invariants

These invariants refer to types and some elementary properties of the variables, the possible relationship between the values of di↵erent variables, or properties of the exchanged messages between nodes. For example, we need to show that any node that has a to-join node other than itself is a Ready node, that a node does not send duplicate messages to the same recipient, or that the sender of a lease reply message is always a Ready/OK node. This group of invariants can be seen as the beginning of the invariant food chain, being straight-forward to prove and heavily used in the proof of the more complex invariants.

[i ] = EmptyLS (i ) ^Probing[i ] = {} ^8 i 2 ReadyNodes : LeafSets[i ] = EmptyLS (i ) ) ReadyNodes = {i } Invariant 34.
If there is a pending probe reply message from node i to node j , then either j is a member i 's leaf set, or i 's leaf set is full with closer members than j . The Join-Probe Relation

These invariants are concerned with the relationship between a joining node and its neighbors, which is necessary to prove the stability of this joining node once it has finished joining. In particular, the aim of these invariants is to show that a Waiting node i does not turn OK before probing node j , its Ready/OK neighbor at the time it turns OK. This is done by analyzing the di↵erent possible orderings of events that led up to i and j being both Ready/OK, in a manner that corresponds to the discussion in Section 6.1.

These invariants represent, by far, the most challenging part of the proof, being the most di cult to come up with and to prove. Invariant 35. Let i and j be two participating nodes, where j is a joining node that has not yet received its join reply message. If j is a member of i 's leaf set, then either j is joining through i , or i is probing j . Invariant 36. Let m be a pending join reply message from r to i . Then the leaf set attached to m contains the Ready/OK neighbors of both r and i . Moreover, any node j in the leaf set attached to m that lies between i and its Ready/OK neighbor is the to-join node of that neighbor.

)} ^i = ToJoin[r ] ^ToJoin[k ] 6 = k ^ToJoin[k ] 6 = i ^ToJoin[k ] / 2 ReadyOKNodes ) _ LeafSets[ToJoin[k ]] = EmptyLS (ToJoin[k ]) _ LeafSets[i ] = EmptyLS (i ) _ ToJoin[k ] 2 Probing[i ] _ i 2 Probing[ToJoin[k ]] _ r 2 Probing[ToJoin[k ]] _ ToJoin[k ] 2 LeafSetContent(LeafSets[i ])
Invariant 38. Suppose there is a pending join reply message to some node x , and a pending probe reply message to some node y, both messages from the same node r (note that r must be a Ready node by Invariant 12). Then one of the following must hold: [START_REF] Onana Alima | A Family of Low Communication, Scalable and Fault-Tolerant Infrastructures for P2P Applications[END_REF] x is in the leaf set attached to the message to y, (2) y is in the leaf set attached to the message to x , (3) y is not in r 's leaf set, and the leaf set of r is full with closer nodes to it than y.

ClosestFromTheLeft(i , ReadyOKNodes \ {i })} : ToJoin[r ] / 2 (LeafSetContent(LeafSets[i ]) [ ReadyOKNodes) ) LeafSets[ToJoin[r ]] = EmptyLS (ToJoin[r ]) _ i 2 Probing[ToJoin[r ]]
Invariant 40. Let m be a pending join reply from r to i . Let n be i 's right or left participating neighbor. Then if n is not Ready/OK, one of the following must hold: (1) n is in the leaf set attached to m, (2) n's leaf set is empty; that is, n has not yet received its own join reply or begun the probing phase, (3) n is probing i , (4) n is probing r . Invariant 41. Let i be a non-Ready/OK node joining through a Ready node r . Let k be another non-Ready/OK node joining through one of r 's Ready neighbors n (here the right or left Ready/OK neighbor). If i is a member of k 's leaf set, then one of the following must hold: (1) i is probing k , (2) k is probing i , (3) k is a member of i 's leaf set.

8 i 2 ParticipatingNodes \ ReadyOKNodes, r 2 ReadyNodes : 8 n 2 {ClosestFromTheRight(r , ReadyOKNodes \ {r }), ClosestFromTheLeft(r , ReadyOKNodes \ {r })} ^ToJoin[n] 6 = n ^ToJoin[n] 6 = i ^ToJoin[n] / 2 ReadyOKNodes ^i = ToJoin[r ] ^i 2 LeafSetContent(LeafSets[ToJoin[n]]) ) _ ToJoin[n] 2 Probing[i ] _ i 2 Probing[ToJoin[n]] _ ToJoin[n] 2 LeafSetContent(LeafSets[i ])
Invariant 44. Let i be a non-Ready/OK node and r its left or right Ready/OK neighbor. Then either i 's leaf set is empty; that is i has not yet received its join reply message or begun the probing phase, r is a member of i 's leaf set, or i is probing r .

8 i 2 ParticipatingNodes \ ReadyOKNodes : 8 r 2 {ClosestFromTheRight(i , ReadyOKNodes), ClosestFromTheLeft(i , ReadyOKNodes)} : _ LeafSets[i ] = EmptyLS (i ) _ r 2 LeafSetContent(LeafSets[i ]) _ r 2 Probing[i ]
Invariant 45. Let i be a non-Ready/OK node and r its left or right Ready/OK neighbor. Then either i 's leaf set is empty; that is i has not yet received its join reply message or begun the probing phase, i is a member of r 's leaf set, or i is probing r .

8 i 2 ParticipatingNodes \ ReadyOKNodes : 8 r 2 {ClosestFromTheRight(i , ReadyOKNodes), ClosestFromTheLeft(i , ReadyOKNodes)} : _ LeafSets[i ] = EmptyLS (i ) _ r 2 Probing[i ] _ i 2 LeafSetContent(LeafSets[r ])

Coverage and Stability

Finally, the following invariants relate to exclusive coverage between di↵erent Ready/OK nodes and are the main invariants used to prove correct delivery. The proof of these invariants and the join/probe invariants of the previous section are heavily inter-dependent. The di culty in proving these invariants lies in the rather involved arithmetic reasoning on coverage. Invariant 46. A Ready node i does not cover a non-Ready/OK k that is the to-join node of (1) itself, (2) its leaf set neighbor, (3) any node j that has granted i a lease, and (4) any node j that i has probed and from which there is a pending probe reply message to i . Proof. By definition of coverage and the leaf set properties "proper", "balanced" and "organized".

8 i , j 2 ReadyNodes : ^_ j = i _ j 2 Leases[i ] _ j = LeftNeighbor (LeafSets[i ]) _ j = RightNeighbor (LeafSets[i ]) _ 9 m 2 MessagePool : ^m.content.type = "ProbeReply" ^m.content.node = j ^m.destination = i ^ToJoin[j ] / 2
Lemma 2. In a stable network where the leaf set invariants hold, the leaf set of a Ready/OK node i does not cover any other Ready/OK node j .

StableNetwork ^LeafSetInvariants ) 8 i , j 2 ReadyOKNodes : i 6 = j ) ¬Covers(LeafSets[i ], j )

Proof. For the sake of contradiction, let i and j be Ready/OK nodes where i 6 = j and i 's leaf set covers j . Let l , r be the closest Ready/OK nodes to i from the left and right, respectively. By Lemma 1, j is not a member of i 's leaf set. Because the network is stable, this means that j 6 = l and j 6 = r . This means that j is separated from i by leaf set members l and r on both sides. We can safely assume that i 6 = j , since for i = j it is trivial to conclude that (1) i is closer to i than k is (the distance between a node and itself is zero), and (2) k does not cover i , by Lemma 2. Similarly, we also know that j 6 = k , since i covers j but cannot cover k , also by Lemma 2.

That ls k does not cover j now follows directly from Invariant 48, which says that no two Ready/OK nodes can cover the same key. It is left to show that

D i  D k .
Without loss of generality, we can assume that j is right-covered by i (the proof works similarly for the left side). The situation is shown in Figure 6.4. Note that k and RN i may be the same node, but the figure shows the general case where k is a node after RN i on the clockwise direction from i .

By definition of coverage, the clockwise distance from i to j is no more than half the distance from i to its right neighbor RN i ,

ClockwiseDistance(i , j )  ClockwiseDistance(i , RN i ) ÷ 2.
From this, it can also be deduced,

ClockwiseDistance(i , j )  ClockwiseDistance(j , RN i ) ClockwiseDistance(i , j )  RingSize ÷ 2
Therefore, it must be that D i = ClockwiseDistance(i , j ). That is, the shortest distance between i and j is the clockwise distance from i to j .

The absolute/shortest distance D k between j and k can be either the clockwise distance from k to j , or the clockwise distance from j to k . Assume that D k = ClockwiseDistance(k , j ). This means that the shortest path between k and j passes through i . In this case, In both cases, we reach the conclusion that D i  D k .

D k = ClockwiseDistance(k , i ) + D i D k > D i On the other hand, if D k = ClockwiseDistance(j , k ), then, D k = ClockwiseDistance(j , k ) = ClockwiseDistance(j , RN i ) + ClockwiseDistance(RN i , k ) ClockwiseDistance(i , j ) + ClockwiseDistance(RN i , k ) ClockwiseDistance(i , j ) D k D i i RN i k j
With the TLA + proof summarized in this chapter, I establish the following. Given a leaf set size of at least three, the LuPastry + network is always stable; that is, every Ready/OK node always knows its true left and right Ready/OK neighbors on the ring. As a consequence, the coverage regions of Ready/OK nodes do not overlap. It is therefore guaranteed that for any lookup request for some key k , at most one Ready node i receives this request, and this node i is (1) the node with the closest ID to key k in terms of shortest distance on the ring, and (2) the only Ready node that covers key k .

In the next chapter, I present a simplified join process for LuPastry + , and show how the proof presented here can be adapted to prove correct delivery for the simplified version of the protocol.

Chapter 7

Simplified LuPastry + By examining the proof of correctness of LuPastry + presented in Chapter 6, it becomes clear that the lease exchange phase of the join process does not play a role in preserving the invariance of correct delivery. In this chapter, I show that this lease exchange phase is, in fact, unnecessary for achieving correct delivery and can be omitted. I present a modified version of LuPastry + , which I denote by Simplified LuPastry + , where a Waiting node directly turns Ready after finishing the probing process, without exchanging leases with its leaf set neighbors. I also show how the TLA + proof of correct delivery in Chapter 6 is adapted for the simplified specification, thereby obtaining a new, complete proof of correct delivery for Simplified LuPastry + .

A Simplified Join Process for LuPastry +

The main di↵erence in Simplified LuPastry + to the original specification of LuPastry + is a simpler join process, shown in Figure 7 The simplified process starts in the same manner as the original one-a Dead node i that wishes to join the network issues a join request, which is eventually forwarded to the Ready node k that covers key i . If k is not currently facilitating the join of any other node, it responds to i 's join request, attaching its own leaf set. Node i receives k 's reply and begins the probing phase.

The key di↵erence is introduced at the point when i has finished the probing phase. In Simplified LuPastry + , as soon as i has finished the probing phase, it directly changes its status to Ready, instead of OK. Compared to the state variables of LuPastry + in Definition 14, the original LuPastry + variables Leases and Grants were omitted, since nodes do not exchange leases. Instead, a new variable Responsible is added, where Responsible[i ] is the Ready node, if any, that is currently helping or has helped i join the network. 1 If i is a non-participating or an initially Ready node, Responsible[i ] = i . There is a need for this new variable in Simplified LuPastry + so that a joining node i notifies its responsible node as soon as it has turned Ready. In the original LuPastry + , this notification was done implicitly through the process of lease exchange: the responsible node k for i is always one of i 's leaf set neighbors, and by exchanging leases with i , k is notified that i has finished its join process.

The new type invariant is given by the following formula.

Invariant 50 (Simplified LuPastry + Type Invariant). Because nodes never have the status "OK" in Simplified LuPastry + , it is always the case that OKNodes = {}, and therefore ReadyOKNodes = ReadyNodes. In the TLA + files, I simply omit the definitions of OKNodes and ReadyOKNodes, and replace all references to ReadyOKNodes with ReadyNodes. For the scope of this chapter, ReadyOKNodes and ReadyNodes are interchangeable.

The initial state of Simplified LuPastry + is modified from the original Definition 15 to accommodate the change in variables. The actions Lookup, RouteLookup, DeliverLookup, Join, RouteJoinRequest, ReceiveJoinRequest, ReceiveProbe and LoseMessage had no e↵ect on the variables Leases and Grants in the original specification. Therefore, they are defined in the same way in Simplified LuPastry + , aside from replacing the postconditions unchanged Leases and unchanged Grants by the post-condition unchanged Responsible.

The action ReceiveJoinReply also had no e↵ect on the variables Leases and Grants in the original specification. However, on receiving a join reply, a node must set its Responsible variable to the sender of the join reply message. Therefore, in the new action formula, the post-conditions unchanged Leases and unchanged Grants are removed, and the variable Responsible is updated as follows. This concludes the list of changes to the specification of LuPastry + . In what follows, I describe the similar changes that had to be made to the proof to adapt it to the simplified specification.

Correct Delivery in Simplified LuPastry +

Adapting the proof of correct delivery for the original LuPastry + specification to the simplified version is straight-forward. In fact, the proof described in Chapter 6 focuses mainly on the probing process and proves properties relating to the set of Ready/OK nodes as a whole, instead of just the set of Ready nodes.

In Chapter 6, I show that the set of Ready/OK nodes in a LuPastry + network is always stable, since every Waiting node must probe or be probed by its left and right Ready/OK neighbor before it turns OK. That is, the probing phase already establishes (and maintains) stability for both Ready and OK nodes.

Eliminating the lease exchange phase and the intermediate OK status in Simplified LuPastry + e↵ectively reduces the set of Ready/OK nodes to the set of Ready nodes. Therefore, we can show that the set of Ready nodes are always stable in Simplified LuPastry + , due to the probing phase.

Since exclusive coverage and correct delivery follow from stability, as shown in the reduction proof of Section 6.4, it is straight-forward to prove (strong) correct delivery for Simplified LuPastry + . The property proven is the same as in Definition 2 in the previous chapter. Adapting the TLA + proof required the following steps.

1. Removing invariants. Invariants relating to the lease exchange phase were no longer needed and therefore eliminated. These are invariants relating to either exchanged lease request and reply messages, or the variables Leases and Grants, like Invariant 9, which says that for any node i , all nodes in the set Leases[i ] are Ready/OK. Since the proof of other invariants is mostly independent from invariants on lease exchange, this step did not cause any significant disturbance to the flow of the overall proof.

2. Modifying invariants. The proof of the remaining invariants had to be adjusted for the new next-state relation. Induction steps for the eliminated actions RequestLease, ReceiveLeaseRequest and ReceiveLeaseReply were removed. For the new action ReceiveNotification, one induction step is added.

3. Adding invariants. A few very simple invariants were added as necessary, to prove some properties about the new variable Responsible, such as Invariant 51 below.

Invariant 51. Let i be a to-join node that is not Ready. If i 's leaf set is not empty, then i 's Responsible field is not set to itself. In summary, it was possible to adapt the TLA + specification of LuPastry + described in Chapter 4 to have a simpler join process, and prove correct delivery for this join process by introducing only a small number of changes to the proof presented in Chapter 6.

Chapter 8 Conclusion

This thesis is concerned with the formal verification of Pastry, a popular implementation of a Distributed Hash Table (DHT). A DHT is a peer-to-peer network that acts as a hash table where di↵erent key-value pairs are stored at di↵erent nodes on the network. Pastry nodes are randomly assigned identifiers from the key space of the hash table. Each node is responsible for managing the portion of the key space numerically closest to its identifier. Like a classic hash table, the main function provided by Pastry is key lookup: a node may issue a lookup request for a certain key, and the request is routed to the Pastry node that manages this key. Pastry is a dynamic network where nodes may join the network at any time by following the join protocol, and leave/fail spontaneously without giving notice to other nodes.

The work presented here is a continuation of Tianxiang Lu's work on verifying the correct delivery of lookup requests in Pastry. Lu defines "correct delivery" as follows: "at any point in time, there is at most one node that answers a lookup request for a key, and this node must be the closest live node to that key." He shows that the full published version of Pastry violates correct delivery, and presents LuPastry, a pure-join variant of Pastry where node failure is not modeled and where a live node on the network may help at most one other node join the network at a time. Lu also gives a partial proof of correct delivery for LuPastry, mechanized in the TLA + proof assistant.

Upon examining Lu's proof, I found that it is based on a large number of unproven assumptions. This is likely due to the sheer size of the proof (over 10,000 lines) and the lack of maturity of the TLA + proof assistant at the time. In attempting to prove these assumptions, I found counterexamples to many of them, such as arithmetic assumptions or assumptions about protocol data structures that ignoring border cases. As a consequence, I was able to find a counterexample to one of Lu's claimed invariants of LuPastry which he uses to prove correct delivery. These discoveries highlighted the need for a new and complete proof of correct delivery in LuPastry.

The contribution of this thesis is manyfold.

1. I present LuPastry + , a TLA + specification based on Lu's specification of 113 LuPastry, which introduces a number of bug fixes and improvements to the definitions of some operators. The improvements make the specification more readable and modular, and significantly improve the automation of the correctness proof.

2. I present a complete proof of correct delivery of lookup requests for LuPastry + in TLA + .

3. I observe that the final step of the node join process of LuPastry/LuPastry + , denoted by the "lease exchange" step, is in fact unnecessary for correct delivery. I present a simplified version of LuPastry + where the lease exchange step is eliminated. I denote the simplified specification by Simplified LuPastry + .

4. I present a complete proof of correct delivery of lookup requests for Simplified LuPastry + in TLA + . This proof is adapted from the TLA + proof for LuPastry + , by introducing the necessary changes.

The lease exchange phase eliminated in Simplified LuPastry + was, in fact, not published as part of the original specification of Pastry, but in a later paper by the authors [START_REF] Haeberlen | Consistent Key Mapping in Structured Overlays[END_REF]. It was included by Lu in his specification of LuPastry in his attempt to devise a variant of Pastry for which correct delivery can be proven [START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF]. Lu shows that in the full specification of Pastry where node failure is modeled, the lease exchange phase does not prevent the protocol from violating the correctness property, since network separation is still possible if too many nodes fail within a small period of time. The proof presented here shows that, in fact, this phase of the join process is not necessary for correctness in the pure-join model.

Aside from the necessary technical di↵erences, both proofs presented here have the same basic idea, and are comparable in size w.r.t. the number of interactive proof steps and the number of invariants proven. Each proof consists of over 32,000 lines. To my knowledge, both Lu's partial proof and the two proofs presented here represent the only two works that employ full theorem proving for formal verification of a DHT protocol, and the proofs presented here may well be the largest proof examples written using the TLA + proof assistant.

Experience and Challenges

Since both TLA + specifications of LuPastry + and Simplified LuPastry + are based on Lu's TLA + specification of LuPastry, I was spared the initial task of creating a specification from scratch, with the challenges that this task entails, such as determining the right level of abstraction, designing the data structures, and resolving ambiguities in the informal specifications found in the literature. In fact, my starting point was analyzing Lu's partial proof, and attempting to complete it by proving the unproven assumptions. It is through this task that I learned the TLA + specification and proof language, also consulting the available references from time to time.

I found the TLA + language natural, expressive, and well-suited for modeling and verifying Pastry. The learning curve was not too long; within the first months I was su ciently competent in TLA + to write involved proofs for some of Lu's assumptions, and, more importantly, to identify room for improvement in Lu's specification to enhance proof automation. Due to the expressiveness of the language, it is typically possible to express one property in many di↵erent ways that are semantically equivalent, but where the performance of the back-end theorem provers varies greatly according to the chosen syntax. For me, this was the first main task which gave me insight into both TLA + and Pastry. At this point, I decided to improve the specification of LuPastry into LuPastry + as described in Chapter 5, before proceeding to write a new and complete proof of correctness.

The second task was to prove a large number of lemmas on arithmetic, set theory and the Pastry data structures. Many of the data structure lemmas were inspired by Lu's unproven assumptions. The arithmetic and set theory lemmas, on the other hand, as well as many more data structure lemmas, were formulated and proven on-the-go whenever the need for them arose in the higher levels of the proof.

The most di cult task was to develop a coherent story for the proof and find the right invariants to prove. Model checking was crucial at this point. I performed model checking on networks of four and sometimes eight nodes for every property I intended to prove as an invariant. For the model checking to be e cient, the key trick is to model-check a restricted specification where actions for lookup and message loss are disabled. 1 Since the safety property "correct delivery" is concerned with the correctness of the node's local view of the network, these actions cannot contribute to any potential counterexamples. The lookup actions only move lookup messages through the network and do not change the node state. Similarly, message loss bears no e↵ect on correct delivery; it can only a↵ect liveness by causing a node to deadlock, waiting on a message that was lost in communication. With these actions disabled, the LuPastry + (and Simplified LuPastry + ) models have a finite number of states; the protocol stabilizes after every key in the key space corresponds to the identifier of a live node. At this point, all join processes have completed, and no more messages are exchanged. This means that model checking takes less than a minute on a network of four nodes instead of days. I found the TLC model checker easy to use from within the TLA + toolbox.

Another challenge in proving the invariants using TLAPS was the lack of counterexamples provided by the back-end provers. When proof obligations fail, the toolbox cites either timeout, or, rarely, a false proof obligation. In the case of a timeout, it takes some e↵ort to determine whether the timeout occurred because the proof obligation was false, or because it was more than the back-end could handle. In my experience, many SMT-reported timeouts were due to a true proof obligation being too involved for the SMT solver to handle, while timeouts reported from general-purpose provers like Zenon and Spass typically meant the input proof obligation was false.

Room for Improvement and Future Work

Node failure. The proof presented here proves correct delivery of lookup messages for pure-join variants of Pastry, where node failure is not modeled. As Lu already shows in [START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF], the full published version of Pastry is inconsistent; the property of correct delivery is violated when node failure is taken into account. Similar results have been found for similar protocols like Chord [START_REF] Zave | Using Lightweight Modeling to Understand Chord[END_REF]. In fact, it is argued that one cannot achieve consistency where node failure is allowed, due to the possibility of network separation [START_REF] Ghodsi | Distributed K-ary System: Algorithms for Distributed Hash Tables[END_REF]. However, there is still no definitive answer to this question. There is no doubt that a full DHT protocol that is formally specified and provably correct using rigorous formal methods would be a remarkable achievement in this research area. A good start would be Pamela Zave's version of Chord presented in [START_REF] Zave | How to Make Chord Correct (Using a Stable Base[END_REF], which she supports with a proof of correctness that is carried out by automated analysis of an Alloy model. Zave's model of Chord operates under the assumption that the key space has a certain minimum size n, and that there is a stable base of n nodes that are permanently online to guarantee connectivity. It would be interesting to apply formal methods like theorem proving to full specifications of Pastry or Chord which allow nodes to join and leave freely, and see if correct delivery holds under the assumption of a stable base.

Proof reuse for other DHT protocols. The strong similarities among the available DHT implementations indicate that there is great potential for proof reuse. This thesis already serves as an example in this direction, where a complete proof as large as 32,000 lines for LuPastry + was directly adapted to prove correctness of a simplified variant of the specification. There is also the possibility of applying formal methods to verify certain properties of a "generic" specification of DHT protocols, from which existing DHT protocols like Pastry can be instantiated. In his thesis, Ghodsi mentions that DKS is a generalization of DHT protocols, from which Pastry and Chord can be instantiated [START_REF] Ghodsi | Distributed K-ary System: Algorithms for Distributed Hash Tables[END_REF]. DKS may serve as a good starting point in this direction.

Figure 2 . 1 -

 21 Figure 2.1 -The TLA + proof system.

Figure 2 . 2 -

 22 Figure 2.2 -Methodology used for the formal verification of Pastry using TLA + .

  Peer-to-Peer (P2P) Networks

  Client/Server Model Peers (b) Peer-to-Peer Model

Figure 3 . 1 -

 31 Figure 3.1 -The client/server model versus the decentralized P2P model.

  choose x : P (x ) An x satisfying P . choose x 2 S : P (x ) An x in the set S satisfying P . Functions, Tuples and Records f [e] The application of function f to expression e. domain f The domain of function f . [X ! Y ] The set of functions with domain X and range Y . [x 2 X 7 ! e] A function f such that f [x ] = e for x in X . [f except ![e 1 ] = e 2 ] A function f equal to f except f [e 1 ] = e 2 . An @ in e 2 equals f [e 1 ].

e 0

 0 The value of e in the final state of an action.unchanged e e 0 = e[A] e A _ (e 0 = e) enabled A An A action is possible.

Figure 3 . 3 -

 33 Figure 3.3 -A summary of TLA + syntax.

Figure 3 .

 3 [START_REF] Bakhshi | Verification of Peer-to-Peer Algorithms: A Case Study[END_REF] shows a TLA + specification of this system in one module named TwoJugs.First, because arithmetic operators such as +, are not built-in operators in TLA + , the module imports TLA + 's standard Naturals module. TLA + provides standard modules for Naturals, Integers and Reals that define arithmetic operators like the following. a + b, a b, a ⇤ b Addition, subtraction, multiplication. a < b, a  b, a > b, a b Binary comparisons. a . . b {n 2 N : a  n  b} a b Exponentiation. a%b a mod b, such that 0  a%b < b a ÷ b Division such that a = b ⇤ (a ÷ b) + (a%b) These modules also define the sets Nat, Int and Real of naturals, integers and real numbers respectively.

  e. the proof is nested. Because this is module TwoJugs extends Naturals constants BigCapacity, SmallCapacity variables big, small Min(x , y) = if x  y then x else y vars = hbig, small i Init = big = 0 ^small = 0 FillSmall = small 0 = SmallCapacity ^big 0 = big FillBig = big 0 = BigCapacity ^small 0 = small EmptySmall = small 0 = 0 ^big 0 = big EmptyBig = big 0 = 0 ^small 0 = small SmallToBig = let poured = Min(big + small , BigCapacity) big in ^big 0 = big + poured ^small 0 = small poured BigToSmall = let poured = Min(big + small , SmallCapacity) small

Figure 3 . 4 - 2 ^SmallCapacity 2

 3422 Figure 3.4 -TLA + specification of the "Two Jugs" problem.

Figure 3 . 5 -

 35 Figure 3.5 -TLA + example proof for the "Two Jugs" problem.

Figure 4 .

 4 1b: each two consecutive live nodes on the ring divide the coverage of keys that lie Ideal distribution of coverage among live nodes.

Figure 4 . 1 -

 41 Figure 4.1 -An example of a Pastry ring of size 16, and the ideal distribution of coverage among its live nodes.

  k

Figure 4 . 3 -

 43 Figure 4.3 -The LuPastry/LuPastry + join protocol.

Figure 4 . 4 -

 44 Figure 4.4 -An overview of the LuPastry + specification in TLA + .

Definition 3 (

 3 Clockwise Distance). ClockwiseDistance(x , y) = if y x then y x else RingSize x + y Definition 4 (Absolute/Shortest Distance). AbsoluteDistance(x , y) = let d 1 = ClockwiseDistance(x , y) d 2 = ClockwiseDistance(y, x ) in if d 1  d 2 then d 1 else d 2 In Figure 4.1, for example, where RingSize = 16, the clockwise distance from node 1 to node 14 is ClockwiseDistance(1, 14) = 13, but the shortest distance between them is counter-clockwise, AbsoluteDistance(1, 14) = 3.

Definition 5 (

 5 Leaf Set). LeafSet = {ls 2 [node : I , left : subset I , right : subset I ] : ^ls.node / 2 ls.left ^ls.node / 2 ls.right ^Cardinality(ls.left)  L ^Cardinality(ls.right)  L}

Definition 6 (

 6 Leaf Set Content). LeafSetContent(ls) = ls.left [ ls.right [ {ls.node} Definition 7 (Empty Leaf Set).

! [type 7 !

 7 "JoinRequest", rt 7 ! EmptyRT , node 7 ! j ]] in ^Status[j ] = "Dead" ^Status[i ] = "Ready" ^Status 0 = [Status except ! [j ] = "Waiting"] ^MessagePool 0 = MessagePool [ {msg} ^unchanged hRoutingTables, LeafSets, Probing, Failed , Leases, Grants, ToJoini Definition 23 (Action Receive Join Reply).

  )) \ {m} ^unchanged hLeases, Status, Grants, ToJoini Definition 25 (Action Receive Probe Reply).

Figure 5 .

 5 Figure 5.1 shows the structure of the original TLA + specification and partial correctness proof of LuPastry by Lu[START_REF] Lu | Formal Verification of the Pastry Protocol[END_REF].1

Figure 5 . 1 -

 51 Figure 5.1 -Structure of the original LuPastry specification and proof.

4

 4

lemma 8 ls 2

 2 LeafSet, k 2 I : LeafSetContent(AddToLS ({k }, ls)) \ {k } = LeafSetContent(ls)

=

  if a = {} then x else choose y 2 a : 8 z 2 a : AbsoluteCloser (x , y, z )

lemma type RightNeighbor = 8 ls 2

 2 LeafSet : RightNeighbor (ls) 2 I proof by type ClosestFromTheRight def RightNeighbor , LeafSet lemma def RightNeighbor = 8 ls 2 LeafSet : ^ls.right = {} ) RightNeighbor (ls) = ls.node ^ls.right 6 = {} ) ^RightNeighbor (ls) 2 ls.right ^8 p 2 ls.right : ClockwiseArc(ls.node, RightNeighbor (ls), p) proof by def ClosestFromTheRight def RightNeighbor , LeafSet

IsBalanced

  (ls) = Cardinality(ls.left) = Cardinality(ls.right) Definition 34 (Proper Leaf Set). A leaf set is proper if members that are exclusively in the left (right) part are left-(right-)closer to the leaf set owner than other members. IsProper (ls) = ^8 x 2 ls.left \ ls.right, y 2 ls.right : ClockwiseArc(y, x , ls.node) ^8 x 2 ls.right \ ls.left, y 2 ls.left : ClockwiseArc(ls.node, x , y) Definition 35 (Organized Leaf Set). A leaf set is organized if the presence of exclusively left or right members indicates that the leaf set is full. IsOrganized (ls) = (ls.left \ ls.right 6 = {} _ ls.right \ ls.left 6 = {}) ) IsComplete(ls)

Figure 5 . 3 -

 53 Figure 5.3 -Structure of the original LuPastry proof versus the new, complete proof.

CorrectCoverage = 8 iFigure 6 . 1 -

 861 Figure 6.1 -Structure of the LuPastry + correctness proof.

  Node i 's coverage oversteps into j 's coverage if i's leaf set neighbor is farther from i than j . i j (b) Nodes i and j are each other's leaf set neighbors. Each node respects the other's coverage range. i . . . j (c) Nodes i and j are separated by other leaf set neighbors. Their coverage end-points are even further apart. i j k (d) Only i is aware of a node k between itself and j . The coverage ranges of i and j still do not overlap.

Figure 6 . 2 -

 62 Figure 6.2 -Possible arrangements for two Ready nodes i and j and their coverage ranges.

L 3 ,

 3 i's leaf set can always accommodate k1 = ToJoin[i], k2 = ToJoin[j ], and i's Ready/OK neighbor j .

Figure 6 . 3 -

 63 Figure 6.3 -Network stability.

Assumption 1 .M 2 Assumption 5 .

 125 NIL is not a valid node. NIL / Assumption 2. A is non-empty set of nodes. A ✓ I ^A 6 = {} Assumption 3. M and L are positive integers. Nat \ {0} ^L 2 Nat \ {0} Assumption 4. B is a positive integer that is strictly less than M and divides M . B 2 Nat ^B > 0 ^B < M ^M %B = 0 The size of the left (right) leaf set is at least 3. L 3

Invariant 3 (

 3 Type Invariant).

^Status 2 [

 2 I ! {"Ready", "OK", "Waiting", "Dead"}] ^Leases 2[I ! subset I ] ^Grants 2 [I ! subset I ] ^MessagePool 2 subset Message ^ToJoin 2 [I ! I ] ^RoutingTables 2 [I ! RoutingTable] ^LeafSets 2 [I ! LeafSet] ^8 i 2 I : LeafSets[i ].node = i ^Probing 2 [I ! subset I ] ^Failed 2 [I ! subset I ]Invariant 4. There is always at least one Ready node, and therefore at least one participating node. ReadyNodes 6 = {} ^ReadyOKNodes 6 = {} ^ParticipatingNodes 6 = {} Invariant 5. All leaf sets are balanced, proper, and organized.

8 i 2 IInvariant 6 . 8 .

 268 : let ls = LeafSets[i ] in IsBalanced (ls) ^IsProper (ls) ^IsOrganized (ls) The leaf set of a participating node consists solely of other participating nodes. 8 i 2 ParticipatingNodes : LeafSetContent(LeafSets[i ]) ✓ ParticipatingNodes Invariant 7. A Dead node is not a to-join node, and consequently, not a participating node. DeadNodes \ (ToJoinNodes [ ParticipatingNodes) = {} Invariant The probe set of a node i consists of participating nodes.

8 i , j 2

 2 ParticipatingNodes , m 2 MessagePool : ^i 6 = j ^j 2 LeafSetContent(LeafSets[i ]) ^m.content.type = "JoinReply" ^m.destination = j ) j 2 Probing[i ] _ j = ToJoin[i ]

8 m 2

 2 MessagePool : let r = m.content.ls.node i = m.destination in 8 n 2 {ClosestFromTheRight(r , ParticipatingNodes \ {r }), ClosestFromTheLeft(r , ParticipatingNodes \ {r })} m.content.type = "JoinReply" ^n / 2 ReadyOKNodes ) _ n 2 LeafSetContent(m.content.ls) _ LeafSets[n] = EmptyLS (n) _ i 2 Probing[n] _ r 2 Probing[n]

Figure 6 . 4 -

 64 Figure 6.4 -Possible arrangement for Ready/OK nodes i and k with respect to a key j right-covered by i .

. 1 .

 1 Compare this figure to the original join process in Figure 4.3.

  msg Lookup = [type : {"Lookup"}, node : I ] msg NoLegalRoute = [type : {"NoLegalRoute"}, key : I ] msg JoinRequest = [type : {"JoinRequest"}, rt : RoutingTable, node : I ] msg JoinReply = [type : {"JoinReply"}, rt : RoutingTable, ls : LeafSet] msg Probe = [type : {"Probe"}, node : I , ls : LeafSet, failed : subset I ] msg ProbeReply = [type : {"ProbeReply"}, node : I , ls : LeafSet, failed : subset I ] msg Notify = [type : {"Notify"}, node : I ] MessageContent = msg Lookup [ msg NoLegalRoute [ msg JoinRequest [ msg JoinReply [ msg Probe [ msg ProbeReply [ msg Notify Message = [destination : I , content : MessageContent] The variables of the new specification are given by the following definition. Definition 37 (Simplified LuPastry + Variables). vars = hMessagePool , Status, LeafSets, RoutingTables, Probing, ToJoin, Responsible, Failed i

^MessagePool 2

 2 subset Message ^Status 2 [I ! {"Ready", "Waiting", "Dead"}] ^RoutingTables 2 [I ! RoutingTable] ^LeafSets 2 [I ! LeafSet] ^8 i 2 I : LeafSets[i ].node = i ^Probing 2 [I ! subset I ] ^Failed 2 [I ! subset I ] ^ToJoin 2 [I ! I ] ^Responsible 2 [I ! I ]

Definition 42 (

 42 Simplified LuPastry + Action Receive Notification).ReceiveNotification(i ) = Status[i ] = "Ready" ^9 m 2 MessagePool : ^m.content.type = "Notify" ^m.destination = i ^m.content.node = ToJoin[i ] ^ToJoin 0 = [ToJoin except ! [i ] = i ] ^MessagePool 0 = (MessagePool \ {m})^unchanged hStatus, RoutingTables, LeafSets, Probing, Failed , Responsiblei

8 i

 8 , j , k 2 I :^Status[i ] = "Ready" ^Status[j ] = "Ready" ^j 6 = i ^Covers(LeafSets[i ], k ) ^9 m 2 MessagePool : m.content.type = "Lookup" ^m.content.node = k ^m.destination = i ) ^AbsoluteDistance(i , k )  AbsoluteDistance(j , k ) ^¬Covers(LeafSets[j ], k )

8 i 2 (

 2 ToJoinNodes \ ReadyNodes) :LeafSets[i ] 6 = EmptyLS (i ) ) i 6 = Responsible[i ]

2 .

 2 Preuve de correction de LuPastry + . Une preuve complète et rigoureuse en TLA + du bon acheminement de requêtes de clefs par LuPastry + est présentée. 3. LuPastry + simplifié. Une variante de LuPastry + est définie dans laquelle le protocole d'intégration de noeuds est simplifié en omettant l'étape d'échange de bail. 4. Preuve de correction pour LuPastry + simplifié. Une preuve complète et rigoureuse en TLA + du bon acheminement de messages de requêtes de clefs par LuPastry + simplifié est présentée. Cette preuve est une adaptation de la preuve de correction de LuPastry, et représente en cela un bon succès en matière de réutilisation de preuves.

  1 7 ! e 1 , . . . , h n 7 ! e n ], e.h i denotes e[h i ], the h i component of the record e. Finally, the last part of the table describes syntax for actions and temporal operators. Union, intersection, subset and set di↵erence. {e 1 , . . . , e n } The set of elements e 1 , . . . , e n . {x 2 S : P } The set of elements x in set S satisfying P .subset S The power set of set S . Logic ^, _, ¬, ), ⌘ Conjunction, disjunction, negation, implication and equivalence. 8x : P For all x , P holds. 9x : P For some x , P holds. 8x 2 S : P For all x in the set S , P holds. 9x 2 S : P For some x in the set S , P holds. true, false Boolean constants for truth > and falsehood ?.

	Sets
	=, 6 = Equality and negated equality. 2 , / Set membership and its negation. 2 [, \, ✓, \

boolean

The set {true, false}.

  e.h The h-component of record e. An n-tuple with i th component e i . S 1 ⇥ • • • ⇥ S n The set of all n-tuples with i th component in S i . d 1 . . . d n or d 1 . . . d m .d m+1 . . . d n Integers and real numbers where d i is a digit. Actions and Temporal Operators

	[h	1 7 ! e

1 , . . . , h n 7 ! e n ] A record whose h i component is e i . [h 1 : S 1 , . . . , h n : S n ] The set of all records with h i component in S i . e[i ] The i th component of tuple e. he 1 , . . . , e n i

  An example routing table of a node with ID 10233102, where node IDs are interpreted as 8 digits in base 2 B = 4.

		10-0-31203 10-1-32102	2	10-3-23302
	3	102-0-0230 102-1-1302 102-2-2302	3
	4	1023-0-322 1023-1-000 1023-2-121	3
	5	10233-0-01	1	10233-2-32
	6	0		102331-2-0
	7			2
	Figure 4.2 -

  Definition 26 (Action Receive Lease Request).

ReceiveLeaseRequest(i ) = Status[i ] 2 {"

OK", "Ready"} ^9 m 2 MessagePool : let gr = m.content.node 2 {LeftNeighbor (LeafSets[i ], RightNeighbor (LeafSets[i ])} msg = [destination 7 ! m.content.node, content 7 ! [type 7 ! "LeaseReply", ls 7 ! LeafSets[i ], grant 7 ! gr ]] in ^m.content.type = "LeaseRequest" ^m.destination = i ^Grants 0 = [Grants except ! [i ] = if gr then @ [ {m.content.node} else @] ^MessagePool 0 = (MessagePool \ {m}) [ {msg} ^unchanged hStatus, RoutingTables, LeafSets, Probing, Failed , Leases, ToJoini Definition 27 (Action Request Lease).

  Reduction to Invariants layer contains the main theorems that reduce the safety property of correct delivery to a set of 50 claimed invariants

	Proof of Invariants
	50 Proven Invariants, 14,500 Lines
	Type Lemmas and Invariant
	3 Proven, 6 Unproven Lemmas, 1230 Lines
	Reduction to Invariants
	16 Proven Lemmas, 620 Lines
	Leaf Set Properties
	112 Unproven Lemmas, 1270 Lines
	Arithmetic and Theory
	140 Unproven Lemmas, 930 Lines
	LuPastry Specification
	1,575 Lines

  Invariant 27. The failed set of any node is empty. Also, the failed set attached to any pending message is empty.Invariant 29. Dead nodes have empty leaf sets and probe sets. If a Ready node has an empty leaf set, it is the only Ready node on the network.

	Invariant 26. Let m be a lease reply message where the lease is granted,
	i.e. m.content.grant = true. Then the destination of m is a Ready or
	OK node.
	8 m 2 MessagePool : m.content.type = "LeaseReply" ^m.content.grant ) Status[m.destination] 2 {"Ready", "OK"}
	8 m 2 MessagePool : ^m.content.type 2 {"JoinRequest", "Probe", "ProbeReply", "LeaseRequest"}
	) Status[m.content.node] 6 = "Dead" ^m.content.type 2 {"JoinReply", "LeaseReply"} ) Status[m.content.ls.node] 6 = "Dead"
	8 i 2 I : Probing[i ] ✓ ParticipatingNodes ^8 i 2 DeadNodes : LeafSets

^8 i 2 I : Failed [i ] = {} ^8 m 2 MessagePool : m.content.type 2 {"Probe", "ProbeReply"} ) m.content.failed = {} Invariant 28. Dead nodes do not send messages.

  ReadyOKNodes ) ¬Covers(LeafSets[i ], ToJoin[j ])Invariant 47. A Ready node r does not cover any to-join node i .8 i 2 ToJoinNodes, r 2 ReadyNodes : r 6 = i ) ¬Covers(LeafSets[r ], i )Invariant 48 (Exclusive Coverage). Two Ready/OK nodes i and j do not both think they cover the same key k .Invariant 49 (Stable Network). Let i be a Ready/OK node and r its left or right Ready/OK neighbor. Then r is a member of i 's leaf set. LeafSet : 8 i 2 (ls.left [ ls.right) : IsProper (ls) ^IsBalanced (ls) ^IsOrganized (ls) ) ¬Covers(ls, i )

	6.4 An Outline of the Reduction Proof
	In what follows, I show that strong correct delivery can be derived from the
	correctness invariants presented above.
	Lemma 1. A proper, balanced and organized leaf set does not cover its
	own members.
	8 ls 2
	StableNetwork =
	8 i 2 ReadyOKNodes : ^ClosestFromTheRight(i , ReadyOKNodes \ {i }) 2 LeafSetContent(LeafSets[i ]) ^ClosestFromTheLeft(i , ReadyOKNodes \ {i }) 2 LeafSetContent(LeafSets[i ])

8 i , j 2 ReadyOKNodes, k 2 I : i 6 = j ^i 6 = k ^j 6 = k ) ¬Covers(LeafSets[i ], k ) _ ¬Covers(LeafSets[j ], k )

  Recall the definition of StrongCorrectDelivery (Invariant 2). Let i and k be two di↵erent Ready nodes and assume i covers some key j . Let m be a pending lookup message for key j addressed to i . It is required to show that (1) i is closer to j than k is in terms of absolute ring distance, and (2) k does not cover j .For brevity, let us denote AbsoluteDistance(i , j ) and AbsoluteDistance(k , j ) by D i and D k , respectively. The leaf sets of i and k are denoted by ls i and ls k . The right and left leaf set neighbors of i are RN i and LN i , respectively, and similarly for k , we use RN k and LN k . The right and left coverage bounds of i 's leaf set are denoted by RC i and LC i (RC k and LC k for k ).

	Theorem 1. Correct delivery follows from the correctness invariants listed in Section 6.3. CorrectnessInvariants ) StrongCorrectDelivery Proof. ^AbsoluteDistance(i , j )  AbsoluteDistance(k , j ) ^¬Covers(LeafSets[k ], j )

  At this point, i has o cially finished the join process; it can directly help new nodes join the network. It does not need to send lease requests to its leaf set neighbors, but instead, sends a notification message to the responsible node k , letting it know that it has finished joining. Once node k has received i 's notification, it may help other new nodes join the network. The TLA + Specification of Simplified LuPastry + I adapt the specification of LuPastry + explained in Section 4.2 as follows. The specification constants, ring description and distance operators remain unchanged in Simplified LuPastry + . Similarly, the data structures for the routing table and leaf set are identical in both specification. The only change to the specification data structures relates to the types of messages exchanged between nodes. Lookup, joining and probing messages work as before. Lease request and reply messages are no longer needed and therefore eliminated from the specification. A new type of message is needed for the final notification at the end of the join process.Definition 36 (Simplified LuPastry + Message).

	7.2
					join reply
	k	i	k	i	k	i
			join request
	j		j		j
		r		r	r
	(a) Dead node i	(b) Node i turns	(c) The join
	wants to join the	"Waiting" and	request is for-
	network.		sends a join	warded to node
			request to node	k , and k re-
			j .		sponds to i.
	probe	probe reply	finished join
	k	i	k	i	k	i
	probe
			probe reply
	j	probe	j	probe reply	j
		r		r		r
	(d) Node i re-	(e) Live nodes re-	(f) Node i turns
	ceives node k 's	spond to i's probe	Ready and noti-
	join reply and	messages.	fies k . Node i
	begins the prob-			may now accept
	ing phase.			join requests.
	k	i
	j
		r
	(g) Node k re-
	ceives i 's notifi-
	cation; k may ac-
	cept new join re-
	quests.
		Figure 7.1 -The Simplified LuPastry + join protocol.
			103

  Definition 38 (Simplified LuPastry+ Initial State). {} ^Status = [i 2 I 7 ! if i 2 A then "Ready" else "Dead"] ^ToJoin = [i 2 I 7 ! i ] ^Responsible = [i 2 I 7 ! i ] ^Probing = [i 2 I 7 ! {}] ^Failed = [i 2 I 7 ! {}] ^LeafSets = [i 2 I 7 ! if i 2 A then AddToLS (A, EmptyLS (i )) else EmptyLS (i )] ^RoutingTables = [i 2 I 7 ! if i 2 A then AddToRT (A, EmptyRT , i ) else AddToRT ({i }, EmptyRT , i )]The next-state relation in Simplified LuPastry + is defined as follows.Definition 39 (Simplified LuPastry + Next-State Relation).

	Init = ^MessagePool = Next

= 9 i , j 2 I : _ Lookup(i , j ) _ RouteLookup(i , j ) _ DeliverLookup(i , j ) _ Join(i , j ) _ RouteJoinRequest(i , j ) _ ReceiveJoinRequest(i ) _ ReceiveJoinReply(i ) _ ReceiveProbe(i ) _ ReceiveProbeReply(i ) _ ReceiveNotification(i ) _ LoseMessage

Plus correctement, étant donné que ces deux théories sont très expressives et indécidables, les solveurs SMT se focalisent typiquement sur des fragments décidables de ces théories comme l'arithmétique linéaire sur les entiers ou les réels, sans quantificateurs.

www.ubuntu.com

www.libreoffice.org

More accurately, since both of these theories are very expressive and undecidable, SMT solvers typically focus on decidable fragments of these theories such as quantifier-free linear arithmetic over integers or reals.

Of course, the names Spec, Init and Next are not significant; they can be substituted for other names.

Fully-active network members that are not still in the process of joining.

As will be discussed in Chapter 5, the actual LuPastry + definitions of ring size, leaf set operations, leaf set neighbors and coverage rely on auxiliary operators but are "flattened" here for clarity.

Visualization and names assigned to proof layers are my own. Line counts represent the total line counts of the individual TLA + files, which may include whitepace and comments. However, I exclude all trailing comments in a file.

Adapting notation for better readability.

See AddToLSetInvCo in module ProofLSetProp of Lu's LuPastry files,[START_REF] Azmy | TLA + Specification and Proof Files of LuPastry, LuPastry + and Simplified LuPastry +[END_REF].

See AddAndDelete in module ProofLSetProp of Lu's LuPastry files,[START_REF] Azmy | TLA + Specification and Proof Files of LuPastry, LuPastry + and Simplified LuPastry +[END_REF].

See SemJoinLeafSet in module MSPastry of Lu's LuPastry files,[START_REF] Azmy | TLA + Specification and Proof Files of LuPastry, LuPastry + and Simplified LuPastry +[END_REF].

The TLA + representation of the invariants has been compressed for better readability and compactness.

In fact, it is possible that r 2 itself was in the process of joining the network, but in this case the same proof applies recursively on r 2 instead of j . For the sake of this abstract discussion, let us ignore this case and assume r 2 was Ready when j started joining.

Since each node joins only once, there is no need to reset Responsible[i] to i after it has finished joining.

Actions Lookup, RouteLookup, DeliverLookup and LoseMessage in the TLA + specification presented in Chapter 4.

Acknowledgments

IsComplete(ls) = Cardinality(ls.right) = L ^Cardinality(ls.left) = L Finally, the interval [LeftCoverage(ls), RightCoverage(ls)] is the coverage region of leaf set ls. The TLA + predicate Covers(ls, k ) is true if key k is in the coverage range of leaf set ls. If every node knows its true right and left neighbors on the ring, this interval computes the ideal coverage as shown in Figure 4.1b. However, if a node's leaf set is not up-to-date, the leaf set neighbor of a node may not be its true live neighbor on the ring. Therefore, a node may under-or over-estimate its coverage region.

Counterexamples to Lu's Assumptions

In what follows, I give some examples of incorrect assumptions in Lu's proof. 2

Counterexamples to Leaf Set Assumptions

Consider the following assumption 3 , which states that after adding some set of nodes a to a leaf set ls1, the right neighbor of the resulting leaf set ls2 can only be closer to the leaf set owner i than the original right neighbor of ls1.

This assumption does not hold if the right-hand part of the leaf set is empty. If ls1.right = {}, then RightNeighbor (ls1) = i , and i is closer to itself than to any other node; ClockwiseDistance(i , i ) = 0. Instead, the assumption needs to be weakened as follows.

Chapter 6

The LuPastry + Correctness Proof

This chapter presents the TLA + proof of correct delivery of lookup messages in LuPastry + . I prove that the safety property correct delivery is an invariant of the TLA + specification of LuPastry + . Correct delivery was defined by Lu in [START_REF] Lu | Formal Verification of the Pastry Protocol Using TLA +[END_REF] as follows.

Invariant 1 (Correct Delivery). Let i and k be two keys on the ring. If DeliverLookup(i , k ) is enabled, then, (1) i is closer to k than any other Ready node j 6 = i is, in terms of absolute distance, and (2) the action DeliverLookup(j , k ) is not enabled for any key j 6 = i.

As per Definition 19 of the action DeliverLookup, DeliverLookup(i , k ) is enabled if and only if i is Ready, its leaf set covers k , and there is a pending lookup message with destination i and key k . ^8 i 2 I :

A node that has issued a pending join request is Waiting, not participating, and has an empty leaf set and probe set. ) m.content.ls.node 2 ParticipatingNodes ^m.content.type 2 {"JoinReply", "Probe", "ProbeReply", "LeaseRequest", "LeaseReply"} ) m.destination 2 ParticipatingNodes Invariant 20. For any two nodes x and y, there cannot be a pending probe from x to y and a pending probe reply from y to x at the same time.

Invariant 42. Let i be a non-Ready/OK node joining through a Ready node r . Let k be a non-Ready/OK node joining through one of r 's Ready neighbors n (here the right or left Ready/OK neighbor of r ). If there is a pending probe reply message m from r to k , then one of the following must hold: (1) i 's leaf set is empty, (2) i is in the leaf set attached to m, (3) i is probing k , (4) k is a member of i 's leaf set.

Similarly, the action ReceiveProbeReply had no e↵ect on the variables Leases and Grants in the original specification. However, it is modified so that on receiving the last expected probe reply (finishing the probing phase), a Waiting node i turns Ready, and, instead of sending lease request messages to its neighbors, notifies its responsible node that it has finished joining. The variable Responsible remains unchanged. Actions RequestLease, ReceiveLeaseRequest and ReceiveLeaseReply from the original specification are no longer needed and are omitted here. Instead, I define an action ReceiveNotification, where a node i receives a notification from its to-join node, letting it know that it has finished the join process and turned Ready. Node i resets its to-join field so that it can help new nodes join the network in the future.