Active and Concurrent Maintenance of a Structured Peer-to-Peer Network Topology

A central problem for structured peer-to-peer networks is topology maintenance, that is, how to properly update neighbor variables when nodes join and leave the network, possibly concurrently. In this paper, we present a protocol that maintains Ranch, a structured peer-to-peer network topology con- sisting of multiple rings. The protocol handles both joins and leaves concurrently and actively (i.e., neighbor variables are updated once a join or a leave occurs). We use an assertional method to prove the correctness of the protocol, that is, we first come up with a global invariant and then show that ev- ery action of the protocol preserves the invariant. The protocol is simple and the proof is rigorous and explicit.