How to Make Chord Correct

"Using lightweight modeling to understand Chord" (Pamela Zave; ACM SIGCOMM Computer Communication Review, 42(2):50-57, April 2012) summarizes the results of modeling and analyzing the Chord ring-maintenance protocol with Alloy. The paper shows that no published version of Chord is correct, even when obvious bugs are fixed.

"Experiences with protocol description" (Pamela Zave; 1st International Workshop on Rigorous Protocol Engineering, Vancouver, Canada, October 2011) explains the nature of some of the flaws in the prior informal reasoning about Chord.

"How to make Chord correct" (Pamela Zave; submitted for publication, 2014) provides a specification of a correct version of Chord, and a proof of its correctness. In addition the paper provides a simple, necessary, and sufficient invariant, as well as interesting new insights into the workings of distributed systems that use ring-shaped data structures in large identifier spaces.

For those who wish to see and compare Alloy models of various versions:

For those who wish to see and compare Promela models (for the Spin model-checker) of various versions:

The new version of Chord that has been proven correct is in chordbase.pml and chordbase.c, with execution instructions in spindocu.txt.