Original title: Pokročilá statická analýza atomičnosti v paralelních programech v prostředí Facebook Infer
Translated title: Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Authors: Harmim, Dominik ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Document type: Master’s theses
Year: 2021
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
Nástroj Atomer je statický analyzátor založený na myšlence, že pokud jsou některé sekvence funkcí vícevláknového programu prováděny v některých bězích pod zámky, je pravděpodobně zamýšleno, že mají být vždy provedeny atomicky. Analyzátor Atomer se tudíž snaží takové sekvence hledat a poté zjišťovat, pro které z nich může být v některých jiných bězích programu porušena atomicita. Autor této diplomové práce ve své bakalářské práci navrhl a implementoval první verzi nástroje Atomer jako zásuvný modul aplikačního rámce Facebook Infer. V této diplomové práci je navržena nová a výrazně vylepšená verze analyzátoru Atomer. Cílem vylepšení je zvýšení jak škálovatelnosti, tak přesnosti. Kromě toho byla přidána podpora pro několik původně nepodporovaných programovacích vlastností (včetně např. možnosti analyzovat programy napsané v jazycích C++ a Java nebo podpory pro reentrantní zámky nebo stráže zámků, tzv. "lock guards"). Prostřednictvím řady experimentů (včetně experimentů s reálnými programy a reálnými chybami) se ukázalo, že nová verze nástroje Atomer je skutečně mnohem obecnější, přesnější a lépe škáluje. Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The author of this master's thesis proposed and implemented the first version of Atomer as a plugin of the Facebook Infer framework in his bachelor's thesis. In the master's thesis, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.
Keywords: abstraktní interpretace; analýza programů; Atomer; atomicita; Facebook Infer; inkrementální analýza; interprocedurální analýza; kompoziční analýza; kontrakty pro paralelismus; modulární analýza; paralelní programy; porušení atomicity; sekvence volání funkcí; statická analýza; vícevláknové programy; škálovatelnost; abstract interpretation; Atomer; atomicity; atomicity violation; compositional analysis; concurrent programs; contracts for concurrency; Facebook Infer; function calls sequence; incremental analysis; interprocedural analysis; modular analysis; multi-threaded programs; programs analysis; scalability; static analysis

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/200216

Permalink: http://www.nusl.cz/ntk/nusl-445592


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Master’s theses