Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer

Czech title

Pokročilá statická analýza atomičnosti v paralelních programech v prostředí Facebook Infer

Language

English

Abstract

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

Facebook Infer, static analysis, abstract interpretation, contracts for concurrency, atomicity violation, concurrent programs, programs analysis, atomicity, incremental analysis, modular analysis, compositional analysis, interprocedural analysis, scalability, Atomer, function calls sequence, multi-threaded programs

Department

Department of Intelligent Systems FIT BUT

Degree Programme

Information Technology and Artificial Intelligence, Specialization Software Verification and Testing

Files

Status

defended, grade A

Date

24 June 2021

Reviewer

Rogalewicz Adam, doc. Mgr., Ph.D.

Committee

Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), předseda
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT), člen
Drábek Vladimír, doc. Ing., CSc. (DCSY FIT BUT), člen
Peringer Petr, Dr. Ing. (DITS FIT BUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT), člen
Smrčka Aleš, Ing., Ph.D. (DITS FIT BUT), člen

Citation

HARMIM, Dominik. Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer. Brno, 2021. Master's Thesis. Brno University of Technology, Faculty of Information Technology. 2021-06-24. Supervised by Vojnar Tomáš. Available from: https://www.fit.vut.cz/study/thesis/24185/

BibTeX

@mastersthesis{FITMT24185,
    author = "Dominik Harmim",
    type = "Master's thesis",
    title = "Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2021,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/24185/"
}