Overview
eXplode systematically checks storage systems by exploring runtime choices in their native environment. Its checking architecture makes it practical to test real systems, while its crash-state exploration permutes modified disk blocks to exercise possible recovery states rather than sampling only crashes that happen at random.
The source tree also includes a generic model checker for code, which can be used to check systems beyond storage software.
Primary Publication
EXPLODE: a Lightweight, General System for Finding Serious Storage System Errors
Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI), November, 2006
Abstract
Storage systems such as file systems, databases, and RAID systems have a simple, basic contract: you give them data, they do not lose or corrupt it. Often they store the only copy, making its irrevocable loss almost arbitrarily bad. Unfortunately, their code is exceptionally hard to get right, since it must correctly recover from any crash at any program point, no matter how their state was smeared across volatile and persistent memory. This paper describes eXplode, a system that makes it easy to systematically check real storage systems for errors. It takes user-written, potentially system-specific checkers and uses them to drive a storage system into tricky corner cases, including crash recovery errors. eXplode uses a novel adaptation of ideas from model checking, a comprehensive, heavyweight formal verification technique, that makes its checking more systematic (and hopefully more effective) than a pure testing approach while being just as lightweight. eXplode is effective. It found serious bugs in a broad range of real storage systems (without requiring source code): three version control systems, Berkeley DB, an NFS implementation, ten file systems, a RAID system, and the popular VMware GSX virtual machine. We found bugs in every system we checked, 36 bugs in total, typically with little effort.
Follow-up Work
These technical reports develop separate extensions to eXplode and retain their own publication pages and citation records.
Resources
- eXplode model-checking project
-
Source releases
eXplode is an in-situ model checker for storage systems.
Coverage
Archived Setup Instructions
Original 2008 virtual machine instructions
Kept for reference. The VM image and the VMware Player download it referred to are no longer available, and the software it describes targets Ubuntu 8.04.
- Get the eXplode virtual machine (VM) image, and start it with VMware Player.
- 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.
- 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.”
- 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.