Soutenance de thèse de Nicolas Waldburger, équipe DEVINE team : Parameterized verification of distributed shared-memory systems

 

Title:  Parameterized verification of distributed shared-memory systems

Summary: Distributed systems consist in several computerized components (called processes) interacting with one another to perform a common task. An example of such a task is consensus, where all processes must agree on a common value. In this thesis, we are interested in shared-memory systems where the processes interact via reading from and writing to a shared memory. We do not work directly on distributed systems, but rather on models of such systems, and we consider questions related to the automated verification of these models. Our models are parameterized: the number of processes is not fixed beforehand and may be arbitrarily large, so that we are able to verify the system regardless of the number of participants. They enjoy some monotonicity property, called copycat property, which simplifies the analysis. Motivated by consensus algorithms from the literature, we consider a model where each process evolves incrementally in a number called round and where each round has its own set of registers. Also, we study the impact of a stochastic scheduler on this round-based model. Our approach is theoretical and we are mostly interested in analyzing our models and in classifying our problems of interest in terms of complexity.

 

-- Français --

Titre: Vérification paramétrée de systèmes distribués à mémoire partagée

Résumé: Les systèmes distribués sont constitués de plusieurs composantes informatisées (que nous appelons processus) qui interagissent pour accomplir une tâche commune. Un exemple de tâche est le consensus, où tous les processus doivent se mettre d’accord sur une valeur commune. Dans cette thèse, nous nous intéressons aux systèmes à mémoire partagée, où les processus interagissent en lisant et en écrivant dans une mémoire partagée. Nous ne travaillons pas directement sur des systèmes distribués, mais plutôt sur des modèles de ces systèmes, où nous considérons des questions de vérification automatique. Nos modèles sont paramétrés : le nombre de processus n’est pas fixé à l’avance et peut être arbitrairement grand, ce qui nous permet de vérifier le système pour tout nombre de participants. Cette hypothèse permet également des propriétés de monotonicité qui simplifient l’analyse. Notre modèle, inspiré par des algorithmes de consensus de la littérature, est à ronde : chaque processus évolue de manière incrémentale en un nombre appelé ronde, et où chaque ronde a sa propre mémoire partagée. Nous étudions de plus l’impact d’un ordonnanceur stochastique sur ce modèle à rondes. Notre approche est théorique et nous nous intéressons principalement à l’analyse de nos modèles et à la classification de nos problèmes en termes de classes de complexité.