Marrella ou la simulation guidée par les structures d'évènements premières
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
This report deals with algorithms applied to distributed systems, and more precisely with verification by simulation of distributed algorithms running on asynchronous networks. We use the model-checking approach : desired properties are checked on a graph that represents the whole set of executions of the system. It is well known that the main difficulty arises in the huge number of nodes of the graph. This is inherently connected to concurrency and non-determinism due to asynchronous communications. To cope with that problem, we propose two strategies the efficiency of which is due to the underlying model, that is prime event structures with binary conflicts. The first algorithm covers the graph by a tree; it is economic in the consideration that any state is constructed exactly once. The second algorithm, called CoMax, does not cover the graph but constructed a number of nodes that is sufficient for the detection of desired properties; it works by executing at once as many concurrent events that possible. We moreover show that this may be applied to a large class of distributed algorithms. The theoretical part of the work ends up in a concrete tool, our simulator Marrella, that has been developed in order to observe our strategies and to test their performances. The comparison of Marrella with other tools using known strategies technique is in favor of Marrella.
Abstract FR:
Cette thèse se situe dans le domaine de l'algorithmique événementielle discrète, et plus précisément dans le cadre de la vérification, par simulation, de l'algorithmique répartie sur réseau. Pour cela, on construit un système de transitions, un graphe étiqueté, représentant toutes les évolutions possibles de l'algorithme sur lequel sont vérifiées les propriétés attendues, approche connue sous le nom de model-checking. Mais cette construction se heurte à un écueil : le phénomène d' "explosion combinatoire du graphe", explosion due à l'indéterminisme (lié à l'asynchronisme des communications) et à l'indépendance (multipliant les entrelacements d'actions). Pour remédier à ce problème nous proposons deux stratégies de parcours efficaces fondées sur les propriétés des structures d'événements premières. La première, appelée Stratégie Arborescente recouvre le graphe par un arbre, évitant de reconstruire plusieurs fois un même état. La seconde, la Stratégie CoMax, couvre le graphe par un parcours partiel obtenu en exécutant "en parallèle" un ensemble maximal d'événements concurrents (i. E. Indépendants), parcours préservant la possibilité d'observer les propriétés stables. Nous montrons qu'une vaste classe d'algorithmes répartis engendrent des systèmes de transitions acycliques restreints (ou treillis bourgeonnants) que l'on sait associer à une structure d'événements. Nous pouvons alors appliquer nos stratégies à ces algorithmes. Ce travail théorique trouve son aboutissement dans un outil concret, le simulateur Marrella, développé pour mettre en oeuvre nos stratégies et évaluer leurs performances face aux procédés de réduction déjà connus, en particulier les méthodes d'ordre partiel de Godefroid et Wolper, Valmari. . . .