How to Make Chord Correct (Using a Stable Base).
Pamela Zave · arXiv (Cornell University) · 2015
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 struc-ture in a large identifier space. Despite claims of proven correctness, i.e., eventual reachability, formal modeling has shown that the Chord ring-maintenance protocol is not correct under its original operating as-sumptions [25]. It has not, however, discovered whether Chord could be made correct with reasonable operating assumptions. The principle con-tribution of this paper is to provide the first specification of a correct version of Chord, using the assumption that there is a small “stable base ” of permanent members. The paper presents a simple, sufficient, and arguably necessary inductive invariant, and a partially automated proof of correctness. 1