Dr. TLA+ Series - TLA+ specifications of the consistency guarantees provided by Cosmos DB (Murat Demirbas)
November 01, 2018 - 10-11:30am PST
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.
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.
see azure-cosmos-tla