New plugin: deadlock

_data/publications.yml

@@ -39,6 +39,8 @@
     name: CELIA
   - id: cost
     name: Cost
+  - id: deadlockf
+    name: DeadlockF
   - id: fanc
     name: Fan-C
   - id: jessie

_fc-plugins/deadlockf.md

+---
+layout: plugin
+title: DeadlockF
+description: Deadlock detection in multithreaded C programs with mutexes.
+key: concurrent
+distrib_mode: free
+repo_url: https://github.com/TDacik/Deadlock
+additional:
+  - name: "Wiki"
+    short: "Wiki" # to be displayed on the documentation part
+    link: https://github.com/TDacik/Deadlock/wiki
+---
+
+## Overview
+
+DeadlockF is a plugin for detection of deadlocks in multithreaded C programs
+with mutexes. The core algorithm is based on an existing tool
+[RacerX](https://web.stanford.edu/~engler/racerx-sosp03.pdf). 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 can use (under-approximated) results of EVA to improve may-points-to
+information for parameters of locking operations.
+
+
+## Quick Start
+
+DeadlockF is available as an external open-source
+[plugin]({{page.additional[0].link}}). 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 `-deadlock` option.
+
+## Technical notes
+
+The analysis is neither sound nor complete. Rather, it searches for
+high-confident deadlocks.
+
+## Dependencies
+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:
+```
+ounit2
+containers
+```

_fc-publications/deadlockf/2020-dacik-bsc.md

+---
+plugin: deadlockf
+authors: ["Tomáš Dacík", "Tomáš Vojnar"]
+title: "Static Analysis in the Frama-C Environment Focused on Deadlock Detection"
+school: "Brno University of Technology, Faculty of Information Technology"
+link: "https://www.fit.vut.cz/study/thesis/22928/.en"
+year: 2020
+category: "other"
+short: "Bachelor thesis describing principles and implementation of the DeadlockF analyser."
+---
+This thesis presents a design of a new static analyser focused on deadlock
+detection, implemented as a plugin of the Frama-C platform. Together with the
+core algorithm of deadlock detection, we also present a light-weight method that
+allows one to analyse (not only for the purposes of deadlock detection)
+multithreaded programs using sequential analysers of Frama-C. Results of
+experiments show that our tool is able to handle real-world C code with high
+precision. Moreover, we demonstrate its extensibility by so-far experimental
+implementation of data race detection.