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. Not one of the claimed invariants is actually an invariant.

"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 reasoning about Chord. Such flaws are typical when there is no formal specification or automated checking.

"How to make Chord correct (using a stable base)" (Pamela Zave; arXiv, February 2015) provides a specification of a correct version of Chord, and gives a proof of its correctness. The proof is based on a simple, sufficient, and arguably necessary inductive invariant.

This work has also led to "A practical comparison of Alloy and Spin" (Pamela Zave; Formal Aspects of Computing 27: 239-253, 2015).

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: