论因果一致性
On Verifying Causal Consistency
摘要：
因果一致性是数据结构分布式实现中最常用的一致性准则之一。它确保操作在所有站点根据其因果优先级执行。我们解决的问题，自动验证是否执行一个数据结构的实现因果一致。我们考虑两个问题：（1）检查单个执行是否是因果一致的，这与开发测试和缺陷发现算法相关，以及（2）验证实现的所有执行是否是因果一致的。我们证明了第一个问题是NP完全的。这甚至适用于读写内存抽象，这是许多现代分布式系统的构建块。实际上，这样的系统通常将数据存储在键值存储中，键值存储是读写存储器抽象的实例。此外，我们证明，令人惊讶的是，第二个问题是不可判定的，这再次举行，即使是读写内存抽象。然而，我们表明，对于读写内存抽象，如果实现是数据独立的，即，它们的行为不依赖于在每个时刻写入或读取的数据值，这是一个现实的假设。
英文摘要：
Causal consistency is one of the most adopted consistency criteria for distributed implementations of data structures. It ensures that operations are executed at all sites according to their causal precedence. We address the issue of verifying automatically whether the executions of an implementation of a data structure are causally consistent. We consider two problems: (1) checking whether one single execution is causally consistent, which is relevant for developing testing and bug finding algorithms, and (2) verifying whether all the executions of an implementation are causally consistent. We show that the first problem is NP-complete. This holds even for the read-write memory abstraction, which is a building block of many modern distributed systems. Indeed, such systems often store data in key-value stores, which are instances of the read-write memory abstraction. Moreover, we prove that, surprisingly, the second problem is undecidable, and again this holds even for the read-write memory abstraction. However, we show that for the read-write memory abstraction, these negative results can be circumvented if the implementations are data independent, i.e., their behaviors do not depend on the data values that are written or read at each moment, which is a realistic assumption.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
