en fr The Analysis and Co-design of Weakly-Consistent Applications Analyse et co-conception dapplications faiblement cohérentes Reportar como inadecuado

en fr The Analysis and Co-design of Weakly-Consistent Applications Analyse et co-conception dapplications faiblement cohérentes - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LIP6 - Laboratoire d-Informatique de Paris 6 2 Regal - Large-Scale Distributed Systems and Applications LIP6 - Laboratoire d-Informatique de Paris 6, Inria de Paris

Abstract : 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. The inherent trade-off between consistency, performance, and availability represents a fundamental issue in design of the replicated database serving applications with integrity rules. 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. The main goal of this thesis is to co-design the application and the associated consistency in order to ensure application invariants with minimal consistency requirements.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. A successful analysis proves that a given program will maintain its integrity invariants. If not, the tool provides a counter-example, which the program developer can leverage to adjust the program design, either by weakening application semantics, and-or by adding concurrency control, in order to disallow toxic concurrency.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. Our co-design approach is able to remove coordination for the most common operations, while retaining a semantics reasonably similar to POSIX.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. Given a class of invariant, we introduce a set of common patterns where synchronisation is not necessary i.e., nothing bad happens for any arbitrary order of operation executions. We also identify patterns where synchronisation is necessary, but can be relaxed in a disciplined manner.

Résumé : xxxx

en fr

Keywords : Replication and consistency Weak consistency Correctness of distributed systems

Mots-clés : xxxx

Autor: Mahsa Najafzadeh -

Fuente: https://hal.archives-ouvertes.fr/


Documentos relacionados