Abstract FR:

Cette thèse traite le problème d'analyse et de conception des algorithmes de synchronisation non déterministes dans les systèmes répartis. Les algorithmes non-déterministes constituent une solution intéressante pour le problème de la synchronisation des horloges, ce qui est témoigné par l'intérêt qui leur a été porté pendant les dernières années. Les algorithmes de synchronisation non-déterministes utilisent des techniques statistiques ou probabilistes et permettent d'obtenir une meilleure précision par rapport aux algorithmes déterministes, le prix à payer étant la probabilité que le système ne réussisse pas à se synchroniser avec la précision souhaitée. Cette probabilité d'échec tend vers zéro avec le nombre de messages échangés et elle peut être réduite à une valeur aussi petite qu'on le souhaite avec un nombre de messages suffisamment grand. Malheureusement, l'évaluation des différentes propositions publiées dans la littérature est difficile, principalement à cause de l'inexistence d'une base commune pour établir les comparaisons. Nous proposons un modèle analytique pour le fonctionnement des algorithmes de synchronisation non-déterministes. Le but est de trouver une expression que le concepteur d'un système distribué puisse utiliser pour calculer le nombre de messages requis pour un certain algorithme, de façon à fournir la synchronisation avec la précision et la probabilité spécifiées. Ce résultat est la Condition de Garantie de Synchronisation, qui définit une condition suffisante qui garantit le succès de la synchronisation non-déterministe sous les conditions spécifiées. Cette condition est établie à partir de paramètres locaux d'un site et de paramètres du système qui sont facilement calculables, tels que le nombre de sites et les paramètres qui décrivent le délai comme une variable aléatoire. Les conditions sous-jacentes au modèle proposé sont vérifiées expérimentalement à l'aide d'une plate-forme basée sur le réseau CAN que nous avons développée. Le test des algorithmes sur cette plate-forme a permis de vérifier la validité des hypothèses qui sont associées au modèle.