Master's Thesis

Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer

---

Diplomová práce

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

---

Author: Harmim Dominik, Bc. [email protected]

Supervisor: Vojnar Tomáš, prof. Ing. Ph.D. (UITS FIT VUT) [email protected]

Reviewer: Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT) [email protected]

Specification:

1. Study limitations of the atomicity analyser Atomer developed in your bachelor thesis as well as the latest developments concerning the Facebook Infer framework.
2. Propose ways of significantly improving precision and/or scalability of the analysis even if for the price of the user providing more input and/or combining it with dynamic analysis.
3. Implement a new version of Atomer including the proposed improvements and supporting analysis of programs written in more programming languages than just C supported by the first version of Atomer.
4. Evaluate the new version of Atomer on suitable benchmarks, including at least real-life code in which some atomicity problems were previously detected.
5. Describe and discuss the achieved results and their further possible improvements.

Category: Software analysis and testing

Implementation language: OCaml

Free software: Facebook Infer

Literature:

1. Rival, X., Yi, K.: Introduction to Static Analysis: An Abstract Interpretation Perspective. MIT Press, 2020.
2. Blackshear, S., Gorogiannis, N., O'Hearn, P. W., Sergey, I.: RacerD: Compositional Static Race Detection. In: Proc. of OOPSLA'18, PACMPL 2(OOPSLA):144:1-144:28, 2018.
3. Gorogiannis, N., O'Hearn, P.W., Sergey, I.: A True Positives Theorem for a Static Race Detector. In: Proc. of POPL'19, PACMPL 3(POPL):57:1-57:29, 2019.
4. Dias, R.J., Ferreira, C., Fiedor, J., Lourenço, J.M., Smrčka, A., Sousa, D.G., Vojnar, T.: Verifying Concurrent Programs Using Contracts, In: Proc. of ICST'17, IEEE, 2017.
5. Harmim, D.: Static Analysis Using Facebook Infer to Find Atomicity Violations. Bachelor thesis, Brno University of Technology, 2019.
6. Marcin, V.: Static Analysis Using Facebook Infer Focused on Deadlock Detection. Bachelor thesis, Brno University of Technology, 2019.

Implementation

The implementation is in the repository harmim/infer. It is a fork of the repository facebook/infer. It is implemented under the branch atomicity-sets, see the diff.

Wiki

More information about the tool, including examples, installation and usage instructions are available at the Wiki.

Useful links:

• Facebook Infer
• Facebook Infer repository
• OCaml
• Patrick Cousot - Abstract Interpretation
• Patrick Cousot - Abstract Interpretation in a Nutshell
• Facebook Infer lab
• Facebook Infer talk
• Facebook Infer INSTALL.md
• Facebook Infer CONTRIBUTING.md
• Open-sourcing RacerD: Fast static race detection at scale
• ThreadSafe: Static Analysis for Java Concurrency
• ThreadSafe: Static Analysis for Java Concurrency - benchmark
• Gluon
• Gluon - validation examples
• VeriFIT Static Analysis Plugins
• ANaConDA Framework
• Apache Cassandra repository
• Apache Cassandra - reported bugs
• Apache Tomcat repository
• Apache Tomcat - reported bugs
• Inferbo: Infer-based buffer overrun analyzer