Title: Concurrent Maintenance of Rings

Authors: Xiaozhou Li, Jayadev Misra, C. Greg Plaxton

Abstract:

  A central problem for structured peer-to-peer networks is topology
  maintenance, that is, how to properly update neighbor variables when
  membership changes (i.e., nodes join or leave the network, possibly
  concurrently). In this paper, we consider the maintenance of the
  ring topology, the basis of several peer-to-peer networks, in the
  fault-free environment. We design, and prove the correctness of,
  protocols that maintain a bidirectional ring under both joins and
  leaves. Our protocols update neighbor variables once a membership
  change occurs. Using an assertional proof method, we show that,
  although the ring topology may be tentatively disrupted during
  membership changes, our protocols eventually restore the ring
  topology once membership changes subside. Our protocols are simple
  and our proofs are rigorous and explicit.

Note:

  Due to time limitation, I will only present (but in detail) the first
  protocol of the paper and its manual proof. We are right now attempting
  an ACL2 proof of the first protocol.