2012/03/29 by Pamela Zave · 3 citations
Computer Science · #Advanced Database Systems and Queries #Advanced Data Storage Technologies #Peer-to-Peer Network Technologies
paper · doi:10.1145/2185376.2185383
openalex publication_date 2012/03/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/18
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.