Affordable Access

Model Checking the Pastry Routing Protocol

Authors
  • Lu, Tianxiang
  • Merz, Stephan
  • Weidenbach, Christoph
Publication Date
Sep 01, 2010
Source
HAL-INRIA
Keywords
Language
English
License
Unknown
External links

Abstract

Pastry is an algorithm for implementing a scalable distributed hash table over an underlying P2P network, an active area of research in distributed systems. Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to churn and fault tolerance, it makes an interesting target for verification. We have modeled Pastry's core routing algorithms in the specification language TLA+ and used its model checker TLC to analyze qualitative properties of Pastry such as correctness and consistency.

Report this publication

Statistics

Seen <100 times