Checking Causal Consistency of MongoDB

MongoDB is one of the first commercial distributed databases that support causal consistency.Its implementation of causal consistency combines several research ideas for achieving scalability,fault tolerance,and security.Given its inherent complexity,a natural question arises:"Has MongoDB correctly implemented causal consistency as it claimed?"To address this concern,the Jepsen team has conducted black-box testing of MongoDB.However,this Jepsen testing has several drawbacks in terms of specification,test case generation,implementation of causal consistency checking algorithms,and testing scenarios,which undermine the credibility of its reports.In this work,we propose a more thorough design of Jepsen testing of causal consistency of MongoDB.Specifically,we fully implement the causal consistency checking algorithms proposed by Bouajjani et al.and test MongoDB against three well-known variants of causal consistency,namely CC,CCv,and CM,under various scenarios including node failures,data movement,and network partitions.In addition,we develop formal specifications of causal consistency and their checking algorithms in TLA⁺,and verify them using the TLC model checker.We also explain how TLA⁺ specification can be related to Jepsen testing.     

PaxosStore中共识协议TPaxos的推导、规约与精化

PaxosStore是腾讯开发的高可用分布式存储系统，现已用于全面支持微信核心业务.PaxosStore实现了分布式共识协议Paxos的一种变体，我们称之为TPaxos.TPaxos的新颖之处在于它的"统一性"：它为每个参与者维护统一的状态类型，并采用统一格式的消息进行通信.然而，这种设计方案也带来了TPaxos与Paxos之间的诸多差异，给理解TPaxos造成了障碍.其次，虽然腾讯开源了TPaxos协议的核心代码（包括伪代码与C++代码），TPaxos仍缺少抽象而精确的形式化规约.最后，就我们所知，TPaxos的正确性尚未经过必要的数学论证或者形式化工具的检验.针对这些情况，本文有三个主要贡献.首先，我们从经典的Paxos协议出发，论证如何逐步推导出TPaxos协议.基于这种推导，我们可以将TPaxos看作Paxos的一种自然变体，更易于理解.其次，我们给出了TPaxos协议的TLA+形式化规约.在开发规约的时候，我们发现TPaxos协议描述中存在至关重要但并未充分阐明的微妙之处：在消息处理阶段，参与者（作为接受者角色）是先作出"不再接受具有更小编号的提议"的承诺（Promise）还是先接受（Accept）提议?这导致对TPaxos的两种不同理解，并促使我们提出TPaxos的一种变体，称为TPaxosAP.在TPaxosAP中，参与者先接受提议后作承诺.最后，我们使用精化（refinement）技术论证了TPaxos与TPaxosAP的正确性.特别地，由于已知的投票机制Voting不能完全描述TPaxosAP的行为，我们首先提出了适用于TPaxosAP的投票机制EagerVoting，然后建立了从TPaxosAP到EagerVoting以及从EagerVoting到Consensus的精化关系，并使用TLC模型检验工具验证了它们的正确性.     

CRDT协议的TLA+描述与验证

无冲突复制数据类型（conflict-free replicated data types，简称CRDT）是一种封装了冲突消解策略的分布式复制数据类型，它能保证分布式系统中副本节点间的强最终一致性，即执行了相同更新操作的副本节点具有相同的状态.CRDT协议设计精巧，不易保证其正确性.旨在采用模型检验技术验证一系列CRDT协议的正确性.具体而言，构建了一个可复用的CRDT协议描述与验证框架，包括网络通信层、协议接口层、具体协议层与规约层.网络通信层描述副本节点之间的通信模型，实现了多种类型的通信网络.协议接口层为已知的CRDT协议（分为基于操作的协议与基于状态的协议）提供了统一的接口.在具体协议层，用户可以根据协议的需求选用合适的底层通信网络.规约层则描述了所有CRDT协议都需要满足的强最终一致性与最终可见性（所有的更新操作最终都会被所有的副本节点接收并处理）.使用TLA+形式化规约语言实现了该框架，然后以Add-Wins Set复制数据类型为例，展示了如何使用框架描述具体协议，并使用TLC模型检验工具验证协议的正确性.     

支持乱序执行的Raft协议

PolarFS是阿里巴巴开发的分布式文件系统，它实现了分布式共识协议Raft的一种变体，称为ParallelRaft.ParallelRaft突破了Raft中顺序提交、顺序执行的限制，允许状态机乱序执行用户命令.然而，文献表明，ParallelRaft并未开源，仅有简短的文字描述，更缺乏严格的形式化规约.更进一步，它的正确性也尚未经过必要的数学论证或形式化检验.本文旨在为ParallelRaft提供严格的形式化规约并证明其正确性.具体而言，本文的主要贡献包括：首先，为了理清ParallelRaft与Raft之间的关系，我们提出了允许乱序提交、顺序执行的ParallelRaft-SE （Sequential Execution）协议，并建立了从ParallelRaft-SE到Multi-Paxos的精化关系.其次，我们发现现有的ParallelRaft描述忽略了可能会违反状态一致性的“幽灵日志”问题.因此，我们在ParallelRaft-SE的基础上提出了ParallelRaft-CE （Concurrent Execution）协议.ParallelRaft-CE限制了ParallelRaft-SE在乱序提交阶段的并行度，避免了“幽灵日志”问题，支持乱序执行，并保证乱序执行下的状态机一致性.我们证明了ParallelRaft-CE的正确性.最后，我们使用TLA+给出了ParallelRaft-SE和ParallelRaft-CE的形式化规约，并对协议参与者数量较小的情形使用TLC模型检验与模拟测试工具验证了从ParallelRaft-SE到Multi-Paxos的精化关系以及ParallelRaft-CE的正确性.