一句话：提出 Carol 语言，利用一致性卫与精化类型，使复制数据存储的操作可模块化、顺序地编程与验证。
复制数据存储的操作开发与验证通常需要同时考虑所有操作对之间的并发交互，难以模块化和顺序推理。本文提出 Carol——一种带精化类型的复制数据存储编程语言。其核心概念是一致性卫（consistency guard）：一个二状态谓词，关联操作所见的本地存储与其更新最终可能应用到的假想远程存储；程序员借此声明精确的一致性需求。对程序员与精化类型检查器而言，卫表现为普通的数据前置条件，从而支持模块化、顺序化的推理；对分布式运行时而言，卫则表现为一致性控制指令。作者实现并评估了 Carol 系统的两部分：（1）将卫静态翻译为运行时协调动作的算法；（2）可执行任意 Haskell DSL 操作的网络副本运行时，并遵循 Carol 语言语义。
We introduce Carol, a refinement-typed programming language for replicated data stores. The salient feature of Carol is that it allows programming and verifying replicated store operations modularly , without consideration of other operations that might interleave, and sequentially , without requiring reference to or knowledge of the concurrent execution model. This is in stark contrast with existing systems, which require understanding the concurrent interactions of all pairs of operations when developing or verifying them. The key enabling idea is the consistency guard , a two-state predicate relating the locally-viewed store and the hypothetical remote store that an operation’s updates may eventually be applied to, which is used by the Carol programmer to declare their precise consistency requirements. Guards appear to the programmer and refinement typechecker as simple data pre-conditions, enabling sequential reasoning, while appearing to the distributed runtime as consistency control instructions. We implement and evaluate the Carol system in two parts: (1) the algorithm used to statically translate guards into the runtime coordination actions required to enforce them, and (2) the networked-replica runtime which executes arbitrary operations, written in a Haskell DSL, according to the Carol language semantics.
@article{paperbot591,
title = {Sequential programming for replicated data stores},
author = {Nicholas V. Lewchenko and Arjun Radhakrishna and Akash Gaonkar and Pavol Černý},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341710}
}