Understanding Inconsistency in Azure Cosmos DB with TLA+

TL;DR

This paper presents a formal specification of Azure Cosmos DB's user-visible behaviors using TLA+, clarifying semantics, identifying issues, and improving reliability for dependent Microsoft services.

Contribution

It introduces a simplified, comprehensive formal specification of Cosmos DB's semantics that uncovers previously misunderstood behaviors and informs improvements in documentation and system reliability.

Findings

Identified inconsistencies in Cosmos DB's documentation

Raised issues leading to documentation updates

Provided a solution to a major outage

Abstract

Beyond implementation correctness of a distributed system, it is equally important to understand exactly what users should expect to see from that system. Even if the system itself works as designed, insufficient understanding of its user-visible semantics can cause bugs in its dependencies. By focusing a formal specification effort on precisely defining the expected user-facing behaviors of the Azure Cosmos DB service at Microsoft, we were able to write a formal specification of the database that was significantly smaller and conceptually simpler than any other specification of Cosmos DB, while representing a wider range of valid user-observable behaviors than existing more detailed specifications. Many of the additional behaviors we documented were previously poorly understood outside of the Cosmos DB development team, even informally, leading to data consistency errors in Microsoft products that depend on it. Using this model, we were able to raise two key issues in Cosmos DB's public-facing documentation, which have since been addressed. We were also able to offer a fundamental solution to a previous high-impact outage within another Azure service that depends on Cosmos DB.