4 ms·

Designed with TLA+! :D Small interview with Leslie Lamport: https://techcrunch.com/2017/05/10/with-cosmos-db-microsoft-wants-to-build-one-database-to-rule-them

Designed with TLA+! :D Small interview with Leslie Lamport: https://techcrunch.com/2017/05/10/with-cosmos-db-microsoft-wants-to-build-one-database-to-rule-them-all/ https://techcrunch.com/2017/05/10/with-cosmos-db-microsoft-w... Hope Cosmos team releases a whitepaper on their experiences with the language. I'd heard snatches of gossip here and there that TLA+ was used inside Cosmos, but no concrete details. edit: apparently there's also a video of Lamport talking about this https://www.youtube.com/watch?v=L_PPKyAsR3w https://www.youtube.com/watch?v=L_PPKyAsR3w

dmix 9y ago
The effort to formalize the database was apparently led by: > Leslie Lamport the Turing Award winner whose work underpins many of these concepts (and who also wrote the LaTeX document preparation system) and who joined Microsoft Research in 2001 Quote about TLA+: > As Shukla noted, though, his idea here was to build a database system that could last decades. To do this, he also brought in Lamport to teach the team TLA+. Lamport has long had a special interest in how developers spec out their applications. TLA+ is essentially a formal language for doing just that. “When we started out in 2010, we wanted to build a system — a lasting system. This was the database of the future for Microsoft,” Shukla told me. “We try to apply as much rigor to our engineering as we possibly can. […] TLA+ has been wonderful in getting that level of rigor in a team of engineers to set the bar high for quality.” TLA+, Lamport noted, allows you to do the high-level design of a system in a completely formal way — and because it’s done formally, it can be checked for correctness, too (and to be fair, AWS and others also use TLA+ to spec out their distributed systems). “I don’t want to give the impression that TLA+ is great and I’m brilliant. It’s great because it’s almost entirely based on mathematics,” Lamport added.
OriginalJGC 9y ago
Here is a longer version with Dr. Lamport with more details https://www.youtube.com/watch?v=L_PPKyAsR3w&feature=youtu.be https://www.youtube.com/watch?v=L_PPKyAsR3w&feature=youtu.be
Quiark 9y ago
Wow, that's cool. TLA+ is the same formalism that Amazon uses to verify (some of) their cloud services.
dharmashuklaMS 9y ago
Cosmos DB codebase consists of multi-million lines of C++ code. It is fully asynchronous and like all large scale (stateful) distributed systems, it is also extremely complex. The database engine of Cosmos DB (including the b-tree and the log structured storage engine) is fully latch free; the engine, resource governance subsystem, global distribution infrastructure, partition management etc -- are all deeply integrated. Each of these subsystems have extremely complex state machines which are hard to describe with the required degree of precision using the English language. Any correctness bug that gets introduced because of lack of precision, can potentially lead to data loss, corruption, partial or complete failures of the entire service. This is where TLA+ comes in. Background: Dr. Leslie Lamport's work has been a constant source of inspiration for the Cosmos DB team. A few of the engineers on the team had learnt TLA+ initially on their own and started seeing its benefits. Subsequently, other members of the team started applying it as well. Leslie had also taught a fantastic class on TLA+ (across Microsoft), which engineers on the Cosmos DB team attended. It was a wonderful, once in a lifetime opportunity for the team to learn TLA+ from Leslie. To be clear, Leslie personally didn't write any of the TLA+ specs for Cosmos DB. It was Cosmos DB engineers who wrote the TLA+ specs to specify & verify the design (incl. consistency models). The net result is that TLA+ made Cosmos DB a more robust system, which is crucial to offer strict and comprehensive SLAs encompassing availability, consistency, throughput and latency at the 99th percentile. Further, writing TLA+ specs for the five consistency models which we have exposed (as well as many that we have experimented, internally) enabled us to precisely define the semantics for each of the consistency models. This in-turn enables developers building apps on top of Cosmos DB, to rely on the well-defined semantics. Hope this is helpful.
- ahelwer 9y ago
  Thanks, Dharma! I probably actually TA'd the TLA+ class which your engineers attended ;) Still hope you write a whitepaper. The AWS paper is super valuable when making the case for TLA+ use in industry.

dmix 9y ago

The effort to formalize the database was apparently led by: > Leslie Lamport the Turing Award winner whose work underpins many of these concepts (and who also wrote the LaTeX document preparation system) and who joined Microsoft Research in 2001 Quote about TLA+: > As Shukla noted, though, his idea here was to build a database system that could last decades. To do this, he also brought in Lamport to teach the team TLA+. Lamport has long had a special interest in how developers spec out their applications. TLA+ is essentially a formal language for doing just that. “When we started out in 2010, we wanted to build a system — a lasting system. This was the database of the future for Microsoft,” Shukla told me. “We try to apply as much rigor to our engineering as we possibly can. […] TLA+ has been wonderful in getting that level of rigor in a team of engineers to set the bar high for quality.” TLA+, Lamport noted, allows you to do the high-level design of a system in a completely formal way — and because it’s done formally, it can be checked for correctness, too (and to be fair, AWS and others also use TLA+ to spec out their distributed systems). “I don’t want to give the impression that TLA+ is great and I’m brilliant. It’s great because it’s almost entirely based on mathematics,” Lamport added.

OriginalJGC 9y ago

Here is a longer version with Dr. Lamport with more details https://www.youtube.com/watch?v=L_PPKyAsR3w&feature=youtu.be https://www.youtube.com/watch?v=L_PPKyAsR3w&feature=youtu.be

Quiark 9y ago

Wow, that's cool. TLA+ is the same formalism that Amazon uses to verify (some of) their cloud services.

dharmashuklaMS 9y ago

Cosmos DB codebase consists of multi-million lines of C++ code. It is fully asynchronous and like all large scale (stateful) distributed systems, it is also extremely complex. The database engine of Cosmos DB (including the b-tree and the log structured storage engine) is fully latch free; the engine, resource governance subsystem, global distribution infrastructure, partition management etc -- are all deeply integrated. Each of these subsystems have extremely complex state machines which are hard to describe with the required degree of precision using the English language. Any correctness bug that gets introduced because of lack of precision, can potentially lead to data loss, corruption, partial or complete failures of the entire service. This is where TLA+ comes in. Background: Dr. Leslie Lamport's work has been a constant source of inspiration for the Cosmos DB team. A few of the engineers on the team had learnt TLA+ initially on their own and started seeing its benefits. Subsequently, other members of the team started applying it as well. Leslie had also taught a fantastic class on TLA+ (across Microsoft), which engineers on the Cosmos DB team attended. It was a wonderful, once in a lifetime opportunity for the team to learn TLA+ from Leslie. To be clear, Leslie personally didn't write any of the TLA+ specs for Cosmos DB. It was Cosmos DB engineers who wrote the TLA+ specs to specify & verify the design (incl. consistency models). The net result is that TLA+ made Cosmos DB a more robust system, which is crucial to offer strict and comprehensive SLAs encompassing availability, consistency, throughput and latency at the 99th percentile. Further, writing TLA+ specs for the five consistency models which we have exposed (as well as many that we have experimented, internally) enabled us to precisely define the semantics for each of the consistency models. This in-turn enables developers building apps on top of Cosmos DB, to rely on the well-defined semantics. Hope this is helpful.

ahelwer 9y ago
Thanks, Dharma! I probably actually TA'd the TLA+ class which your engineers attended ;) Still hope you write a whitepaper. The AWS paper is super valuable when making the case for TLA+ use in industry.