Thesis Details

Static Analysis Using Facebook Infer Focused on Errors in RCU-Based Synchronisation

Bachelor's Thesis Student: Marek Daniel Academic Year: 2021/2022 Supervisor: Vojnar Tomáš, prof. Ing., Ph.D.
Czech title
Statická analýza v nástroji Facebook Infer zaměřená na chyby v RCU synchronizaci
Language
English
Abstract

Read Copy Update (RCU) is a synchronization mechanism, found mostly in the Linux kernel. Its sought-after features include almost zero overhead and high speed when reading shared memory. RCU has a set of rules of use, which need to be followed in order for the synchronization to work properly. To the best of our knowledge, there is no analyzer that sufficiently verifies if the RCU rules of use are adhered to. To overcome this, we propose a new analyzer, with the focus on finding violations in the use of RCU rules. The analyzer is based on static analysis and implemented as a module for the static analysis framework Facebook/Meta Infer. This platform was chosen because it provides scalability, which is needed when dealing with such an extensive software as the Linux kernel. The designed analyzer is capable of detecting multiple different ways in which the RCU usage rules can be broken, each causing either a race condition or a deadlock. It is also capable of generating warnings for situations when a deprecated function call is used or when the use of incompatible RCU reader and writer primitives is detected. The analyzer is the first of its kind. It may become a basis for future analyzer development in the field of Read Copy Update. Furthermore, it may be used as a test tool in the Linux kernel development cycle.

Keywords

Read Copy Update, RCU, RCU rules violation, Facebook/Meta Infer RCU analyzer, Static RCU analyzer, RCU analyzer, RCU checker

Department
Degree Programme
Information Technology
Files
Status
defended, grade A
Date
13 June 2022
Reviewer
Committee
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), předseda
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Martínek Tomáš, doc. Ing., Ph.D. (DCSY FIT BUT), člen
Peringer Petr, Dr. Ing. (DITS FIT BUT), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT), člen
Citation
MAREK, Daniel. Static Analysis Using Facebook Infer Focused on Errors in RCU-Based Synchronisation. Brno, 2022. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2022-06-13. Supervised by Vojnar Tomáš. Available from: https://www.fit.vut.cz/study/thesis/25138/
BibTeX
@bachelorsthesis{FITBT25138,
    author = "Daniel Marek",
    type = "Bachelor's thesis",
    title = "Static Analysis Using Facebook Infer Focused on Errors in RCU-Based Synchronisation",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2022,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/25138/"
}
Back to top