DeadlockF

Overview

DeadlockF is a plugin for detection of deadlocks in multithreaded C programs with mutexes. The core algorithm is based on an existing tool RacerX. The so-called lockset analysis traverses control flow graph and computes the set of locks held at any program point. When lock b is acquired with current lockset already containing lock a, dependency a -> b is added to lockgraph. Each cycle in this graph is then reported as a potential deadlock.

The plugin can use (under-approximated) results of EVA to improve may-points-to information for parameters of locking operations.

Quick Start

DeadlockF is available as an external open-source plugin. To install it, clone the repository and run:

cd Deadlock
make setup
make
make install

Alternatively, the latest stable version can be installed using opam by running opam install deadlock.

Once installed, the plugin is enabled with the -deadlock option.

Technical notes

The analysis is neither sound nor complete. Rather, it searches for high-confident deadlocks.

Dependencies

The current version is compatible with Frama-C Vanadium and requires Ocaml version at least 4.12. Besides Frama-C, the plugin requires following opam packages to be installed:

ounit2
containers