Home

Deadlock is a static analyser for detection of potential deadlocks in C programs implemented as a plugin of Frama-C.

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.

Example

This example demonstrates output for the program with simple deadlock. 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);
}

Output:

[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)

Limitations

The plugin is still in development. Some of known limitations are:

• Lock/unlock wrappers and generally functions, that take mutexes as parameters can result in significant imprecision. Possible solution is to inline such functions with kernel option -inline-calls <f1, ..., fn>
• For some programs reported trace can be senseless due to caching
• Currently only POSIX threads and mutexes are supported

Installation

The current version is compatible with Frama-C Chlorine, it's detailed installation guide can be found in user manual. After installing Frama-C, clone this repository and run cd src, make and make install.

Usage

The plugin can be run by command:

frama-c -deadlock *source_file.c* 

Contact

If you have any questions, do not hesitate to contact the tool/method authors:

• Tomáš Dacík <[email protected]>
• Tomáš Vojnar <[email protected]>

License

The plugin is available under MIT license.