Product Details
Atomer: Atomicity Violations Analyser, Version 2.0
Created: 2022
Concurrent programs, multithreaded programs, low-level synchronisation, mutexes,
atomicity, static analysis, abstract interpretation, function summaries,
Meta/Facebook Infer.
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.
Free software under the MIT license (cf. https://opensource.org/licenses/MIT).