论文地址：最终一致性的云类型——Burckhardt等人。2012年

    为云存储、同步和断开连接的操作提供良好的编程抽象对于在今天和明天的移动设备上加速有用的和新颖的应用程序的生产似乎至关重要。

    本文提出了一个基于云类型（可以与编程语言集成）的模型。程序员专注于声明数据结构和访问它们的客户机代码：

    程序员使用特殊的云类型声明他们希望共享的数据。这些数据在所有设备之间自动共享，并自动保存在本地存储和云存储中。我们的云类型包括简单类型（云整数、云字符串）和结构化类型（云数组、云实体）。由于云类型是精心选择的，可以在并发修改下进行可预测的行为，因此冲突解决是自动的，开发人员不需要编写特殊的代码来处理合并。

    然后，系统使用修订图来保证云类型的最终一致性：

    从概念上讲，云存储主版本，而设备维护定期同步的本地版本。修订图让人想起源代码管理系统，并为推理多个版本和最终一致性提供了极好的直觉。

    云类型类似于CRDTs，因为它们将最终一致数据类型的使用与实现分离开来。在将云类型与CRDTs进行比较时，作者可以这样说：

    CRDTs可以用作云类型（如[13]中提出的观测移除集所示）。然而，我们不知道如何将单个crdt组合成一个更大的模式。此外，CRDTs只支持交换操作，而我们的方法支持非交换操作，同时仍然实现最终的一致性。此外，我们在同一框架中支持更强的同步原语，如flush（如果需要）。

    正如我们昨天所研究的，云类型被实现为fork-join自动化（FJ-QUA）。例如，这就是CInt类型的云类型FJ-QUA的行为方式：

    对于云整数，我们支持get和set操作来读取和写入当前值以及add。在状态中，我们存储三个值：一个布尔值，指示当前修订是否执行了任何设置操作、一个基值和一个偏移量。在fork上，布尔值重置，基值设置为当前值，偏移设置为零。添加操作只更改偏移量，而设置操作将布尔值设置为true，设置基值，然后重置偏移量。在连接时，我们假设连接的修订的值（如果它执行了一个集合）或添加其偏移量（否则）。

    对于CString：

    对于云字符串，我们支持读取和写入当前值的get和set操作，以及条件操作setIfEmpty。在该状态下，我们记录当前值以及它是否已被写入（wr）、已被写入（wr）或已被有条件写入（cond）。只有当当前值为空且合并时重复此测试时，条件写入才会成功。

    云类型语言还支持数组、集合和实体。事实证明，云类型程序的完整状态本身可以建模为FJ QUA：

    值得注意的是，完全状态FJA操作本身是可交换的。唯一不可交换的操作是在实现云类型的FJAs中。此属性使得使用数组和实体非常自然，并且不会引入意外的冲突解决方案。此外，我们的设计非常小心，使完整的状态FJA相对于云类型实现能够完全模块化实现。在某种程度上，这种结构使得单一的参数化、可重用的云存储和同步实现成为可能。任何模式和云类型的任何扩展都可以支持，而无需进一步更改。

    客户端编程语言包括划分事务的屈服（根据最终一致的事务论文），以及在需要更强的同步性时的额外刷新操作。

    最终的一致性并不总是足够的。有些问题，如在飞机上预定座位，或从银行账户取款，涉及的资源有限，需要真正的仲裁。在这种情况下，我们必须建立服务器连接并等待响应…刷新时，执行块直到

    • （1）所有本地更新都应用到主修订版，以及
    • （2）结果对本地修订版可见。

    文中给出了全云类型语言的语法和语义。还定义了一个具有多个客户端和弹性服务器池的可操作的整个系统模型。这遵循了我们昨天看到的总体蓝图。一个复杂的问题是，确保遵守最终一致的事务（带有修订图）所需的联接规则/条件（joiner必须位于派生被联接方的fork的下游）。这是通过引入整数来解决的。

    为了确保这种情况，我们为服务器和客户机分配轮号，并使用轮图（矢量时钟的一种形式）来确定合格性（通过确定哪些分叉在可见的历史记录中）
    客户机和服务器从第0轮开始，但在第1轮中开始（并永远保留）的主修订版除外。

    在每个fork之后，客户机或服务器的整数将递增。

    作者的结论是：

    为云存储、同步和断开连接的操作提供良好的编程抽象，对于在当今和未来的移动设备上加快有用的和新颖的应用程序的生产似乎至关重要。在本文中，我们提供了一个坚实的基础，通过使用自动同步的云数据类型，可以使用索引数组和实体组成更大的数据模式来构建这样的编程抽象。我们提出的设计允许一次性实现这样一个系统的所有困难部分（云服务、本地持久性、缓存、冲突解决和同步），同时保证最终的一致性。