Pamela Zave
Abstract
Correctness of the Chord ring-maintenance protocol would mean that the protocol can eventually repair all disruptions in the ring structure, given ample time and no further disruptions while it is working. In other words, it is "eventual reachability." Under the same assumptions about failure behavior as made in the Chord papers, no published version of Chord is correct. This result is based on modeling the protocol in Alloy and analyzing it with the Alloy Analyzer. By combining the right selection of pseudocode and textual hints from several papers, and fixing flaws revealed by analysis, it is possible to get a version that may be correct. The paper also discusses the significance of these results, describes briefly how Alloy is used to model and reason about Chord, and compares Alloy analysis to model-checking.
- M. J. Freedman, K. Lakshminarayanan, S. Rhea, and I. Stoica. Non-transitive connectivity and DHTs. In Proceedings of the 2nd Conference on Real, Large, Distributed Systems, pages 55--60. USENIX, 2005. Google Scholar
Digital Library
- L. Glendenning, I. Beschastnikh, A. Krishnamurthy, and T. Anderson. Scalable consistency in Scatter. In Proceedings of the 23rd ACM Symposium on Operating Systems Principles. ACM, October 2011. Google ScholarDigital Library
- G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2004. Google ScholarDigital Library
- D. Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, 2006. Google ScholarDigital Library
- C. Killian, J. A. Anderson, R. Jhala, and A. Vahdat. Life, death, and the critical transition: Finding liveness bugs in systems code. In Proceedings of the 4th USENIX Symposium on Networked System Design and Implementation, pages 243--256, 2007. Google ScholarDigital Library
- S. Krishnamurthy, S. El-Ansary, E. Aurell, and S. Haridi. A statistical theory of Chord under churn. In Peer-to-Peer Systems IV. Springer-Verlag LNCS 3640, 2005. Google ScholarDigital Library
- D. Liben-Nowell, H. Balakrishnan, and D. Karger. Analysis of the evolution of peer-to-peer systems. In Proceedings of the 21st ACM Symposium on Principles of Distributed Computing, pages 233--242. ACM, 2002. Google ScholarDigital Library
- B. T. Loo, T. Condie, J. M. Hellerstein, P. Maniatis, T. Roscoe, and I. Stoica. Implementing declarative overlays. In Proceedings of the 20th ACM Symposium on Operating System Principles, pages 75--90. ACM, 2005. Google ScholarDigital Library
- I. Stoica, R. Morris, D. Karger, M. F. Kaashoek, and H. Balakrishnan. Chord: A scalable peer-to-peer lookup service for Internet applications. In Proceedings of SIGCOMM. ACM, August 2001. Google ScholarDigital Library
- I. Stoica, R. Morris, D. Liben-Nowell, D. Karger, M. F. Kaashoek, F. Dabek, and H. Balakrishnan. Chord: A scalable peer-to-peer lookup service for Internet applications. MIT LCS Technical Report 819, www.pdos.lcs.mit.edu/chord/papers/chord-tn, 2001.Google Scholar
- I. Stoica, R. Morris, D. Liben-Nowell, D. Karger, M. F. Kaashoek, F. Dabek, and H. Balakrishnan. Chord: A scalable peer-to-peer lookup protocol for Internet applications. IEEE/ACM Transactions on Networking, 11(1), February 2003. Google ScholarDigital Library
- M. Yabandeh, A. Anand, M. Canini, and D. Kosti . Almost-invariants: From bugs in distributed systems to invariants. Technical report, EPFL NSL-REPORT-2009-007, 2009.Google Scholar
- M. Yabandeh, N. Knezevi , D. Kosti , and V. Kuncak. CrystalBall: Predicting and preventing inconsistencies in deployed distributed systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation. USENIX, April 2009. Google ScholarDigital Library
- P. Zave. Lightweight modeling of network protocols: The case of Chord. Technical report, AT&T Laboratories|Research, January 2010.Google Scholar
- P. Zave. Experiences with protocol description. Technical report, AT&T Laboratories|Research, June 2011. Presented at the 1st International Workshop on Rigorous Protocol Engineering, October 2011, Vancouver, British Columbia.Google Scholar
Index Terms
- Using lightweight modeling to understand chord
Recommendations
Improving lookup latency in distributed hash table systems using random sampling
Distributed hash table (DHT) systems are an important class of peer-to-peer routing infrastructures. They enable scalable wide-area storage and retrieval of information, and will support the rapid development of a wide variety of Internet-scale ...
Trust overlay networks for global reputation aggregation in P2P grid computing
IPDPS'06: Proceedings of the 20th international conference on Parallel and distributed processingThis paper presents a new approach to trusted Grid computing in a Peer-to-Peer (P2P) setting. Trust and security are essential to establish lasting working relationships among the peers. A P2P reputation system collects peer trust scores and aggregates ...
Software Defined Underlay-aware Structured Peer-to-Peer Overlay
ICDCN '18: Proceedings of the 19th International Conference on Distributed Computing and NetworkingStructured Peer-to-Peer (P2P) overlay networks based on Distributed Hash Table (DHT) provide self-organization and fault tolerance along with good look-up efficiency. This makes them a perfect alternative for designing distributed applications where ...
Comments