2016/10/31 by Pamela Zave · 1 citation
Computer Science · #Advanced Data Storage Technologies #Caching and Content Delivery #Peer-to-Peer Network Technologies #cs.DC
paper · pdf · doi:10.1109/tse.2017.2655056
published as ACM/IEEE Transactions on Software Engineering, December 2017 · 14 pages including references; 6 figures. arXiv admin note: text overlap with arXiv:1502.06461
openalex publication_date 2017/01/18 · arxiv created 2019/07/25 · arxiv updated 2019/07/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
The Chord distributed hash table (DHT) is well-known and often 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. Previous work has not, however, discovered whether Chord could be made correct under the same 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 two independent proofs of correctness. One proof is informal and intuitive, and applies to networks of any size. The other proof is based on a formal model in Alloy, and uses fully automated analysis to prove the assertions for networks of bounded size. The two proofs complement each other in several important ways.