NAJAFZADEH Mahsa

doctorant à Sorbonne Université
Équipe : REGAL
https://lip6.fr/Mahsa.Najafzadeh

Direction de recherche : Marc SHAPIRO

L’analyse et co-design des applications faiblement-cohérentes

Afin d’assurer disponibilité et réactivité, de nombreux systèmes distribués reposent sur des bases de données répliquées qui maintiennent des copies (répliques) des données sur différents serveurs. Un utilisateur peut accéder à une réplique locale et agir sans devoir se synchroniser avec les autres répliques. Ces accès locaux évitent les coûts liés aux latence réseau entre les répliques, et ne sont pas sujets à des fautes telles que la déconnexion des répliques. La cohérence constitue un défi important dans la mise en oeuvre des bases de données répliquées. La cohérence forte fournit un modèle d’accès séquentiel, familier aux développeurs d’applications, mais nécessite un ordre total, pour toutes les répliques, sur l’exécution des opéra- tions (réplication synchrone). A l’inverse, un modèle à cohérence faible, comme la cohérence à terme, guarantit des réponses immédiates, mais favorise l’apparition de bugs applicatifs, comme la divergence d’états ou la violation d’invariants. Les concepteurs de bases de données repliquées doivent faire un choix difficile entre une cohérence forte, qui guarantit une large gamme d’invariants applicatifs, mais qui est lente et fragile, et une réplication asynchrone, qui assure un bon niveau de disponibilité et de réactivité, mais laisse le programmeur face à de possibles anomalies liées à la concurrence. Pour résoudre ce dilemme, des bases de données commerciales et recherche fournissent une cohérence hybride qui permet au programmeur d’exiger une cohérence forte pour certaines opérations, et d’ainsi permettre une synchronisation. Cependant, utiliser des modèles de cohérence hybride est loin d’être trivial. Exiger une cohérence forte trop souvent peut affecter négativement les performances et la disponibilité, et l’exiger trop peu souvent peut causer des erreurs. Trouver le juste équilibre implique pour le programmeur d’appréhender le comportement de l’application confronté à la sémantique com- plexe du modèle de cohérence, prenant en compte quelles anomalies peuvent être évitées par un renforcement local de la cohérence, et quelles anomalies éviter pour assurer l’abscence d’erreur. Cette thèse étudie l’analyse et la mise en oeuvre d’une application et de la cohérence asso- ciée, de manière à assurer les invariants de cette application avec un minimum d’éxigences de cohérence. Les trois principales contributions de cette thèse sont :

  1. Nous proposons le premier outil d'analyse statique destiné à prouver la validité d'invariants d'applications de base de données à modèle de cohérence hybride.
  2. Nous présentons la mise en application de notre outil d'analyse dans le cadre de la conception d'un système de fichiers dont la sémantique permet un comportement similaire à POSIX et à un coût raisonnable.
  3. Nous proposons un ensemble de patterns utiles, susceptibles d'aider les développeurs d'application dans l'implémentation d'invariants les plus communs.

Soutenance : 22/04/2016

Membres du jury :

Mme.Carla Ferreirai, Universidade Nova de Lisboa [Rapporteur]
M.Vivien Quéma, Grenoble INP / ENSIMAG [Rapporteur]
M.Vianney Rancurel, Scality, Paris
M.Philippe Pucheral, University of Versailles Saint-Quentin en Yvelines
M.Pierre-Evariste Dagand, LIP6, Paris
Mme .Béatrice Bérard, LIP6, Paris
M. Pascal Molli, Université de Nantes
M. Marc Shapiro, LIP6, Paris

Date de départ : 19/08/2016

Publications 2013-2018