DeadlockF, Version 1.0

Static analysis, concurrent programs, multithreaded programs, deadlock, Frama-C,
plugin.

DeadlockF Version 1.0 is the first version of a static analyser for 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 DeadlockF plugin uses EVA (a value analysis plugin of Frama-C) to compute
may-point-to information for parameters of locking operations. Because EVA cannot
natively analyse concurrent programs, DeadlockF first identifies all threads in
a program and then runs EVA for each thread separately with contexts of the
program points where the thread was created. The result is then an
under-approximation, which does not take into account thread's interleavings.

https://github.com/TDacik/Deadlock/releases/tag/1.0

Free software under the MIT license (cf. https://opensource.org/licenses/MIT).