Formalization and Concretization of Ordered Networks

Laurence Rideau 1 Bernard Serpette 2 Cédric Tedeschi 3
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
2 INDES - Secure Diffuse Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
3 MYRIADS - Design and Implementation of Autonomous Distributed Systems
Inria Rennes – Bretagne Atlantique , IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
Abstract : Overlay networks have been extensively studied as a solution to the dynamic nature, scale and heterogeneity of large computing platforms, and are a fundamental layers of most existing peer-to-peer networks. The basic mechanism offered by an overlay network, is routing, i.e., the mechanism enabling the delivery of messages from any node to any other node in the network. On top of routing are built crucial functionalities of peer-to-peer networks, such as networks maintenance (nodes joining and leaving the network) and information distribution and retrieval. Over the years, different topologies and routing mechanisms have been proposed in literature. However, there is a lack of formal works unifying these different designs and establishing their correctness. This paper proposes a formal common basis, partially validated with the Coq theorem prover, with the nice property of only requiring the definition of a total order on the nodes. We investigate how such a basic design can be used to build deadlock/livelock-free algorithms for routing, node insertion, and node deletion in the fault-free environment. The genericity of our design is then explored through the construction of orders on nodes corre- sponding to different topologies commonly encountered in the peer-to-peer domain. To validate the methodology proposed, a simulator tool was developed. This tool is able, given the definition of an order and the definition of shortcuts, to simulate the corresponding overlay network and to explore its performance.
Document type :
[Research Report] RR-8172, INRIA. 2012, pp.22
Contributor : Cédric Tedeschi <>
Submitted on : Friday, December 7, 2012 - 3:11:37 PM
Last modification on : Saturday, September 17, 2016 - 1:38:56 AM


Files produced by the author(s)


  • HAL Id : hal-00762627, version 1



Laurence Rideau, Bernard Serpette, Cédric Tedeschi. Formalization and Concretization of Ordered Networks. [Research Report] RR-8172, INRIA. 2012, pp.22. <hal-00762627>




Record views


Document downloads