DPU: Dynamic Program Unfolding

DPU is a research tool to perform dynamic analysis of POSIX multithreaded C programs. It will automatically and exhaustively test all possible thread schedules of a C program that uses POSIX threads.

The tool instruments the source with a specific runtime that gets the control on every call to a pthread_* function. That way it can (a) discover the relevant thread interleavings and (b) control the thread scheduler to deterministically replay threaded executions.

Detected Flaws

For each execution of the program DPU can currently detect the following flaws:

• Assertion violations, as triggered by the function assert(3).
• Calls to abort(3).
• Executions where the program calls exit(3) with a non-zero exit code. This is not necessarily a flaw, but a non-zero exit code usually denotes that an error ocurred.
• Data races.
• Deadlocks.

Assumptions About the Input Program

DPU assumes that your program is data-deterministic, that is, the only source of non-determinism in an execution is the order in which independent, concurrent statements can be interleaved. As a result, all sources of non-deterministic execution (e.g., command-line arguments, input files) need to be fixed before running the tool.

Data-race Detection

DPU can detect and report data-races in the input program (option -a dr), but those will not be used as source of thread interference to find new thread interleavings. The tool will not explore two execution orders for the two instructions that exhibit a data-race.

When data-race analysis is enabled, DPU will record memory load/store operations performed by the program, in addition to the calls to pthread_* functions. This detection happens for a user-provided percentage (option --drfreq, default 10%) of the executions explored by the tool. This analysis is thus not guaranteed to find all data-races, but any data-race found is a genuine one.

Exploration Algorithm

The tool explores the state-space of thread interleavings using optimal and non-optimal unfolding-based Partial-Order Reduction (POR) algorithms extending those presented in our CONCUR'15 paper (arXiv:1507.00980).

Installing Precompiled Binaries

The following steps assume that you have a Debian/Ubuntu distribution:

1. Install Clang v6.0 and LLVM v6.0 (see the LLVM releases):

   sudo apt-get install clang-6.0 llvm-6.0
   

   The commands clang-6.0 and llvm-link-6.0 should now be available in your $PATH.

2. Download the precompiled binaries from the latest release and unpack them anywhere in your machine.

3. The DPU tool is located within the folder dpu-vx.x.x/bin in the downloaded package. You can either run it from there or update your $PATH variable to include this folder. In the second case add the following line to your ~/.bashrc file and restart your teminal:

   export PATH=$PATH:/path/to/dpu-vx.x.x/bin
   

4. You should now be able to run:

   dpu --help
   dpu --version
   

Compilation

Instructions for compiling from the sources are available in the COMPILING.rst file.

Tutorial

TODO

• Hello world
• Options
• wllvm

Related tools

• POET
• Nidhugg
• CHESS
• Maple

Contact

DPU is currently maintained by César Rodríguez. Please feel free to contact me in case of questions or to send feedback.