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
- M. Najafzadeh, M. Shapiro, P. Eugster : “Co-Design and Verification of an Available File System”, VMCAI 2018 - International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 10747, Lecture Notes in Computer Science, Los Angeles, CA, United States, pp. 358-381, (Springer) (2018)
- M. Najafzadeh : “The Analysis and Co-design of Weakly-Consistent Applications”, thesis, defence 04/22/2016, supervision Shapiro, Marc (2016)
- M. Najafzadeh, A. Gotsman, H. Yang, C. Ferreira, M. Shapiro : “The CISE Tool: Proving Weakly-Consistent Applications Correct”, PaPoC 2016 - 2nd Workshop on the Principles and Practice of Consistency for Distributed Data, Londres, United Kingdom, (ACM) (2016)
- V. Balegas, Ch. Li, M. Najafzadeh, D. Porto, A. Clement, S. Duarte, C. Ferreira, J. Gehrke, J. Leitão, N. Preguiça, R. Rodrigues, M. Shapiro, V. Vafeiadis : “Geo-Replication: Fast If Possible, Consistent If Necessary”, Bulletin of the Technical Committee on Data Engineering, vol. 39 (1), IEEE Data Engineering Bulletin, Special Issue on Data Consistency across Research Communities, pp. 12, (IEEE Computer Society) (2016)
- M. Najafzadeh, A. Gotsman, H. Yang, C. Ferreira, M. Shapiro : “The CISE Tool: Proving Weakly-Consistent Applications Correct”, (2016)
- A. Gotsman, H. Yang, C. Ferreira, M. Najafzadeh, M. Shapiro : “’Cause I’m Strong Enough: Reasoning about Consistency Choices in Distributed Systems”, Symposium on Principles of Programming Languages, Saint Petersburg, FL, United States, pp. 371–384 (2016)
- M. Shapiro, M. Najafzadeh : “CISE Safety Tool”, (2015)
- V. Balegas, S. Duarte, C. Ferreira, R. Rodrigues, M. Najafzadeh, M. Shapiro, N. Preguiça : “Towards Fast Invariant Preservation in Geo-replicated Systems”, Operating Systems Review, vol. 49 (1), ACM SIGOPS Operating Systems Review - Special Issue on Repeatability and Sharing of Experimental Artifacts, pp. 5, (Association for Computing Machinery) (2015)
- V. Balegas, S. Duarte, C. Ferreira, R. Rodrigues, N. Preguiça, M. Najafzadeh, M. Shapiro : “Putting Consistency back into Eventual Consistency”, European Conference on Computer Systems (EuroSys), Bordeaux, France, pp. 6:1-6:16, (ACM) (2015)
- V. Balegas, M. Najafzadeh, S. Duarte, C. Ferreira, M. Shapiro, R. Rodrigues, N. Preguiça : “Putting the Consistency Back Into Eventual Consistency”, Large-Scale Distributed Systems and Middleware (LADIS) 2014, Large-Scale Distributed Systems and Middleware (LADIS) 2014, Cambridge, United Kingdom (2014)
- V. Balegas, N. Preguiça, S. Duarte, C. Ferreira, R. Rodrigues, M. Najafzadeh, M. Shapiro : “The Case for Fast and Invariant-Preserving Geo-Replication”, SRDSW 2014 - 33rd International Symposium on Reliable Distributed Systems Workshops, Reliable Distributed Systems Workshops (SRDSW), 2014 IEEE 33rd International Symposium on, Nara, Japan, pp. 5, (IEEE) (2014)
- M. Najafzadeh, M. Shapiro, V. Balegas, N. Preguiça : “Improving the scalability of geo-replication with reservations”, DCC 2013 : Workshop on Distributed Cloud Computing, Dresden, Germany, pp. 441-445, (IEEE Computer Society) (2013)