No description available.

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. la cohérence constitue un défi important dans la mise en oeuvre des bases de données répliquées. 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.cette thèse étudie l'analyse et la mise en oeuvre d'une application et de la cohérence associée, de manière à assurer les invariants de cette application avec un minimum d'exigences 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 résonable. 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. / Distributed databases take advantage of replication to bring data close to the client, and to always be available. the primary challenge for such databases is to ensure consistency. recent research provide hybrid consistency models that allow the database supports asynchronous updates by default, but synchronisation is available upon request. to help programmers exploit the hybrid consistency model, we propose a set of useful patterns,proof rules, and tool for proving integrity invariants of applications. in the first part, we study a sound proof rule that enables programmers to check whether the operations of a given application semantics maintain the application invariants under a given amount of parallelism. we have developed a smt-based tool that automates this proof, and verified several example applications using the tool. in the second part, we apply the above methodology to the design of a replicated file system.the main invariant is that the directory structure forms a tree. we study three alternative semantics for the file system. each exposes a different amount of parallelism, and different anomalies. using our tool-assisted rules, we check whether a specific file system semantics maintains the tree invariant, and derive an appropriate consistency protocol. in the third part of this thesis, we present three classes of invariants: equivalence, partial order, and single-item generic. each places some constraints over the state. each of these classes maps to a different storage-layer consistency property: respectively, atomicity, causal ordering, or total ordering.