Atomer: Atomicity Violations Analyser, Version 1.0

Atomer: Atomicity Violations Analyser, Version 1.0

Software

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.

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.

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

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

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

K využití výsledku jiným subjektem je vždy nutné nabytí licence

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