Just-Right Consistency for massive geo-replicated storage

PhD Student: Sreeja Nair
Advisor: Marc Shapiro, Sorbonne-Université & Inria

Background

In distributed system design, strong consistency promotes correct applications, but is bad for availability because of frequent synchronisation. Reducing remote synchronisation enables high performance and scalability [1,3], but the weaker consistency is error-prone for developers. The Regal group has developed several technologies that reduce the gap between strong and weak consistency: (i) CRDTs, data types that encapsulate conflit resolution and are provably safe [7,8]; (ii) the Antidote massively-replicated database guarantees the strongest consistency model that is compatible with availability [2]; (iii) the CISE tool performs static analysis of an application to prove that it is correct above a weak consistency model [4,5,6].

Problem statement

Our new collaborative project RainbowFS proposes a “Just-Right Consistency” approach to developing geo-distributed applications, whereby an application pays only the consistency price that it strictly requires. The tools contributed by the project will prove that the application is safe, while at the same time ensuring that it is highly available and scalable, and will contribute to the rapid deployment and to the monitoring and analysis of system behaviour and performance. The project applies this approach to the design of a high performance, highly scalable, tunable geo-replicated file system. This includes three challenges:

To help the developer make correct choices in the safety-vs.-availability trade-off: with too much synchronisation the application is non-available, but with too little it is incorrect. Therefore, we shall develop static and dynamic analysis tools that verify whether consistency is sufficient for the application, and if not, that help the developer to fix the problem (either by weakening the application or strengthening the synchronisation).
To translate the resulting specification into a running, efficient, deployable application. We analyse consistency needs in a structured way, and develop tools for constructing, deploying, monitoring, analysing and debugging applications under the conflicting goals of safety and availability.
To validate our approach on a demanding application, an entreprise-grade, highly available, performant and scalable file system.

Research directions

Logics and tools for application co-design, extending our existing CISE logic and tool for proving the correctness of applications above weak consistency [4,5,6]. The logic should be extended to include transactional and non-causal models. The current prototype tool should be improved towards more automation, by extracting information from the application source, and by helping design a correct and efficient protocol (taking into account expert heuristics and experimental measurement). Finally, we wish tools to generate test scenarios.

The RainbowFS consortium

RainbowFS is funded by Agence Nationale de la Recherche (France). The partners are the Regal team of Inria and LIP6 (leader), ERODS team at CNRS-LIG ACMES group at Télécom SudParis, and Scality SA. It is due to start in the late Fall of 2016.

Bibliography

1: D. J. Abadi. Consistency tradeoffs in modern distributed database system design: CAP is only part of the story. IEEE Computer, 45 (2): 37-42, Feb. 2012.
2: D. D. Akkoorath, A. Z. Tomsic, M. Bravo, Z. Li, T. Crain, A. Bieniusa, N. Preguiça, and M. Shapiro. Cure: Strong semantics meets high availability and low latency. In Int. Conf. Distributed Comp. Sys. (ICDCS), p. 405-414, Nara, Japan, June 2016.
3: K. Birman, G. Chockler, and R. van Renesse. Toward a Cloud Computing research agenda. ACM SIGACT News, 40 (2): 68-80, June 2009.
4: A. Gotsman, H. Yang, C. Ferreira, M. Najafzadeh, and M. Shapiro. 'Cause I'm strong enough: Reasoning about consistency choices in distributed systems. In Symp. Principles of Prog. Lang. (POPL), pages 371-384, St. Petersburg, FL, USA, 2016.
5: M. Najafzadeh and M. Shapiro. Demo of the CISE tool, Nov. 2015.
6: M. Najafzadeh, A. Gotsman, H. Yang, C. Ferreira, and M. Shapiro. The CISE tool: Proving weakly-consistent applications correct. Rapport de Recherche RR-8870, Inria, Rocquencourt, France, Feb. 2016.
7: M. Shapiro, N. Preguiça, C. Baquero, and M. Zawirski. Conflict-free replicated data types. In Int. Symp. Stabilization, Safety, and Security of Dist. Sys. (SSS), volume 6976 of Lecture Notes in Comp. Sc., pages 386-400, Grenoble, France, Oct. 2011a. Springer-Verlag.
8: M. Shapiro, N. Preguiça, C. Baquero, and M. Zawirski. Convergent and commutative replicated data types. Bulletin of the European Association for Theoretical Computer Science (EATCS), (104): 67-88, June 2011.
9: M. Shapiro, M. Saeida Ardekani, and G. Petri. Consistency in 3D. In J. Desharnais and R. Jagadeesan, editors, Int.. Concurrency Theory (CONCUR), volume 59 of Leibniz Int. Proc. in Informatics (LIPICS), pages 3:1-3:14, Québec, Québec, Canada, Aug. 2016.

Marc.Shapiro =at= acm.org