Skip to content
/ vut-dip Public

Master's Thesis - Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer

License

Notifications You must be signed in to change notification settings

harmim/vut-dip

Repository files navigation

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]
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: