Inspect: A Framework for Dynamic Verification of Multithreaded C Programs |
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. )
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
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
Bugs? Send to yuyang@cs.utah.edu.
This document was translated from LATEX by HEVEA.