|
|
# About
|
|
|
L2D2 is a plugin of Facebook Infer for detecting low-level deadlocks in C/C++ programs. L2D2 statically analyzes C/C++ code to detect potential deadlocks. This analysis does not attempt to prove the absence of concurrency issues, rather, it searches for a high-confidence class of deadlocks. A textbook example of such a bug is illustrated in the following example. Of course, in real deadlocks, the lock acquisitions may be separated by deeply nested call chains and L2D2 has support for detecting these deadlocks too.
|
|
|
|
|
|
```c
|
|
|
void *thread1(...) {
|
|
|
pthread_mutex_lock(&L1);
|
|
|
pthread_mutex_lock(&L2);
|
|
|
}
|
|
|
void *thread2(...) {
|
|
|
pthread_mutex_lock(&L2);
|
|
|
pthread_mutex_lock(&L1);
|
|
|
}
|
|
|
```
|
|
|
#### Background:
|
|
|
L2D2 works in two phases. In the first phase, it computes a set of locking dependencies for each function (regardless of its context, resulting in high scalability). In the second phase, L2D2 looks through all the computed locking dependencies and checks if there is a cyclic dependency between some of the used locks. More details on the algorithm can be found in [**Related papers**](#related-papers).
|
|
|
|
|
|
#### Bug types:
|
|
|
|
|
|
Let's take a look at the different types of bugs that L2D2 flags. We distinguish two types of reports in our analyser:
|
|
|
* **Deadlock** -- occurs when two distinct threads try to acquire two locks in reverse orders. Bugs of this kind are reported as **errors**.
|
|
|
* **Multiple (un)locking** -- occurs when one tries to acquire/release a lock that is already acquired/released. Bugs of this kind are reported as **warnings**.
|
|
|
|
|
|
# Installation
|
|
|
[INSTALL.md](https://pajda.fit.vutbr.cz/xmarci10/fbinfer_concurrency/blob/master/INSTALL.md) - all the information necessary to get Infer (containing L2D2) working.
|
|
|
# Usage
|
|
|
To run the analysis, you can use plain `infer` or `infer --deadlock-only` (to run only L2D2). L2D2 itself accepts its input in the form of C/C++ files and prints all detected bugs on the standard output.
|
|
|
|
|
|
#### Possible instances of running L2D2:
|
|
|
|
|
|
* **Default mode** -- prints all detected deadlocks and warnings.
|
|
|
|
|
|
* `infer --deadlock-only -- gcc -c source_code.c`
|
|
|
|
|
|
* **Extended mode** -- suppressing the warnings and reducing the number of false positives (**warning:** it may cause false negatives!!!).
|
|
|
|
|
|
* `infer --deadlock-only --locking_error -- gcc -c source_code.c`
|
|
|
# Contact
|
|
|
If you have any questions, do not hesitate to contact the tool/method authors:
|
|
|
* **Vladimir Marcin** <<xmarci10@stud.fit.vutbr.cz>>
|
|
|
* [**Tomas Vojnar**](http://www.fit.vutbr.cz/~vojnar/) <<vojnar@fit.vutbr.cz>>
|
|
|
# Related Papers
|
|
|
1. MARCIN, Vladimír. [Static Analysis Using Facebook Infer Focused on Deadlock Detection](https://www.vutbr.cz/www_base/zav_prace_soubor_verejne.php?file_id=197934).
|
|
|
Brno, 2019. Bachelor’s thesis. Brno University of Technology, Faculty of Information
|
|
|
Technology. Supervisor prof. Ing. Tomáš Vojnar, Ph.D.
|
|
|
2. Harmim, D.; Marcin, V.; Onřej, P.: [Scalable Static Analysis Using Facebook Infer](http://excel.fit.vutbr.cz/submissions/2019/059/59.pdf). In
|
|
|
Excel@FIT’19. Brno, Czech Republic. 2019. |
|
|
\ No newline at end of file |