We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 37 Issue 1
January  2022
Turn off MathJax
Article Contents
Abstract
References
Related Articles
Supplements
Hong-Rong Ouyang, Heng-Feng Wei, Hai-Xiang Li, An-Qun Pan, Yu Huang. Checking Causal Consistency of MongoDB[J]. Journal of Computer Science and Technology, 2022, 37(1): 128-146. DOI: 10.1007/s11390-021-1662-8
Citation: Hong-Rong Ouyang, Heng-Feng Wei, Hai-Xiang Li, An-Qun Pan, Yu Huang. Checking Causal Consistency of MongoDB[J]. Journal of Computer Science and Technology, 2022, 37(1): 128-146. DOI: 10.1007/s11390-021-1662-8
shu

Checking Causal Consistency of MongoDB

  • 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

Funds: 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.
More Information
  • Author Bio:

    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.

  • Corresponding author:

    Heng-Feng Wei E-mail: hfwei@nju.edu.cn

    Hai-Xiang Li E-mail: blueseali@tencent.com

  • Received Date: May 31, 2021
  • Revised Date: October 08, 2021
  • Accepted Date: December 19, 2021
  • Published Date: January 27, 2022
    Abstract
  • 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 ofcausal 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.
    • FullText(HTML)
    • References (29)
  • [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.
    • Relative Articles

  • Related Articles

    [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. DOI: 10.1007/s11390-020-0516-0
    [2]Jia-Qi Yin, Hui-Biao Zhu, Yuan Fei. Specification and Verification of the Zab Protocol with TLA+[J]. Journal of Computer Science and Technology, 2020, 35(6): 1312-1323. DOI: 10.1007/s11390-020-0538-7
    [3]Luca Aceto, Jens A. Hansen, Anna Ingolfsdottir, Jacob Johnsen, John Knudsen. The Complexity of Checking Consistency of Pedigree Information andRelated Problems[J]. Journal of Computer Science and Technology, 2004, 19(1).
    [4]ZHAO Jianhua. Checking Timed Automata for Linear Duration Properties[J]. Journal of Computer Science and Technology, 2000, 15(5): 423-429.
    [5]NI Bin, FENG Yulin. Dynamic Checking Frameworkfor Java Beaus Semantic Constraints[J]. Journal of Computer Science and Technology, 1999, 14(4): 408-413.
    [6]CHEN Yangjun. On the Arc Consistency Problem[J]. Journal of Computer Science and Technology, 1999, 14(4): 298-308.
    [7]WANG Bingshan, LI Zhoujun, CHEN Huowang. Universal Abstract Consistency Class and Universal Refutation[J]. Journal of Computer Science and Technology, 1999, 14(2): 165-172.
    [8]Hu Weiwu, Shi Weisong, Tang Zhimin. A Framework of Memory Consistency Models[J]. Journal of Computer Science and Technology, 1998, 13(2): 110-124.
    [9]Shao Zhiqing, Song Guoxin. An Algebraic Characterization of Inductive Soundness in Proof by Consistency[J]. Journal of Computer Science and Technology, 1995, 10(3): 285-288.
    [10]Shen Yidong. An Algorithm for Determining Database Consistency Under the Closed World Assumption[J]. Journal of Computer Science and Technology, 1992, 7(4): 289-294.
    • Supplements (2)

  • Others

  • Cited by

    Periodical cited type(1)

    1. Mehria Nawaz. ONLINE SKILL TEST PLATFORM. JOURNAL OF MECHANICS OF CONTINUA AND MATHEMATICAL SCIENCES, 2022, 17(11) DOI:10.26782/jmcms.2022.11.00003

    Other cited types(0)

Catalog

    Get Citation
    PDF
    XML
    Read Online
    Article views (162) PDF downloads (1) Cited by(1)
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    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

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return