Tree [169865] master /
History



File Date Author Commit
check 2009-09-27 Junfeng Yang Junfeng Yang [16db1d] fixed compilation issues for gcc 4.4
crash 2009-09-29 Junfeng Yang Junfeng Yang [9a9923] now use std::tr1 instead of gnu_cxx and boost
driver 2009-09-27 Junfeng Yang Junfeng Yang [16db1d] fixed compilation issues for gcc 4.4
ekm-bsd-6.0 2008-09-25 Junfeng Yang Junfeng Yang [57a717]
ekm-common 2008-09-25 Junfeng Yang Junfeng Yang [57a717]
ekm-linux-2.6 2009-09-17 Junfeng Yang Junfeng Yang [6f2641] split explode.default.options into different op...
kernel 2009-09-19 Junfeng Yang Junfeng Yang [4df8cb] Merge branch 'master' of git.ncl.cs.columbia.ed...
mcl 2009-09-29 Junfeng Yang Junfeng Yang [169865] shared_ptr compatibility header
mtd-linux-2.6 2008-09-25 Junfeng Yang Junfeng Yang [57a717]
rdd-bsd-6.0 2008-09-18 Junfeng Yang Junfeng Yang [6777e8] Import
rdd-linux-2.6 2009-09-19 explode testing explode testing [1f7799] fixed a stupid&nasty bug: memcpy src and dst sw...
rpc 2009-09-23 Junfeng Yang Junfeng Yang [7335a9] now random includes both unix random and enum r...
scripts 2008-09-26 Junfeng Yang Junfeng Yang [8c9f02] change version to 0.1pre
storage 2009-09-26 Junfeng Yang Junfeng Yang [f7ab29] add string.h in generated *-options.h files so ...
testsuite 2009-09-17 Junfeng Yang Junfeng Yang [6ae322] each options section is in an anonymous space t...
COPYING 2008-09-25 Junfeng Yang Junfeng Yang [651d5f]
Makefile.am 2009-09-18 Junfeng Yang Junfeng Yang [0465f1] mtd can't be compiled with 2.6.24...
Makefile.in 2009-09-18 Junfeng Yang Junfeng Yang [0465f1] mtd can't be compiled with 2.6.24...
README 2009-09-23 Junfeng Yang Junfeng Yang [7335a9] now random includes both unix random and enum r...
README.student 2009-09-18 Junfeng Yang Junfeng Yang [950713] updated README
TODO 2008-09-18 Junfeng Yang Junfeng Yang [6777e8] Import
acinclude.m4 2008-09-18 Junfeng Yang Junfeng Yang [6777e8] Import
config.h.in 2009-09-18 Junfeng Yang Junfeng Yang [a50603] fixed autoconf error
configure.ac 2009-09-27 Junfeng Yang Junfeng Yang [16db1d] fixed compilation issues for gcc 4.4
develop-log 2009-09-16 junfeng junfeng [ecfb9b] test git repo
gen-opt.pl 2009-09-26 Junfeng Yang Junfeng Yang [f7ab29] add string.h in generated *-options.h files so ...
setup 2008-09-18 Junfeng Yang Junfeng Yang [6777e8] Import
sysincl.h 2008-09-25 Junfeng Yang Junfeng Yang [57a717]

Read Me

eXplode is a storage system checker.  It comes with a model checker (in
directory mcl/) for real code instead of abstract models.  Model checking
is a formal verification technique that systematically enumerates the
possible execution paths of a system by starting from an initial state and
repeatedly performing all possible actions to this state and its
successors.  This state-space exploration makes rare actions such as
network failures appear as often as common ones, thereby quickly driving
the target system (i.e., the system we check) into corner cases where
subtle bugs surface.

eXplode's model checkier is a generic model checker that you can use to
check other systems as well (not just storage systems).  To learn more
information on using this model checker, please refer to mcl/README.

Conventional model checking is heavyweight and difficult to apply to real
systems; eXplode avoids the overheads associated with model checking using
new checking architecture that checks a system in-situ, in its native
environment.  This architecture makes it really easy to check new systems.
For example, a lot of the checkers we write have only less than 100 lines
of code.

Most of the other code in eXplode implements a crash simulator.  With this
simulator, you can check if your storage system correctly handles crashes
and recoveries.  Note 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
http://rcs.cs.columbia.edu/explode/vm/, and start it with VMware Player
(http://www.vmware.com/products/player).

2. Boot eXplode VM with VMware Player, and in the grub boot menu, select
"Ubuntu 8.04.1, kernel 2.6.24.3-eXplode."  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 below.

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/check/explode.options; this file stores user options.  For all
options users can configure, check out the "Configure eXplode" section
below.




Installation from Source
=========================

Download and uncompress the eXplode source code:
  % wget http://rcs.cs.columbia.edu/explode/explode-latest.tar.gz
  % tar xzvf explode-latest.tar.gz
  % mv explode-latest explode

Download and uncompress an eXplode-supported kernel into explode/kernel
  % cd explode/kernel
  % wget http://www.kernel.org/pub/linux/kernel/v2.6/linux-2.6.24.3.tar.bz2
  % tar xjvf linux-2.6.24.3.tar.bz2

Patch, build and install the kernel
  % cd linux-2.6.24.3
  % patch -p1 < ../patch/linux-2.6.24.3
  % make menuconfig
  % ...

Configure and build eXplode:

  % cd explode
  % configure --with-kernel=kernel/linux-2.6.24.3
  % make





Directory Structure
===================

The directory structure of eXplode is as follows:

  explode/

	mcl/                          Generic model checking library.  For details, 
                                      read mcl/README

	crash/                        Code in this directory implements crash 
                                      and recovery checking

	driver/                       Generic file system test driver

        storage/                      Wrappers to storage system utilities,
                                      such as mkfs and fsck

	check/                        Checkers for different storage systems.

        rpc/                          Wrappers to eXplode kernel modules below

	rdd-linux-2.6/                Simple RAM disk driver for Linux 2.6

	rdd-bsd-6.0/                  Simple RAM disk driver for FreeBSD 6.0

        mtd-linux-2.6/                Simple flash disk driver for Linux 2.6

	ekm-linux-2.6/                Explode kernel module for Linux 2.6

        ekm-bsd-6.0/                  Explode kernel module for FreeBSD 6.0

  kernel/
  
        patches/                      eXplode kernel patches

        linux-2.6.24/                 Full Linux kernel tree with eXplode patch applied




How does eXplode work?
====================

When a marchine crashes, we lose the cached dirty blocks.  Given a set of
cached dirty blocks, depending on the order in which the disk scheduler
writes out these cached blocks, any subset of these cached writes could
occur on a crashed disk.  If we test crashes simply by unplugging
powercords, we may see only a few different crashed disks because the disk
write order is mostly deterministic.  To increase coverage by testing many
different crashed disks, eXplode will keep track of the set of dirty
blocks in the buffer cache and try to enumerate all subsets of these dirty
blocks.  Since using real disks to simulate these crashes would be slow,
eXplode provides a RAM disk driver that simulates a block device.  Thus,
simulating crashes in eXplode is fast and easy: simply memcpying the
subset of cached dirty blocks onto the RAM disk.




Configure eXplode
====================

You can configure eXplode by providing an explode.options file in the
directory where you run an eXplode executable.  To see all available
options, run the following command

% find . -name \*.default.options -exec cat {} \;

This command essentially prints out all default options stored in
*.default.options files.




Re-building After You've Made Changes
==================

- Compiling eXplode

    eXplode uses autoconf and automake. If you have only modified existing
    files, re-building eXplode is easy.  Simply run:
       
       explode@explode-vm:~/explode$ make

    If you add new files or directories, add them to the corresponding Makefile.am, then:

       explode@explode-vm:~/explode$ ./setup
       explode@explode-vm:~/explode$ ./configure
       explode@explode-vm:~/explode$ make       


- Compiling and installing the kernel
    
    Normally you wouldn't need to touch the kernel.  But if you do, use
    the following instructions to install a new kernel:

    explode@explode-vm:~/explode/kernel/linux-2.6.24$ make bzImage
    [this may take a while ...]

    explode@explode-vm:~/explode/kernel/linux-2.6.24$ sudo cp arch/i386/boot/bzImage /boot/vmlinuz-2.6.24
    [this installs the new kernel]


- Updating eXplode

  We use git (http://git-scm.com/) to manage eXplode source.  To update eXplode, simply run:

       explode@explode-vm:~/explode$ git pull

  This command will pull the updates from the eXplode source forge
  repository (git://explode.git.sourceforge.net/gitroot/explode/explode)


Checking a New Storage System
==================

Three steps:

1. Create a checker

2. Create a storage component

3. Assemble a checking stack

You'll find plenty of storage component examples in storage/ and test
driver examples in driver/ and check/

For more details, please refer to the eXplode paper
(http://rcs.cs.columbia.edu/papers/yang_osdi06.pdf).