微软在今天召开的Build开发者大会上发布了新的全局分布式数据库：Cosmos DB，微软技术院士达尔玛·舒克拉（Dharma Shukla）与我聊起该数据库时说：“我们希望这是未来的数据库，能够在今后延续几十年。”而对于舒克拉来说，这是一个始于七年前的项目，当时他开始建立原型，研究全局分布式数据库会是什么样子，微软经常喜欢将全局分布式称之为“全球规模”（planet-scale）。这个项目（当初名为“Project Florence”）最初变成了Azure的NoSQL数据库服务：DocumentDB，该数据库服务于2015年发布，现在演变成了Cosmos DB。

　　用舒克拉的话来说，相比DocumentDB所提供的功能，Cosmos DB“向前迈出了一大步”。DocumentDB提供的功能只是如今的Cosmos DB的一小部分，难怪知名IT网站ZDNet将Cosmos DB称为是DocumentDB的超集。DocumentDB实际上是存储Java对象标注（JSON）数据的数据库，而Cosmos DB覆盖的范围要广泛得多。它拓展了无索引数据库系统这个概念，增添了支持多种新型数据的功能，这让Cosmos DB拥有足够的灵活性，比如说足以充当图形数据库，或者充当键值数据库。对于期望存储较为传统的列式关系型数据的那些人来说，Cosmos DB还将提供支持那类数据的功能。

　　这一切都秉承这年头你与微软开发部门的人员交谈时，几乎免不了都会听到的这句口号：“我们想要满足开发人员的需要，无论他们在什么地方。”所以，虽然你也可以使用MongoDB API来访问DocumentDB中的数据，但是Cosmos DB还支持SQL表、Gremlin表和Azure表，开发团队计划在不远的将来发布一大批类似的驱动层和转换层。

　　舒克拉告诉我：“没有数据天生就是关系型数据。在现实世界中，没有人从模式（schema）方面来考虑――他们考虑图形，或者如果面对的是物联网设备，可能考虑JSON文档。我们想要确保，我们开发的系统有一个通用引擎，可以高效地处理不同的数据模型。”

　　考虑到其渊源，Cosmos DB在许多方面借鉴了DocumentDB，这不足为奇。其中一个方面就是拥有可调整的一致性模型（consistency model）。如果你平时不常考虑全局分布式数据库，那么一致性模型对你来说根本不是那么重要，但是大多数与之竞争的数据库系统（包括谷歌最近发布的Cloud Spanner，https://cloud.google.com/spanner/）只有两种一致性模型：强一致性（strong consistency）和最终一致性（eventual consistency）。比如说，直播，就强一致性而言，只要数据被写入到数据库，所有的不同节点（这些节点可能分布于全球各地的数据中心）都要先就一个新的值达成一致，之后新的值才出现在应用程序中。任何时刻，任何用户或节点都可以读到最近一次成功更新的副本数据。由于这种方法增添了延迟，这在性能方面显然存在着一些不足。最终一致性实际上是一种比较宽容的系统；所有节点并不同时更新，而是只有在一段时间没有任何最近的更新后，才就某个值达成一致。

　　图灵奖得主莱斯利·兰伯特（Leslie Lamport）对我说：“Cosmos DB不同寻常的地方在于，它提供了不同的一致性模型，那样用户可以在获得多强的一致性与承受多大的性能开销之间作一个取舍。”许多这些概念都离不开兰伯特的研究工作，他还开发了LaTeX文档准备系统（https://en.wikipedia.org/wiki/LaTeX），2001年加入了微软研究中心。Cosmos DB为不同的使用场景提供了三种不同类型的一致性。兰伯特解释道：“那种中间一致性保证机制之前就存在于人们为了编写论文而开发的学术系统。”Cosmos DB是最先商用化的提供这多种一致性模型的数据库系统之一。

　　比如说，对于Cosmos DB（以及之前的DocumentDB）而言，那意味着，你可以选择这种一致性模型：允许读取操作比写入操作只延后某一段时间（毫秒级），也可以选择这种一致性模型：专注于为某种特定的客户会话提供一致性（比如在类似Twitter的应用中），但是每个用户在同一时间（或者以完全一样的顺序）看到每次写入的数据又不是那么重要。

　　不过正如舒克拉特别指出，他在这里的想法是，开发一种可以延续几十年之久的数据库系统。为此，他还请来兰伯特教团队TLA+（）。兰伯特长期以来对于开发人员如何为应用软件编写规范有着特别浓厚的兴趣。TLA+实际上就是一种完全适用于此的正规语言。舒克拉对我说：“我们在2010年开始着手时，想开发一种经久不衰的系统。这就是微软眼里的未来数据库。我们努力确保为自己的工程团队赋予尽量严谨的理念……TLA+的魅力在于，它可以将这种严谨的设计理念灌输给工程师团队，以便树立很高的质量标准。”兰伯特特别指出，TLA+让你可以以一种完全正规的方式，做好系统的概要性设计――又由于它是以正规方式完成的，所以还可以检查正确性（客观地说，AWS及其他公司也使用TLA+为分布式系统编写规范，详见）。兰伯特补充道：“我倒不是想炫耀TLA+有多棒、我有多出色。TLA+之所以很棒，是因为它几乎完全基于数学。”