Modern distributed systems often partition and replicate the data they manage across a large number of nodes and a wide geographical span. A key challenge that such systems have to address is maintaining data consistency in the presence of concurrent modifications at different nodes and despite inevitable failures. There is a spectrum of consistency models that a system can provide, and navigating it is far from trivial. Strong consistency models give the programmer the illusion that all nodes are always in sync, but hinder system scalability. In contrast, weak consistency models expose the programmer to the effects of replication in exchange for more scalable implementations. We will present modern methods for formally specifying consistency models of distributed systems and reasoning about how their choice affects system correctness.
References
- Sebastian Burckhardt. Principles of Eventual Consistency. Now Publishers, 2014.
- Marc Shapiro, Nuno Preguiça, Carlos Baquero, Marek Zawirski. A comprehensive study of Convergent and Commutative Replicated Data Types. INRIA Technical Report, 2011.
- Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. Replicated data types: specification, verification, optimality. POPL'14.
- Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. 'Cause I'm strong enough: reasoning about consistency choices in distributed systems. POPL'16.
Slides and exercises