Reasoning about identifier spaces: How to make Chord correct

TL;DR

This paper establishes the first formal correctness specifications and proofs for the Chord DHT, demonstrating how to ensure its ring-maintenance protocol is correct under original assumptions.

Contribution

It provides the first correct operation specification, an inductive invariant, and two independent correctness proofs for Chord's ring-maintenance protocol.

Findings

Correctness of Chord can be formally established.

Two independent proofs validate Chord's correctness.

Automated analysis confirms correctness for bounded network sizes.

Abstract

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.