Detail produktu
DeadlockF, Version 1.0
Vznik: 2021
Statická analýza, paralelní programy, vícevláknové programy, uváznutí, Frama-C, zásuvný modul.
DeadlockF verze 1.0 je první verzí statického analyzátoru pro detekci potenciálních deadlocků v programech v jazyce C implementovaného jako zásuvný modul platformy Frama-C.
Jádro algoritmu vychází z existujícího nástroje RacerX. Takzvaná lockset analýza prochází grafem toku řízení a počítá množinu zámků držených v libovolném bodě programu. Pokud je získán zámek b s aktuální sadou zámků, která již obsahuje zámek a, je do lockgraphu přidána závislost a -> b. Každý cyklus v tomto grafu je pak nahlášen jako potenciální deadlock.
Zásuvný modul používá EVA (zásuvný modul analýzy hodnot analyzátoru Frama-C) k výpočtu informací may-point-to pro parametry zamykacích operací. Protože EVA neumí nativně analyzovat souběžné programy, DeadlockF nejprve identifikuje všechna vlákna v programu a poté spustí EVA pro každé vlákno zvlášť s kontexty bodů programu, kde bylo vlákno vytvořeno. Výsledkem je pak podaproximace, která nezohledňuje prokládání vláken.
Volně šiřitelný software poskytovaný pod MIT licencí (přesné znění licence je dostupné na stránce https://opensource.org/licenses/MIT).