Jens M. Jepsen has lived in China for a decade now.He heads the Motion Controls Division of DanfossChina, a Danish-based maker of mechanical and elec-tronic products and controls that has been listed amongthe World’s...Jens M. Jepsen has lived in China for a decade now.He heads the Motion Controls Division of DanfossChina, a Danish-based maker of mechanical and elec-tronic products and controls that has been listed amongthe World’s Top 500 Companies by Forbes Magazine.展开更多
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 secur...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.展开更多
文摘Jens M. Jepsen has lived in China for a decade now.He heads the Motion Controls Division of DanfossChina, a Danish-based maker of mechanical and elec-tronic products and controls that has been listed amongthe World’s Top 500 Companies by Forbes Magazine.
基金supported by the CCF-Tencent Open Fund under Grant No.RAGR20200124the 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.
