摘要: 1、研究背景：
目前已有的分布式存储系统通常采用副本技术，通过将数据的多个副本存放在不同的物理节点以提供可用性和容错性，并降低访问延迟。然而多副本技术也会导致数据一致性问题。根据CAP定理，在分布式系统中强数据一致性、可用性与分区容错性无法同时满足。因此，为了能在网络分区情况下保障系统的可用性，许多分布式存储系统选择实现弱一致性协议。因果一致性协议是一种被广泛使用的弱一致性模型，它可以保证客户端以相同的顺序观察到具有因果关系的操作。已有文献表明，因果一致性是在网络分区情况下能实现的最强的一致性模型。MongoDB是最早支持因果一致性的商用分布式数据库之一。然而，为了提供系统的可用性、容错性与安全性，MongoDB因果一致性的实现包含混合逻辑时钟、基于Raft的共识协议以及签名验证等机制，这大大增加了MongoDB因果一致性协议实现的复杂性。尽管著名的分布式系统测试机构Jepsen对于MongoDB的因果一致性进行了检测，但是该检测在规约、测试样例、算法与测试场景下都存在许多不足，这大大降低测试的可信度。
2、研究目的：
作为目前世界上使用率排名第一的非关系型数据库，MongoDB近年来得到了很多应用。我们希望能够在Jepsen测试的基础上对MongoDB的因果一致性协议进行一次更系统更充分的测试。
3、研究方法：
我们在Jepsen已有测试的基础上，通过对规约、测试样例、算法与测试场景的完善与改进对MongoDB的因果一致性协议进行一次更系统更充分的测试。具体而言，首先，我们采用使用形式化规约语言TLA+与模型检验工具TLC对因果一致性变体CC，CM和CCv的规约，与基于“非法模式”的因果一致性检测算法进行形式化建模。然后，在Jepsen已有测试的基础上，我们引入了网络分区，节点失效与数据块迁移的测试场景，并收集MongoDB在由YCSB生成的覆盖率更广的测试样例下得到的操作历史。最后，使用基于“非法模式”的因果一致性检测算法检测MongoDB操作历史对于CC，CM和CCv这三种因果一致性变体的满足情况。
4、研究结果：
我们首先成功用TLA+对因果一致性变体CC，CM和CCv的规约和基于“非法模式”的因果一致性检测算法进行形式化建模，通过对从模型检验的角度验证了算法的正确性。接着，通过使用Jepsen框架对MongoDB因果一致性协议进行的更充分测试，我们得到MongoDB在不同情况下对于因果一致性的满足情况：在网络分区、节点失效等干扰存在的情况下，那么只有majority的写关注与majority的读关注设置下MongoDB才能提供因果一致性的保障。如果系统时钟正常运行，那么最弱的w1写关注与local读关注设置下MongoDB也能提供因果一致性的保障。
5、研究结论：
我们通过从规约、样例生成、算法以及测试场景四个方面对Jepsen关于MongoDB因果一致性协议的测试进行改进，对MongoDB并进行了更为充分的测试，并得到了在不同网络条件下不同读关注与写关注设置的MongoDB对因果一致性三种主要变体（CC，CM与CCv）的支持情况，这对于用户使用MongoDB的因果一致性有很大的参考价值。未来，我们希望能够使用TLA+对MongoDB的事务协议进行形式化建模与验证。