Deadlock is a static analyser for the detection of potential deadlocks in C programs implemented as a plugin of the Frama-C platform.
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 uses EVA (Value analysis plugin of Frama-C) to compute may-point-to information for parameters of locking operations. Because EVA can't natively analyse concurrent programs, we first identify all threads in a program and then run it for each thread separately with contexts of program points, where the thread was created. The result is then under-approximation, which doesn't take into account thread's interleavings.
This example demonstrates output for the program with simple deadlock. The more complex example can be found here.
void * thread1(void *v)
{
pthread_mutex_lock(&lock1);
pthread_mutex_lock(&lock2);
...
pthread_mutex_unlock(&lock2);
pthread_mutex_unlock(&lock1);
}
void * thread2(void *v)
{
pthread_mutex_lock(&lock2);
pthread_mutex_lock(&lock1);
...
pthread_mutex_unlock(&lock1);
pthread_mutex_unlock(&lock2);
}[kernel] Parsing simple_deadlock.c (with preprocessing)
[Deadlock] Deadlock analysis started
[Deadlock] === Assumed threads: ===
[Deadlock] main
[Deadlock] thread1
[Deadlock] thread2
[Deadlock] === Lockgraph: ===
[Deadlock] lock1 -> lock2
[Deadlock] lock2 -> lock1
[Deadlock] ==== Results: ====
[Deadlock] Deadlock between threads thread1 and thread2:
Trace of dependency (lock2 -> lock1):
In thread thread2:
Lock of lock2 (simple_deadlock.c:20)
Lock of lock1 (simple_deadlock.c:21)
Trace of dependency (lock1 -> lock2):
In thread thread1:
Lock of lock1 (simple_deadlock.c:10)
Lock of lock2 (simple_deadlock.c:11)
The current version is compatible with Frama-C Vanadium, it's detailed installation guide can be found in user manual and requires Ocaml version at least 4.12. Besides Frama-C, Deadlock requires following opam packages to be installed:
ounit2
containers
After installing dependencies and cloning this repositary, Deadlock can be installed as follows:
cd Deadlock
make setup
make
make install
You may also run Deadlock in docker either by using docker run -it tdacik/deadlock or by running make docker to build an image of the most recent version.
The simplest way to run the plugin is:
frama-c -deadlock source_file1.c source_file2.c ...
For more advanced usage, see list of command line options for tuning the analysis and gui manual for visualisation of results in Frama-C's gui application.
Dacík T. Static Deadlock Detection in Frama-C In Proceedings of Excel@FIT'20. Brno University of Technology, Faculty of Information Technology. 2020
Dacík T. Static Analysis in the Frama-C Environment Focused on Deadlock Detection Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2020-07-10. Supervised by Vojnar Tomáš.
If you have any questions, do not hesitate to contact the tool/method authors:
- Tomáš Dacík <xdacik00@stud.fit.vutbr.cz>
- Tomáš Vojnar <vojnar@fit.vutbr.cz>
The plugin is available under MIT license.