ANaConDA Framework

About

ANaConDA is a framework that simplifies the creation of dynamic analysers for analysing multi-threaded C/C++ programs on the binary level. The framework provides a monitoring layer offering notification about important events, such as thread synchronisation or memory accesses, so that developers of dynamic analysers can focus solely on writing the analysis code. In addition, the framework also supports noise injection techniques to increase the number of interleavings witnessed in testing runs and hence to increase chances to find concurrency-related errors.

Download

Linux (x86 32-bit/64-bit)

Latest Release

ANaConDA suite latest beta (Sources) (includes framework, libdie and libdie-wrapper libraries, analysers, and tools)

Special Releases

ANaConDA suite 0.4 for AQUAS (Sources) (includes framework, libdie and libdie-wrapper libraries, analysers, and tools)

Supports caching of memory access instruction locations.
Contains the Eraser and FastTrack data race detectors.

Older Releases

ANaConDA suite 0.2 beta (Sources) (includes framework, libdie and libdie-wrapper libraries, analysers, and tools)

ANaConDA framework 0.1 beta (Sources) (compilation requires libdie and pinlib-die libraries)

libdie library 0.1 beta (Sources)
pinlib-die library 0.1 beta (Sources)
Event Printer analyser 0.1 beta (Sources) (A simple analyser which prints all reveived events to the standard output)
AtomRace analyser 0.1 beta (Sources) (A simple data race detector implementing the AtomRace algorithm)

Windows (x86 32-bit/64-bit)

Latest Release

ANaConDA suite latest beta (Sources) (includes framework, libdie and libdie-wrapper libraries, analysers, and tools)

Special Releases

ANaConDA suite 0.4 for AQUAS (Sources) (includes framework, libdie and libdie-wrapper libraries, analysers, and tools)

Supports caching of memory access instruction locations.
Contains the Eraser and FastTrack data race detectors.

Older Releases

ANaConDA suite 0.2 beta (Sources) (includes framework, libdie and libdie-wrapper libraries, analysers, and tools)

ANaConDA framework 0.1 beta (Windows 64-bit)

Event Printer analyser 0.1 beta (Windows 64-bit) (A simple analyser which prints all reveived events to the standard output)
AtomRace analyser 0.1 beta (Windows 64-bit) (A simple data race detector implementing the AtomRace algorithm)

Usage

Running ANaConDA

Linux

To run ANaConDA on Linux, do the following (source release only):

Run tools/build.sh --setup-runtime

This will check if the tools needed to run ANaConDA are available and if not, it will download and install them.
Run tools/build.sh all

This will build the ANaConDA framework with all of its libraries and all analysers.
Run tools/run.sh <analyser> <program>

This will start the analysis of a given program.

Windows

To run ANaConDA on Windows, do the following (binary release only):

Run tools/cygwin.bat --quiet

This will start a Cygwin terminal where the scripts for running ANaConDA can be executed. If Cygwin is not found, the script will download it and install it (with all the required packages). If you want to choose where to download and install Cygwin, start the script without --quiet option.
Run tools/build.sh --setup-runtime (in the started Cygwin terminal)

This will check if the tools needed to run ANaConDA are available and if not, it will download and install them.
Run tools/run.sh <analyser> <program> (in the started Cygwin terminal)

This will start the analysis of a given program.

Analysing a Program

To perform an analysis of a given program, run the following command:

tools/run.sh <analyser> <program> [<program-parameters>]

where

<analyser> is a name of the analyser to be used to perform the analysis, and
<program> is a name of the program to be analysed or path to its executable

The names of analysers can be found in the Repository Layout section under the analysers node (the trailing slash (/) is not part of their name) with a brief description of what the analyser does.

Instead of a path to a program executable, one may register a program under an alias and then use this alias to specify the program to be analysed instead of the path to it. See section Registering a Program for more information.

For example, printing the information about the operations (accesses to memory, lock acquisitions, ...) performed by the 'ls' command with the '-la' parameter can be done using the following command:

tools/run.sh event-printer /usr/bin/ls -la

Examples

Bank

A simple program containing a data race. To analyse this program using the AtomRace data race detector (included in the ANaConDA suite), execute the tools/run.sh atomrace <path-to-bank-executable> command.

Bank (Windows 64-bit)

Bank (Sources)

Bank with contracts (Sources)

Contact

If you have further questions, do not hesitate to contact author ( Jan Fiedor ).

Related Papers

[1]

Jan Fiedor and Tomas Vojnar. Noise-based Testing and Analysis of Multi-threaded C/C++ Programs on the Binary Level. In Proc. of 10th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging—PADTAD'12, Minneapolis, USA, pages 36–46, 2012. ACM Press.

[2]

Jan Fiedor and Tomas Vojnar. ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level. In Proc. of 3rd International Conference on Runtime Verification—RV'12, Istanbul, Turkey, 2012. Volume 7687 of LNCS, pages 35–41, 2012. Springer-Verlag. The best tool paper award of RV'12.

[3]

Jan Fiedor, Vendula Hruba, Bohuslav Krena, Zdenek Letko, Shmuel Ur, and Tomas Vojnar. Advances in Noise-based Testing of Concurrent Software. In Software Testing, Verification and Reliability—STVR, Volume 25 Issue 3, pages 272–309, 2015, John Wiley and Sons Ltd.

[4]

Jan Fiedor, Zdenek Letko, Joao Lourenco, and Tomas Vojnar. Dynamic Validation of Contracts in Concurrent Code. In Proc. of 15th International Conference on Computer Aided Systems Theory—EUROCAST'15, Las Palmas, Spain, 2015. Volume 9520 of LNCS, pages 555–564, 2015. Springer-Verlag.

[5]

Ricardo J. Dias, Carla Ferreira, Jan Fiedor, Joao M. Lourenco, Ales Smrcka, Diogo G. Sousa, and Tomas Vojnar. Verifying Concurrent Programs Using Contracts. In Proc. of 10th IEEE International Conference on Software Testing, Verification and Validation—ICST'17, Tokyo, Japan, pages 196–206, 2017. IEEE.

Acknowledgement

This work was supported by the Czech Science Foundation (project P103/10/0306), the Czech Ministry of Education (projects COST OC10009 and MSM 0021630528), the EU/Czech IT4Innovations Centre of Excellence project CZ.1.05/1.1.00/02.0070, the internal Brno University of Technology projects FIT-S-11-1 and FIT-S-12-1, and the Artemis JU project 7H13004 HoliDes.

Development of this tool has been supported by AQUAS project (Aggregated Quality Assurance for Systems, https://aquas-project.eu/). This project has received funding from the Electronic Component Systems for European Leadership Joint Undertaking under grant agreement No 737475. This Joint Undertaking receives support from the European Union's Horizon 2020 research and innovation programme and Spain, France, United Kingdom, Austria, Italy, Czech Republic, Germany.

This tool as well as the information provided on this web page reflects only the author's view and ECSEL JU is not responsible for any use that may be made of the information it contains.