Bachelor's Thesis

Static Analysis Using Facebook Infer to Find Atomicity Violations

---

Bakalářská práce

Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti

---

Author: Dominik Harmim xharmi00@stud.fit.vutbr.cz

Supervisor: prof. Ing. Tomáš Vojnar, Ph.D. (UITS FIT VUT) vojnar@fit.vutbr.cz

Reviewer: Ing. Aleš Smrčka, Ph.D. (UITS FIT VUT) smrcka@fit.vutbr.cz

Specification:

1. Prostudujte principy statické analýzy založené na abstraktní interpretaci. Zvláštní pozornost věnujte přístupům zaměřeným na odhalování problémů v synchronizaci paralelních procesů.
2. Seznamte se s nástrojem Facebook Infer, jeho podporou pro abstraktní interpretaci a s existujícímí analyzátory vytvořenými v prostředí Faceboook Infer.
3. V prostředí Facebook Infer navrhněte a naimplementujte analyzátor zaměřený na odhalování chyb typu porušení atomicity.
4. Experimentálně ověřte funkčnost vytvořeného analyzátoru na vhodně zvolených netriviálních programech.
5. Shrňte dosažené výsledky a diskutujte možnosti jejich dalšího rozvoje v budoucnu.

Category: Software analysis and testing

Implementation language: OCaml

Free software: Facebook Infer

Literature:

• Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
• Blackshear, S., O'Hearn, P.: Open-Sourcing RacerD: Fast Static Race Detection at Scale, 2017. Dostupné on-line: https://code.fb.com/android/open-sourcing-racerd-fast-static-race-detection-at-scale.
• Atkey, R., Sannella, D.: ThreadSafe: Static Analysis for Java Concurrency, Electronic Communications of the EASST, 72, 2015. Dostupné on-line: https://bentnib.org/threadsafe.html.
• Bielik, P., Raychev, V., Vechev, M.T.: Scalable Race Detection for Android Applications, In: Proc. of OOPSLA'15, ACM, 2015.
• 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.

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 product, including examples, installation, and usage are available at the Wiki.

Useful links:

• Facebook Infer
• Facebook Infer GitHub
• OCaml
• Real Wolrd OCaml
• Abstract interpretation - Patrick Cousot intro
• Facebook Infer lab
• Facebook Infer presentation
• Facebook Infer INSTALL
• Facebook Infer CONTRIBUTING
• Open-sourcing RacerD: Fast static race detection at scale
• ThreadSafe: Static Analysis for Java Concurrency
• Scalable Race Detection for Android Applications
• Verifying Concurrent Programs Using Contracts
• How to Use C Mutex Lock
• A True Positives Theorem for a Static Race Detector
• Gluon
• VeriFIT Static Analysis Plugins