Journal of Computer Science and Technology ›› 2022, Vol. 37 ›› Issue (1): 128-146.doi: 10.1007/s11390-021-1662-8

Special Issue: Software Systems

• Special Section on Software Systems 2021 • Previous Articles     Next Articles

Checking Causal Consistency of MongoDB

Hong-Rong Ouyang1 (欧阳鸿荣), Heng-Feng Wei1,2,* (魏恒峰), Member, CCF, Hai-Xiang Li3,* (李海翔), Member, CCF, An-Qun Pan3 (潘安群), Member, CCF, and Yu Huang1 (黄宇), Member, CCF        

  1. 1State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210023, China
    2Software Institute, Nanjing University, Nanjing 210093, China
    3Tencent Distributed SQL Team of Technology and Engineering Group of Tencent, Tencent Inc., Shenzhen 518054, China
  • Received:2021-06-01 Revised:2021-10-09 Accepted:2021-12-20 Online:2022-01-28 Published:2022-01-28
  • Contact: Heng-Feng Wei, Hai-Xiang Li E-mail:hfwei@nju.edu.cn, blueseali@tencent.com
  • About author:Heng-Feng Wei received his B.S. and Ph.D. degrees in computer science and technology from Nanjing University, Nanjing, in 2009 and 2016, respectively. He is currently a research assistant with Software Institute and the State Key Laboratory for Novel Software Technology at Nanjing University, Nanjing. His research interests include distributed computing and formal methods. He is a member of CCF.
    Hai-Xiang Li is currently a chief researcher and chief architect of the distributed database system TDSQL at Tencent Inc., Shenzhen. His research interests include distributed computing, cloud database, transaction processing, and query optimization. He is a member of CCF.
  • Supported by:
    This work was supported by the CCF-Tencent Open Fund under Grant No.RAGR20200124 and the National Natural Science Foundation of China under Grant Nos.61702253 and 61772258.

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.

Key words: MongoDB; casual consistency; Jepsen; consistency checking; TLA+;

[1] Schultz W, Avitabile T, Cabral A. Tunable consistency in MongoDB. Proc. VLDB Endow., 2019, 12(12): 2071-2081. DOI: 10.14778/3352063.3352125.
[2] Tyulenev M, Schwerin A, Kamsky A, Tan R, Cabral A, Mulrow J. Implementation of cluster-wide logical clock and causal consistency in MongoDB. In Proc. the 2019 International Conference on Management of Data, June 30-July 5, 2019, pp.636-650. DOI: 10.1145/3299869.3314049.
[3] Abadi D. Consistency tradeoffs in modern distributed database system design: CAP is only part of the story. IEEE Computer, 2012, 45(2): 37-42. DOI: 10.1109/MC.2012.33.
[4] Brewer E A. Towards robust distributed systems (abstract). In Proc. the 19th Annual ACM Symposium on Principles of Distributed Computing, July 2000, Article No.7. DOI: 10.1145/343477.343502.
[5] Gilbert S, Lynch N. Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services. ACM SIGACT News, 2002, 33(2): 51-59. DOI: 10.1145/564585.564601.
[6] Brzezinski J, Sobaniec C, Wawrzyniak D. From session causality to causal consistency. In Proc. the 12th Euromicro Conference on Parallel, Distributed and Network-Based Processing, Feb. 2004, pp.152-158. DOI: 10.1109/EMPDP.2004.1271440.
[7] Kulkarni S S, Demirbas M, Madappa D, Avva B, Leone M. Logical physical clocks. In Proc. the 18th International Conference on Principles of Distributed Systems, Dec. 2014, pp.17-32. DOI: 10.1007/978-3-319-14472-6-2.
[8] Du J, Iorgulescu C, Roy A, Zwaenepoel W. GentleRain: Cheap and scalable causal consistency with physical clocks. In Proc. the ACM Symposium on Cloud Computing, Nov. 2014, Article No.4. DOI: 10.1145/2670979.2670983.
[9] Akkoorath D D, Tomsic A Z, Bravo M, Li Z, Crain T, Bieniusa A, Preguiça N, Shapiro M. Cure: Strong semantics meets high availability and low latency. In Proc. the 36th International Conference on Distributed Computing Systems, June 2016, pp.405-414. DOI: 10.1109/ICDCS.2016.98.
[10] Ongaro D, Ousterhout J. In search of an understandable consensus algorithm. In Proc. the 2014 USENIX Conference on USENIX Annual Technical Conference, June 2014, pp.305-320.
[11] Bouajjani A, Enea C, Guerraoui R, Hamza J. On verifying causal consistency. In Proc. the 44th ACM Symposium on Principles of Programming Languages, Jan. 2017, pp.626-638. DOI: 10.1145/3009837.3009888.
[12] Burckhardt S. Principles of eventual consistency. Found. Trends Program. Lang., 2014, 1(1/2): 1-150. DOI: 10.1561/2500000011.
[13] Perrin M, Mostéfaoui A, Jard C. Causal consistency: Beyond memory. In Proc. the 21st ACM Symposium on Principles and Practice of Parallel Programming, Aug. 2016, Article No.26. DOI: 10.1145/2851141.2851170.
[14] Ahamad M, Neiger G, Burns J E, Kohli P, Hutto P W. Causal memory: Definitions, implementation, and programming. Distributed Computing, 1995, 9(1): 37-49. DOI: 10.1007/BF01784241.
[15] Lynch N A. Distributed Algorithms. Morgan Kaufmann Publishers Inc., 1996.
[16] Ouyang H R, Wei H F, Huang Y. Checking causal consistency of MongoDB. In Proc. the 12th Asia-Pacific Symposium on Internetware, Nov. 2020, pp.209-216. DOI: 10.1145/3457913.3457928.
[17] Lamport L. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 1978, 21(7): 558-565. DOI: 10.1145/359545.359563.
[18] Lesani M, Bell C J, Chlipala A. Chapar: Certified causally consistent distributed key-value stores. In Proc. the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan. 2016, pp.357-370. DOI: 10.1145/2837614.2837622.
[19] Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers (1st edition). Addison-Wesley Professional, 2002.
[20] Lamport L. The temporal logic of actions. ACM Trans. Program. Lang. Syst., 1994, 16(3): 872-923. DOI: 10.1145/177492.177726.
[21] Wei H F, Tang R Z, Huang Y, Lv J. Jupiter made abstract, and then refined. Journal of Computer Science and Technology, 2020, 35(6): 1343-1364. DOI: 10.1007/s11390-020-0516-0.
[22] Yu Y, Manolios P, Lamport L. Model checking TLA+ specifications. In Proc. the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Sept. 1999, pp.54-66. DOI: 10.1007/3-540-48153-2-6.
[23] Cooper B F, Silberstein A, Tam E, Ramakrishnan R, Sears R. Benchmarking cloud serving systems with YCSB. In Proc. the 1st ACM Symposium on Cloud Computing, June 2010, pp.143-154. DOI: 10.1145/1807128.1807152.
[24] Bowles J, Caminati M B. A verified algorithm enumerating event structures. In Proc. the 10th International Conference on Intelligent Computer Mathematics, July 2017, pp.239-254. DOI: 10.1007/978-3-319-62075-6-17.
[25] Gibbons P, Korach E. Testing shared memories. SIAM Journal on Computing, 1997, 26(4): 1208-1244. DOI: 10.1137/S0097539794279614.
[26] Herlihy M P, Wing J M. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 1990, 12(3): 463-492. DOI: 10.1145/78969.78972.
[27] Attiya H, Welch J L. Sequential consistency versus linearizability. ACM Trans. Comput. Syst., 1994, 12(2): 91-122. DOI: 10.1145/176575.176576.
[28] Wei H, Huang Y, Cao J, Ma X, Lv J. Verifying Pipelined-RAM consistency over read/write traces of data replicas. IEEE Transactions on Parallel and Distributed Systems, 2013, 27(5): 1511-1523. DOI: 10.1109/TPDS.2015.2453985.
[29] Lipton R J, Sandberg J. PRAM: A scalable shared memory. Technical Report, Department of Computer Science, Princeton University, 1988. https://www.cs.princeton.edu/research/techreps/TR-180-88, Aug. 2021.
[1] Heng-Feng Wei, Rui-Ze Tang, Yu Huang, Jian Lv. Jupiter Made Abstract, and Then Refined [J]. Journal of Computer Science and Technology, 2020, 35(6): 1343-1364.
[2] Luca Aceto, Jens A. Hansen, Anna Ingolfsdottir, Jacob Johnsen and John Knudsen. The Complexity of Checking Consistency of Pedigree Information and Related Problems [J]. , 2004, 19(1): 0-0.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] Min Yinghua;. Easy Test Generation PLAs[J]. , 1987, 2(1): 72 -80 .
[2] Sun Yongqiang; Lu Ruzhan; Huang Xiaorong;. Termination Preserving Problem in the Transformation of Applicative Programs[J]. , 1987, 2(3): 191 -201 .
[3] Feng Yulin;. Hierarchical Protocol Analysis by Temporal Logic[J]. , 1988, 3(1): 56 -69 .
[4] Xu Jie; Li Qingnan; Huang Shize; Xu Jiangfeng;. DFTSNA:A Distributed Fault-Tolerant Shipboard System[J]. , 1990, 5(2): 109 -116 .
[5] Li Jintao; Min Yinghua;. Product-Oriented Test-Pattern Generation for Programmable Logic Arrays[J]. , 1990, 5(2): 164 -174 .
[6] Su Bogong; Wang Jian; Xia Jinshi;. TST——An Algorithm for Global Microcode Compaction with Timing Constraints[J]. , 1991, 6(1): 97 -107 .
[7] Li Tao;. Competition Based Neural Networks for Assignment Problems[J]. , 1991, 6(4): 305 -315 .
[8] Tang Zesheng;. Octree Representation and Its Applications in CAD[J]. , 1992, 7(1): 29 -38 .
[9] Zhou Di;. Adapting Backward Error Recovery to Parallel Real Time Systems[J]. , 1992, 7(3): 257 -267 .
[10] Shen Yidong;. An Algorithm for Determining Database Consistency Under the Closed World Assumption[J]. , 1992, 7(4): 289 -294 .

ISSN 1000-9000(Print)

         1860-4749(Online)
CN 11-2296/TP

Home
Editorial Board
Author Guidelines
Subscription
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
Tel.:86-10-62610746
E-mail: jcst@ict.ac.cn
 
  Copyright ©2015 JCST, All Rights Reserved