How to Make Chord Correct
Pamela Zave

TL;DR
This paper establishes the first formal correctness specification and proof for the Chord DHT, demonstrating that with a stable base, large networks can be correct despite issues in small configurations.
Contribution
It provides a formal correctness specification, an inductive invariant, and a proof for Chord, addressing previous uncertainties about its correctness under realistic assumptions.
Findings
Correctness depends on a minimum ring size and a stable base.
Most correctness issues are anomalies in small networks.
Large networks do not require maintaining a stable base.
Abstract
The Chord distributed hash table (DHT) is well-known and frequently used to implement peer-to-peer systems. Chord peers find other peers, and access their data, through a ring-shaped pointer structure in a large identifier space. Despite claims of proven correctness, i.e., eventual reachability, previous work has shown that the Chord ring-maintenance protocol is not correct under its original operating assumptions. It has not, however, discovered whether Chord could be made correct with reasonable operating assumptions. The contribution of this paper is to provide the first specification of correct operations and initialization for Chord, an inductive invariant that is necessary and sufficient to support a proof of correctness, and the proof itself. Most of the proof is carried out by automated analysis of an Alloy model. The inductive invariant reflects the fact that a Chord network…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsPeer-to-Peer Network Technologies · Advanced Data Storage Technologies · Caching and Content Delivery
