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
IRISA-D1 - SYSTÈMES LARGE ÉCHELLE, Inria Rennes – Bretagne Atlantique
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
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00762627
Contributeur : Cédric Tedeschi <>
Soumis le : vendredi 7 décembre 2012 - 15:11:37
Dernière modification le : samedi 2 décembre 2017 - 09:36:13
Document(s) archivé(s) le : samedi 17 décembre 2016 - 22:58:41

Fichier

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

Identifiants

  • HAL Id : hal-00762627, version 1

Citation

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

Partager

Métriques

Consultations de la notice

352

Téléchargements de fichiers

462