eXplode is a storage system checker. It comes with a generic model checker for code (mcl/), which you can use to check other systems as well (not just storage systems). Model checking is a heavyweight formal verification technique. eXplode adapts the core idea from Model Checking, exploring all choices, to comprehensively check a storage system. Meanwhile, it has a new checking architecture that checks a system in-situ, in its native environment, thus makes it really easy to check new systems. Most of the other code in eXplode checks storage system crashes and recoveries. eXplode will not simply check random crashes that merely occur; it will systematically generate *possible* crashes by permuting modified disk blocks in the buffer cache.

Quick Start

1. Get the eXplode virtual machine (VM) image from here, and start it with VMware Player.
2. In the GRUB boot menu, select "Ubuntu 8.04.1, kernel 2.6.24.3." Use username "explode" and password "#explode" to log in. The eXplode source tree is in ~/explode. For the tree structure, refer to the Directory Structure in README.student.
3. To check a file system, go to directory "~/explode/check," and run "./check-fs." All checkers are in directory "~/explode/check." You can also check cvs by running "./check-cvs."
4. To check a different file system, change fs::type and rdd::sectors in ~/explode/explode.options; this file stores user options. For all options eXplode supports, check out explode.default.options in the same directory.

More Information