Original title: Static Analysis Using the Meta Infer Framework to Detect Data Races
Translated title: Statická analýza v nástroji Meta Infer zaměřená na detekci souběhu nad daty
Authors: Svobodová, Lucie ; Fiedor, Jan (referee) ; Vojnar, Tomáš (advisor)
Document type: Bachelor's theses
Year: 2023
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
Vícevláknové programy jsou v moderních softwarových systémech využívány ke zlepšení výkonu a zvýšení efektivity. Zajištění spolehlivosti a bezpečnosti takových programů však může být náročné kvůli zvýšenému množství chyb, které se v nich vyskytují, včetně souběhu nad daty. V této práci představujeme nový statický detektor souběhu nad daty, DarC, navržený k analýze programů napsaných v jazyce C využívajících knihovnu Pthreads. Navrhovaný nástroj byl implementován jako zásuvný modul prostředí Meta Infer, což je nástroj pro statickou analýzu programů, který klade důraz na kompoziční, inkrementální a díky tomu i vysoce škálující analýzu programů. Nový analyzátor zaznamenává množinu přístupů ke sdíleným proměnným, ke kterým v analyzovaném programu došlo, spolu s informací o množině zámků uzamknutých při jednotlivých přístupech. Množina přístupů je dále použita k identifikaci dvojic přístupů, mezi nimiž by k souběhu nad daty mohlo dojít. Nástroj byl úspěšně ověřen na sadě testovacích vícevláknových programů, stejně tak jako na několika programech běžně využívaných v praxi, čímž byl ukázán jeho potenciál pro efektivní detekci souběhu nad daty v programech napsaných v programovacím jazyce C. Modern software systems often use concurrent programs to improve performance and increase efficiency. However, ensuring the reliability and safety of such systems can be challenging due to the increased potential for bugs, including data races, to arise. In this thesis, we introduce a new static data race detector, DarC, designed for programs written in C using the Pthreads library. The proposed detector is implemented as an analyser plugin in Meta Infer, a static analysis framework with an emphasis on compositional, incremental, and consequently highly-scalable analysis. Our approach involves recording a set of accesses that occur in the analysed program along with information about the set of locks held during these accesses. The tool then identifies pairs of accesses that may lead to data races and reports them to the user. Our tool was successfully evaluated on a set of benchmarking programs as well as on real-life projects, showing its potential for effectively detecting data races in C programs.
Keywords: abstraktní interpretace; analýza programů; Infer; inkrementální analýza; paralelní programy; souběh nad daty; statická analýza; verifikace programů; vícevláknové programy; škálovatelnost; abstract interpretation; concurrent programs; data race; incremental analysis; Infer; multi-threaded programs; program analysis; program verification; scalability; static analysis

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/212768

Permalink: http://www.nusl.cz/ntk/nusl-530997


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Bachelor's theses