Inspect: A Framework for Dynamic Verification of Multithreaded C Programs


Installation Usage Related projects

Inspect is a tool for systematic testing multithreaded C programs under specific inputs. It can systematically explore different interleavings of multithreaded programs under specific inputs by repeatedly executing the program. Inspect is aimed to reveal concurrency related bugs, such as data races, deadlocks, etc. (Because of the lack of a C++ source code transformer, Inspect cannot automatically instrument C++ programs. With manual instrumentation, we can still use Inspect to check multithreaded C++ programs. But you need to know more about how Inspect works to do the manual instrumentation. )

1  Download and Installation

The file inspect-0.3.tar.gz contains the complete source distribution. Inspect is written in C++ and Ocaml. You need Ocaml release 3.10 or higher, and a C++ compiler to build Inspect. Inpect has been tested under Linux systems. It has not been tested under Windows or other Unix systems yet. The source can be compiled with the following commands:

  tar xzf inspect-0.3.tar.gz
  cd inspect-0.3
  make distclean
  make 

2  How to Use Inspect

The following command line shows how to use Inspect. First we instrument the multithreaded code. Then we compile the instrumented code, and linked with a wrapper library. After this,we got an executable which can be systematically test using inspect.

  bin/instruemnt   examples/dpor-example1.c
  bin/compile      dpor-example1.instr.c
  ./inspect ./target

3  Related Projects

Bugs? Send to yuyang@cs.utah.edu.


This document was translated from LATEX by HEVEA.