DeadlockF, Version 1.0

DeadlockF, Version 1.0

Software

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.

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.

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

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

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

In order to use the result by another entity, it is always necessary to acquire a license

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