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 -> 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.
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
The analysis is neither sound nor complete. Rather, it searches for high-confident deadlocks.
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: