Atomer: Atomicity Violations Analyser, Version 1.0

Název česky

Atomer: detektor porušení atomičnosti, 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

Harmim Dominik, Ing. (FIT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)

Klíčová slova

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

Popis

Jedná se o první 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í Facebook Infer.

Umístění

https://github.com/harmim/vut-ibt/raw/master/atomer-v1.0.tgz

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)