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
Résumé : Les réseaux d'overlays ont été proposés comme une solution à la nature hétérogène et dy- namique des plates-formes de calcul à large échelle. Ils sont une couche fondamentale de beau- coup de réseaux pair-à-pair existants. Le mécanisme de base offert par un réseau d'overlay est le routage, c'est-à-dire le mécanisme permettant l'acheminement d'un message depuis n'importe quel nœud du réseau vers n'importe quel autre. Au-dessus du routage, on peut construire des fonctionnalités telles que la maintenance de la connexité du réseau (en présence de dynamicité) et la distribution et la recherche d'information. Différentes topologies et mécanismes de routage ont été proposés dans la littérature. Toute- fois, peu de travaux plus formels unifiant ces différentes propositions, et établissant plus formelle- ment leur correction ont été proposés. Ce rapport présente une base formelle commune, partiellement validée avec l'assistant de preuve Coq. En particulier, la construction proposée ne suppose que la présence d'un ordre total sur les nœuds. Nous montrons comment cette seule hypothèse peut être suffisante pour construire des algorithmes sans deadlocks ni livelocks pour router, insérer des nœuds, et supprimer des nœuds dans un environnement non sujet aux fautes. La généricité de notre approche est explorée à travers la construction d'ordres au-dessus de topologies fréquemment rencontrées dans les systèmes pair-à-pair. Afin de valider la méthode proposée, un outil de simulation a été développé. Ce simulateur prend en entrée la définition d'un ordre et des raccourcis du réseau et rend un ensemble d'indicateurs de performances de la topologie ainsi construite.
Type de document :
Rapport
[Research Report] RR-8172, INRIA. 2012, pp.22


https://hal.inria.fr/hal-00762627
Contributeur : Cédric Tedeschi <>
Soumis le : vendredi 7 décembre 2012 - 15:11:37
Dernière modification le : jeudi 20 octobre 2016 - 11:34:27

Fichier

RR-8172.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00762627, version 1

Collections

Citation

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

Exporter

Partager

Métriques

Consultations de
la notice

229

Téléchargements du document

381