eXplode: Effective Model Checking of Real Systems

We are developing an approach called in-situ model checking to thoroughly check general systems software in a lightweight manner. We’ve made our approach so easy that we have applied it to more than 20 widely used, well tested systems and found nearly a hundred serious errors. Some of these errors can cause unrecoverable loss of an entire file system. Currently we’re collaborating with researchers at Microsoft Research to apply the eXplode approach to distributed systems.

Read More…

Publications

Practical Software Model Checking via Dynamic Interface Reduction

Huayang Guo, Ming Wu, Lidong Zhou, Gang Hu, Junfeng Yang, Lintao Zhang
Proceedings of the 23rd ACM Symposium on Operating Systems Principles (SOSP ’11), October 2011

Abstract

PDF

 

MODIST: Transparent Model Checking of Unmodified Distributed Systems

Junfeng Yang, Tisheng Chen, Ming Wu, Zhilei Xu, Xuezheng Liu, Haoxiang Lin, Mao Yang, Fan Long, Lintao Zhang, Lidong Zhou
Proceedings of the Sixth Symposium on Networked Systems Design and Implementation (NSDI ’09), April 2009

Abstract

PDF

 

EXPLODE: a Lightweight, General System for Finding Serious Storage System Errors

Proceedings of the Seventh Symposium on Operating Systems Design and Implementation (OSDI ’06), November 2006

Abstract

PDF

 

Using Model Checking to Find Serious File System Errors

Junfeng Yang, Paul Twohey, Dawson Engler, Madanlal Musuvathi
ACM Transactions on Computer Systems, Volume 24, Issue 4, November 2006

Abstract

PDF

 

eXplode: A Lightweight, General Approach for Finding Serious Errors in Storage Systems

Junfeng Yang, Paul Twohey, Ben Pfaff, Can Sar, Dawson Engler
Proceedings of the first Workshop on the Evaluation of Software Defect Detection Tools (BUGS ’05), June 2005

Abstract

PDF

 

Using Model Checking to Find Serious File System Errors

Junfeng Yang, Paul Twohey, Dawson Engler, Madanlal Musuvathi
Proceedings of the Sixth Symposium on Operating Systems Design and Implementation (OSDI ’04), December 2004

Abstract

PDF

 

Download eXplode

The above are three ways to get eXplode. You can download the eXplode source code locally, or download a virtual machine image with eXplode and eXplode-patched kernels compiled, or get the source code from sourceforge. You can browse the version history of eXplode at sourceforge.

For instructions to compile, build, and use eXplode, Please refer to the README file in the top-level directory after you uncompress the explode tar ball.

The eXplode distribution contains a generic model checker that can be applied to other systems. For details, please refer to the README file under directory mcl.
Real systems are difficult to get right because they must correctly handle a practically infinite number of rare events. For example, file systems must correctly recover from all possible crashes; distributed systems must ensure consistency and liveness despite of a large variety of rare events, such as machine crashes, network partition, message delays, and message loss. The complexity to handle these rare events often leads to corner-case errors that are difficult to test, and once detected in the field, impossible to reproduce.

Columbia University Department of Computer Science