earthquake

Earthquake: Dynamic Model Checker for Distributed Systems

Earthquake is a dynamic model checker (DMCK) for real implementations of distributed system (such as ZooKeeper).

Blog: http://osrg.github.io/earthquake/

Earthquakes permutes C/Java function calls, Ethernet packets, and injected fault events in various orders so as to find implementation-level bugs of the distributed system. When Earthquake finds a bug, Earthquake automatically records the event history and helps you to analyze which permutation of events triggers the bug.

Basically, Earthquake permutes events in a random order, but you can write your own state exploration policy (in Go or Python) for finding deep bugs efficiently.

Found/Reproduced Bugs

• ZooKeeper:
• Found ZOOKEEPER-2212: blog article (repro code)
• Reproduced ZOOKEEPER-2080: (repro code)
• etcd:
• Found #3517, fixed in #3530: (repro code)

Quick Start

• How to set up the environment: GettingStarted (some extra info)
• Example: Finding a distributed race condition bug of ZooKeeper(ZOOKEEPER-2212): blog article (repro code)

NOTE: the latest release might be stabler than the master branch.

Talks

• Earthquake was presented at the poster session of ACM Symposium on Cloud Computing (SoCC). (August 27-29, 2015, Hawaii)

How to Contribute

We welcome your contribution to Earthquake. Please feel free to send your pull requests on github!

Copyright

Copyright (C) 2015 Nippon Telegraph and Telephone Corporation.

Released under Apache License 2.0.