Detail práce
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
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.
Facebook Infer, statická analýza, abstraktní interpretace, kontrakty pro paralelismus, porušení atomicity, paralelní programy, analýza programů, atomicita, inkrementální analýza, modulární analýza, kompoziční analýza, interprocedurální analýza, škálovatelnost, Atomer, sekvence volání funkcí, vícevláknové programy
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm A.
- Plánujete podniknout další kroky pro zařazení Atomeru do hlavní větve frameworku Facebook Infer?
- Jakým způsobem funguje rozpoznávání atomické sekce?
- Dotaz na Read-Write zámky.
- Jakou nepřesnost do analýzy vnáší použitá aproximace?
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT), člen
Drábek Vladimír, doc. Ing., CSc. (UPSY FIT VUT), člen
Peringer Petr, Dr. Ing. (UITS FIT VUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT), člen
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT), člen
@mastersthesis{FITMT24185,
author = "Dominik Harmim",
type = "Diplomov\'{a} pr\'{a}ce",
title = "Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2021,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/24185/"
}