"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 seven claimed invariants is actually an invariant.

A correct version of Chord is documented in "How to make Chord correct" (Pamela Zave; submitted for publication, 2015). This paper also includes examples explaining why original Chord is incorrect, a necessary and sufficient inductive invariant, and a detailed presentation of the proof of correctness.

The following Alloy models include the formal specification of correct Chord, the invariant, and all proof steps.

- correctChord3.als allows successor lists of any length. The length parameter in the file is set to 3.
- correctChord2.als is hard-coded for successor lists of length 2. It is easier to read than the general version.

"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 of a protocol.

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 interested in the comparison, chordfull.als is the model of the original Chord protocol used in the first paper.

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

- A version similar to the original, but with many bugs fixed, is chordbestccr.pml and chordbestccr.c, with execution instructions in spindocu.txt.
- A version of Chord that has been proven correct is in chordbase.pml and chordbase.c, with execution instructions in spindocu.txt. In this model concurrency has been restricted somewhat.