L2D2: A Low Level Deadlock Detector, Version 1.0

Czech title

L2D2: nízko-úrovňový detektor uváznutí, verze 1.0

Type

software

License

required - free

Authors

Marcin Vladimír, Ing. (FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)

Keywords

Concurrent programs, multithreaded programs, low-level synchronisation, mutexes, deadlocks, static analysis, abstract interpretation, function summaries, Facebook Infer.

Description

L2D2 version 1.0 is the first version of a static detector of deadlocks in concurrent programs written in C, C++, or Java and using low-level synchronisation by explicit mutex locking and unlocking. The tool is a static analyser based on abstract interpretation and function summaries, which are computed along the call tree, starting from its leaves so as to achieve good scalability. The detector is implemented in Ocaml as a plugin of the Facebook Infer Framework.

Location

https://pajda.fit.vutbr.cz/xmarci10/fbinfer_concurrency/-/tree/c533ea95e8a9a222ee6b9040e104e7ce2d27b131

Licence

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

Projects

AQUAS: Aggregated Quality Assurance for Systems (8A17001)

Research groups

Automated Analysis and Verification Research Group - VeriFIT (VZ VERIFIT)

Departments

Department of Intelligent Systems FIT BUT (DITS FIT BUT)