一句话：研究事务程序对因果一致性的鲁棒性验证，并归约为顺序一致性下的状态可达性。
现代分布式存储和数据库常实现弱于可串行化的因果一致性。本文研究如何自动验证事务程序对因果一致性的鲁棒性，即程序在任意因果一致数据库上的所有行为是否都可串行化。作者比较多种因果一致性变体，证明无写写竞争的程序在这些变体下具有相同行为集合；并给出多项式时间归约，将鲁棒性检查化为顺序一致性共享内存上事务程序的状态可达性。该归约揭示：行为集合不可比较的因果一致性变体可拥有可比较的鲁棒程序集合，并使现有并发验证方法与工具可用于分析因果一致数据库上的程序；当各站点程序为有限状态时，鲁棒性检查可判定。
Distributed storage systems and databases are widely used by various types of applications. Transactional access to these storage systems is an important abstraction allowing application programmers to consider blocks of actions (i.e., transactions) as executing atomically. For performance reasons, the consistency models implemented by modern databases are weaker than the standard serializability model, which corresponds to the atomicity abstraction of transactions executing over a sequentially consistent memory. Causal consistency for instance is one such model that is widely used in practice. In this paper, we investigate application-specific relationships between several variations of causal consistency and we address the issue of verifying automatically if a given transactional program is robust against causal consistency, i.e., all its behaviors when executed over an arbitrary causally consistent database are serializable. We show that programs without write-write races have the same set of behaviors under all these variations, and we show that checking robustness is polynomial time reducible to a state reachability problem in transactional programs over a sequentially consistent shared memory. A surprising corollary of the latter result is that causal consistency variations which admit incomparable sets of behaviors admit comparable sets of robust programs. This reduction also opens the door to leveraging existing methods and tools for the verification of concurrent programs (assuming sequential consistency) for reasoning about programs running over causally consistent databases. Furthermore, it allows to establish that the problem of checking robustness is decidable when the programs executed at different sites are finite-state.
@article{paperbot1341,
title = {Robustness Against Transactional Causal Consistency},
author = {Sidi Mohamed Beillahi and Ahmed Bouajjani and Constantin Enea},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:12)2021}
}