Welcome to a new episode of the Dr. TLA+ Series:
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
* live streaming <https://meet.lync.com/microsoft/makuppe/s74g7zkl>