典型文献
Checking Causal Consistency of MongoDB
文献摘要：
MongoDB is one of the first commercial distributed databases that support causal consistency.Its implemen-tation 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.
文献关键词：
中图分类号：
作者姓名：
Hong-Rong Ouyang;Heng-Feng Wei;Hai-Xiang Li;An-Qun Pan;Yu Huang
作者机构：
State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210023,China;Software Institute,Nanjing University,Nanjing 210093,China;Tencent Distributed SQL Team of Technology and Engineering Group of Tencent,Tencent Inc.,Shenzhen 518054,China
文献出处：
引用格式：
[1]Hong-Rong Ouyang;Heng-Feng Wei;Hai-Xiang Li;An-Qun Pan;Yu Huang-.Checking Causal Consistency of MongoDB)[J].计算机科学技术学报（英文版）,2022(01):128-146
A类：
Checking,Jepsen,Bouajjani,CCv,TLA+,checker,TLA+specification
B类：
Causal,Consistency,MongoDB,one,first,commercial,distributed,databases,that,support,causal,consistency,Its,combines,several,research,ideas,achieving,scalability,fault,tolerance,security,Given,its,inherent,complexity,natural,question,arises,Has,correctly,implemented,claimed,To,address,this,concern,team,has,conducted,black,box,testing,However,drawbacks,terms,case,generation,implementation,checking,algorithms,scenarios,which,undermine,credibility,reports,In,more,thorough,design,Specifically,fully,proposed,by,against,three,well,known,variants,namely,CM,various,including,node,failures,movement,network,partitions,addition,develop,formal,specifications,their,verify,them,using,TLC,model,We,also,explain,how,can,be,related
AB值：
0.525493
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
