How To Make Chord Correct

The Chord distributed hash table (DHT) is well-known, frequently used to implement peer-to-peer systems, and frequently used as a foundation for research on designing DHTs with additional properties. Despite claims of proven correctness, previous work has shown that the Chord ring-maintenance protocol is not correct. It has not, however, discovered whether Chord could be made correct. The principle contribution of this paper is to solve the problem by providing the first specification of a correct version of Chord, and a proof of its correctness. In addition the paper provides a simple, necessary, and sufficient inductive invariant, as well as interesting new insights into the workings of distributed systems that use ring-shaped data structures in large identifier spaces. This paper is a regular submission. It is not eligible for a student paper award. i