Project Overview

The Chord distributed hash table (DHT) is wellknown and often used to implement peer-to-peer systems. Chord
peers find other peers, and access their data, through a ringshaped 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.


Pamela Zave

Relevant Links

Reasoning about identifier spaces: How to make Chord correct Paper