L2D2: A Low Level Deadlock Detector, Version 1.0

Název česky

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

Typ

software

Licence

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Licenční poplatek

Poskytovatel licence na výsledek nepožaduje licenční poplatek

Autoři

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

Klíčová slova

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

Popis

Jedná se o první verzi detektoru uváznutí v paralelních programech napsaných v jazycích C, C++ či Java a používajících nízko-úrovňovou synchronizaci pomocí explicitního zamykání a odemykání synchronizačních zámků ("mutexů"). Nástroj je statickým analyzátorem založeným na abstraktní interpretaci s využitím souhrnů funkcí počítaných dle stromu volání funkcí, a to počínaje jeho listy tak, aby bylo dosaženo vysoké škálovatelnosti. Detektor je implementován v jazyce Ocaml jako zásuvný modul ("plugin") pro prostředí Facebook Infer.

Umístění

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

Licenční podmínky

Volně šiřitelný software poskytovaný pod MIT licencí (přesné znění licence je dostupné na stránce https://opensource.org/licenses/MIT).

Projekty

AQUAS: Agregované metody řízení kvality, MŠMT, Společná technologická iniciativa ECSEL, 8A17001, 737475, 2017-2020, ukončen

Výzkumné skupiny

Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)

Pracoviště

Ústav inteligentních systémů (UITS)