Přístupnostní navigace
E-application
Search Search Close
Applied result detail
HARMIM, D.; VOJNAR, T.
Original Title
Atomer: Atomicity Violations Analyser, Version 2.0
English Title
Type
Software
Abstract
Atomer version 2.0 is the second version of a static detector of violations of atomicity of call sequences in concurrent programs written in the C language using low-level synchronisation by explicit mutex locking and unlocking. The tool is a static analyser based on abstract interpretation and function summaries, which are computed along the call tree, starting from its leaves so as to achieve good scalability. The detector is implemented in OCaml as a plugin of the Meta/Facebook Infer Framework.Compared to the first version, support for various types of locks (re-entrant locks, locks with a limited validity range and automatic unlocking, etc.) has been added, the analysis has been made more precise (by adding static resolution of lock instances), the analysis mechanism for passing parameters between analysed functions has been improved, and various other improvements have been made to the abstract domains and operations over them, which are motivated by the desire for higher accuracy and better scalability of the analysis.
Abstract in English
Keywords
Concurrent programs, multithreaded programs, low-level synchronisation, mutexes, atomicity, static analysis, abstract interpretation, function summaries, Meta/Facebook Infer.
Key words in English
Location
https://github.com/harmim/infer/releases/tag/atomer-v2.0.0
Licence fee
In order to use the result by another entity, it is always necessary to acquire a license
www