Detail produktu
Atomer: Atomicity Violations Analyser, Version 2.0
Vznik: 2022
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Concurrent programs, multithreaded programs, low-level synchronisation, mutexes, atomicity, static analysis, abstract interpretation, function summaries, Meta/Facebook Infer.
Jedná se o druhou verzi detektoru porušení atomičnosti v paralelních programech napsaných v jazyce C 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í Meta/Facebook Infer.
Oproti první verzi došlo k doplnění podpory různých typů zámků (reentrantní zámky, zámky s omezeným rozsahem platnosti a automatickým odemykáním apod.), ke zpřesnění analýzy (dodáním statického rozlišení instancí zámků), k vylepšení mechanismu analýzy předávání parametrů mezi analyzovanými funkcemi a k různým dalším zdokonalením používaných abstraktních domén a operací nad nimi, jež jsou motivovány snahou o vyšší přesnost a lepší škálovatelnost analýzy.
Volně šiřitelný software poskytovaný pod MIT licencí (přesné znění licence je dostupné na stránce https://opensource.org/licenses/MIT).