[Dr. TLA+ Series] TLA+ specifications of the consistency guarantees provided by Cosmos DB (Murat Demirbas)

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

Welcome to a new episode of the Dr. TLA+ Series:

Dr. TLA+ Series - TLA+ specifications of the consistency guarantees provided by Cosmos DB (Murat Demirbas)

Time

November 01, 2018 - 10-11:30am PST

Abstract

Microsoft Azure Cosmos DB provides 5 well defined operation consistency properties to the clients: strong consistency, bounded staleness, session consistency, consistent prefix, and eventual consistency. Here we provide client-centric TLA+ specifications of these properties to help the users understand the consistency guarantees provided to them. We refrain from discussing the models for Cosmos DB internals as that is not very useful/relevant for the Cosmos DB users.

Bio

Murat Demirbas is a Professor of Computer Science & Engineering at University at Buffalo, SUNY. He is currently on sabbatical with the Microsoft Azure Cosmos DB team. Murat received his Ph.D. from The Ohio State University in 2004 and did a postdoc at the Theory of Distributed Systems Group at MIT in 2005. His research interests are in distributed and networked systems and cloud computing. Murat received an NSF CAREER award in 2008, UB Exceptional Scholars Young Investigator Award in 2010, UB School of Engineering and Applied Sciences Senior Researcher of the Year Award in 2016. He maintains a popular blog on distributed systems at http://muratbuffalo.blogspot.com.

Spec

See Azure-Cosmos-tla

Media

  * live streaming <https://meet.lync.com/microsoft/makuppe/s74g7zkl>