Especificación y análisis del protocolo Chord en Maude

Abstract

Los sistemas peer-to-peer estructurados basan su funcionamiento en la implementación de una Tabla Hash Distribuida (THD), entre las cuales destacan: Kademlia, Chord, CAN y Pastry. Este documento presenta la especificación en Maude de un sistema peer-to-peer implementado con la Tabla Hash Distribuida Chord. Chord organiza su espacio de identificadores utilizando un anillo, donde cada nodo es responsable de un conjunto de claves las cuales se reasignan cuando un nodo entra o sale a la red. Además, cada nodo mantiene una tabla de encaminamiento, denominada tabla finger, utilizada para llevar a cabo el algoritmo de búsqueda. La especificación implementada ha sido diseñada para la compartición de archivos, de forma que los nodos puedan conectarse de la red, desconectarse de la red, publicar un fichero o buscar un fichero en un máximo de log n saltos, siendo n el número de nodos que conforman la red. [ABSTRACT] Distributed Hash Tables (DHT) is an essential component in most peer-to-peer systems. A large number of DHTs have been studied through theoretical simulations and analyses over the last years, such as: Kademlia, Chord, CAN, and Pastry. This paper presents the distributed specification of a peer-to-peer network that uses the Chord DHT in the formal specification language Maude. Identifiers are ordered on the Chord ring. A key is assigned to the first node whose identifier is equal to or follows the key in the identifier space. Each node maintains a routing table, called the finger table, which is used by the lookup algorithm. The contribution of this paper is a specification for lookup in a dynamic peer-to-peer system with frequent node arrivals and departures, which guarantees that the lookup algorithm takes no longer than log n steps.