Atomer: Atomicity Violations Analyser, Version 1.0

Czech title

Atomer: detektor porušení atomičnosti, verze 1.0

Type

software

License

In order to use the result by another entity, it is always necessary to acquire a license

License Fee

The licensor does not require a license fee for the result

Authors

Harmim Dominik, Ing. (FIT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)

Keywords

Concurrent programs, multithreaded programs, low-level synchronisation, mutexes, atomicity, static analysis, abstract interpretation, function summaries, Facebook Infer.

Description

Atomer version 1.0 is the first 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 Facebook Infer Framework.

Location

https://github.com/harmim/vut-ibt/raw/master/atomer-v1.0.tgz

License Conditions

Free software under the MIT license (cf. https://opensource.org/licenses/MIT).

Projects

AQUAS: Aggregated Quality Assurance for Systems, MŠMT, Společná technologická iniciativa ECSEL, 8A17001, 737475, 2017-2020, completed

Research groups

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Departments

Department of Intelligent Systems (DITS)