Supervision : Marc SHAPIRO
Designing safe and highly available distributed applications
Designing distributed applications involves a fundamental trade-off between safety and performance as described by CAP theorem. We focus on the cases where safety is the top requirement.
For the subclass of state-based distributed systems, we propose a proof methodology for establishing that a given application maintains a given invariant. Our approach allows reasoning about individual operations separately. We demonstrate that our rules are sound, and with a mechanized proof engine, we illustrate their use with some representative examples.
For conflicting operations, the developer can choose between conflict resolution or coordination. We present a novel replicated tree data structure that supports coordination-free concurrent atomic moves, and arguably maintains the tree invariant. Our analysis identifies cases where concurrent moves are inherently safe. For the remaining cases we devise a conflict resolution algorithm. The trade-off is that in some cases a move operation "loses".
Given the coordination required by some application for safety, it can be implemented in many different ways. Even restricting to locks, they can use various configurations, differing by lock granularity, type, and placement. The performance of each configuration depends on workload. We study the "coordination lattice", i.e., design space of lock configurations, and define a set of metrics to systematically navigate them.
Defence : 07/01/2021 - 09h30 - Campus Jussieu, salle Jacques Pitrat (25-26/105) - https://youtu.be/qcn6Lrhc6RE
Jury members :
M Carlos Baquero, Associate professor, Universidade do Minho [Rapporteur]
M Éric Gressier-Soudan, Professeur, Conservatoire National des Arts et Métiers [Rapporteur]
Mme Béatrice Bérard, Professeur, Sorbonne Université
Mme Carla Ferreira, Associate professor, Universidade Nova de Lisboa
M Bradley King, Co-founder & Field CTO, Scality
M Martin Kleppmann, Senior Research Associate and Affiliated Lecturer, University of Cambridge
M Gustavo Petri, Researcher, Arm Cambridge
M Marc Shapiro, Distinguished Research Scholar (Emeritus) Sorbonne Université-Inria
- S. Nair : “Designing safe and highly available distributed applications”, thesis, defence 07/01/2021, supervision Shapiro, Marc (2021)
- S. Nair, F. Meirim, M. Pereira, C. Ferreira, M. Shapiro : “A coordination-free, convergent, and safe replicated tree”, 36 pages (2021)
- S. Nair, G. Petri, M. Shapiro : “Proving the safety of highly-available distributed objects”, ESOP 2020 - 29th European Symposium on Programming, Dublin, Ireland (2020)
- S. Nair, G. Petri, M. Shapiro : “Proving the safety of highly-available distributed objects (Extended version)”, (2020)
- S. Nair, G. Petri, M. Shapiro : “Invariant Safety for Distributed Applications”, Workshop on Principles and Practice of Consistency for Distributed Data (PaPoC), Workshop on Principles and Practice of Consistency for Distributed Data (PaPoC), Dresden, Germany (2019)
- S. Nair, M. Shapiro : “Improving the "Correct Eventual Consistency" Tool”, (2018)
- S. Nair : “Evaluation of the CEC (Correct Eventual Consistency) Tool”, 1-27 pages (2017)