Název: Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti
Překlad názvu: Static Analysis Using Facebook Infer to Find Atomicity Violations
Autoři: Harmim, Dominik ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Typ dokumentu: Bakalářské práce
Rok: 2019
Jazyk: cze
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [cze] [eng]
Cílem této práce je navrhnout statický analyzátor, který bude sloužit pro detekci porušení atomicity. Navržený analyzátor Atomer je implementován jako modul pro Facebook Infer, což je volně šířený a snadno rozšířitelný nástroj, který umožňuje efektivní modulární a inkrementální analýzu. Analyzátor pracuje na úrovni sekvencí volání funkcí. Navržené řešení je založeno na předpokladu, že sekvence, které jsou zavolány atomicky jednou, by měly být pravděpodobně volány atomicky vždy. Implementovaný analyzátor byl úspěšně ověřen a vyhodnocen jak na malých programech, vytvořených pro testovací účely, tak na veřejně dostupných testovacích programech, které vznikly ze skutečných nízkoúrovňových programů. The goal of this thesis is to propose a static analyser that detects atomicity violations. The proposed analyser Atomer is implemented as a module of Facebook Infer, which is an open-source and extendable static analysis framework that promotes efficient modular and incremental analysis. The analyser works on the level of sequences of function calls. The proposed solution is based on the assumption that sequences executed atomically once should probably be executed always atomically. The implemented analyser has been successfully verified and evaluated on both smaller programs created for testing purposes as well as publicly available benchmarks derived from real-life low-level programs.
Klíčová slova: abstraktní interpretace; analýza programů; atomicita; atomické sekvence; Facebook Infer; inkrementální analýza; interprocedurální analýza; kompoziční analýza; kontrakty pro souběžnost; modulární analýza; paralelní programy; porušení atomicity; statická analýza; abstract interpretation; atomic sequences; atomicity; atomicity violation; compositional analysis; concurrent programs; contracts for concurrency; Facebook Infer; incremental analysis; interprocedural analysis; modular analysis; programs analysis; static analysis

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: http://hdl.handle.net/11012/180173

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-403045


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Bakalářské práce