PhD graduated
Team : REGAL
Departure date : 08/19/2016

Supervision : Marc SHAPIRO

The Analysis and Co-design of Weakly-Consistent Applications

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.

Defence : 04/22/2016

Jury members :

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

Departure date : 08/19/2016

2013-2018 Publications

Mentions légales
Site map