验证 MongoDB 的事务一致性
分布式、并行与集群计算
2022-06-17 v3
摘要
MongoDB 是一种流行的通用面向文档分布式 NoSQL 数据库。它在三种不同部署中支持事务：在独立节点上利用 WiredTiger 存储引擎的单文档事务，由一个主节点和多个从节点组成的副本集中的多文档事务，以及由多个副本集组成的数据在其中分片的分片集群中的分布式事务。关于 MongoDB 事务的一个自然且基本的问题是：每种部署中的 MongoDB 事务提供什么样的事务一致性保证？然而，它既缺乏每种部署中 MongoDB 事务的简洁伪代码，也缺乏 MongoDB 声称提供的一致性保证的形式化规范。在本研究中，我们形式化地规范并验证了 MongoDB 的事务一致性协议。具体而言，基于官方文档和源代码，我们为每种 MongoDB 部署（即 WIREDTIGER、REPLICASET 和 SHARDEDCLUSTER）中的事务一致性协议提供了简洁的伪代码。然后，我们证明 WIREDTIGER、REPLICASET 和 SHARDEDCLUSTER 分别满足快照隔离的不同变体，即 Strong-SI、Realtime-SI 和 Session-SI。我们还提出并评估了针对 MongoDB 事务协议一致性保证的高效白盒检测算法，有效地在理论上规避了 NP 困难障碍。
引用
@article{arxiv.2111.14946,
title = {Verifying Transactional Consistency of MongoDB},
author = {Hongrong Ouyang and Hengfeng Wei and Yu Huang and Haixiang Li and Anqun Pan},
journal= {arXiv preprint arXiv:2111.14946},
year = {2022}
}
备注
v0.2, update with proof of correctness. 17 pages(16 pages excluding reference), 8 algorithms, 5 tables and 2 figures